Peirce's law

{{logic}} The classically valid but intuitionistically non-valid formula <math> ((P \to Q) \to P) \to P </math> of propositional calculus, which can be used as an substitute for the law of excluded middle in implicational propositional calculus.