nic-dfneg Show Code edit
# Define negation in terms of 'nand'. Analogous to
# #(<-> (-/\ ph ph) (-. ph))#. In a pure (standalone) treatment of
# Nicod's axiom, this theorem would be changed to a definition ($a
# statement).
thm (nic-dfneg () () (-/\ (-/\ (-/\ ph ph) (-. ph)) (-/\ (-/\ (-/\ ph ph) (-/\ ph ph)) (-/\ (-. ph) (-. ph)))) ph nic-justneg bicomi (-/\ ph ph) (-. ph) nic-justbi mpbi)
(-/\ (-/\ (-/\ ph ph) (-. ph)) (-/\ (-/\ (-/\ ph ph) (-/\ ph ph)) (-/\ (-. ph) (-. ph))))
edit