Description: Peirce's axiom. This
odd-looking theorem is the "difference" between an
intuitionistic system of propositional calculus and a classical system and
is not accepted by intuitionists. When Peirce's axiom is added to an
intuitionistic system, the system becomes equivalent to our classical
system ax-1 7 through ax-3 9. A curious fact about this theorem is
that
it requires ax-3 9 for its proof even though the result has no
negation
connectives in it. (Contributed by NM, 5-Aug-1993.) (Proof shortened by
Wolf Lammen, 9-Oct-2012.) |