Proof. Let „ be a closed tableau starting with X1 , . . . , Xk . Thus there is a ¬nite

sequence of tableaux „0 , „1 , . . . , „n = „ such that

X1

„0 = ..

.

Xk

and each „i+1 is an immediate extension of „i . Suppose X1 , . . . , Xk is satis¬able.

Then „0 is satis¬able, and by induction on i using Lemma 2.3.8, it follows that all

of the „i are satis¬able. In particular „n = „ is satis¬able, but this is impossible

since „ is closed.

2.4 Logical Equivalence

De¬nition 2.4.1. Given a formula A, let A = A[x1 /a1 , . . . , xk /ak ], where

x1 , . . . , xk are the variables which occur freely in A, and a1 , . . . , ak are parame-

ters not occurring in A. Note that A has no free variables, i.e., it is a sentence.

We de¬ne A to be satis¬able if and only if A is satis¬able, in the sense of De¬-

nition 2.3.7. We de¬ne A to be logically valid if and only if A is logically valid,

in the sense of De¬nition 2.3.7.

Exercises 2.4.2. Let A be a formula.

1. Show that A is logically valid if and only if ¬ A is not satis¬able. Show

that A is satis¬able if and only if ¬ A is not logically valid.

2. Let x be a variable. Show that A is logically valid if and only if ∀x A is

logically valid. Show that A is satis¬able if and only if ∃x A is satis¬able.

3. Let x be a variable, and let a be a parameter not occurring in A. Show

that A is logically valid if and only if A[x/a] is logically valid. Show that

A is satis¬able if and only if A[x/a] is satis¬able.

27

De¬nition 2.4.3. Let A and B be formulas. A and B are said to be logically

equivalent, written A ≡ B, if A ” B is logically valid.

Exercise 2.4.4. Assume A ≡ B. Show that for any variable x, ∀x A ≡ ∀x B

and ∃x A ≡ ∃x B. Show that for any variable x and parameter a, A[x/a] ≡

B[x/a].

Exercise 2.4.5. For a formula A, it is not in general true that A ≡ A , where

A is as in De¬nition 2.4.1. Also, it is not in general true that A ≡ ∀x A, or that

A ≡ ∃x A, or that A ≡ A[x/a]. Give examples illustrating these remarks.

Exercise 2.4.6. If A and B are formulas, put A = A[x1 /a1 , . . . , xk /ak ] and

B = B[x1 /a1 , . . . , xk /ak ], where x1 , . . . , xk are the variables occurring freely in

A and B, and a1 , . . . , ak are parameters not occurring in A or in B. Show that

A ≡ B if only if A ≡ B .

Remark 2.4.7. The results of Exercises 1.3.3 and 1.3.4 and Remark 1.3.5 for

formulas of the propositional calculus, also hold for formulas of the predicate

calculus.

In particular, if A1 ≡ A2 , then for any formula C containing A1 as a part,

if we replace one or more occurrences of the part A1 by A2 , then the resulting

formula is logically equivalent to C.

Remark 2.4.8. Some useful logical equivalences are:

1. (a) ∀x A ≡ A, provided x does not occur freely in A

(b) ∃x A ≡ A, provided x does not occur freely in A

(c) ∀x A ≡ ∀y A[x/y], provided y does not occur in A

(d) ∃x A ≡ ∃y A[x/y], provided y does not occur in A

2. (a) ∀x (A & B) ≡ (∀x A) & (∀x B)

(b) ∃x (A ∨ B) ≡ (∃x A) ∨ (∃x B)

(c) ∃x (A ’ B) ≡ (∀x A) ’ (∃x B)

Note however that, in general, ∃x (A & B) ≡ (∃x A) & (∃x B), and

∀x (A ∨ B) ≡ (∀x A) ∨ (∀x B), and ∀x (A ’ B) ≡ (∃x A) ’ (∀x B).

On the other hand, we have:

3. (a) ∃x (A & B) ≡ A & (∃x B), provided x does not occur freely in A

(b) ∃x (A & B) ≡ (∃x A) & B, provided x does not occur freely in B

(c) ∀x (A ∨ B) ≡ A ∨ (∀x B), provided x does not occur freely in A

(d) ∀x (A ∨ B) ≡ (∀x A) ∨ B, provided x does not occur freely in B

(e) ∀x (A ’ B) ≡ A ’ (∀x B), provided x does not occur freely in A

(f) ∀x (A ’ B) ≡ (∃x A) ’ B, provided x does not occur freely in B

4. (a) ∃x ¬ A ≡ ¬ ∀x A

28

(b) ∀x ¬ A ≡ ¬ ∃x A

(c) ∀x A ≡ ¬ ∃x ¬ A

(d) ∃x A ≡ ¬ ∀x ¬ A

De¬nition 2.4.9 (prenex form). A formula is said to be quanti¬er-free if it

contains no quanti¬ers. A formula is said to be in prenex form if it is of the form

Q1 x1 · · · Qn xn B, where each Qi is a quanti¬er (∀ or ∃), each xi is a variable,

and B is quanti¬er-free.

Example 2.4.10. The sentence

∀x ∀y ∃z ∀w (Rxy ’ (Rxz & Rzy & ¬ (Rzw & Rwy)))

is in prenex form.

Exercise 2.4.11. Show that every formula is logically equivalent to a formula

in prenex form.

Example 2.4.12. Consider the sentence (∃x P x) & (∃x Qx). We wish to put

this into prenex form. Applying the equivalences of Remark 2.4.8, we have

≡

(∃x P x) & (∃x Qx) (∃x P x) & (∃y Qy)

≡ ∃x (P x & (∃y Qy))

≡ ∃x ∃y (P x & Qy)

and this is in prenex form.

Exercises 2.4.13. Let A and B be quanti¬er-free formulas. Put the following

into prenex form.

1. (∃x A) & (∃x B)

2. (∀x A) ” (∀x B)

3. (∀x A) ” (∃x B)

De¬nition 2.4.14 (universal closure). Let A be a formula. The universal

closure of A is the sentence A— = ∀x1 · · · ∀xk A, where x1 , . . . , xk are the vari-

ables which occur freely in A. Note that A—— = A— .

Exercises 2.4.15. Let A be a formula.

1. Show that A is logically valid if and only if A— , the universal closure of A,

is logically valid.

2. It is not true in general that A ≡ A— . Give an example illustrating this.

3. It is not true in general that A is satis¬able if and only if A— is satis¬able.

Give an example illustrating this.

4. For formulas A and B, it is not true in general that A ≡ B if and only if

A— ≡ B — . Give an example illustrating this.

29

For completeness we state the following de¬nition.

De¬nition 2.4.16. Let A1 , . . . , Ak , B be formulas. We say that B is a logi-

cal consequence of A1 , . . . , Ak if (A1 & · · · & Ak ) ’ B is logically valid. This is

equivalent to saying that the universal closure of (A1 & · · · & Ak ) ’ B is logi-

cally valid.

Remark 2.4.17. A and B are logically equivalent if and only if each is a log-

ical consequence of the other. A is logically valid if and only if A is a logical

consequence of the empty set. ∃x A is a logical consequence of A[x/a], but the

converse does not hold in general. A[x/a] is a logical consequence of ∀x A, but

the converse does not hold in general.

2.5 The Completeness Theorem

Let U be a nonempty set, and let S be a set of (signed or unsigned) L-U -

sentences.

De¬nition 2.5.1. S is closed if S contains a conjugate pair of L-U -sentences.

In other words, for some L-U -sentence A, S contains T A, F A in the signed

case, A, ¬ A in the unsigned case. S is open if it is not closed.

De¬nition 2.5.2. S is U -replete if S “obeys the tableau rules” with respect to

U . We list some representative clauses of the de¬nition.

1. If S contains T ¬ A, then S contains F A. If S contains F ¬ A, then S

contains T A. If S contains ¬ ¬ A, then S contains A.

2. If S contains T A & B, then S contains both T A and T B. If S contains

F A & B, then S contains at least one of F A and F B. If S contains A & B,

then S contains both A and B. If S contains ¬ (A & B), then S contains

at least one of ¬ A and ¬ B.

3. If S contains T ∃x A, then S contains T A[x/a] for at least one a ∈ U . If

S contains F ∃x A, then S contains F A[x/a] for all a ∈ U . If S contains

∃x A, then S contains A[x/a] for at least one a ∈ U . If S contains ¬ ∃x A,

then S contains ¬ A[x/a] for all a ∈ U .

4. If S contains T ∀x A, then S contains T A[x/a] for all a ∈ U . If S contains

F ∀x A, then S contains F A[x/a] for at least one a ∈ U . If S contains

∀x A, then S contains A[x/a] for all a ∈ U . If S contains ¬ ∀x A, then S

contains ¬ A[x/a] for at least one a ∈ U .

Lemma 2.5.3 (Hintikka™s Lemma). If S is U -replete and open7 , then S is

satis¬able. In fact, S is satis¬able in the domain U .

7 See also Exercise 2.5.7.