// laws and rules · Fundamental law
Peirce's law_
Peirce's law is a remarkable curiosity: a classical tautology written purely with conditionals, without a single negation. Its statement, ((p ⇒ q) ⇒ p) ⇒ p, looks baffling at first sight, but the truth table confirms it in all four rows.
Example
((p ⇒ q) ⇒ p) ⇒ p
What the variables mean
- ▸ p: “The project is approved”
- ▸ q: “The budget is increased”
In plain words
If the mere fact that “approval implies a budget increase” is enough for the project to be approved, then the project is approved anyway.
Truth table
| p | q | p ⇒ q | (p ⇒ q) ⇒ p | ((p ⇒ q) ⇒ p) ⇒ p★ |
|---|---|---|---|---|
| T | T | T | T | T |
| T | F | F | T | T |
| F | T | T | F | T |
| F | F | T | F | T |
Classification: Tautology · 4 rows
Statement
The law states that ((p ⇒ q) ⇒ p) ⇒ p is a tautology. It was formulated by Charles Sanders Peirce, the same logician who helped formalise truth tables.
Its theoretical interest is that adding it to an intuitionistic system containing only implications turns that system into classical logic. In other words, it captures by itself all the missing “classicality”.
Why it holds: reading the table
The only way for the outer implication to be false would be for the antecedent (p ⇒ q) ⇒ p to be true while p is false. Suppose p = F: then p ⇒ q is T (false antecedent), so (p ⇒ q) ⇒ p becomes T ⇒ F, which is F. The antecedent turns out false, and the outer implication is T.
If p = T, the final consequent is true and the outer implication is T straight away. No row yields F, hence the tautology.
Why it feels counter-intuitive
The formula seems to pull p out of nowhere: from a hypothesis about p it concludes p. The catch lies in the material definition of the conditional, whereby an implication with a false antecedent is true.
That is exactly why intuitionistic logic rejects it: it provides no construction of p, it merely rules out the alternative. It is the implication-flavoured counterpart of what excluded middle does for disjunction.
Connection to computer science
Under the Curry-Howard correspondence, which matches propositions with types and proofs with programs, Peirce's law corresponds to the type of the call/cc operator (call with current continuation).
That parallel explains why languages with continuations or control operators can inhabit a type that pure functional programming cannot construct.
Relation to other laws
Over an intuitionistic base it is equivalent to excluded middle and to double-negation elimination: adding any of the three yields the same classical system.
Unlike those, it never mentions negation, which makes it especially handy when studying fragments of logic containing only the conditional.
Try it yourself
Edit the expression in the calculator and watch how every step of the table changes.
Open in the calculator →Related operators
Frequently asked questions
Why is it a tautology if it seems to pull p out of nowhere? ▼
Because the material conditional treats any implication with a false antecedent as true. Assuming p is false makes the whole antecedent false, so the outer implication is true.
What is its connection to call/cc? ▼
Under the Curry-Howard correspondence, the type of call/cc is exactly Peirce's law. It is the standard example of a non-constructive classical formula with computational content.
Is it valid in intuitionistic logic? ▼
No. In fact, adding it to an intuitionistic system is enough to obtain full classical logic.