Добавил:
Опубликованный материал нарушает ваши авторские права? Сообщите нам.
Вуз: Предмет: Файл:
Boolos et al. Computability and Logic, 5ed, CUP, 2007.pdf
Скачиваний:
593
Добавлен:
10.08.2013
Размер:
2.33 Mб
Скачать

19.2. SKOLEM NORMAL FORM

247

both satisfiable or both unsatisfiable, though generally when we prove the existence of such equivalents our proof will actually provide some additional information, indicating a stronger relationship between the two sets. Two different results on the existence of equivalents for satisfiability will be established in sections 19.2 and 19.4. In each case, will be shown to have an equivalent for satisfiability * whose sentences will be of a simpler type syntactically, but which will involve new nonlogical symbols.

In this connection some terminology will be useful. Let L be any language, and L+ any language containing it. Let Mbe an interpretation of L, and M+ an interpretation of L+. If the interpretations have the same domain and assign the same denotations to nonlogical symbols in L (so that the only difference is that the one assigns denotations to symbols of L+ not in L, while the other does not), then M+ is said to be an expansion of M to L+, and M to be the reduct of M+ to L. Note that the notions of expansion and reduct pertain to changing the language while keeping the domain fixed.

19.2 Skolem Normal Form

A formula in prenex form with all quantifies universal (respectively, existential) may be called a universal or -formula (respectively, an existential or -formula). Consider a language L and a sentence of that language in prenex form, say

(1)

x1 y1 x2 y2 R(x1, y1, x2, y2).

Now for each existential quantifier, let us introduce a new function symbol with as many places as there are universal quantifiers to its left, to obtain an expanded language L+. Thus in our example there would be two new function symbols, say f1 and f2, corresponding to y1 and y2, the former having one place corresponding to x1, and the latter two places corresponding to x1 and x2. Let us replace each existentially quantified variable by the term that results on applying the corresponding function symbol to the universally quantified variable(s) to its left. The resulting-formula, which in our example would be

(2)

x1 x2 R(x1, f1(x1), x2, f2(x1, x2))

is called the Skolem normal form of the original sentence, and the new function symbols occurring in it the Skolem function symbols.

A little thought shows that (2) logically implies (1). In any interpretation of the expanded language L+ with the new function symbols, it is the case that for every element a1 of the domain there is an element b1, such that for every element a2 there is an element b2, such that a1, b1, a2, b2 satify R(x1, y1, x2, y2): namely, take for b1 the result of applying to a1 the function denoted by f1, and for b2 the result of applying to a1 and a2 the function denoted by f2.

We cannot, of course, say that conversely (1) implies (2). What is true is that (2) is implied by (1) together with the following:

(3.1)

x1( y1 x2 y2 R(x1, y1, x2

, y2) x2 y2 R(x1, f1(x1), x2, y2))

(3.2)

x1 x2( y2 R(x1, f1(x1), x2

, y2) R(x1, f1(x1), x2, f2(x1, x2))).

248 NORMAL FORMS

For (1) and (3.1) imply

x1 x2 y2 R(x1, f1(x1), x2, y2)

which with (3.2) implies (2). The sentences (3) are called the Skolem axioms.

For a prenex formula of a different kind, with different numbers of universal and existential quantifiers, the number and number of places of the required Skolem functions would be different, and the Skolem axioms correspondingly so. For instance, for

(1 )

y0 x1 x2 y1 y2 x3 Q(y0, x1, x2, y1, y2, x3)

we would need one zero-place function symbol (which is to say, one constant) f0 and two two-place function symbols f1 and f2. The Skolem normal form would be

(2 )

x1 x2 x3 Q( f0, x1, x2, f1(x1, x2), f2(x1, x2), x3)

and the Skolem axioms would be

(3.0 )

y0 x1 x2 y1 y2 x3 Q(y0, x1, x2, y1, y2, x3)

(3.1 )

x1 x2 y1 y2 x3 Q( f0, x1, x2, y1, y2, x3)

x1 x2

( y1 y2 x3 Q( f0, x1, x2, y1, y2, x3)

(3.2 )

 

y2 x3 Q( f0, x1, x2, f1(x1, x2), y2, x3))

x1 x2

( y2 x3 Q( f0, x1, x2, f1(x1, x2), y2, x3)

 

 

x3 Q( f0, x1, x2, f1(x1, x2), f2(x1, x2), x3)).

But in exactly the same way in any example, the Skolem normal form will imply the original formula, and the original formula together with the Skolem axioms will imply the Skolem normal form.

If L is a language and L+ is the result of adding Skolem functions for some or all of its sentences, then an expansion M+ of an interpretation M of L to an interpretation of L+ is called a Skolem expansion if it is a model of the Skolem axioms.

19.6 Lemma (Skolemization). Every interpretation of L has a Skolem expansion.

Proof: The essential idea of the proof is sufficiently illustrated by the case of our original example (1) above. The proof uses a set-theoretic principle known as the axiom of choice. According to this principle, given any family of nonempty sets, there is a function ε whose domain is that family of sets, and whose value ε(X) for any set Y in the family is some element of Y . Thus ε ‘chooses’ an element out of each Y in the family. We apply this assumption to the family of nonempty subsets of |M| and use ε to define a Skolem expansion N = M+ of M.

We first want to assign a denotation f1N that will make the Skolem axiom (3.1) come out true. To this end, for any element a1 in |M| consider the set B1 of all b1in |M| such that a1 and b1 satisfy x2 y2 R(x1, y1, x2, y2) in M. If B1 is empty, then no matter what we take f1N (a1) to be, a1 will satisfy the conditional

y1 x2 y2 R(x1, y1, x2, y2) x2 y2 R(x1, f1(x1), x2, y2)

since it will not satisfy the antecedent. But for definiteness, let us say that if B1 is empty, then we are to take f1N (a1) to be ε(|M|). If B1 is nonempty, then we

19.2. SKOLEM NORMAL FORM

249

take f1N (a1) to be ε(B1): we use ε to choose one particular element b1 such that a1 and b1 satisfy x2 y2 R(x1, y1, x2, y2). Then since a1 and f1N (a1) will satisfyx2 y2 R(x1, y1, x2, y2), it follows that a1 will satisfy the foregoing conditional, and since this will be the case for any a1, it follows that (3.1) will be true.

We next want to assign a f2N that will make the Skolem axiom (3.2) come out true. We proceed in exactly the same way. For any a1 and a2, consider the set B2 of all b2 such that a1, a2, and b2 satisfy R(x1, f1(x1), x2, y2). If B1 is empty, we take f2N (a1, a2) to be ε(|M|), and otherwise take it to be ε(B2). The procedure would be the same no matter how many Skolem function symbols we needed to assign denotations to, and how many Skolem axioms we needed to make true.

Let be any set of sentences of any language L, and for each sentence A in , first associate to it a logically equivalent prenex sentence A* as in the preceding section, and then associate to A* its Skolem form A# as above, and let # be the set of all these sentences A# for A in . Then # is a set of -sentences equivalent for satisfiability to the original set . For if # is satisfiable, there is an interpretation N in which each A# in # comes out true, and since A# implies A* and A* is equivalent to A, we thus have an interpretation in which each A in comes out true, so is satisfiable. Conversely, if is satisfiable, there is an interpretation M of the original language in which each A in and hence each A* comes out true. By the preceding lemma, M has an expansion N to an interpretation in which each A* remains true and all Skolem axioms come out true. Since A* together with the Skolem axioms implies A#, each A# in # comes out true in N, and # is satisfiable. We have thus shown how we can associate to any set of sentences a set of -sentences equivalent to it for satisfiability. This fact, however, does not exhaust the content of the Skolemization lemma. For it can also be used to give a proof of the Lowenheim¨ –Skolem theorem, and in a stronger version than that stated in chapter 12 (and proved in chapter 13).

To state the strong Lowenheim¨ –Skolem theorem we need the notion of what it is for one interpretation B to be a subinterpretation of another interpretation A. Where function symbols are absent, the definition is simply that (1) the domain |B| should be a subset of the domain |A|, (2) for any b1, . . . , bn in |B| and any predicate R one has

(S1) RB(b1, . . . , bn ) if and only if RA((b1), . . . , (bn ))

and (3) for every constant c one has

(S2) (cB) = cA.

Thus, B is just like A, except that we ‘throw away’ the elements of |A| that are not in |B|.

Where function symbols are present, we have also to require that for any b1, . . . , bn in |B| and any function symbol f the following should hold:

(S3)

f B(b1, . . . , bn ) = f A(b1, . . . , bn ).

Note that this last implies that f A(b1, . . . , bn ) must be in |B|: Where function symbols are absent, any nonempty subset B of A can be the domain of a subinterpretation of A, but where function symbols are present, only those nonempty subsets B

250

NORMAL FORMS

can be the domains of subinterpretations that are closed under the functions f A that are the denotations of function symbols of the language, or in other words, that contain the value of any of these functions for given arguments if they contain the arguments themselves.

When B is a subinterpretation of A, we say that A is an extension of B. Note that the notions of extension and subinterpretation pertain to enlarging or contracting the domain, while keeping the language fixed.

Note that it follows from (S1) and (S3) by induction on complexity of terms that every term has the same denotation in B as in A. It then follows by (S1) and (S2) that any atomic sentence has the same truth value in B as in A. It then follows by induction on complexity that every quantifier-free sentence has the same truth value in B as in A. Essentially the same argument shows that, more generally, any given elements of B satisfy the same quantifier-free formulas in B as in A. If an-sentence x1 . . . xn R(x1, . . . , xn ) is true in B, then there are elements b1, . . . , bn of |B| that satisfy the quantifier-free formula R(x1, . . . , xn ) in B and hence, by what has just been said, in A as well, so that the -sentence x1. . . xn R(x1, . . . , xn ) is also true in A. Using the logical equivalence of the negation of an -sentence to an-sentence, we have the following result.

19.7 Proposition. Let A be any interpretation and B any subinterpretation thereof. Then any -sentence true in A is true in B.

19.8 Example (Subinterpretations). Proposition 19.7 is in general as far as one can go. For consider the language with just the two-place predicate <. Let P, Q, and R have domains the integers, rational numbers, and real numbers, respectively, and let the denotation of <in each case be the usual order relation < on the numbers in question. Since the order of integers qua integers is the same as their order qua rational numbers, and the order of rational numbers qua rational numbers is the same as their order qua real numbers, P is a subinterpretation of Q and R, and Q is a subinterpretation of R. Consider, however, the sentence

x y(x < y z(x <z & z < y))

or its prenex equivalent

x y z(x < y (x <z & z < y)).

R and Q are models of this sentence, since between any two real numbers a and b with a < b there is some other real number c with a < c and c < b, such as (b a)/2, and similarly for rational numbers. But P is not a model of the sentence, since between the integers 0 and 1 there is no other integer. (Of course, the sentence here is not an -sentence, but it is, so to speak, just one step beyond, an -sentence.)

Thus a subinterpretation of a model of a sentence C (or set of sentences ) may, but in general need not, also be a model of C (or ): if it is, it is called a submodel. Without further ado, here is the strong version of the Lowenheim¨–Skolem theorem. (The phrase ‘enumerable’ is redundant, given that we are restricting our attention to enumerable languages, but we include it to emphasize that we are making this restriction.)

19.2. SKOLEM NORMAL FORM

251

19.9 Theorem (Strong Lowenheim¨

–Skolem theorem). Let A be a nonenumerable

model of an enumerable set of sentences . Then A has an enumerable subinterpretation that is also a model of .

Proof: It will suffice to prove the theorem for the special case of sets of -sentences. For suppose we have proved the theorem in this special case, and consider the general case where A is a model of some arbitrary set of sentences . Then as in our earlier discussion, A has an expansion A# to a model of #, the set of Skolem forms of the sentences in . Since Skolem forms are -sentences, by the special case of the theorem there will an enumerable subinterpretation B# that is also a model of #. Then since the Skolem form of a sentence implies the original sentence, B# will also be a model of , and so will be its reduct B to the original language. But this B will be an enumerable subinterpretation of A.

To prove the theorem in the special case where all sentences in are -sentences, consider the set B of all denotations in A of closed terms of the language of . (We may assume there are some closed terms, since if not, we may add a constant c to the language and the logically valid sentence c = c to .) Since that language is enumerable, so is the set of closed terms, and so is B. Since B is closed under the functions that are denotations of the function symbols of the language, it is the domain of an enumerable subinterpretation B of A. And by Proposition 19.7, every-sentence true in A is true in B, so B is a model of .

Two interpretations A and B for the same language are called elementarily equivalent if every sentence true in the one is true in the other. Taking for in the above version of the Lowenheim¨ –Skolem theorem the set of all sentences true in A, the theorem tells us that any interpretation has an enumerable subinterpretation that is elementarily equivalent to it. A subinterpretation B of an interpretation A is called an elementary subinterpretation if for any formula F(x1, . . . , xn ) and any elements b1, . . . , bn of |B|, the elements satisfy the formula in A if and only if they satisfy it in B. This implies elementary equivalence, but is in general a stronger condition. By extending the notion of Skolem normal form to formulas with free variables, the above strong version of the Lowenheim¨ –Skolem theorem can be sharpened to a still stronger one telling us that any interpretation has an enumerable elementary subinterpretation.

Applications of Skolem normal form will be given in the next section. Since we are not going to be needing the sharper result stated in the preceding paragraph for these applications, we do not go into the (tedious but routine) details of its proof. Instead, before turning to applications we wish to discuss another, more philosophical issue. At one time the Lowenheim¨ –Skolem theorem (especially in the strong form in which we have proved it in this section) was considered philosophically perplexing because some of its consequences were perceived as anomalous. The apparent anomaly, sometime called ‘Skolem’s paradox’, is that there exist certain interpretations in which a certain sentence, which seems to say that nonenumerably many sets of natural numbers exist, is true, even though the domains of these interpretations contain only enumerably many sets of natural numbers, and the predicate in the sentence that we would be inclined to translate

252

NORMAL FORMS

as ‘set (of natural numbers)’ is true just of the sets (of natural numbers) in the domains.

19.10 Example (The ‘Skolem paradox’). There is no denying that the state of affairs thought to be paradoxical does obtain. In order to see how it arises, we first need an alternative account of what it is for a set E of sets of natural numbers to be enumerable, and for this we need to use the coding of an ordered pair (m, n) of natural numbers by a single number J (m, n), as described in section 1.2. We call a set w of natural numbers an enumerator of a set E of sets of natural numbers if

z(z is a set of natural numbers & z is in E x(x is a natural number &

z( y(y is a natural number (y is in z J (x, y) is in w)))).

The fact about enumerators and enumerability we need is that a set E of sets of natural numbers is enumerable if and only if E has an enumerator.

[The reason: suppose E is enumerable. Let e0, e1, e2, . . . be an enumeration of sets of natural numbers that contains all the members of E, and perhaps other sets of natural numbers also. Then the set of numbers J (x, y) such that y is in ex is an enumerator of E. Conversely, if w is an enumerator of E, then letting ex be the set of those numbers y such that J (x, y) is in w, we get an enumeration e0, e1, e2, . . . that contains all members of E, and E is enumerable.]

We want now to look at a language and some of its interpretations. The language contains just the following: constants 0, 1, 2, . . . , two one-place predicates N and S, a two-place predicate , and a two-place function symbol J. An interpretation I of the kind we are interested in will have as the elements of its domain all the natural numbers, some or all of the sets of natural numbers, and nothing else. The denotations of 0, 1, 2, and so on will be the numbers 0, 1, 2, and so on. The denotation of N will be the set of all natural numbers, and of S will be the set of all sets of natural numbers in the domain; while the denotation of will be the relation of membership between numbers and sets of numbers. Finally, the denotation of J will be the function J , extended to give some arbitrary value—say 17—for arguments that are not both numbers (that is, one or both of which are sets). Among such interpretations, the standard interpretation J will be the one in which the domain contains all sets of natural numbers.

Consider the sentence w F(w) where F(w) is the formula

Sw & z(Sz x(Nx & y(N y (y z J(x, y) w)))).

In each of the interpretations I that concern us, w F(w) will have a truth value. It will be true in I if and only if there is set in the domain of I that is an enumerator of the set of all sets of numbers that are in the domain of I , as can be seen by compairing the formula F(w) with the definition of enumerator above. We cannot say, more simply, that the sentence is true in the interpretation if and only if there is no enumerator of the set of all sets of numbers in its domain, because the quantifier w only ‘ranges over’ or ‘refers to’ sets in the domain.

There is, as we know, no enumerator of the set of all sets of numbers, so the sentencew F(w) is true in the standard interpetation J , and can be said to mean ‘nonenumerably many sets of numbers exist’ when interpreted ‘over’ J , since it then denies that there is an