Appendix: Examples Propositional natural deduction

Proof 1

SP {⊢ NOT(p AND NOTp)} PL {1} {1} {p AND NOTp} {A} PL {1} {2} {p} {1 ANDE} PL {1} {3} {NOTp} {1 ANDE} PL {} {4} {NOT(p AND NOTp)} {2, 3 [1] RAA} EP

This theorem, known as the law of non-contradiction, is obviously correct and simple enough to prove. Start by assuming that the contradiction p AND NOTp is true. That immediately leads to the two conflicting statements p and NOTp, so by RAA we can discharge and deny the absurd assumption.

Proof 2

SP {NOT(p AND q) ⊢ NOTp OR NOTq} PL {1} {1} {NOT(p AND q)} {A} PL {2} {2} {NOT(NOTp OR NOTq)} {A} PL {3} {3} {NOTp} {A} PL {3} {4} {NOTp OR NOTq} {3 ORI} PL {2} {5} {NOTNOTp} {2, 4 [3] RAA} PL {2} {6} {p} {5 NOTNOTE} PL {7} {7} {NOTq} {A} PL {7} {8} {NOTp OR NOTq} {7 ORI} PL {2} {9} {NOTNOTq} {2, 8 [7] RAA} PL {2} {10} {q} {9 NOTNOTE} PL {2} {11} {p AND q} {6, 10 ANDI} PL {1} {12} {NOTNOT(NOTp OR NOTq)} {1, 11 [2] RAA} PL {1} {13} {NOTp OR NOTq} {12 NOTNOTE} EP

This is a more complex proof. The sequent is of the form NOTA  ⊢  B, and the key move is to contrapose it and prove NOTB  ⊢  A. The two sub-proofs consisting of lines 3 — 6 and lines 7 — 10 are essentially similar. Line 11 puts them together. Since this contradicts line 1, we are done in a couple more steps. Note that this theorem essentially requires the rule NOTNOTE: without that it cannot be proved.

I like this sequent so much, I'll prove it again. This proof is shorter and a bit more direct, although the main point of assuming the negation of the desired conclusion in order to show that it can't fail is still the same:

Proof 2a

SP {NOT(p AND q) ⊢ NOTp OR NOTq} PL {1} {1} {NOT(p AND q)} {A} PL {2} {2} {NOT(NOTp OR NOTq)} {A} PL {3} {3} {p} {A} PL {4} {4} {q} {A} PL {3,4} {5} {p AND q} {3, 4 ANDI} PL {1,3} {6} {NOTq} {1, 5 [4] RAA} PL {1,3} {7} {NOTp OR NOTq} {6 ORI} PL {1,2} {8} {NOTp} {2, 7 [3] RAA} PL {1,2} {9} {NOTp OR NOTq} {8 ORI} PL {1} {10} {NOTNOT(NOTp OR NOTq)} {2, 9 [2] RAA} PL {1} {11} {NOTp OR NOTq} {10 NOTNOTE} EP

Proof 3

SP {NOTp OR NOTq ⊢ NOT(p AND q)} PL {1} {1} {NOTp OR NOTq} {A} PL {2} {2} {p AND q} {A} PL {2} {3} {p} {2 ANDE} PL {2} {4} {q} {2 ANDE} PL {5} {5} {NOTp} {A} PL {5} {6} {NOT(p AND q)} {3, 5 [2] RAA} PL {7} {7} {NOTq} {A} PL {7} {8} {NOT(p AND q)} {4, 7 [2] RAA} PL {1} {9} {NOT(p AND q)} {1, 6 [5], 8 [7] ORE} EP

This is simpler, although it requires a use of ORE. The premise is a disjunction, and each disjunct is easily shown to contradict the assumption at line 2. By ORE, therefore, that assumption has to be false given assumption 1.

Proof 4

SP {p OR p ⊢ p} PL {1} {1} {p OR p} {A} PL {2} {2} {p} {A} PL {1} {3} {p} {1, 2 [2], 2 [2] ORE} EP

There is not much to say about this short and sweet proof. Just make sure you see how the inference is an instance of the ORE rule as stated: the "two" assumptions of p are both the same, so we may as well recycle the first to do duty as the second. Then the two sub-derivations of p from the assumptions are so short that they contain no inferences at all, but only the assumption! Nonetheless, it meets all the criteria for being a proof.

Proof 5

SP {p IMP q, NOTp IMP q ⊢ q} PL {1} {1} {p IMP q} {A} PL {2} {2} {NOTp IMP q} {A} PL {3} {3} {NOTq} {A} PL {4} {4} {p} {A} PL {1,4} {5} {q} {1, 4 IMPE} PL {1,3} {6} {NOTp} {3, 5 [4] RAA} PL {1,2,3} {7} {q} {2, 6 IMPE} PL {1,2} {8} {NOTNOTq} {3, 7 [3] RAA} PL {1,2} {9} {q} {8 NOT¬E} EP

This sequent corresponds to a common form of argument: suppose q holds whether or not p holds; it follows that q is the case. The thought behind this is that p has to be either true or false, and either way we get q, so q holds no matter what. The structure of the proof, however, is a little different from this. On supposition that NOTq, p leads to a contradiction (because it implies q). p is therefore false if q is. But NOTp also implies q, so NOTq leads to its own negation, and hence to a contradiction, and so must be false. Finally, we have to infer q from NOTNOTq, and again this appeal to NOTNOTE is essential in the sense that the sequent cannot be proved without it.