<<

. 92
( 107 .)



>>




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 ’

<<

. 92
( 107 .)



>>