Peirce's law

Peirce's law is the propositional formula ((P → Q) → P) → P. It is valid in classical logic but not derivable in intuitionistic logic.

Classical logic: A logic that includes the law of excluded middle and permits classical rules of inference. Peirce's law is valid in this broader logical system.
Propositional logic: The study of arguments built from propositions and logical connectives. Peirce's law is a formula within this logic.
Kripke semantics: A semantics for modal and intuitionistic logics using ordered worlds and relations between them. Its intuitionistic models can falsify Peirce's law.
Charles Sanders Peirce: An American philosopher, logician, and scientist who helped establish pragmatism and modern logic. The principle bears Peirce's name and appears in his logical work.
Intuitionistic logic: A logic that requires constructive justification and does not generally accept excluded middle. It cannot derive Peirce's law without adding classical principles.
Material implication: The classical connective P → Q, false only when P is true and Q is false. The law's nested implications are interpreted classically using this connective.
Heyting algebra: A bounded lattice equipped with an implication operation, providing algebraic semantics for intuitionistic logic. The law fails in general Heyting algebras, though it holds in Boolean algebras.
Intuitionism: A philosophical and mathematical position that treats mathematical objects as constructions and proofs as constructive evidence. Its rejection of Peirce's law follows from its constructive account of proof.
Law of excluded middle: The principle that every proposition or its negation is true: P ∨ ¬P. Like Peirce's law, it is classically valid but not intuitionistically derivable in general.
Negation: The logical connective that expresses the denial of a proposition. Expanding implication through negation reveals classical principles equivalent to Peirce's law.

Linked from 3 pages

Consequentia mirabilisRelated: It is another characteristic classical principle whose intuitionistic failure helps locate consequentia mirabilis.