ńņš. 93 |

18.16 Prove the inductive step in the sound- 18.17 Prove the inductive step in the sound-

ness proof corresponding to the rule ā ness proof corresponding to the rule ā

Intro. Intro.

Section 18.4

The completeness of the shape axioms

In Section 12.5 (on page 339), we promised to convince you that the ten

axioms we gave for shape are complete, that is, that they completely bridged

the gap between ļ¬rst-order consequence and the intuitive notion of logical

consequence for the blocks language, as far as shape is concerned. We list the

axioms again here for your convenience:

Basic Shape Axioms:

1. Ā¬āx (Cube(x) ā§ Tet(x))

2. Ā¬āx (Tet(x) ā§ Dodec(x))

3. Ā¬āx (Dodec(x) ā§ Cube(x))

4. āx (Tet(x) āØ Dodec(x) āØ Cube(x))

SameShape Introduction Axioms:

Chapter 18

The completeness of the shape axioms / 513

5. āx āy ((Cube(x) ā§ Cube(y)) ā’ SameShape(x, y))

6. āx āy ((Dodec(x) ā§ Dodec(y)) ā’ SameShape(x, y))

7. āx āy ((Tet(x) ā§ Tet(y)) ā’ SameShape(x, y))

SameShape Elimination Axioms:

8. āx āy ((SameShape(x, y) ā§ Cube(x)) ā’ Cube(y))

9. āx āy ((SameShape(x, y) ā§ Dodec(x)) ā’ Dodec(y))

10. āx āy ((SameShape(x, y) ā§ Tet(x)) ā’ Tet(y))

We need to show that any argument that is logically valid in virtue of the

meanings of the shape predicates (and the ļ¬rst-order quantiļ¬ers, connectives,

and identity) is ļ¬rst-order valid once we add these ten axioms as premises.

To show this, it suļ¬ces to show that any ļ¬rst-order structure M making the

axioms true is just like one where the means of the four shape predicates is

the intended one.2

The reason this suļ¬ces is not hard to see. For suppose we have an argument

A that is valid in virtue of the meanings of the shape predicates. We want to

show that the result A of adding the ten axioms gives us an argument that is

ļ¬rst-order valid. To do this, it suļ¬ces to show that any ļ¬rst-order structure M

making the original premises and the ten axioms true is just like a structure

M where the predicates mean what they should. Hence, by the presumed

validity of the argument A in the latter such structures, the conclusion holds

in M . But since M is just like M , the conclusion also holds in M. Hence,

since the structure M was an arbitrary one making the original premises and

the ten axioms true, this will show that A is ļ¬rst-order valid.

So now let us prove our claim about M and M . Recall that M is any

ļ¬rst-order structure making our ten shape axioms true. Let Cu, Do, and T e

be the extensions in M of Cube, Dodec, and Tet, respectively. Axiom 1 insures

that Cu and T e are disjoint. Similarly, by Axioms 2 and 3, all three of the

sets are disjoint from the others. Axiom 4 insures us that everything in the

domain D of M is in one of these three sets.

Recall from Exercise 15.43 that a partition of D is a set P of non-empty

subsets of D with the property that every element of D is in exactly one

member of P. As we saw in that exercise, every such partition is the set of

equivalence classes of an equivalence relation, the relation of being in the same

member of the partition. This applied directly to our setting. Not all of these

2 What ājust likeā means here is that the structures are isomorphic, a notion we have

not deļ¬ned. The intuitive notion should be enough to convince you of our claim.

Section 18.4

514 / Advanced Topics in FOL

sets Cu, Do and T e need be non-empty, but if we restrict attention to those

that are, the preceding paragraph shows that we have a partition of D.

Now let S be the extension of SameShape in M. The remaining six axioms

insure that this relation is the equivalence relation generated by our partition.

Replace each object in Cu by a cube, each object in Do by a dodecahedron,

and each object in T e by a tetrahedron, making sure to use distinct blocks to

replace distinct objects of M. This is possible because we have a partition of

D. Call the resulting structure M . The extension of SameShape in M is just

the like S, except with the new blocks. Hence, the meaning of our predicates

is what we want it to be. Since the structures are otherwise unchanged, the

structures satisfy the same sentences of the blocks language.

Exercises

18.18 Let M be the structure whose domain 18.19 Let M be any ļ¬rst-order structure mak-

is the natural numbers, where Cube, ing the ļ¬rst four shape axioms true.

Dodec, and Tet have as extensions the Prove that there is a unique way to in-

sets of natural numbers of the forms 3n, terpret SameShape so as to make all ten

3n + 1, and 3n + 2. Can we interpret axioms true.

SameShape so as to make the ten shape

axioms true? If so, in how many ways

can we do this?

Section 18.5

Skolemization

One important role function symbols play in ļ¬rst-order logic is as a way of

simplifying (for certain purposes) sentences that have lots of quantiļ¬ers nested

inside one another. To see an example of this, consider the sentence

āx āy Neighbor(x, y)

Given a ļ¬xed domain of discourse (represented by a ļ¬rst-order structure M,

say) this sentence asserts that every b in the domain of discourse has at least

one neighbor c. Let us write this as

M |= Neighbor(x, y)[b, c]

rather than the more formal M |= Neighbor(x, y)[g] where g is the variable

assignment that assigns b to x and c to y. Now if the original quantiļ¬ed

Chapter 18

Skolemization / 515

sentence is true, then we can pick out, for each b, one of bā™s neighbors, say his

nearest neighbor or favorite neighbor. Let f (b) be this neighbor, so that we

have, for every b

M |= Neighbor(x, y)[b, f (b)]

Now, we would like to say the following: if we had a function symbol f ex-

pressing our function f.

M |= āx Neighbor(x, f(x))

This would reduce the quantiļ¬er string āāx āyā in the original sentence to the

simpler āāx.ā So we need to expand our ļ¬rst-order language and give ourselves

such a function symbol f to use as a name of f.

This important trick is known as Skolemization, after the Norwegian lo- Skolemization

gician Thoralf Skolem. The function f is called a Skolem function for the Skolem function

original quantiļ¬ed sentence. The new sentence, the one containing the func-

tion symbol but no existential quantiļ¬er, is called the Skolem normal form of Skolem normal form

the original sentence.

Notice that we did not say that a sentence is logically equivalent to its

Skolemization. The situation is a little more subtle than that. If our language

allowed existential quantiļ¬cation to apply to function symbols, we could get

a logically equivalent sentence, namely

āf āx P(x, f(x))

This sort of sentence, however, takes us into what is known as second-order

logic, which is beyond the scope of this book.

Skolem functions, and Skolem normal form, are very important in ad-

vanced parts of logic. We will discuss one application of them later in the

chapter, when we sketch how to apply the resolution method to fol with

quantiļ¬ers.

One of the reasons that natural language does not get bogged down in lots Skolemization in

natural language

of embedded quantiļ¬ers is that there are plenty of expressions that act like

function symbols, so we can usually get by with Skolemizations. Possessives,

for example, act as very general Skolem functions. We usually think of the

possessive āapostrophe sā as indicating ownership, as in Johnā™s car. But it re-

ally functions much more generally as a kind of Skolem function. For example,

if we are trying to decide where the group will eat out, then Maxā™s restaurant

can refer to the restaurant that Max likes best. Or if we are talking about

logic books, we can use Kleeneā™s book to refer not to one Kleene owns, but to

one he wrote.

Section 18.5

516 / Advanced Topics in FOL

Remember

(Simplest case of Skolemization) Given a sentence of the form āx āy P(x, y)

in some ļ¬rst-order language, we Skolemize it by choosing a function sym-

bol f not in the language and writing āx P(x, f(x)). Every world that makes

the Skolemization true also makes the original sentence true. Every world

that makes the original sentence true can be turned into one that makes

the Skolemization true by interpreting the function symbol f by a func-

tion f which picks out, for any object b in the domain, some object c

such that they satisfy the wļ¬ P(x, y).

Exercises

18.20 Discuss the logical relationship between 18.21 Skolemize the following sentence using

the following two sentences. [Hint: One the function symbol f.

is a logical consequence of the other, but

āz āy [(1 + (z Ć— z)) < y]

they are not logically equivalent.]

āy āz ParentOf(z, y) Which of the following functions on nat-

āy ParentOf(bestfriend(y), y) ural numbers could be used as a Skolem

function for this sentence?

Explain under what conditions the sec-

1. f(z) = z 2

ond would be a Skolemization of the

2. f(z) = z 2 + 1

ļ¬rst.

3. f(z) = z 2 + 2

4. f(z) = z 3

Section 18.6

Uniļ¬cation of terms

We now turn to a rather diļ¬erent topic, uniļ¬cation, that applies mainly to

languages that contain function symbols. Uniļ¬cation is of crucial importance

when we come to extend the resolution method to the full ļ¬rst-order language.

The basic idea behind uniļ¬cation can be illustrated by comparing a couple

of claims. Suppose ļ¬rst that Nancy tells you that Maxā™s father drives a Honda,

and that no oneā™s grandfather drives a Honda. Now this is not true, but there is

nothing logically incompatible about the two claims. Note that if Nancy went

on to say that Max was a father (so that Maxā™s father was a grandfather)

Chapter 18

Unification of terms / 517

we could then accuse her of contradicting herself. Contrast Nancyā™s claim

with Maryā™s, that Maxā™s grandfather drives a Honda, and that no oneā™s father

drives a Honda. Mary can be accused of contradicting herself. Why? Because

grandfathers are, among other things, fathers.

More abstractly, compare the following pairs, where P is a unary predicate

symbol, f and g are unary function symbols, and a is an individual constant.

First pair: P(f(a)), āx Ā¬P(f(g(x)))

Second pair: P(f(g(a))), āx Ā¬P(f(x))

The ļ¬rst pair is a logical possibility. It is perfectly consistent to suppose that

the object f (a) has property P but that no object of the form f(g(b)) has

property P . This can only happen, though, if a is not of the form g(b). By con-

trast, the second pair is not a logical possibility. Why? Because if āx Ā¬P(f(x))

holds, so does the instance where we substitute g(a) for x: Ā¬P(f(g(a))). But

this contradicts P(f(g(a))).

Uniļ¬cation gives us a useful test to see if sets of claims like the above are uniļ¬cation

contradictory or not. You look at the terms involved and see whether they are

āuniļ¬able.ā The terms f(a) and f(g(x)) in the ļ¬rst pair of sentences are not

uniļ¬able, whereas the terms in the second pair, f(g(a)) and f(x), are uniļ¬able.

What this means is that in the second case there is a way to substitute a term

for x so that the results coincide. This agreement produces a clash between

the two original sentences. In the ļ¬rst pair of terms, however, there is no such

way to make the terms coincide. No way of substituting a term in for the

variable x in f(g(x)) is going to give you the term f(a), since a is an individual

constant.

These examples motivate the following deļ¬nition.

Deļ¬nition Terms t1 and t2 are uniļ¬able if there is a substitution of terms for deļ¬nition of

uniļ¬able terms

some or all of the variables in t1 and t2 such that the terms that result from

the substitution are syntactically identical terms.

ńņš. 93 |