Appendix: Examples Propositional natural deduction
The following proofs provide more illustrations of the use of the rules. Linear format is used for writing them out, for reasons of typography.
You may find it helpful to try constructing the proofs using the interactive proof editor. Links are provided to facilitate this. You should try to become familiar with the proof editor, as it not only takes care of the book-keeping and layout, resulting in a nicely presented proof, but gives you feedback at every step to ensure that you get it right. It's like having an infinitely patient personal tutor to help you.
Click on any of the labels to try them yourself.
Proof 1
SP {p AND (q AND r) ⊢ (p AND q) AND r} PL {1} {1} {p AND (q AND r)} {A} PL {1} {2} {p} {1 ANDE} PL {1} {3} {q AND r} {1 ANDE} PL {1} {4} {q} {3 ANDE} PL {1} {5} {r} {3 ANDE} PL {1} {6} {p AND q} {2, 4 ANDI} PL {1} {7} {(p AND q) AND r} {5, 6 ANDI} EPHere there is only one assumption, which is inherited by every line because the conjunction rules cannot create or destroy assumptions. The conclusion is a conjunction, so the aim is to derive the two conjuncts in order to apply ANDI. This is achieved at lines 5 and 6. One of the conjuncts (p AND q) is again a conjunction, so first we derive its conjuncts at lines 2 and 4.
Proof 2
SP {p IMP q ⊢ (r IMP p) IMP (r IMP q)} PL {1} {1} {p IMP q} {A} PL {2} {2} {r IMP p} {A} PL {3} {3} {r} {A} PL {2,3} {4} {p} {2,3 IMPE} PL {1,2,3} {5} {q} {1,4 IMPE} PL {1,2} {6} {r IMP q} {5 [3] IMPI} PL {1} {7} {(r IMP p) IMP (r IMP q)} {6 [2] IMPI} EPThis is a classic proof by IMPI. Line 2 is the assumption of the antecedent of the desired conclusion; the aim is then to derive the consequent from it, which is achieved at line 6. The sub-goal is in turn another conditional r IMP q, so the conditional proof strategy is repeated, assuming the antecedent r at line 3 and deriving the conclusion q from it at line 5.
Proof 3
SP {(p IMP q) AND (q IMP r) ⊢ p IMP (p AND (q AND r))} PL {1} {1} {(p IMP q) AND (q IMP r)} {A} PL {2} {2} {p} {A} PL {1} {3} {p IMP q} {1 ANDE} PL {1} {4} {q IMP r} {1 ANDE} PL {1,2} {5} {q} {2, 3 IMPE} PL {1,2} {6} {r} {4, 5 IMPE} PL {1,2} {7} {q AND r} {5, 6 ANDI} PL {1,2} {8} {p AND (q AND r)} {2, 7 ANDI} PL {1} {9} {p IMP (p AND (q AND r))} {8 [2] IMPI} EPAgain the conclusion is a conditional p IMP (p AND (q AND r)) so again the strategy is to assume its antecedent p and try to derive its consequent p AND (q AND r). The latter is a conjunction, so as usual we derive the two conjuncts separately.
Proof 4
SP {p IMP (p IMP q) ⊢ p IMP q} PL {1} {1} {p IMP (p IMP q)} {A} PL {2} {2} {p} {A} PL {1,2} {3} {p IMP q} {1, 2 IMPE} PL {1,2} {4} {q} {2, 3 IMPE} PL {1} {5} {p IMP q} {4 [2] IMPI} EPThis little proof is worth a second look. What the sequent says in effect is that if p gets you from itself to q then p (all on its own) gets you to q. That is, once an assumption has been made it can be re-used as often as we like, and all of those uses may be discharged in one move. Line 5 is an immediate consequence of line 4, or if you like of the sub-derivation of q from p which occupies lines 2—4. It does not matter that the assumption of p is used more than once in this sub-derivation: the rules allow that. Notice that line 3 and line 5 are not the same. Line 3 represents the sequent with assumptions 1 and 2 (that is, p IMP (p IMP q) and p) as premises and p IMP q as conclusion; line 5 represents a sequent with the same conclusion and the same first premise but without the second premise p.
Proof 5
SP {p IMP q ⊢ (p AND r) IMP (q AND r)} PL {1} {1} {p IMP q} {A} PL {2} {2} {p AND r} {A} PL {2} {3} {p} {2 ANDE} PL {2} {4} {r} {2 ANDE} PL {1,2} {5} {q} {1, 3 IMPE} PL {1,2} {6} {q AND r} {4, 5 ANDI} PL {1} {7} {(p AND r) IMP (q AND r)} {6 [2] IMPI} EPThe conclusion of this sequent is a conditional, so we get it by assuming the antecedent p AND r and deriving the consequent q AND r. That is, lines 2—6 of the proof are a sub-derivation of which the conclusion (line 7) is an immediate consequence by IMPI.
Proof 6
SP {p IMP q, q IMP r, r IMP s, s IMP t ⊢ p IMP t} PL {1} {1} {p IMP q} {A} PL {2} {2} {q IMP r} {A} PL {3} {3} {r IMP s} {A} PL {4} {4} {s IMP t} {A} PL {5} {5} {p} {A } PL {1,5} {6} {q} {1, 5 IMPE} PL {1,2,5} {7} {r} {2, 6 IMPE} PL {1,2,3,5} {8} {s} {3, 7 IMPE} PL {1,2,3,4,5} {9} {t} {4, 8 IMPE} PL {1,2,3,4} {10} {p IMP t} {9 [5] IMPI} EPThe five assumptions are the four premises plus p, the antecedent of p IMP t, in preparation for the IMPI move at line 10. Then the chain of inferences (lines 6 – 9) through the successive conditionals is carried out entirely by means of the elimination rule ANDE. Note that the sequent proved at line 9 is
p IMP q, q IMP r, r IMP s, s IMP t, p ⊢ t
Finally, the assumption of p is discharged, leaving the required
p IMP q, q IMP r, r IMP s, s IMP t ⊢ p IMP t
Proof 7
SP {p ⊢ q IMP p} PL {1} {1} {p} {A} PL {1} {2} {q IMP p} {1 [] IMPI} EPThis illustrates the use of vacuous discharge. Although no assumption of q is used in deriving line 1, q can still be introduced as the antecedent of the conditional at the IMPI step. If it had been one of the assumptions, it could have been discharged, but such involvement of q in the sub-derivation is optional.
On the other hand, we may find it more convincing to go through a longer proof, avoiding vacuous discharge thus:
SP {p ⊢ q IMP p} PL {1} {1} {p} {A} PL {2} {2} {q} {A} PL {1,2} {3} {p AND q} {1, 2 ANDI} PL {1,2} {4} {p} {3 ANDE} PL {1} {5} {q IMP p} {4 [2] IMPI} EP