Solution
= Solution
A derivation of the <law of excluded middle> using only the supplied primitive rules is
``
1 | ¬(A ∨ ¬A) assumption
2 | | A assumption
3 | | A ∨ ¬A ∨-intro-L 2
4 | | ⊥ ¬-elim 3,1
5 | ¬A ¬-intro 2–4
6 | A ∨ ¬A ∨-intro-R 5
7 | ⊥ ¬-elim 6,1
8 ¬¬(A ∨ ¬A) ¬-intro 1–7
9 A ∨ ¬A ¬¬-elim 8
``
Both boxes have been discharged, so the final formula has no undischarged assumptions.