= Solution
This instance of <Peirce's law> uses the supplied classical <double-negation elimination> rule. First derive $P\to Q$ while assuming $\neg P$, using <explosion> inside a further temporary assumption.
``
1. (P → Q) → P premise
2. ¬P assumption [i]
3. P assumption [j]
4. ⊥ ¬E, 2, 3
5. Q ⊥E, 4
6. P → Q →I, 3–5, discharging [j]
7. P →E, 1, 6
8. ⊥ ¬E, 2, 7
9. ¬¬P ¬I, 2–8, discharging [i]
10. P ¬¬E, 9
``
This is a formal <natural deduction> proof from exactly the given premise; no unproved excluded-middle lemma is needed.
Back to article page
