Peirce's law

Peirce's law in logic is named after the philosopher and logician Charles Sanders Peirce. It was taken as an axiom in his first axiomatisation of propositional logic. The axiom can be used as an alternative to the excluded middle.

In propositional calculus, Peirce's law says that ((P→Q)→P)→P. Written out, this says that if you can show that P implying Q forces P to be true, then P must be true.

Peirce's law does not hold in intuitionistic logic or intermediate logics.

Under the Curry-Howard isomorphism, Peirce's law is the type of continuation operators.

Proof of Peirce's law

Showing Peirce's Law applies does not mean that P→Q is true, we have that P is true but only (P→Q)→P, not P→(P→Q) (see affirming the consequent).

The fastest proof of Peirce's Law is to prove the contrapositive ¬P→¬((P→Q)→P) thus:

¬P→(P→Q) (vacuous truth)

But then we have (P→Q) and ¬P, so ((P→Q)→P) is false.

Thus ¬((P→Q)→P) is true, Q.E.D.