Appendix: Examples Expressing generality
Proof 1
SP {NOTSOMEx Fx ⊢ ALLx NOTFx} PL {1} {1} {NOTSOMEx Fx} {A} PL {2} {2} {Fa} {A} PL {2} {3} {SOMEx Fx} {2 SOMEI} PL {1} {4} {NOTFa} {1, 3 [2] RAA} PL {1} {5} {ALLx NOTFx} {4 ALLI} EPWhat does this sequent say? It says that if no F exists, then everything that does exist is non-F. The reasoning is very simple: suppose (line 2) that some individual, which we'll call a, were F. Then (line 3) there would exist an F, contradicting the premise of the sequent, so (line 4) given the premise, a in particular is not an F. But the name a was chosen arbitrarily, so we can generalise (line 5): what is true of a is true of everything.
Proof 2
SP {ALLx NOTFx ⊢ NOTSOMEx Fx} PL {1} {1} {ALLx NOTFx} {A} PL {2} {2} {SOMEx Fx} {A} PL {3} {3} {Fa} {A} PL {1} {4} {NOTFa} {1 ALLE} PL {1,3} {5} {BAD} {3, 4 NOTE} PL {1,2} {6} {BAD} {2, 5 [3] SOMEE} PL {1} {7} {NOTSOMEx Fx} {6 [2] NOTI} EPThe converse of the previous sequent, this says that if everything in the world is non-F then no F exists. Again the reasoning is simple: suppose (line 2) there were an F; call it a (line 3). Then a has to be both F and not F, which is a contradiction (line 5). The Bad Thing BAD does not contain the name a, and nor does any side assumption, so this counts as a derivation of The Bad Thing from the existential (line 6). Hence, on the assumption of the premise, the existential assumption must be false.
In this proof we have used the NOTE and NOTI rules instead of RAA , partly for practice, and partly because they are convenient for getting a contradiction in which a does not occur.
Proof 3
SP {ALLx (Fx OR p) ⊢ p OR ALLx Fx} PL {1} {1} {ALLx (Fx OR p)} {A} PL {2} {2} {NOT(p OR ALLx Fx)} {A} PL {1} {3} {Fa OR p} {1 ALLE} PL {4} {4} {Fa} {A} PL {5} {5} {p} {A} PL {5} {6} {p OR ALLx Fx} {5 ORI} PL {2,5} {7} {NOTNOTFa} {2, 6 [ ] RAA} PL {2,5} {8} {Fa} {7 NOTNOTE} PL {1,2} {9} {Fa} {3, 4 [4], 8 [5] ORE} PL {1,2} {10} {ALLx Fx} {9 ALLI} PL {1,2} {11} {p OR ALLx Fx} {10 ORI} PL {1} {12} {NOTNOT(p OR ALLx Fx)} {2, 11 [2] RAA} PL {1} {13} {p OR ALLx Fx} {12 NOTNOTE} EPThis sequent says that a universal quantifier over a disjunction may be confined to one of the disjuncts if the variable it binds does not occur in the other. To prove it, we assume the negation of the desired conclusion (line 2) and derive a contradiction from it: in fact, we derive at line 11 the conclusion of which it is the negation, so RAA gets us to the double negation of what we want.
Proof 4
SP {SOMEx (Fx OR Gx) ⊢ SOMEx Fx OR SOMEx Gx} PL {1} {1} {SOMEx (Fx OR Gx)} {A} PL {2} {2} {Fa OR Ga} {A} PL {3} {3} {Fa} {A} PL {3} {4} {SOMEx Fx} {3 SOMEI} PL {3} {5} {SOMEx Fx OR SOMEx Gx} {4 ORI} PL {6} {6} {Ga} {A} PL {6} {7} {SOMEx Gx} {6 SOMEI} PL {6} {8} {SOMEx Fx OR SOMEx Gx} {7 ORI} PL {2} {9} {SOMEx Fx OR SOMEx Gx} {2, 5 [3], 8 [6] ORE} PL {1} {10} {SOMEx Fx OR SOMEx Gx} {1, 9 [2] SOMEE} EPHere the premise is existential, so the proof strategy is that for SOMEE. We assume at line 2 a typical instance of the existential, derive the desired conclusion from that (at line 9) and then, since the chosen name a does not occur in the conclusion, apply SOMEE to give a derivation of the same conclusion from assumption 1. The subproof occupying lines 2–9 proceeds by ORE, since line 2 is a disjunction. Note that the conclusion SOMEx Fx OR SOMEx Gx occurs no less than four times on different lines of the proof, but these four lines all represent different sequents because their assumptions are different