1. Everyone admires someone who admires them unless they admire

Quaid.

2. There are people who admire each other, at least one of whom admires

Quaid.

Suppose we want to use resolution to show that under one plausible reading of

these sentences, (2) is a ¬rst-order consequence of (1). The readings we have

in mind are the following, writing A(x, y) for Admires(x, y), and using q for the

name Quaid:

(S1 ) ∀x [¬A(x, q) ’ ∃y (A(x, y) § A(y, x))]

(S2 ) ∃x ∃y [A(x, q) § A(x, y) § A(y, x)]

(When you ¬gure out why S1 logically entails S2 in Problem 18.27, you may

decide that these are not reasonable translations of the English. But that is

beside the point here.)

Our goal is to show that S1 and ¬S2 are not jointly fo-satis¬able. The

sentence ¬S2 is equivalent to the following universal sentence, by DeMorgan™s

Laws:

∀x ∀y (¬A(x, q) ∨ ¬A(x, y) ∨ ¬A(y, x))

The sentence S1 is not logically equivalent to a universal sentence, so we

must Skolemize it. First, note that it is equivalent to the prenex form:

∀x ∃y [A(x, q) ∨ (A(x, y) § A(y, x))]

Skolemizing, we get the universal sentence,

∀x [A(x, q) ∨ (A(x, f(x)) § A(f(x), x))]

Putting the quanti¬er-free part of this in conjunctive normal form gives us:

∀x [(A(x, q) ∨ A(x, f(x))) § (A(x, q) ∨ A(f(x), x))]

This in turn is logically equivalent to the conjunction of the following two

sentences:

∀x [A(x, q) ∨ A(x, f(x))]

∀x [A(x, q) ∨ A(f(x), x))]

Next, we change variables so that no variable is used in two sentences, drop

the universal quanti¬ers, and form clauses from the results. This leaves us

with the following three clauses:

Section 18.7

524 / Advanced Topics in FOL

1. {A(x, q), A(x, f(x))}

2. {A(y, q), A(f(y), y)}

3. {¬A(z, q), ¬A(z, w), ¬A(w, z)}

Finally, we apply resolution to derive the empty clause.

Resolvent Resolved Clauses Substitution

4. {A(q, f(q))} 1, 3 q for w, x, z

5. {A(f(q), q)} 2, 3 q for w, y, z

6. {¬A(q, f(q))} 3, 5 f(q) for z, q for w

7. 4, 6 none needed

The FO Con routine of Fitch

The resolution method provides us with a way to try to demonstrate logical

automated deduction

consequence that is really rather di¬erent from giving an informal proof, or

even giving a formal proof in a system like F that models normal informal

methods. What it really involves is trying to build a counterexample to a claim

of ¬rst-order consequence. If the method ¬nds an insurmountable obstacle

to building such a counterexample, in the form of , then it declares the

conclusion a ¬rst-order consequence of the premises.

Methods like this turn out to be much more tractable to implement on

computers than trying to ¬nd a natural proof in a system like F . The reason

is that one can set things up in a systematic way, rather than requiring the

kind of semantic insight that is needed in giving proofs. After all, computers

cannot, at least not yet, really pay attention to the meanings of sentences, the

way we can.

You have learned that Fitch has a routine, FO Con, that checks for ¬rst-

FO Con routine

order consequence. While it does not actually use resolution, it uses a method

that is very similar in spirit. It basically tries to build a ¬rst-order structure

that is a counterexample to the claim of consequence. If it ¬nds an obstruction

to building such a structure, then it declares the inference valid. Of course

sometimes it is able to build such a counterexample. In these cases, it declares

the inference invalid. And then sometimes it simply runs out of steam, room,

or time, and, like the best of us, gives up.

Exercises

18.27 Give an informal proof that S2 is a log- 18.28 Give an informal proof that the sentence

ical consequence of S1 . given as a prenex form of S1 really is

logically equivalent to it.

Chapter 18

Resolution, revisited / 525

18.29 There are usually many ways to proceed 18.30 Use the resolution method to show that

in resolution. In our derivation of in the following sentence is a logical truth:

the last two examples, we chose optimal

∃x (P(x) ’ ∀y P(y))

derivations. Work out di¬erent deriva-

tions for both.

Section 18.7

Chapter 19

Completeness and

Incompleteness

This introduction to ¬rst-order logic culminates in discussions of two very

famous and important results. They are the so-called Completeness Theorem

and Incompleteness Theorem of fol. Both are due to the logician Kurt G¨del, o

no doubt the greatest logician yet. We present a complete proof of the ¬rst,

together with a explanation of the second, with just a sketch of its proof.

In this book you have learned the main techniques for giving proofs that

one statement is a logical consequence of others. There were simple valid rea-

soning steps and more intricate methods of proof, like proof by contradiction

or the method of general conditional proof. But the de¬nition of logical con-

sequence was fundamentally a semantic one: S is a logical consequence of

premises P1 ,. . . ,Pn if there is no way for the premises to be true without the

conclusion also being true. The question arises as to whether the methods of

proof we have given are su¬cient to prove everything we would like to prove.

Can we be sure that if S is a logical consequence of P1 ,. . . ,Pn , then we can

¬nd a proof of S from P1 ,. . . ,Pn ?

The answer is both yes and no, depending on just how we make the notion

of logical consequence precise, and what language we are looking at.

The answer to our question is yes if by logical consequence we mean ¬rst-

order consequence. G¨del™s Completeness Theorem for fol assures us that if S

o

G¨del™s Completeness

o

Theorem is a ¬rst-order consequence of some set T of ¬rst-order sentences then there is

a formal proof of S using only premises from T . The main goal of this chapter

is to give a full proof of this important result. The ¬rst such completeness

proof was given by G¨del in his dissertation in 1929. (His proof was actually

o

about a somewhat di¬erent formal system, one used by Bertrand Russell and

Alfred North Whitehead in their famous work Pincipia Mathematica, but the

formal systems have the same power.)

Suppose, though, that we are using some speci¬c ¬rst-order language and

we are interested in the logical consequence relation where the meaning of the

predicates of the language is taken into account. Do we need other methods

of proof? If so, can these somehow be reduced to those we have studied? Or

G¨del™s Incompleteness

o

Theorem is it conceivable that there simply is no complete formal system that captures

the notion of logical consequence for some languages? We will return to these

526

The Completeness Theorem for fol / 527

questions at the end of the chapter, with a discussion of interpreted languages

and G¨del™s Incompleteness Theorem.

o

Section 19.1

The Completeness Theorem for fol

The ¬rst few sections of this chapter are devoted to giving a complete proof

of the G¨del Completeness Theorem just referred to. We use the terms “the-

o

ory” and “set of sentences” interchangeably. (Some authors reserve the term theories

“theory” for a set of ¬rst-order sentences which is “closed under provability,”

that is, satisfying the condition that if T S then S ∈ T .) In this section we

write T S to mean there is a proof of S from the theory T in the full system T S

F .1 As mentioned in Chapter 17, this notation does not mean that all the

sentences in T have to be used in the formal proof of S, only that there is

a proof of S whose premises are all elements of T . In particular, the set T

could be in¬nite (as in the case of proofs from zfc or pa) whereas only a ¬nite

number of premises can be used in any one proof. This notation allows us to

state the Completeness Theorem as follows.

Theorem (Completeness Theorem for F). Let T be a set of sentences of a Completeness Theorem

for F

¬rst-order language L and let S be a sentence of the same language. If S is a

¬rst-order consequence of T , then T S.

Exactly as in the case of propositional logic, we obtain the following as an

immediate consequence of the Completeness Theorem.

Theorem (Compactness Theorem for fol). Let T be a set of sentences of Compactness Theorem

a ¬rst-order language L. If for each ¬nite subset of T there is a ¬rst-order

structure making this subset of T true, then there are ¬rst-order structures

M that makes all the sentences of T true.

The Completeness Theorem for fol was ¬rst established by Kurt G¨del, as

o

we mentioned above. The proof of the Completeness Theorem for ¬rst-order

consequence is, as we shall see, considerably subtler than for tautological

consequence. The proof we give here is simpler than G¨del™s original, though,

o

and is based on a proof known as the Henkin method, named after the logician Henkin method

Leon Henkin who discovered it.

Recall from Section 10.1 that the truth table method is too blunt to take

account of the meaning of either the quanti¬ers ∀ and ∃ or the identity symbol

1

Recall that the formal proof system F includes all the introduction and elimination

rules, but not the Con procedures.

Section 19.1

528 / Completeness and Incompleteness

=. In Exercise 18.12, we illustrated this defect. We noted there, for exam-

ple, that there are truth assignments that assign true to both the sentences

Cube(b) and ¬∃x Cube(x) (since from the point of view of propositional logic,

∃x Cube(x) is an atomic sentence unrelated to Cube(b)), whereas no ¬rst-order

structure can make both of these sentences true.

Henkin™s method ¬nds a clever way to isolate the exact gap between the

¬rst-order validities and the tautologies by means of a set of fol sentences H.

In a sense that we will make precise, H captures exactly what the truth table

method misses about the quanti¬ers and identity.2 For example, H will contain

the sentence Cube(b) ’ ∃x Cube(x), thereby ruling out truth assignments like

those mentioned above that assign true to both Cube(b) and ¬∃x Cube(x).

Here is an outline of our version of Henkin™s proof.

Adding witnessing constants: Let L be a ¬xed ¬rst-order language. We

witnessing constants

want to prove that if a sentence S of L is a ¬rst-order consequence of

a set T of L sentences, then T S. The ¬rst step is to enrich L to

a language LH with in¬nitely many new constant symbols, known as

witnessing constants, in a particular manner.

The Henkin theory: We next isolate a particular theory H in the enriched

Henkin theory (H)

language LH . This theory consists of various sentences which are not

tautologies but are theorems of ¬rst-order logic, plus some additional

sentences known as Henkin witnessing axioms. The latter take the form

∃x P(x) ’ P(c) where c is a witnessing constant. The particular constant

is chosen carefully so as to make the Henkin Construction Lemma and

Elimination Theorem (described next) true.

The Elimination Theorem: The Henkin theory is weak enough, and the

Elimination Theorem

formal system F strong enough, to allow us to prove the following (The-

orem 19.4): Let p be any formal ¬rst-order proof whose premises are all

either sentences of L or sentences from H, with a conclusion that is also

a sentence of L. We can eliminate the premises from H from this proof in

favor of uses of the quanti¬er rules. More precisely, there exists a formal

proof p whose premises are those premises of p that are sentences of L

and with the same conclusion as p.

The Henkin Construction: On the other hand, the Henkin theory is strong

Henkin construction

enough, and the notion of ¬rst-order structure wide enough, to allow us

to prove the following result (Theorem 19.5): for every truth assignment

2 This remark will be further illustrated by Exercises 19.3“19.5, 19.17 and 19.18, which

we strongly encourage you to do when you get to them. They will really help you understand

the whole proof.

Chapter 19

Adding witnessing constants / 529

h that assigns true to all w¬s in H there is a ¬rst-order structure Mh