/-
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