Chapter 18

Truth and satisfaction, revisited / 507

Exercises

18.7 (Modifying variable assignments.) Suppose D = {a, b, c, d} and let g be the variable assignment

which is de¬ned only on the variable x and takes value b. Describe explicitly each of the

following:

1. g[y/c]

2. g[x/c]

3. g[z/b]

4. g[x/b]

5. (g[x/c])[z/d]

6. (g[x/c])[x/d]

18.8 Consider the language with only one binary predicate symbol P and let M be the structure

with domain D = {1, 2, 3} and where the extension of P consists of those pairs n, m such

that m = n + 1. For each of the following w¬s, ¬rst describe which variable assignments are

appropriate for it. Then describe the variable assignments which satisfy it, much the way we

described the variable assignments that satisfy the w¬ ∀z Likes(x, z) on page 501.

1. P(y,z)

2. ∃y P(y, z)

3. ∀z P(y, z)

4. P(x,x)

5. ∃x ¬P(x, x)

6. ∀x P(x, x)

7. P(x, x) ∨ P(y, z)

8. ∃x (P(x, x) ∨ P(y, z))

9. ∃y (P(x, x) ∨ P(y, z))

10. ∀y ∃z P(y, z)

11. ∀y ∃y P(y, z)

Now consider the structure N with the same domain but where the extension of P is the set

of those pairs n, m such that n ¤ m. How do your answers change?

18.9 Let g be a variable assignment in M which is appropriate for the w¬ P. Show that the following

three statements are equivalent:

1. g satis¬es P in M

2. g satis¬es P in M for some extension g of g

3. g satis¬es P in M for every extension g of g

Intuitively, this is true because whether a variable assignment satis¬es P can depend only on

the free variables of P, but it needs a proof. What does this result say in the case where P is

a sentence? Express your answer using the concept of truth. [Hint: You will need to prove this

by induction on w¬s.]

Section 18.2

508 / Advanced Topics in FOL

18.10 Give a proof of Proposition 1.

The next two exercises should be attempted before going on to Chapter 20. They contain some key insights

that will be important in the proof of the Completeness Theorem for F.

18.11 (From ¬rst-order structures to truth assignments.) Recall from Section 10.1 that when dealing

with sentences containing quanti¬ers, any sentence that starts with a quanti¬er is treated just

like an atomic sentence from the point of view of truth tables and hence truth assignments.

Given a ¬rst-order structure M for a language L, de¬ne a truth assignment hM as follows: for

any sentence S that is atomic or begins with a quanti¬er,

hM (S) = true if and only if M |= S

Show that the same “if and only if” holds for all sentences.

18.12 (From truth assignments to ¬rst-order structures.) Let h be any truth assignment for a ¬rst-

order language without function symbols. Construct a ¬rst-order structure Mh as follows. Let

the domain of M be the set of individual constants of the language. Given a relation symbol

R, binary let™s say for simplicity of notation, de¬ne its extension to be

{ c, d | h(R(c, d)) = true}

Finally, interpret each individual constant as naming itself.

1. Show that for any sentence S that does not contain quanti¬ers or the identity symbol:

Mh |= S i¬ h(S) = true

[Hint: use induction on w¬s.]

2. Show that the result in (1) does not extend to sentences containing the identity symbol.

[Hint: consider an h that assigns false to b = b.]

3. Recall from Section 10.1 that it is possible for a truth assignment h to assign true to

Cube(b) but false to ∃x Cube(x). Show that for such an h, the result in (1) does not

extend to quanti¬ed sentences.

18.13 (An important problem about satis¬ability.) Open Skolem™s Sentences. You will notice that

‚| these sentences come in pairs. Each even-numbered sentence is obtained from the preceding

sentence by replacing some names with variables and existentially quantifying the variables.

The odd-numbered sentence logically implies the even-numbered sentence which follows it, of

course, by existential generalization. The converse does not hold. But something close to it

does. To see what, open Thoralf™s First World and check the truth values of the sentences in

the world. The even numbered sentences all come out true, while the odd sentences can™t be

evaluated because they contain names not in use in the world.

Extend Thoralf™s First World by assigning the names b, c, d and e in such a way that the odd

Chapter 18

Soundness for fol / 509

numbered sentences are also true. Do the same for Thoralf™s Second World, saving the resulting

worlds as World 18.13.1 and World 18.13.2. Submit these worlds.

Explain under what conditions a world in which ∃x P(x) is true can be extended to one in

which P(c) is true. Turn in your explanation to your instructor.

Section 18.3

Soundness for fol

Having made the notion of ¬rst-order consequence more precise using the

notion of ¬rst-order structure, we are now in a position to state and prove

the Soundness Theorem for fol. Given a set T of sentences we write T S

to mean there is a proof of S from premises in T in the full system 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

Soundness Theorem as follows.

Theorem (Soundness of F ) If T S, then S is a ¬rst-order consequence of soundness of F

set T .

Proof: The proof is very similar to the proof of the Soundness The-

orem for FT , the propositional part of F, on page 215. We will show

that any sentence that occurs at any step in a proof p in F is a ¬rst-

order consequence of the assumptions in force at that step (which

include the premises of p). This claim applies not just to sentences

at the main level of proof p, but also to sentences appearing in sub-

proofs, no matter how deeply nested. The theorem follows from this

claim because if S appears at the main level of p, then the only as-

sumptions in force are premises drawn from T . So S is a ¬rst-order

consequence of T .

Call a step of a proof valid if the sentence at that step is a ¬rst-order

consequence of the assumptions in force at that step. Our earlier

proof of soundness for FT was actually a disguised form of induction

on the number of the step in question. Since we had not yet discussed

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

rules, but not the Con procedures.

Section 18.3

510 / Advanced Topics in FOL

induction, we disguised this by assuming there was an invalid step

and considering the ¬rst of these. When you think about it, you

see that this is really just the inductive step in an inductive proof.

Assuming we have the ¬rst invalid step allows us to assume that all

the earlier steps are valid, which is the inductive hypothesis, and

then prove (by contradiction) that the current step is valid after all.

We could proceed in the same way here, but we will instead make

the induction explicit. We thus assume that we are at the nth step,

that all earlier steps are valid, and show that this step is valid as

well.

The proof is by cases, depending on which rule is applied at step

n. The cases for the rules for the truth-functional connectives work

out pretty much as before. We will look at one, to point out the

similarity to our earlier soundness proof.

’ Elim: Suppose the nth step derives the sentence R from an appli-

cation of ’ Elim to sentences Q ’ R and Q appearing earlier in the

proof. Let A1, . . . , Ak be a list of all the assumptions in force at step

n. By our induction hypothesis we know that Q ’ R and Q are both

established at valid steps, that is, they are ¬rst-order consequences

of the assumptions in force at those steps. Furthermore, since F only

allows us to cite sentences in the main proof or in subproofs whose

assumptions are still in force, we know that the assumptions in force

at steps Q ’ R and Q are also in force at R. Hence, the assump-

tions for these steps are among A1 , . . . , Ak . Thus, both Q ’ R and

Q are ¬rst-order consequences of A1 , . . . , Ak . We now show that R is

a ¬rst-order consequence of A1 , . . . , Ak .

Suppose M is a ¬rst-order structure in which all of A1 , . . . , Ak are

true. Then we know that M |= Q ’ R and M |= Q, since these sen-

tences are ¬rst-order consequences of A1, . . . , Ak . But in that case,

by the de¬nition of truth in a structure we see that M |= R as well.

So R is a ¬rst-order consequence of A1 , . . . , Ak . Hence, step n is a

valid step.

Notice that the only di¬erence in this case from the corresponding

case in the proof of soundness of FT is our appeal to ¬rst-order

structures rather than rows of a truth table. The remaining truth-

functional rules are all similar. Let™s now consider a quanti¬er rule.

∃ Elim: Suppose the nth step derives the sentence R from an appli-

Chapter 18

Soundness for fol / 511

cation of ∃ Elim to the sentence ∃x P(x) and a subproof containing

R at its main level, say at step m. Let c be the new constant intro-

duced in the subproof. In other words, P(c) is the assumption of the

subproof containing R:

.

.

.

j. ∃x P(x)

.

.

.

c P(c)

.

.

.

m. R

.

.

.

.

.

.

n. R

Let A1 , . . . , Ak be the assumptions in force at step n. Our induc-

tive hypothesis assures us that steps j and m are valid steps, hence

∃x P(x) is a ¬rst-order consequence of the assumptions in force at

step j, which are a subset of A1 , . . . , Ak , and R is a ¬rst-order conse-

quence of the assumptions in force at step m, which are a subset of

A1, . . . , Ak , plus the sentence P(c), the assumption of the subproof

in which m occurs.

We need to show that R is a ¬rst-order consequence of A1 , . . . , Ak

alone. To this end, assume that M is a ¬rst-order structure in which

each of A1 , . . . , Ak is true. We need to show that R is true in M as

well. Since ∃x P(x) is a consequence of A1, . . . , Ak , we know that this

sentence is also true in M. Notice that the constant c cannot occur

in any of the sentences A1 , . . . , Ak , ∃x P(x), or R, by the restriction

on the choice of temporary names imposed by the ∃ Elim rule. Since

M |= ∃x P(x), we know that there is an object, say b, in the domain

of M that satis¬es P(x). Let M be exactly like M, except that it

assigns the object b to the individual constant c. Clearly, M |= P(c),

by our choice of interpretation of c. By Proposition 1 on page 505

M also makes each of the assumptions A1 , . . . , Ak true. But then

M |= R, because R is a ¬rst-order consequence of these sentences.

Since c does not occur in R, R is also true in the original structure

M, again by Proposition 1.

Section 18.3

512 / Advanced Topics in FOL

The case of ∀ Intro is very similar to ∃ Elim, and the remaining

two cases are much simpler. We leave these cases as exercises.

The Soundness Theorem for F assures us that we will never prove an in-

valid argument using just the rules of F. It also warns us that we will never be

able to prove a valid argument whose validity depends on meanings of pred-

icates other than identity. The Completeness Theorem for F is signi¬cantly

harder to prove than the Soundness Theorem for F, or for that matter, than

the Completeness Theorem for FT . In fact, it is the most signi¬cant theorem

that we prove in this book and forms the main topic of Chapter 19.

Exercises

18.14 Prove the inductive step in the sound- 18.15 Prove the inductive step in the sound-

ness proof corresponding to the rule § ness proof corresponding to the rule ’