30

Proof. Assume S is U -replete and open. We de¬ne an L-structure M by putting

UM = U and, for each n-ary predicate P of L,

PM = {(a1 , . . . , an ) ∈ U n : T P a1 · · · an ∈ S}

in the signed case, and

PM = {(a1 , . . . , an ) ∈ U n : P a1 · · · an ∈ S}

in the unsigned case.

We claim that for all L-U -sentences A,

(a) if S contains T A, then vM (A) = T

(b) if S contains F A, then vM (A) = F

in the signed case, and

(c) if S contains A, then vM (A) = T

(d) if S contains ¬ A, then vM (A) = F

in the unsigned case.

In both cases, the claim is easily proved by induction on the degree of A.

We give the proof for some representative cases.

1. deg(A) = 0. In this case A is atomic, say A = P a1 · · · an .

(a) If S contains T P a1 · · · an , then by de¬nition of M we have (a1 , . . . , an ) ∈

PM , so vM (P a1 · · · an ) = T.

(b) If S contains F P a1 · · · an , then S does not contain T P a1 · · · an since

S is open. Thus by de¬nition of M we have (a1 , . . . , an ) ∈ PM , so

/

vM (P a1 · · · an ) = F.

(c) If S contains P a1 · · · an , then by de¬nition of M we have (a1 , . . . , an ) ∈

PM , so vM (P a1 · · · an ) = T.

(d) If S contains ¬ P a1 · · · an , then S does not contain P a1 · · · an since

S is open. Thus by de¬nition of M we have (a1 , . . . , an ) ∈ PM , so

/

vM (P a1 · · · an ) = F.

2. deg(A) > 0 and A = ¬ B. Note that deg(B) < deg(A) so the inductive

hypothesis applies to B.

3. deg(A) > 0 and A = B & C. Note that deg(B) and deg(C) are < deg(A)

so the inductive hypothesis applies to B and C.

(a) If S contains T B & C, then by repleteness of S we see that S contains

both TB and TC. Hence by inductive hypothesis we have vM (B) =

vM (C) = T. Hence vM (B & C) = T.

31

(b) If S contains F B & C, then by repleteness of S we see that S contains

at least one of FB and FC. Hence by inductive hypothesis we have

at least one of vM (B) = F and vM (C) = F. Hence vM (B & C) = F.

(c) If S contains B & C, then by repleteness of S we see that S contains

both B and C. Hence by inductive hypothesis we have vM (B) =

vM (C) = T. Hence vM (B & C) = T.

(d) If S contains ¬ (B & C), then by repleteness of S we see that S con-

tains at least one of ¬ B and ¬ C. Hence by inductive hypothe-

sis we have at least one of vM (B) = F and vM (C) = F. Hence

vM (B & C) = F.

4. deg(A) > 0 and A = ∃x B. Note that for all a ∈ U we have deg(B[x/a]) <

deg(A), so the inductive hypothesis applies to B[x/a].

5. deg(A) > 0 and A = ∀x B. Note that for all a ∈ U we have deg(B[x/a]) <

deg(A), so the inductive hypothesis applies to B[x/a].

We shall now use Hintikka™s Lemma to prove the completeness of the tableau

method. As in Section 2.3, Let V = {a1 , . . . , an , . . .} be the set of parameters.

Recall that a tableau is a tree whose nodes carry L-V -sentences.

Lemma 2.5.4. Let „0 be a ¬nite tableau. By applying tableau rules, we can

extend „0 to a (possibly in¬nite) tableau „ with the following properties: every

closed path of „ is ¬nite, and every open path of „ is V -replete.

Proof. The idea is to start with „0 and use tableau rules to construct a sequence

of ¬nite extensions „0 , „1 , . . . , „i , . . .. If some „i is closed, then the construction

halts, i.e., „j = „i for all j ≥ i, and we set „ = „i . In any case, we set

∞

„ = „∞ = i=0 „i . In the course of the construction, we apply tableau rules

systematically to ensure that „∞ will have the desired properties, using the fact

that V = {a1 , a2 , . . . , an , . . .} is countably in¬nite.

Here are the details of the construction. Call a node X of „i quasiuniversal

if it is of the form T ∀x A or F ∃x A or ∀x A or ¬ ∃x A. Our construction begins

with „0 . Suppose we have constructed „2i . For each quasiuniversal node X of

„2i and each n ¤ 2i, apply the appropriate tableau rule to extend each open

path of „2i containing X by T A[x/an ] or F A[x/an ] or A[x/an ] or ¬ A[x/an ] as

the case may be. Let „2i+1 be the ¬nite tableau so obtained. Next, for each

non-quasiuniversal node X of „2i+1 , extend each open path containing X by

applying the appropriate tableau rule. Again, let „2i+2 be the ¬nite tableau so

obtained.

In this construction, a closed path is never extended, so all closed paths of

„∞ are ¬nite. In addition, the construction ensures that each open path of „∞

is V -replete. Thus „∞ has the desired properties. This proves our lemma.

Theorem 2.5.5 (the Completeness Theorem). Let X1 , . . . , Xk be a ¬nite

set of (signed or unsigned) sentences with parameters. If X1 , . . . , Xk is not

32

satis¬able, then there exists a ¬nite closed tableau starting with X1 , . . . , Xk . If

X1 , . . . , Xk is satis¬able, then X1 , . . . , Xk is satis¬able in the domain V .

Proof. By Lemma 2.5.4 there exists a (possibly in¬nite) tableau „ starting with

X1 , . . . , Xk such that every closed path of „ is ¬nite, and every open path of „

is V -replete. If „ is closed, then by K¨nig™s Lemma (Theorem 1.6.6), „ is ¬nite.

o

If „ is open, let S be an open path of „ . Then S is V -replete. By Hintikka™s

Lemma 2.5.3, S is satis¬able in V . Hence X1 , . . . , Xk is satis¬able in V .

De¬nition 2.5.6. Let L, U , and S be as in De¬nition 2.5.1. S is said to be

atomically closed if S contains a conjugate pair of atomic L-U -sentences. In

other words, for some n-ary L-predicate P and a1 , . . . , an ∈ U , S contains

T P a1 · · · an , F P a1 · · · an in the signed case, and P a1 · · · an , ¬ P a1 · · · an in the

unsigned case. S is atomically open if it is not atomically closed.

Exercise 2.5.7. Show that Lemmas 2.5.3 and 2.5.4 and Theorem 2.5.5 continue

to hold with “closed” (“open”) replaced by “atomically closed” (“atomically

open”).

Remark 2.5.8. Corollaries 1.5.9, 1.5.10, 1.5.11 carry over from the proposi-

tional calculus to the predicate calculus. In particular, the tableau method

provides a test for logical validity of sentences of the predicate calculus.

Note however that the test is only partially e¬ective. If a sentence A is

logically valid, we will certainly ¬nd a ¬nite closed tableau starting with ¬ A.

But if A is not logically valid, we will not necessarily ¬nd a ¬nite tableau which

demonstrates this. See the following example.

Example 2.5.9. In 2.2.12 we have seen an example of a sentence A∞ which

is satis¬able in a countably in¬nite domain but not in any ¬nite domain. It is

33

instructive to generate a tableau starting with A∞ .

A∞

.

.

.

∀x ∀y ∀z ((Rxy & Ryz) ’ Ryz)

∀x ∀y (Rxy ’ ¬ Ryx)

∀x ∃y Rxy

∃y Ra1 y

Ra1 a2

∀y (Ra1 y ’ ¬ Rya1 )

Ra1 a2 ’ ¬ Ra2 a1

\

/

¬ Ra1 a2 ¬ Ra2 a1

∃y Ra2 y

Ra2 a3

.

.

.

¬ Ra3 a2

∀y ∀z ((Ra1 y & Ryz) ’ Ra1 z)

∀z ((Ra1 a2 & Ra2 z) ’ Ra1 z)