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 the propositional schema
Here \(P\) and \(Q\) are arbitrary propositions. The outer conditional says that if the supposition “\(P\) implies \(Q\)” would already be enough to establish \(P\), then \(P\) can be concluded. The formula is provable in ordinary classical logic, but not in intuitionistic logic. Its significance is therefore not a surprising truth-table value alone: an implication-only sentence exposes a difference between two proof disciplines.[1][2]
In a classical proof, assume \((P\to Q)\to P\). If \(P\) were false, \(P\to Q\) would follow, and the assumption would then yield \(P\), a contradiction. Classical reductio discharges the supposition that \(P\) is false and obtains \(P\). An intuitionistic system does not in general allow that last move from a refuted \(\neg P\) to an arbitrary \(P\); a Kripke countermodel makes the failure explicit.[1][2]
Structural Signature¶
Sig role-phrases: arbitrary propositions \(P,Q\) → nested premise \((P\to Q)\to P\) → unconditional conclusion \(P\) → logic-relative proof boundary → optional typed-control interpretation.
- Arbitrary propositions: the law is a Schema under substitution, not a claim about one chosen pair of sentences. \(Q\) may be unrelated to \(P\).[1]
- Nested premise: the inner \(P\to Q\) is itself the antecedent of an implication back to \(P\). The self-returning shape distinguishes the formula from a simple conditional or modus ponens.[1]
- Outer conclusion: the whole schema discharges the nested premise and yields \(P\). Its classical proof requires a rule strong enough to turn a failed \(\neg P\) supposition into \(P\).[1]
- Proof boundary: classical theoremhood and intuitionistic non-theoremhood are both necessary to the way this named law is used as a discriminator. The formula is not “valid” without naming the logic and semantics.[2]
- Typed-control reading: in a specified Curry–Howard calculus, Griffin relates a Peirce rule to a typed control operator. That is a formal interpretation of the law, not a claim that any untyped Scheme
call/ccexpression itself has this exact type.[3][4]
What It Is Not¶
It is not modus ponens. Modus ponens begins with \(P\) and \(P\to Q\) to infer \(Q\); Peirce's Law is a formula with nested implications and no free premise \(P\). It is not a theorem of intuitionistic logic merely because its surface uses only implication. Fellin and Negri supply an intuitionistic countermodel rather than an intuitionistic derivation.[2]
It is not intrinsically an axiom. Classical systems can prove it using their inference rules, while a calculus may also choose it as an added axiom or rule. The live prime Axiom describes a selected starting principle; that status is a role Peirce's Law can take, not its defining nature. Nor is the logical law identical to the Scheme procedure call-with-current-continuation: Griffin analyzes typed control operators and a proof/program correspondence; the language standard specifies operational continuation behavior without making a universal typing assertion about Peirce's formula.[3][4]
Scope of Application¶
The first setting is proof theory. A classical prover can establish the exact schema, as the Isabelle/HOL Peirce theory does with an explicit classical step. An intuitionistic proof search must instead reject it as a theorem; Fellin and Negri use Peirce's Law to illustrate how a terminating intuitionistic calculus produces a countermodel for a failed proof search. The contrast is about derivability in specified logics, not a factual disagreement over \(P\) or \(Q\).[1][2]
The second setting is typed control. Griffin's original formulae-as-types study shows how classical proof principles can correspond to programs equipped with control operators. In his analysis, extending an intuitionistic system with Peirce's rule corresponds to a typed operator \(K\); a double-negation control operator can then be defined from \(K\). Scheme's standard call/cc supplies the concrete continuation behavior that motivated this line of work, but the mathematical mapping depends on Griffin's typed calculus and should not be read as a generic type for every Scheme program.[3][4]
Clarity¶
Read the parentheses from the inside out. First \(P\to Q\) is a hypothetical implication. Next \((P\to Q)\to P\) says that hypothetical implication suffices for \(P\). Finally the whole formula says that this sufficiency entails \(P\) outright. The variable \(Q\) is arbitrary: replacing it with a particular formula creates an instance, whereas the named law is the uniformly quantified schema.[1]
“Classically valid” means every classical valuation makes the full formula true. “Not intuitionistically valid” means there is an intuitionistic model/world at which it fails; it does not mean intuitionistic logic proves its negation or that every substitution instance fails. A two-world model can have a root where \(P\) is not yet forced, a successor where \(P\) is forced, and \(Q\) never forced. At the root \(P\to Q\) is not forced, so \((P\to Q)\to P\) can be forced while \(P\) is not: the outer implication fails there.[2]
Manages Complexity¶
The compact formula marks a large methodological choice. Rather than arguing vaguely that classical and constructive reasoning differ, one can ask whether a formal system proves this exact implication-only schema. A positive classical proof and a negative intuitionistic model jointly fix the boundary. The schema also gives a target for typed-control correspondence: the nested implication becomes a type shape to be inhabited by an operator under explicit control rules.[1][2][3]
This compression has a cost. The formula alone does not identify which proof rule did the work, and a program with control syntax alone does not establish the typing. A sound account must state the ambient logic or typed calculus. Isabelle's proof identifies its classical rule; Griffin specifies his operator and typing judgment.[1][3]
Abstract Reasoning¶
To test classical provability, take \(H:(P\to Q)\to P\) and assume \(\neg P\). From a hypothetical \(P\), the contradiction with \(\neg P\) allows any \(Q\), so \(P\to Q\). Applying \(H\) gives \(P\), contradicting \(\neg P\). Classical contradiction elimination therefore yields \(P\) and discharges \(H\) to obtain the full schema. The final conclusion from \(\neg\neg P\) is precisely the step that cannot simply be imported into intuitionistic reasoning.[1]
To test the other side, use the two-world Kripke frame described above. Both worlds fail \(P\to Q\): at the successor \(P\) holds while \(Q\) does not. Thus \((P\to Q)\to P\) is forced at the root, but \(P\) is not. This is a concrete counterexample to intuitionistic validity; the construction is an explanatory simplification of Fellin and Negri's formal countermodel, not a claim that their displayed proof-search tree uses these exact labels.[2]
Knowledge Transfer¶
The transfer from proof theory to programming is disciplined rather than metaphorical. Under Curry–Howard, propositions can be treated as types and proofs as typed terms. Griffin's Peirce rule maps a derivation from \((\alpha\to\beta)\to\alpha\) to \(\alpha\) onto a control operator taking a term of the former type to one of the latter. This explains how classical proof strength can have computational content once continuation-like control is admitted.[3]
The transfer stops at the type-system boundary. R7RS describes call/cc as capturing the current continuation and allowing later invocation to abandon the intervening one. That operational fact motivates the correspondence, but it does not make arbitrary untyped Scheme expressions proofs of Peirce's Law, nor does every continuation use require the entire formula schema.[4][3]
Examples¶
Classical proof in Isabelle/HOL. The authored Peirce theory states ((A ⟶ B) ⟶ A) ⟶ A and proves it by assuming the nested antecedent, introducing a classical step, deriving \(A\to B\) under \(\neg A\), and obtaining \(A\). This is a direct formal instance of the proof role, not an illustrative slogan.[1]
Mapped back: \(A,B\) instantiate \(P,Q\); (A ⟶ B) ⟶ A is the nested premise; \(A\) is the outer conclusion; rule classical witnesses the logic-specific step.
Typed control in Griffin's calculus. Griffin considers an intuitionistic system extended by the Peirce rule: from a term of type \((\alpha\to\beta)\to\alpha\), a typed operator \(K\) yields type \(\alpha\). He then derives a double-negation control operator from that rule. This is a constructive formal reading of a classical rule in a richer computational language, not the claim that an ordinary Scheme expression by itself proves the law.[3]
Mapped back: \(\alpha,\beta\) play the \(P,Q\) roles; the input type represents the nested premise; \(K\) produces the conclusion type; the typed control rule marks the classical extension.
Structural Tensions¶
Classical proof power versus constructive warrant. Classical reductio proves the schema; intuitionistic proof search refuses the final step and can furnish a countermodel. The gain is a stronger implication calculus, while the cost is that a proof no longer has to be constructive in the intuitionistic sense. Diagnostic: Which logic and inference rules license the step from the nested premise to \(P\)?[1][2]
Logical type versus operational control. The typed correspondence gives a computational interpretation of the classical rule, while Scheme's real continuation operator has operational semantics not fully described by the formula alone. Conflating type and behavior overclaims the transfer. Diagnostic: Is a particular typed calculus and control rule specified, or only a language feature named call/cc?[3][4]
Structural–Framed Character¶
Its character: Peirce's Law is a strongly structural, domain-specific logical schema. The exact nesting of implications and logic-relative validity survive notation changes, but the formula presupposes propositions, implication, and a proof system rather than supplying a new general cross-substrate prime.[1][2]
- Vocabulary travel: the schema travels from proof theory into typed programming-language semantics only when propositions-as-types and a particular control rule are supplied; merely reusing the name for a recursive argument would not preserve the law.[3]
- Evaluative weight: the formula is neither a defect nor a virtue by definition. Whether accepting it is desirable depends on the proof discipline—classical theoremhood and intuitionistic non-theoremhood are formal statuses, not praise and blame.[1][2]
- Institutional origin: the historical name and the choice to use the formula as an axiom belong to mathematical practice, while its proof in Isabelle and countermodel in intuitionistic semantics are checkable independently of the name.[1][2]
- Human-practice dependence: a researcher chooses the ambient calculus and may adopt a control interpretation; given those choices, derivability and typing have determinate formal tests. A natural-language argument is not automatically in either calculus.[3]
- Import versus recognition: recognizing the nested formula and its logic-relative status requires the formal roles. Importing a Peirce type onto arbitrary Scheme
call/ccsyntax without Griffin's typed calculus would assert more than the sources establish.[3][4]
The programming interpretation is more framed than the bare formula because the same type shape matters only under an explicit Curry–Howard and control-operator calculus. This preserves the correspondence without conflating a language feature with a proof of the schema.[3][4]
Structural Core vs. Domain Accent¶
The core is the schema \(((P\to Q)\to P)\to P\) together with its classical/intuitionistic boundary. Isabelle's syntax and Griffin's Greek type variables are accents. The formal proof and countermodel are unlike evidential routes to the same identity; Griffin's typed operator is a transfer setting that preserves the nested premise/conclusion relationship under a specified interpretation.[1][2][3]
A stripped-down pattern—an assumed route from \(P\) to an arbitrary \(Q\) returning to \(P\)—might be noticed in other forms of reasoning, but without propositions, implication and the classical/intuitionistic contrast it is not Peirce's Law. Whether that broader self-returning conditional has an independently useful cross-domain invariant is a future-prime question, not an additional prime asserted by this entry. The current live Prime catalog supplies no demonstrated genus for that residual.
The law can be chosen as an axiom of a calculus or proven as a theorem in another, so no strict DAG parent to live Axiom is proposed. A later catalog may supply a broader node for classical implicational principles, but topical similarity to all logic nodes does not justify inventing an edge now.
Instantiates / Related Primes¶
Live Axiom is a related role, not a necessary genus. If a formal system declares Peirce's Law as a starting assumption, that instance is an axiom; the named law also exists where derived. The entry is narrower than classical reasoning as a whole and distinct from ordinary implication or a logical inference rule taken without its fixed formula shape.[1][3]
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
Not to Be Confused With¶
- Modus ponens: a rule from \(P\) and \(P\to Q\) to \(Q\), not the nested Peirce schema.
- Law of excluded middle: a differently shaped classical principle; equivalence can depend on the assumed base logic, so do not treat the formulas as literal aliases.
- Double-negation elimination: a related classical principle used in a proof of this law; it is not the same string or independently necessary formulation.[1][3]
- A generic
call/cccall: continuation capture behavior in Scheme, not automatically an inhabitant of Griffin's Peirce type.[4][3]
References¶
[1] Makarius, “Theory Peirce,” Isabelle/HOL Examples, original formalization, Peirce schema and explicit classical proof. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k ↩l ↩m ↩n ↩o ↩p ↩q ↩r
[2] Giulio Fellin and Sara Negri, “A Terminating Intuitionistic Calculus,” Journal of Symbolic Logic, published online 2023, §3.3, original proof-search and countermodel for Peirce's Law. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k ↩l ↩m
[3] Timothy G. Griffin, “A Formulae-as-Types Notion of Control”, POPL 1990 original paper, introduction and §5 (Peirce rule and typed operator \(K\)). registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k ↩l ↩m ↩n ↩o ↩p ↩q
[4] Scheme Reports editors, Revised⁷ Report on the Algorithmic Language Scheme, §6.10 call-with-current-continuation operational definition; the standard is not itself a Peirce-typing source. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h