Peirce's Law

Theorem

Formulation 1

$\paren {p \implies q} \implies p \vdash p$

Formulation 2

$\vdash \paren {\paren {p \implies q} \implies p} \implies p$

Strong Form

$\paren {\paren {p \implies q} \implies p} \dashv \vdash p$

Also see

• Peirce's Law is Equivalent to Law of Excluded Middle

Source of Name

This entry was named for Charles Sanders Peirce.

Historical Note

Peirce's own statement and proof of the Peirce's Law:

A fifth icon is required for the principle of excluded middle and other propositions connected with it. One of the simplest formulae of this kind is:

$\paren {\paren {x \mathop {-\!\!\!<} y} \mathop {-\!\!\!<} x} \mathop {-\!\!\!<} x$

This is hardly axiomatical. That it is true appears as follows. It can only be false by the final consequent $x$ being false while its antecedent $\paren {x \mathop {-\!\!\!<} y} \mathop {-\!\!\!<} x$ is true. If this is true, either its consequent $x$ is true, when the whole formula would be true, or its antecedent $x \mathop{-\!\!\!<} y$ is false. But in the last case the antecedent of $x \mathop{-\!\!\!<} y$, that is $x$, must be true.

Peirce goes on to point out an immediate application of the law:

From the formula just given, we at once get:

$\paren {\paren {x \mathop {-\!\!\!<} y} \mathop {-\!\!\!<} a} \mathop {-\!\!\!<} x$

where the $a$ is used in such a sense that $\paren {x \mathop {-\!\!\!<} y} \mathop {-\!\!\!<} a$ means that from $\paren {x \mathop {-\!\!\!<} y}$ every proposition follows. With that understanding, the formula states the principle of excluded middle, that from the falsity of the denial of $x$ follows the truth of $x$.

Note the use by Peirce of the sign of illation $-\!\!\!<$ for implication.

Sources

• 1885: Charles Sanders Peirce: On the Algebra of Logic: A Contribution to the Philosophy of Notation (Amer. J. Math. Vol. 7: pp. 180 – 202)  www.jstor.org/stable/2369451