= Solution
Write $H$ for $(\phi\to\psi)\to\phi$. The following derives <Peirce's law> directly from the printed primitive rules, including <double-negation elimination>:
|| Line
|| Formula
|| Justification
| 1
| $H$
| Assume for the final implication
| 2
| $\neg\phi$
| Assume locally
| 3
| $\phi$
| Assume inside the scope of 2
| 4
| $\bot$
| <Negation elimination rule>, 2 and 3
| 5
| $\psi$
| <Logical falsity elimination rule>, 4
| 6
| $\phi\to\psi$
| <Implication introduction rule>, discharging 3–5
| 7
| $\phi$
| <Implication elimination rule>, 1 and 6
| 8
| $\bot$
| <Negation elimination rule>, 2 and 7
| 9
| $\neg\neg\phi$
| <Negation introduction rule>, discharging 2–8
| 10
| $\phi$
| <Double-negation elimination>, 9
| 11
| $((\phi\to\psi)\to\phi)\to\phi$
| <Implication introduction rule>, discharging 1–10
Every assumption is discharged, so the last formula is a theorem. In particular, no unproved appeal to the derived `RAA` rule is hidden in the argument.
Back to article page
