= Solution
Use only the displayed <natural deduction> rules. Let $A$ abbreviate $\phi\lor\neg\phi$. Indentation below marks <temporary assumptions>; the closing rule names the assumption discharged.
``
1 | ¬A assume
2 | | φ assume
3 | | A ∨-intro-L, 2
4 | | ⊥ ¬-elim, 3 and 1
5 | ¬φ ¬-intro, discharge 2–4
6 | A ∨-intro-R, 5
7 | ⊥ ¬-elim, 6 and 1
8 ¬¬A ¬-intro, discharge 1–7
9 A ¬¬-elim, 8
``
There are no undischarged assumptions at line 9, so this proves the <law of excluded middle>. The use of <double-negation elimination> is explicit; an unproved appeal to the derived RAA rule is unnecessary.
Back to article page
