Appendix: Examples More about first order logic

The following proofs illustrate the rules of immediate consequence for restricted quantifiers.

Proof 1

SP {ALL(x: Fx) Gx, ALL(x: Gx) Hx ⊢ ALL(x: Fx) Hx} PL {1} {1} {ALL(x: Fx) Gx} {A} PL {2} {2} {ALL(x: Gx) Hx} {A} PL {3} {3} {Fa} {A} PL {1,3} {4} {Ga} {1, 3 ALLE_R} PL {1,2,3} {5} {Ha} {2, 4 ALLE_R} PL {1,2} {6} {ALL(x: Fx) Hx} {5 [3] ALLI_R} EP

This argument form was among the first ever pointed out as valid by Aristotle, and was known in traditional logical theory as the syllogism "AAA in the first figure" or by the mnemonic "Barbara". Note that restricted quantifiers allow it to be stated and proved without the use of any connectives.

Proof 2

SP {ALL(x: Fx) Gx, ALL(x: Hx) NOTGx ⊢ ALL(x: Fx) NOTHx} PL {1} {1} {ALL(x: Fx) Gx} {A} PL {2} {2} {ALL(x: Hx) NOTGx} {A} PL {3} {3} {Fa} {A} PL {1,3} {4} {Ga} {1, 3 ALLE_R} PL {5} {5} {Ha} {A} PL {2,5} {6} {NOTGa} {2, 5 ALLE_R} PL {1,2,3} {7} {NOTHa} {4, 6 [5] RAA} PL {1,2} {8} {ALL(x: Fx) NOTHx} {7 [3] ALLI_R} EP

This is quite straightforward. Note that the assumptions Fa and Ha are necessary for ALLE_R to apply, and that they are discharged later. The contradiction at lines 4 and 6 could be used to negate any of the four assumptions. Having derived at line 7 that a is not H, we conclude that every F satisfies NOTH, discharging the assumption that a is one of the Fs.

Proof 3

SP {NOTSOME(x: Fx) Gx ⊢ ALL(x: (Fx AND Gx)) Hx} PL {1} {1} {NOTSOME(x: Fx) Gx} {A} PL {2} {2} {Fa AND Ga} {A} PL {2} {3} {Fa} {2 ANDE} PL {2} {4} {Ga} {2 ANDE} PL {2} {5} {SOME(x: Fx) Gx} {3, 4 SOMEI_R} PL {1,2} {6} {NOTNOTHa} {1, 5 [ ] RAA} PL {1,2} {7} {Ha} {6 NOTNOTE} PL {1} {8} {ALL(x: (Fx AND Gx)) Hx} {7 [2] ALLI_R} EP

Apart from the vacuous discharge used to blame the contradiction on NOTHa, there is little to note here. Again line 2 is assumed in order to get a typical instance for the universal generalisation step. The sub-derivation at lines 2 – 5 also occurs in showing that SOMEx (Fx AND Gx) implies SOME(x: Fx) Gx. At the final step, the assumed conjunction becomes the sort indicator of the restricted universal quantifier.

Proof 4

SP {ALL(x: Fx) Hx, ALL(x: Gx) Hx ⊢ ALL(x: Fx OR Gx) Hx} PL {1} {1} {ALL(x: Fx) Hx} {A} PL {2} {2} {ALL(x: Gx) Hx} {A} PL {3} {3} {Fa OR Ga} {A} PL {4} {4} {Fa} {A} PL {1,4} {5} {Ha} {1, 4 ALLE_R} PL {6} {6} {Ga} {A} PL {2,6} {7} {Ha} {2, 6 ALLE_R} PL {1,2,3} {8} {Ha} {3, 5 [4], 7 [6] ORE} PL {1,2} {9} {ALL(x: Fx OR Gx) Hx} {8 [3] ALLI_R} EP

This is more of the same. Work through it with the proof editor, just to remind yourself of how to operate ORE in such contexts.

Proof 5

SP {ALL(x: Fx) SOME(y: Rxy) Gy ⊢ ALL(y: Fy) SOME(x: Ryx) Gx} PL {1} {1} {ALL(x: Fx) SOME(y: Rxy) Gy} {A} PL {2} {2} {Fa} {A} PL {1,2} {3} {SOME(y: Ray) Gy} {1, 2 ALLE_R} PL {4} {4} {Rab} {A} PL {5} {5} {Gb} {A} PL {4,5} {6} {SOME(x: Rax) Gx} {4, 5 SOMEI_R} PL {1,2} {7} {SOME(x: Rax) Gx} {3, 6 [4, 5] SOMEE_R} PL {1} {8} {ALL(y: Fy) SOME(x: Ryx) Gx} {7 [2] ALLI_R} EP

As in the case of unrestricted quantifiers, variables may be rewritten without changing anything essential.