BOUNDS ON TRANSFER PRINCIPLES 5 III. METHODS FOR LIMITATION OF QUANTIFIERS This section gives a general framework for the limitation of quantifiers. By a limitation of quantifiers in a model K we mean that given a statement F the quantifiers Qx of F may be replaced by limited quantifiers Qxe A, where A C K and the limited quantifier has the obvious meaning, such that the limited statement is equivalent to the original in the theory of K. One may, of course, always make the trivial limitation A = K but we hope to make A a finite set. When A is a finite set which can be effectively determined and with which we can effectively compute the functions and relations of the theory, then we obtain a decision procedure for the theory of K. All of the results of this section are superficial but they provide a useful frame- work for organizing subsequent proofs. If E is an equivalence relation, then write [ajr- for the equivalence class containing a and write a = b for [a] F = [b] E . If D and E are equivalence relations on the same set, let D _ E mean that a = ^ b implies a = b for all a and b. Let L be a first order language, K a structure for L, and F a formula in L with i free variables. Let eq(F) be the equivalence relation on Kl such that a = /T ^ b iff F(a)*«- F(b) eq(-b) holds in K. For E an equivalence relation on K1 let pro(E) be the equivalence relation on K such that a = p r o /E ) a* iff { [a, b]^ | b e K } = { [a1, b']£ | b' e K } . That is, a and aT are pro(E) equivalent iff the set of E equivalence classes which project to a equals the set of E equivalence classes which project to a\ For E an equivalence relation on K1 and a e K^ with j i let E | a be the restriction of E to a x K1-^. That is, b = i - b] iff (a, b) = (a, b'). We allow j = 0 in which case we take a = the empty vector and E | a = E. LEMMA 1: If F is a formula with free variables x-^ to x^, Q is a quantifier, and E _ eq(F) then pro(E) eq(Q X i F). ***************************************************** PROOF: Say Q is "there exists", a = a!, E eq(F), and Qx, F(a,x.) holds in K. We have pro_(E) ~" l l b e K such that F(a, b) holds in K. Since a = ,„ a' we have b' e K such that (a, b) = ^ (a', br) so v pro(E)v \ v (a,b) = (a',b') and F(a',b') holds in K. Thus Qx[ F ^ x ^ holds in K. This shows that Qx^ F^jX^) - Qx^ F^'jX^). The reverse implication follows by symmetry and shows that a and a' are in the same eq(Qx. F) equivalence class. This proves pro(E) _ eq{Qx. F) and finishes the case Q = "there exists". The case Q = "for all" follows by taking negations. *****************************************************
Previous Page Next Page