= Peirce's law
{c}
{title2=$((P\to Q)\to P)\to P$}
{wiki}
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>.
Back to article page
