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