. .
∀x A ¬ ∃x A
. .
. .
. .
 
¬ A[x/a]
A[x/a]
where a is an arbitrary parameter
. .
. .
. .
∃x A ¬ ∀x A
. .
. .
. .
 
¬ A[x/a]
A[x/a]
where a is a new parameter
Remark 2.3.3. In the above tableau rules, “a is new” means that a does not
occur in the path that is being extended. Or, we can insist that a not occur in
the tableau that is being extended.
Remark 2.3.4. We are going to prove that the tableau method for predicate
calculus is sound (Theorem 2.3.9) and complete (Theorem 2.5.5). In particular,
a sentence A of the predicate calculus is logically valid if and only if there exists
a ¬nite closed signed tableau starting with F A, or equivalently a ¬nite closed
unsigned tableau starting with ¬ A.
24
Example 2.3.5. The signed tableau
F (∃x ∀y Rxy) ’ (∀y ∃x Rxy)
T ∃x ∀y Rxy
F ∀y ∃x Rxy
T ∀y Ray
F ∃x Rxb
T Rab
F Rab
is closed. Therefore, by the Soundness Theorem, (∃x ∀y Rxy) ’ (∀y ∃x Rxy) is
logically valid.
Example 2.3.6. The unsigned tableau
¬ (∃x (P x ∨ Qx)) ” ((∃x P x) ∨ (∃x Qx))
\
/
∃x (P x ∨ Qx) ¬ ∃x (P x ∨ Qx)
¬ ((∃x P x) ∨ (∃x Qx)) (∃x P x) ∨ (∃x Qx)
¬ ∃x P x \
/
¬ ∃x Qx ∃x P x ∃x Qx
P a ∨ Qa Pa Qa
/\ ¬ (P a ∨ Qa) ¬ (P a ∨ Qa)
¬Pa ¬Pa
Pa Qa
¬Pa ¬ Qa ¬ Qa ¬ Qa
is closed. Therefore, by the Soundness Theorem,
(∃x (P x ∨ Qx)) ” ((∃x P x) ∨ (∃x Qx))
is logically valid.
The rest of this section is devoted to proving the Soundness Theorem 2.3.9.
De¬nition 2.3.7.
1. An LV structure consists of an Lstructure M together with a mapping
φ : V ’ UM . If A is an LV sentence, we write
Aφ = A[a1 /φ(a1 ), . . . , ak /φ(ak )]
where a1 , . . . , ak are the parameters occurring in A. Note that Aφ is an
LUM sentence. Note also that, if A is an Lsentence, then Aφ = A.
2. Let S be a ¬nite or countable set of (signed or unsigned) LV sentences.
An LV structure M, f is said to satisfy S if vM (Aφ ) = T for all A ∈ S.
S is said to be satis¬able 6 if there exists an LV structure satisfying S.
Note that this de¬nition is compatible with De¬nition 2.2.7.
6 Similarly, the notions of logical validity and logical consequence are extended to LV 
sentences, in the obvious way, using LV structures. An LV sentences is said to be logically
valid if it satis¬ed by all LV structures. An LV sentence is said to be a logical consequence
of S if it is satis¬ed by all LV structures satisfying S.
25
3. Let „ be an Ltableau. We say that „ is satis¬able if at least one path of
„ is satis¬able.
Lemma 2.3.8. Let „ and „ be tableaux such that „ is an immediate extension
of „ , i.e., „ is obtained from „ by applying a tableau rule to a path of „ . If „
is satis¬able, then „ is satis¬able.
Proof. The proof consists of one case for each tableau rule. We consider some
representative cases.
Case 1. Suppose that „ is obtained from „ by applying the rule
.
.
.
A∨B
.
.
.
/\
A B
to the path θ in „ , where a is a parameter. Since „ is satis¬able, it has at least
one satis¬able path, S. If S = θ, then S is a path of „ , so „ is satis¬able. If
S = θ, then θ is satis¬able, so let M and φ : V ’ UM satisfy θ. In particular
vM ((A ∨ B)φ ) = T, so we have at least one of vM (Aφ ) = T and vM (B φ ) = T.
Thus M and f satisfy at least one of θ, A and θ, B. Since these are paths of „ ,
it follows that „ is satis¬able.
Case 2. Suppose that „ is obtained from „ by applying the rule
.
.
.
∀x A
.
.
.

A[x/a]
to the path θ in „ . Since „ is satis¬able, it has at least one satis¬able path,
S. If S = θ, then S is a path of „ , so „ is satis¬able. If S = θ, then θ is
satis¬able, so let M and φ : V ’ UM satisfy θ. In particular vM (∀x (Aφ )) =
vM ((∀x A)φ ) = T, so vM (Aφ [x/c]) = T for all c ∈ UM . In particular
vM (A[x/a]φ ) = vM (Aφ [x/φ(a)]) = T.
Thus M and φ satisfy θ, A[x/a]. Since this is a path of „ , it follows that „ is
satis¬able.
Case 3. Suppose that „ is obtained from „ by applying the rule
.
.
.
∃x A
.
.
.

A[x/a]
26
to the path θ in „ , where a is a new parameter. Since „ is satis¬able, it has at
least one satis¬able path, S. If S = θ, then S is a path of „ , so „ is satis¬able.
If S = θ, then θ is satis¬able, so let M and φ : V ’ UM satisfy θ. In particular
vM (∃x (Aφ )) = vM ((∃x A)φ ) = T, so vM (Aφ [x/c]) = T for at least one c ∈ UM .
Fix such a c and de¬ne φ : V ’ UM by putting φ (a) = c, and φ (b) = φ(b) for
all b = a, b ∈ V . Since a is new, we have B φ = B φ for all B ∈ θ, and Aφ = Aφ ,
hence A[x/a]φ = Aφ [x/φ (a)] = Aφ [x/c]. Thus vM (B φ ) = vM (B φ ) = T for all
B ∈ θ, and vM (A[x/a]φ ) = vM (Aφ [x/c]) = T. Thus M and φ satisfy θ, A[x/a].
Since this is a path of „ , it follows that „ is satis¬able.
Theorem 2.3.9 (the Soundness Theorem). Let X1 , . . . , Xk be a ¬nite set
of (signed or unsigned) sentences with parameters. If there exists a ¬nite closed