= Solution
The following <natural deduction> tables record the active assumption lines explicitly. A rule may use an earlier line only while all of that line's assumptions remain available; <assumption discharge> closes the indicated case or hypothesis. The first proof makes the case split first, constructs the whole required <logical conjunction> in each case, and then closes the cases.
\Table[
|| Line
|| Open assumptions
|| Formula
|| Justification
| 1
| 1
| $P\lor(Q\land R)$
| Premise
| 2
| 1, 2
| $P$
| <Temporary assumption>
| 3
| 1, 2
| $P\lor Q$
| <disjunction introduction> L 2
| 4
| 1, 2
| $P\lor R$
| <disjunction introduction> L 2
| 5
| 1, 2
| $(P\lor Q)\land(P\lor R)$
| <conjunction introduction> 3, 4
| 6
| 1, 6
| $Q\land R$
| <Temporary assumption>
| 7
| 1, 6
| $Q$
| <conjunction elimination> L 6
| 8
| 1, 6
| $R$
| <conjunction elimination> R 6
| 9
| 1, 6
| $P\lor Q$
| <disjunction introduction> R 7
| 10
| 1, 6
| $P\lor R$
| <disjunction introduction> R 8
| 11
| 1, 6
| $(P\lor Q)\land(P\lor R)$
| <conjunction introduction> 9, 10
| 12
| 1
| $(P\lor Q)\land(P\lor R)$
| <disjunction elimination> 1, 2, 5, 6, 11
]
{title=First proof: one case split constructs both conjuncts}
The second proof instead splits the goal first. It proves each required <logical disjunction> by a separate use of <disjunction elimination>, then applies <conjunction introduction> at the end.
\Table[
|| Line
|| Open assumptions
|| Formula
|| Justification
| 1
| 1
| $P\lor(Q\land R)$
| Premise
| 2
| 1, 2
| $P$
| <Temporary assumption>
| 3
| 1, 2
| $P\lor Q$
| <disjunction introduction> L 2
| 4
| 1, 4
| $Q\land R$
| <Temporary assumption>
| 5
| 1, 4
| $Q$
| <conjunction elimination> L 4
| 6
| 1, 4
| $P\lor Q$
| <disjunction introduction> R 5
| 7
| 1
| $P\lor Q$
| <disjunction elimination> 1, 2, 3, 4, 6
| 8
| 1, 8
| $P$
| <Temporary assumption>
| 9
| 1, 8
| $P\lor R$
| <disjunction introduction> L 8
| 10
| 1, 10
| $Q\land R$
| <Temporary assumption>
| 11
| 1, 10
| $R$
| <conjunction elimination> R 10
| 12
| 1, 10
| $P\lor R$
| <disjunction introduction> R 11
| 13
| 1
| $P\lor R$
| <disjunction elimination> 1, 8, 9, 10, 12
| 14
| 1
| $(P\lor Q)\land(P\lor R)$
| <conjunction introduction> 7, 13
]
{title=Second proof: separate case splits establish the two conjuncts}
The essential difference is the order of proof construction: the first shares one case split between both goals, whereas the second duplicates that split and combines the results outside the cases. Both use only the stated <natural deduction> rules, and both conclude
$$
\boxed{(P\lor Q)\land(P\lor R).}
$$
Back to article page