The implication introduction rule opens a subproof with a temporary assumption , derives , and discharges that assumption to conclude . The negation introduction rule opens a subproof with a temporary assumption , derives logical falsity , and discharges it to conclude .
The boxes record the scopes and dependencies of the temporary assumptions. A result derived inside a box cannot be used outside it without the appropriate discharge rule; it may depend on the boxed assumption. Other, surrounding assumptions remain in force. This is how the natural deduction rules distinguish a conditional derivation from an unconditional assertion.
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,13Proof by contradiction, or reductio ad absurdum, has the formdischarging the assumption . This is the classical rule that concludes directly, as opposed to the negation introduction rule, which concludes a negation.
To derive double-negation elimination using RAA without assuming double-negation elimination itself, useHere line 1 is the negation of line 2. Thus only negation elimination rule inside the subproof, followed by RAA, is needed.
1 ¬¬φ premise
2 | ¬φ assumption
3 | ⊥ ¬-elim 2,1
4 φ RAA 2–3Abbreviate and . Use the primitive natural deduction rules, including double-negation elimination:The outer premise is redundant: the proof uses the locally assumed , so the conclusion is already a theorem. Keeping the redundant premise is allowed. The successive discharges give with exactly the requested assumption scopes.
1 H premise
2 | H assumption
3 | | K assumption
4 | | | ¬P assumption
5 | | | Q →-elim 2,4
6 | | | ¬Q →-elim 3,4
7 | | | ⊥ ¬-elim 5,6
8 | | ¬¬P ¬-intro 4–7
9 | | P ¬¬-elim 8
10 | K → P →-intro 3–9
11 H → (K → P) →-intro 2–10First derive by double-negation elimination, then derive by negation introduction. The logical falsity elimination rule is used only inside the attempt to derive .Reiteration at line 12 merely uses an assumption that remains in scope. The final follows by conjunction introduction. This explicitly supplies the classical step needed to obtain rather than just .
1 ¬(A → B) premise
2 | ¬A assumption
3 | | A assumption
4 | | ⊥ ¬-elim 3,2
5 | | B ⊥-elim 4
6 | A → B →-intro 3–5
7 | ⊥ ¬-elim 6,1
8 ¬¬A ¬-intro 2–7
9 A ¬¬-elim 8
10 | B assumption
11 | | A assumption
12 | | B reiteration 10
13 | A → B →-intro 11–12
14 | ⊥ ¬-elim 13,1
15 ¬B ¬-intro 10–14
16 A ∧ ¬B ∧-intro 9,15 Articles by others on the same topic
There are currently no matching articles.