Retain the two given logical implications and temporarily assume their common starting proposition.
1 P → Q premise
2 Q → R premise
3 | P assume
4 | Q →-elim, 3 and 1
5 | R →-elim, 4 and 2
6 P → R →-intro, discharge 3–5Only the original premises remain undischarged, giving the required composition of logical implications.
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–13This proof uses logical falsity elimination rule, but does not need law of excluded middle or double-negation elimination.
Articles by others on the same topic
There are currently no matching articles.