Paper
On the Algebra of Logic: A Contribution to the Philosophy of Notation, 1885. American Journal of Mathematics, vol. 7, pp. 180–202. The linked first installment covers pp. 180–196. Read a transcription of the paper.
Connection to the paper
This artifact isolates Peirce’s law from the paper’s treatment of propositional logic and rewrites it using modern implication notation. It is a new Lean proof of the selected law, rather than a line-by-line transcription of Peirce’s derivation.
The result
Suppose that being able to infer Q from P would let you establish P. In classical logic, P then follows.
((P → Q) → P) → P
Proof in plain English
- Keep the hypothesis. Assume that a proof of P → Q would give you P. We want to establish P.
- Split into two cases. Classical excluded middle says either P holds or it does not. If P holds, the proof is already finished.
- Resolve the other case. If P is false, assuming P yields a contradiction, from which Q follows. That gives P → Q. Apply the original hypothesis to obtain P.
Scope & assumptions
One propositional law, for arbitrary propositions P and Q. The paper’s wider algebra of logic, relations, and quantifier rules are outside this artifact.
The proof uses classical excluded middle: P is true or P is false. This assumption matters; the same law is not generally available in intuitionistic logic. P and Q are arbitrary propositions, with no extra hypotheses.
Notation in Lean
| Meaning | Lean |
|---|---|
| Two arbitrary propositions | P Q : Prop |
| If P, then Q | P → Q |
| The hypothesis | (P → Q) → P |
| The classical case split | Classical.em P |
| The complete formal statement | peirces_law |
Lean proof
/-
Paper to Lean · Peirce's law
C. S. Peirce, On the Algebra of Logic: A Contribution to the Philosophy
of Notation, American Journal of Mathematics 7 (1885), pp. 180–202.
https://doi.org/10.2307/2369451
Scope: Peirce's law in modern propositional notation, not the whole paper.
The proof uses classical excluded middle through Classical.em.
Lean 4.33.1; only Lean's automatically imported core library is needed.
Run: lean -DwarningAsError=true Peirce.lean
License: MIT (see the project LICENSE).
-/
namespace PaperToLean.Peirce
-- If deriving P from (P → Q) is possible, then P holds, classically.
theorem peirces_law (P Q : Prop) : ((P → Q) → P) → P := by
intro hypothesis
cases Classical.em P with
| inl trueP => exact trueP
| inr falseP =>
apply hypothesis
intro trueP
exact False.elim (falseP trueP)
#print axioms peirces_law
end PaperToLean.Peirce
Inspect the verification record
Lean reports propext, Classical.choice, and Quot.sound as transitive dependencies of this proof through Classical.em. These are Lean’s standard foundational axioms, not additional claims assumed from the paper. There are no custom axioms or unfinished proof placeholders.
Lean 4.33.1
Dependencies: Lean core
File: Peirce.lean
SHA-256: 8f37cce3e3ff48615c53644f49198751e414cc76cdb983896279f8e9e2043edc
Result: passed
'PaperToLean.Peirce.peirces_law' depends on axioms: [propext, Classical.choice, Quot.sound]
SHA-256: 8f37cce3e3ff48615c53644f49198751e414cc76cdb983896279f8e9e2043edc
Run it
Install Lean with elan, download Peirce.lean, then run:
lean +leanprover/lean4:v4.33.1 -DwarningAsError=true Peirce.lean