Peirce's Law

From ProofWiki
Jump to navigation Jump to search


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

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.