# 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} EP
What 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} EP
The 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} EP
Here 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
SOME*x Fx* OR SOME*x 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