<< Ļšåäūäółą’ ńņš. 93(čē 107 ńņš.)ĪĆĖĄĀĖÅĶČÅ Ńėåäóžłą’ >>
Intro. Intro.

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
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(čē 107 ńņš.)ĪĆĖĄĀĖÅĶČÅ Ńėåäóžłą’ >>