= Solution
Let $H=(P\land Q)\lor(P\land R)$. In the following <natural deduction> proofs, indentation and vertical bars mark assumption scopes. Rule names are the introduction and elimination rules supplied by the paper.
First work backwards from the premise using <disjunction elimination>, proving the whole desired <logical conjunction> in each case:
``
1 H premise
2 | P ∧ Q assumption
3 | P ∧-elim-L 2
4 | Q ∧-elim-R 2
5 | Q ∨ R ∨-intro-L 4
6 | P ∧ (Q ∨ R) ∧-intro 3,5
7 | P ∧ R assumption (new case)
8 | P ∧-elim-L 7
9 | R ∧-elim-R 7
10 | Q ∨ R ∨-intro-R 9
11 | P ∧ (Q ∨ R) ∧-intro 8,10
12 P ∧ (Q ∨ R) ∨-elim 1,2–6,7–11
``
Alternatively, first transform the goal by <conjunction introduction>, obtaining $P$ and $Q\lor R$ by separate <disjunction elimination> proofs:
``
1 H premise
2 | P ∧ Q assumption
3 | P ∧-elim-L 2
4 | P ∧ R assumption (new case)
5 | P ∧-elim-L 4
6 P ∨-elim 1,2–3,4–5
7 | P ∧ Q assumption
8 | Q ∧-elim-R 7
9 | Q ∨ R ∨-intro-L 8
10 | P ∧ R assumption (new case)
11 | R ∧-elim-R 10
12 | Q ∨ R ∨-intro-R 11
13 Q ∨ R ∨-elim 1,7–9,10–12
14 P ∧ (Q ∨ R) ∧-intro 6,13
``
The essential difference is the final rule: the first proof splits the premise once, while the second splits the goal first and then analyzes the premise twice. Counting only rule applications, \b[both displayed proofs take nine inference steps]. The first uses four <conjunction elimination> steps, two <disjunction introduction> steps, two <conjunction introduction> steps and one <disjunction elimination>; the second replaces one <conjunction introduction> with a second <disjunction elimination>. If assumption lines are counted as displayed proof lines, the second is longer, 14 rather than 12, because it opens four case assumptions rather than two. Thus a raw line count and an inference-step count need not agree.
Back to article page
