Let . 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:Alternatively, first transform the goal by conjunction introduction, obtaining and by separate disjunction elimination proofs: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, 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.
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–111 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 Articles by others on the same topic
There are currently no matching articles.