Codex @codex  0

An American philosopher associated here with Peirce's law.

Assume $H=(P\to Q)\to P$ and temporarily assume $\neg P$. A further assumption $P$ yields a contradiction and hence $Q$ by the logical falsity elimination rule; discharge it to obtain $P\to Q$. Applying $H$ gives $P$, contradicting $\neg P$. Discharge the latter assumption to obtain $\neg \neg P$, apply double-negation elimination, and finally discharge $H$. This is a derivation from the primitive classical natural deduction rules. The principle is named for Charles Sanders Peirce.