Quantifiers in proofs Expressing Generality
This section concerns the proof system of first-order logic or the lower predicate calculus. The notion of 'proof' is much as it was for sentential logic, except that we have a new definition of 'formula' and some new rules for introducing and eliminating quantifiers. The rules for connectives are simply inherited from the sentential case. We approach the quantifier rules by way of a simplification of the formal language. Our quantifiers are designed for saying things like 'Some bats eat fruit' and 'All kangaroos are marsupials'. Recall that these are written
SOME(x: Bx) Fx
ALL(x: Kx) Mx
respectively, with obvious mnemonic choice of predicate symbols. Now suppose we want to say not that some bat enjoys fruit but merely that something does; that there exists such a thing as a fructivore. Well, we could do it by paraphrasing as 'Something that eats fruit eats fruit'
SOME(x: Fx) Fx
though this is rather unnatural. It would be more convenient to have a notation for the unrestricted quantifier 'There exists something such that...' and the straightforward way to get one is simply to omit the sort indicator (and associated parentheses):
SOMEx Fx
We hereby officially extend our first order language by allowing quantifiers to be unrestricted, with the reading that they range not over things of a specified sort but over the whole universe. Because it is comparatively easy, and because it is standard, we shall develop the proof system in terms of unrestricted quantifiers only.
This extension of the language is more apparent than real, for we could have defined the unrestricted quantifiers in terms of restricted ones, by choosing a "restriction" that everything satisfies:
ALLvAvm
=def ALL(v: Fv
IMP Fv) Avm
SOMEvAvm
=def SOME(v: Fv
IMP Fv) Avm
4vAvm
=def 4(v: Fv
IMP Fv) Avm
MOST vAvm
=def MOST (v: Fv
IMP Fv) Avm
etc.
Alternatively, for the universal and existential quantifiers (though not for more exotic ones like 'most') we could have proceeded by defining SOMEv Avmto mean SOME(v: Avm) Avm. That is, we could have chosen to regard the unrestricted existential quantifier by definition as a mere abbreviation for a restricted one whose sort indicator is the same as the open formula constituting the rest of its scope. Having defined the unrestricted existential quantifier, we could add an unrestricted universal one simply by taking advantage of the duality between the two already noted, defining: ALLvAvmas NOT(SOMEv)NOTAvm. All that is to say, nothing has really changed when unrestricted quantifiers are allowed into first order logic, because in a good sense they were there all along. As far as the existential and universal quantifiers go, the converse is also true: we lose nothing essential by considering only the logic of these unrestricted cases, since anything we can express with restricted or sorted 'SOME' and 'ALL' is expressible with unrestricted quantifiers, aided by connectives. SOME(x: Fx) Gx is equivalent to SOMEx(Fx AND Gx) and ALL(x: Fx) Gx is equivalent to ALLx(Fx IMP Gx). These equivalences generalise easily to cases with formulas of any complexity in place of F and G. To see why they hold, consider first the existential SOMEx(Fx AND Gx). What this says is that there exists something which is both F and G. Plainly, any such thing is an F which is G, so if SOMEx(Fx AND Gx) is true then some F is G. Conversely, suppose that some F is G. That is, at least one of the Fs is G. Choose any such F; it is an F and it is a G, so there is something which is both F and G as required. The universal case is similar: ALLx(Fx IMP Gx) means 'Take anything you like: if it's an F then it's a G', and this is clearly true if every F is G. Without more ado, then, we shall proceed with the proof system for unrestricted quantifiers only.
|
|
The rules of ALLE (Universal Elimination) and SOMEI (Existential Introduction) are very easy to state, motivate and use. ALLE corresponds to the valid argument form known as instantiation. For example:
Everyone makes mistakes
Therefore Slaney makes mistakes
What is true of everything is true of any named thing in particular, including the author. The formal statement of the rule is given in rules1. To read the abstract notation, note that A is an open formula in which the variable v occurs, and that Amv is the formula which results from it by substituting the name m for v throughout.
SOMEI also corresponds to an obviously valid form of argument, the form of
We shall meet on Saturday
Therefore we shall meet sometime
That is, what is true of a particular time, such as Saturday, is thereby true of at least one time. The only detail to be noted in the way the SOMEI rule is stated is that the direction of inference is opposite from the direction of substitution (of name for variable). This becomes important when the name m occurs in SOMEv A, as in the inference from Fa IMP Fa to the further theorem SOMEx (Fx IMP Fa). That is, not all of the occurrences of m need turn into v.
SP {ALLx(Fx IMP Gx) ⊢ ALLx Fx IMP SOMEx Gx} PL {1} {1} {ALLx (Fx IMP Gx)} {A} PL {2} {2} {ALLx Fx} {A} PL {1} {3} {Fa IMP Ga} {1 ALLE} PL {2} {4} {Fa} {2 ALLE} PL {1,2} {5} {Ga} {3,4 IMPE} PL {1,2} {6} {SOMEx Gx} {5 SOMEI} PL {1} {7} {ALLx Fx IMP SOMEx Gx} {6 [2] IMPI} EP|
|
For a simple proof showing both ALLE and SOMEI, see easyproof. The sequent says that from the assumption that all Fs are Gs it follows that if everything is F then at least one thing is G. Notice that the annotation for each of these rules is just the input line number and the rule name. The assumption numbers are not affected by either rule.
The rules to introduce the universal quantifier and eliminate the existential one are a little harder to state and use because they are subject to some restrictions. It is convenient to approach them by comparing the quantifiers with the connectives AND and OR. The universal quantifier behaves rather like conjunction. To say that everyone who has been to the moon is American is rather like saying 'Armstrong is American and Aldrin is American and ...'. Similarly, the existential quantifier is kind of disjoiner: there is a prime number between 1000 and 1020 if either 1001 is prime or 1002 is prime or ... or 1019 is prime. Listing all the objects in the universe in this way, however, is not in general possible, which is why we have quantifiers.
|
The rule ALLE corresponds closely to ANDE. ANDE takes us from a conjunction to one of its conjuncts; ALLE takes us from a generalisation (like a big conjunction) to [any one of] its instances. Similarly, where ORI gives us a disjunction based on one of its disjuncts, SOMEI gives us an existential claim based on one of its instances. The remaining quantifier rules, not surprisingly, correspond similarly to ANDI and ORE. ANDI gives us the inference from both conjuncts to a conjunction, so analogously ALLI ought to take us from all the instances to a generalisation. Unfortunately, the universe tends to be infinite; and even if it is finite, some things in it may have no names. Physicists do not have to name every individual photon before they can reason about photons, for instance. So it is usually impossible to produce all the instances of a generalisation. What we do instead is to pick a typical instance and infer the generalisation from that. This is a familiar style of reasoning. In geometry, for example, we say 'Let ABC be a triangle,' and then go on to prove that it has at most one obtuse angle or whatever. Provided no assumptions have been made about ABC except for its triangularity, the result stands proved for all triangles. What is true of a really typical individual is true universally, since whatever reasoning was applied to it could have been applied equally to anything else. The formal rule corresponding to this kind of reasoning is shown in allI. Notice the proviso which ensures that the arbitrary name involved is indeed typical. If the conclusion had depended on side assumptions which mentioned m then to generalise the case would have been unfair. That is, special pleading is ruled out. Notice also that the substitution this time is of variable v for name m , not the other way about as it was for ALLE. This blocks the fallacious "proof":
SP {⊢ ALLx ALLy(Fx IMP Fy)} PL {1} {1} {Fb} {A} PL {} {2} {Fb IMP Fb} {1 [1] IMPI} PL {} {3} {ALLy (Fb IMP Fy)} {2 ALLI ??? No!} PL {} {4} {ALLx ALLy (Fx IMP Fy)} {3 ALLI} EP|
|
Of course, it would have been entirely in order to infer at line (3)
ALLy (Fy IMP Fy).
SP {ALLx (Fx IMP Gx) ⊢ ALLx(NOTGx IMPNOTFx)} PL {1} {1} {ALLx (Fx IMP Gx)} {A} PL {2} {2} {NOTGa} {A} PL {1} {3} {Fa IMP Ga} {1 ALLE} PL {4} {4} {Fa} {A} PL {1,4} {5} {Ga} {3,4 IMPE} PL {1,2} {6} {NOTFa} {2,5 [4] RAA} PL {1} {7} {NOTGa IMP NOTFa} {6 [2] IMPI} PL {1} {8} {ALLx (NOTGx IMPNOT Fx)} {7 ALLI} EP|
|
allIproof shows a correct proof in which ALLE and ALLI work together: The proof strategy is worth a second look. The desired conclusion is universal in form, so it will be derived from a typical instance by ALLI . That is, the intermediate goal is to prove the sequent
ALLx (Fx IMP Gx) ⊢ NOTGa IMP NOTFa
which will be achieved at line (7). The conclusion of this new goal is a conditional, so the usual IMPI strategy applies. That is why NOTGa is assumed at line (2). The IMPI strategy gives us a further new goal
ALLx (Fx IMP Gx), NOTGa ⊢ NOTFa
The conclusion of this is negative in form, so naturally we assume Fa, the formula to be negated, and aim for a contradiction. In fact, we easily get Ga at line (5), contradicting the earlier assumption of NOTGa. The assumptions involving the arbitrary name a must be discharged before we are allowed to generalise.
It may be useful to reconstruct this proof yourself, using the proof editor. Try it here if you like.
SOMEE is related to ORE much as ALLI is to ANDI. The upshot of ORE is that a disjunction entails just what follows regardless of which disjunct we choose. SOMEE reflects an analogous principle which mathematicians call the Rule of Choice. If a conclusion B follows from a premise Am whatever name we take for m then it follows from the existence of something or other satisfying the description A. The rule of choice is in very common use. If we are proving a theorem about, say, groups of exponent 6 we may well say '... So there exist elements x such that xn ≠ e for all n < 6. Choose one such element; call it a. Now... ' Then we reason some more until we reach a conclusion to which the particular identity of a is irrelevant, at which point we are justified in asserting that conclusion based just on the existential. As in the case of ALLI, we have to ensure that the chosen term is typical. This requires that it not occur in the conclusion (otherwise we should have proved only some fact about a, not a general one) and also that it not occur in any side assumptions on which the conclusion depends.
|
||||||||
The formal statement of SOMEE is given in someE. Note that m is an arbitrary name which occurs at least once in formula A. Note also that again the substitution is so defined that m may not occur in the existential premise SOMEv Avm. The way to ensure this in practice is to choose an arbitrary name which is foreign to the entire context of the rest of the proof. The annotation for SOMEE in the linear proof format consists of the two input line numbers, together with the number of the discharged assumption A, and the rule name.
Applications of SOMEE have to be "set up" in a way reminiscient of ORE, though not as complicated because only one sub-proof is involved instead of two. Given an existential formula to be broken up by SOMEE, first assume a typical instance of it (using a name which does not occur in the desired conclusion or side assumptions). Then derive the conclusion from it. Notice that the special assumption is just that—an assumption produced by the rule A—and not in any way derived from the existential.
There now follows a proof illustrating the strategy associated with SOMEE. It constitutes part of a demonstration that as long as every formula remains well-formed, bound variables may be re-rwitten without changing the sense of anything. So SOMEx Fx is the same thing as SOMEy Fy, both expressing 'Something is F'.
SP {SOMEx Fx ⊢ SOMEy Fy} PL {1} {1} {SOMEx Fx} {A} PL {2} {2} {Fa} {A} PL {2} {3} {SOMEy Fy} {2 SOMEI} PL {1} {4} {SOMEy Fy} {1,3 [2] SOMEE} EP|
|
Here the premise is existential, so the SOMEE strategy applies. We should try to get the conclusion from a typical instance. So assume one. Note that the rule is that for assumptions, not SOMEE at this stage. The SOMEI rule lets us remove the name a in favour of a variable so that SOMEE can apply without violating the restriction on its use. This combination of SOMEI followed by SOMEE is very common. It should be easy to remember 'I before E'.
Now here is a proof of the validity of the argument with which this chapter began: All logicians are rational; some philosophers are not rational; so not all philosophers are logicians:
SP {ALLx (Lx IMP Rx), SOMEx (Px AND NOTRx) ⊢ NOTALLx (Px IMP Lx)} PL {1} {1} {ALLx (Lx IMP Rx)} {A} PL {2} {2} {SOMEx (Px AND NOTRx)} {A} PL {3} {3} {ALLx (Px IMP Lx)} {A} PL {4} {4} {Pa AND NOTRa} {A} PL {3} {5} {Pa IMP La} {3 ALLE} PL {4} {6} {Pa} {4 ANDE} PL {3,4} {7} {La} {5, 6 IMPE} PL {1} {8} {La IMP Ra} {1 ALLE} PL {1,3,4} {9} {Ra} {7, 8 IMPE} PL {4} {10} {NOTRa} {4 ANDE} PL {1,4} {11} {NOTALLx (Px IMP Lx)} {9, 10 [3] RAA} PL {1,2} {12} {NOTALLx (Px IMP Lx)} {2, 11 [4] SOMEE} EP|
|
For the walkthrough, click here.
Alternatively (or additionally) reconstruct it yourself.