. 95
( 107 .)


1. Everyone admires someone who admires them unless they admire
2. There are people who admire each other, at least one of whom admires

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
∀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
∀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.


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

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
G¨del™s Completeness
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
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
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

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.

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-
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
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,
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
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


. 95
( 107 .)