Restricted quantifiers revisited More about first order logic

When quantifiers were introduced, in Sheet 4 of these notes, they were defined as binary operators, applying to two formulae A and B to form longer formulae. The universal and existential quantifiers in particular are used to express the compound assertions "Every A is B" and "Some A is B" respectively. These are called restricted quantifiers, as they have the effect that the variable bound in B does not range over the whole domain but is restricted to the things (if any) satisfying A. When we came to the point of including them in the deduction system, however, we reduced them to the unary versions "Everything is B" and "Something is B". We should, now consider extending the deduction system a little to encompass proofs involving the binary versions of quantifiers.

Recall that where A′ and B′ are two formulae in which some name n occurs but the variable v does not, and where A and B result from them by substituting v for n, ALL(v: A) B is equivalent to the more familiar ALLv (A IMP B). We need rules for introducing and eliminating the former construction, and so should look at those for dealing with the latter and adapt them.

Recall that n is a "dummy" name used only to get the definition of the formula right. It never actually appears anywhere.

The elimination rule for the unary universal quantifier takes us from the universal ALLv (A IMP B) to any instance of it A^t_vIMP B^t_v where t is a term, possibly involving function symbols. To go further and eliminate the implication connective, we need to apply the conditional formula to its antecedent, detaching its consequent by the rule IMPE. Putting the two steps together, we obtain:

ALLv (A IMP B)		ALLE
	A^t_vIMP B^t_v		A^t_v	IMPE
	B^t_v

With the restricted quantifier in place of the unrestricted one and the connective, the two inference steps get collapsed into one:

	ALL(v: A) B	A^t_v	ALLE_R
	B^t_v

Note that we decorate the name of the rule with the letter 'R', meaning that it is applied to a restricted quantifier. This ALLE_R rule gives us a one-step proof of the validity, for example, of the sequent

ALL(x: Fx) Gx, Fa ⊢ Ga

which is precisely the form of the argument about Socrates the footballer with which this series of notes began. In order to conclude from the proposition that all footballers are bipeds that Socrates is a biped, we need the extra assumption that Socrates is a footballer.

The introduction rule for the restricted universal quantifier may be derived in a similar way from those for the conditional and the unresreicted quantifier. Where m is a name occurring in A and B, we pass from this


	X, A ⊢ B	IMPI
	X ⊢ A IMP B	IMPI	ALLI
X ⊢ ALLv ( A^v_m IMP B^v_m)			ALLI

to this

	X, A ⊢ B	ALLI_R
	X ⊢ ALL(v: A^v_m) B^v_m	ALLI_R

As before, the name m must not occur in any formula in X. It does occur in the discharged assumption A, of course.

Proofs using these restricted quantifier rules follow the same strategies as those using unrestricted quantifiers, except that some of the steps involving connectives are elided. For example:

SP {ALL(x: Fx) Gx ⊢ ALL(x: NOTGx) NOTFx} PL {1} {1} {ALL(x: Fx) Gx} {A} PL {2} {2} {NOTGa} {A} PL {3} {3} {Fa} {A} PL {1,3} {4} {Ga} {1, 3 ALLE_R} PL {1,2} {5} {NOTFa} {2, 4 [3] RAA} PL {1} {6} {ALL(x: NOTGx) NOTFx} {5 [2] ALLI_R} EP

The existential quantifier marches together with conjunction in the same way as the universal with implication. Thus the rules for introduction and elimination of the restricted existential quantifier may be derived from those for the unrestricted one and 'AND'.

Where A and B are the results of putting a variable v into formulae as for the ALLE rule above, and t is any term at all, with unrestricted quantifiers, we have:

A^t_v		B^t_v	ANDI
	A^t_v AND B^t_v	SOMEI	ANDI
	SOMEv (A AND B)	SOMEI

It is straightforward to turn this into an introduction rule for the restricted existential quantifier, with the same two inputs—which, we may note, can occur in either order:

	A^t_v		B^t_v	SOMEI_R
	SOME(v: A) B			SOMEI_R

Just as in the unrestricted case, of course, the direction of substitution is the opposite of the direction of the inference: A^t_v and B^t_v are the results of substituting term t for the variable v in A and B respectively.

The rule for eliminating the unrestricted existential quantifier gives us:

	X ⊢ SOMEv ( A^v_m AND B^v_m)		Y, A AND B ⊢ C	SOMEE
	X, Y ⊢ C			SOMEE

provided the name m does not occur in C or in any of the assumptions in Y. It is not too hard to see that we may rewrite this as a rule for the restricted existential quantifier thus:

	X ⊢ SOME(v: A^v_m) B^v_m		Y, A, B ⊢ C	SOMEE_R
	X, Y ⊢ C			SOMEE_R

with the same proviso. The only difference is that the two conjuncts A and B are now separate assumptions, both of which may be discharged. In fact, since they contain the name m, they may not remain in Y, so if they are present at all in the subproof, they must be discharged.

Note that the rules are given for the case where the quantifier binds a single variable only. Where there is more than one variable, we apply the rules as though the first variable were part of an unrestricted quantifier. That is, we think of ALL(x,y₁,..., y_n: A) B as short for ALLx ALL(y₁,..., y_n: A) B and reason with it on that basis. The existential quantifier with multiple variables is similar. Thus, for instance, ALL (y: Ray) (Fa OR Fy) is an immediate consequence of ALL(x,y: Rxy) (Fx OR Fy) by the rule ALLE for the unrestricted universal quantifier.

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

The classic sequents involving restricted quantification are those corresponding to syllogisms such as the one known in older literature as Darii:

All F is G;
Some H is F;
Therefore some H is G

RQproof shows a proof. Notice that the structure of the proof is similar to that we might expect from proving the analogous sequent with unrestricted quantifiers. Click here to see the two versions of this proof. If you wish to step through the construction for yourself, click here.

SP {ALL(x: Fx) SOMEy Rxy, ALLxALL(y: Rxy) (Ryx AND ALL(z: Ryz) Rxz) ⊢ ALL(x: Fx) Rxx} PL {1} {1} {ALL(x: Fx) SOMEy Rxy} {A} PL {2} {2} {ALLxALL(y: Rxy) (Ryx AND ALL(z: Ryz) Rxz)} {A} PL {3} {3} {Fa} {A} PL {1,3} {4} {SOMEy Ray} {1, 3 ALLE_R} PL {5} {5} {Rab} {A} PL {2} {6} {ALL(y: Ray) (Rya AND ALL(z: Ryz) Raz)} {2 ALLE} PL {2,5} {7} {Rba AND ALL(z: Rbz) Raz} {5, 6 ALLE_R} PL {2,5} {8} {Rba} {7 ANDE} PL {2,5} {9} {ALL(z: Rbz) Raz} {7 ANDE} PL {2,5} {10} {Raa} {8, 9 ALLE_R} PL {1,2,3} {11} {Raa} {4, 10 [5] SOMEE} PL {1,2} {12} {ALL(x: Fx) Rxx} {11 [3] ALLI_R} EP

The two kinds of quantifier may be mixed together. It is sometimes convenient to do so, but care must be taken in constructing proofs to use each rule in the right way for the right kind of formula. mixed shows an example. The sequent says that a relation which is symmetric and transitive (premise 2) and which is connected on things of type F (premise 1) is also reflexive on things satisfying F. The conclusion (12) is derived from a typical instance (11) discharging the appropriate assumption (3). Make sure you see how this is an instance of the rule ALLI_R. The typical instance (11) comes by SOMEE. This is "ordinary" old SOMEE, since the existential quantifier involved (4) is unrestricted. Although the name a occurs in the conclusion, this is fine because the name instantiating the existentially quantified variable y (5) is not a but b. The formula Raa (10) is derived by ALLE_R from the two lines just above it (8) and (9). These in turn are the two conjuncts of a conjunction (7). This in turn comes by ALLE_R, substituting b for the universally quantified variable y (6). Notice that (6) comes from (2) by ALLE for the unrestricted quantifier, as the x has to be instantiated first before the y becomes accessible.