Peirce's Law¶
An implication-only formula valid in classical logic but not intuitionistic logic: if (P→Q) implies P, then P.
Core Idea¶
Peirce's Law is \(((P\to Q)\to P)\to P\): if the supposition that \(P\) implies an arbitrary \(Q\) would already establish \(P\), then \(P\) holds. It is provable in classical propositional logic but not in intuitionistic logic. The formula's nested implication therefore marks a precise proof-theoretic boundary, not a claim about one chosen pair of propositions.[ref-5d78e2480433][ref-7660caae7013]
Scope of Application¶
Isabelle/HOL proves the schema using an explicit classical step. Fellin and Negri use the same formula to exhibit an intuitionistic proof-search failure and countermodel. In typed programming-language theory, Griffin relates the Peirce rule to a typed control operator, connecting a classical logical principle to continuation-like computation. Scheme's call/cc operationally captures a continuation, but its language-standard description alone is not a proof of the exact Peirce typing judgment.[ref-5d78e2480433][ref-7660caae7013][ref-e87bd220b036][ref-a7bff6a951f5]
Clarity¶
The formula is not modus ponens: \(P\to Q\) is inside an antecedent, and the whole statement concludes \(P\) without a free premise \(P\). Classical reductio proves it by assuming \(\neg P\), deriving \(P\to Q\), applying \((P\to Q)\to P\), and then discharging the contradiction. An intuitionistic two-world model with \(P\) eventually forced and \(Q\) never forced gives a root where the nested premise holds but \(P\) does not.[ref-5d78e2480433][ref-7660caae7013]
Manages Complexity¶
The single schema tests whether an implication calculus allows this form of classical reasoning. A proof, a countermodel, and a typed-control interpretation answer different questions, so the ambient logic or calculus must always be stated. Calling the formula an “axiom” is contingent on a system choosing it as a starting principle; it can also be a derived theorem, so live Axiom is not a necessary DAG parent.[ref-5d78e2480433][ref-7660caae7013][^ref-e87bd220b036]
Abstract Reasoning¶
Identify the variables \(P,Q\), the nested premise \((P\to Q)\to P\), and the outer conclusion \(P\). Test the law under a named logic. In classical logic it follows by reductio; in intuitionistic Kripke semantics the delayed truth of \(P\) blocks universal validity. Treat it as a formula schema under substitution, not as a rule that every ordinary language conditional obeys.[ref-5d78e2480433][ref-7660caae7013]
Knowledge Transfer¶
Under Griffin's specified Curry–Howard extension, a term of type \((\alpha\to\beta)\to\alpha\) can be passed to a typed control operator producing \(\alpha\). The \(P,Q\) roles become type variables and the conclusion becomes the result type. That disciplined transfer explains why control can give computational content to classical proof, while an untyped Scheme call/cc call does not automatically count as an instance of the law.
[^ref-5d78e2480433]: Makarius, “Theory Peirce,” Isabelle/HOL Examples, original formal proof. [^ref-7660caae7013]: Giulio Fellin and Sara Negri, “A Terminating Intuitionistic Calculus,” Journal of Symbolic Logic, 2023, §3.3 countermodel. [^ref-e87bd220b036]: Timothy G. Griffin, “A Formulae-as-Types Notion of Control”, POPL 1990, §5 typed Peirce rule. [^ref-a7bff6a951f5]: Revised⁷ Report on the Algorithmic Language Scheme, §6.10 continuation behavior.
Neighborhood in Abstraction Space¶
Peirce's Law sits in a moderately populated region (43rd percentile for distinctiveness): it has near-neighbors but no dense thicket of look-alikes.
Family — Argumentation Fallacies & Inference (15 abstractions)
Nearest neighbors
- Denying the Antecedent — 0.88
- Formal Theory — 0.87
- Logical Consequence — 0.87
- Cut-Elimination Theorem — 0.86
- Intuitionistic Type Theory — 0.86
Computed from structural-signature embeddings · 2026-10-08