= Solution
Work backwards from the outermost available <logical connective>. One strategy applies the <disjunction elimination rule> to the premise first, constructs the whole target in each case, and then closes the cases. In the tables, a context such as $\{1,2\}$ means that assumptions on lines 1 and 2 remain open. A range in a discharge rule denotes the entire local subproof.
|| Line
|| Context
|| Formula
|| Justification
| 1
| $\{1\}$
| $(P\land Q)\lor(P\land R)$
| Premise
| 2
| $\{1,2\}$
| $P\land Q$
| Temporary assumption
| 3
| $\{1,2\}$
| $P$
| <conjunction elimination rule> $\land\text{-elim-L}$ on 2
| 4
| $\{1,2\}$
| $Q$
| <conjunction elimination rule> $\land\text{-elim-R}$ on 2
| 5
| $\{1,2\}$
| $Q\lor R$
| <disjunction introduction rule> $\lor\text{-intro-L}$ on 4
| 6
| $\{1,2\}$
| $P\land(Q\lor R)$
| <conjunction introduction rule> $\land\text{-intro}$ on 3, 5
| 7
| $\{1,7\}$
| $P\land R$
| Temporary assumption
| 8
| $\{1,7\}$
| $P$
| <conjunction elimination rule> $\land\text{-elim-L}$ on 7
| 9
| $\{1,7\}$
| $R$
| <conjunction elimination rule> $\land\text{-elim-R}$ on 7
| 10
| $\{1,7\}$
| $Q\lor R$
| <disjunction introduction rule> $\lor\text{-intro-R}$ on 9
| 11
| $\{1,7\}$
| $P\land(Q\lor R)$
| <conjunction introduction rule> $\land\text{-intro}$ on 8, 10
| 12
| $\{1\}$
| $P\land(Q\lor R)$
| <disjunction elimination rule> $\lor\text{-elim}$ on 1, 6, 11; discharge 2, 7
A second strategy applies the <conjunction introduction rule> backwards to the target first. Prove $P$ and $Q\lor R$ separately, each by the <disjunction elimination rule> on the premise, and combine them:
|| Line
|| Context
|| Formula
|| Justification
| 1
| $\{1\}$
| $(P\land Q)\lor(P\land R)$
| Premise
| 2
| $\{1,2\}$
| $P\land Q$
| Temporary assumption
| 3
| $\{1,2\}$
| $P$
| <conjunction elimination rule> $\land\text{-elim-L}$ on 2
| 4
| $\{1,4\}$
| $P\land R$
| Temporary assumption
| 5
| $\{1,4\}$
| $P$
| <conjunction elimination rule> $\land\text{-elim-L}$ on 4
| 6
| $\{1\}$
| $P$
| <disjunction elimination rule> $\lor\text{-elim}$ on 1, 3, 5; discharge 2, 4
| 7
| $\{1,7\}$
| $P\land Q$
| Temporary assumption
| 8
| $\{1,7\}$
| $Q$
| <conjunction elimination rule> $\land\text{-elim-R}$ on 7
| 9
| $\{1,7\}$
| $Q\lor R$
| <disjunction introduction rule> $\lor\text{-intro-L}$ on 8
| 10
| $\{1,10\}$
| $P\land R$
| Temporary assumption
| 11
| $\{1,10\}$
| $R$
| <conjunction elimination rule> $\land\text{-elim-R}$ on 10
| 12
| $\{1,10\}$
| $Q\lor R$
| <disjunction introduction rule> $\lor\text{-intro-R}$ on 11
| 13
| $\{1\}$
| $Q\lor R$
| <disjunction elimination rule> $\lor\text{-elim}$ on 1, 9, 12; discharge 7, 10
| 14
| $\{1\}$
| $P\land(Q\lor R)$
| <conjunction introduction rule> $\land\text{-intro}$ on 6, 13
Both derivations establish
$$
\boxed{((P\land Q)\lor(P\land R))\vdash P\land(Q\lor R).}
$$
Counting only applications of <inference rules>, each proof has \b[nine] steps: four <conjunction elimination rule> applications, two <disjunction introduction rule> applications, and three remaining applications. The first uses two <conjunction introduction rule> applications and one <disjunction elimination rule>; the second uses one and two, respectively. The second has two additional temporary-assumption lines, giving 14 displayed lines instead of 12, but assumptions are not additional inference applications. Its duplicated case analysis is exchanged for avoiding construction of the complete <logical conjunction> separately in both cases. In a proof tree it also repeats the use of the original premise.
Back to article page
