= Solution
Apply the complete <logical derivation> of the <law of excluded middle> in (a) to $Q$, obtaining $Q\lor\neg Q$. Then use the <disjunction elimination rule>, constructing each <logical implication> by an explicit hypothetical subproof:
``
1 Q ∨ ¬Q result of (a), φ := Q
2 | Q first case
3 | | P assume
4 | | Q available from 2
5 | P → Q →-intro, discharge 3–4
6 | (P → Q) ∨ (P → ¬Q) ∨-intro-L, 5
7 | ¬Q second case
8 | | P assume
9 | | ¬Q available from 7
10 | P → ¬Q →-intro, discharge 8–9
11 | (P → Q) ∨ (P → ¬Q) ∨-intro-R, 10
12 (P → Q) ∨ (P → ¬Q) ∨-elim, 1, cases 2–6 and 7–11
``
Both case assumptions and both hypothetical $P$ assumptions have been discharged. Thus the conclusion is a theorem, not a <logical implication> that depends on assuming $P$.
Back to article page
