= Solution
The <logical implication> associates to the right. Assume its two antecedents, then use nested applications of the <disjunction elimination rule>.
``
1 | P ∨ Q assume
2 | | P ∨ ¬Q assume
3 | | | P first case of 1
4 | | | P available from 3
5 | | | Q second case of 1
6 | | | | P first case of 2
7 | | | | P available from 6
8 | | | | ¬Q second case of 2
9 | | | | ⊥ ¬-elim, 5 and 8
10 | | | | P ⊥-elim, 9
11 | | | P ∨-elim, 2, cases 6–7 and 8–10
12 | | P ∨-elim, 1, cases 3–4 and 5–11
13 | (P ∨ ¬Q) → P →-intro, discharge 2–12
14 (P ∨ Q) → ((P ∨ ¬Q) → P) →-intro, discharge 1–13
``
This <proof> uses <logical falsity elimination rule>, but does not need <law of excluded middle> or <double-negation elimination>.
Back to article page
