vM : {A : A is an L-UM -sentence} ’ {T, F}

de¬ned as follows:

if a1 , . . . , an ∈ PM ,

T

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

if a1 , . . . , an ∈ PM .

F /

T if vM (A) = F ,

2. vM (¬ A) =

F if vM (A) = T .

T if vM (A) = vM (B) = T ,

3. vM (A & B) =

F if at least one of vM (A), vM (B) = F .

T if at least one of vM (A), vM (B) = T ,

4. vM (A ∨ B) =

F if vM (A) = vM (B) = F .

5. vM (A ’ B) = vM (¬ (A & ¬ B)) .

T if vM (A) = vM (B) ,

6. vM (A ” B) =

F if vM (A) = vM (B) .

the special case n = 0 we obtain the notion of a 0-ary relation, i.e., a subset of { }.

2 In

There are only two 0-ary relations, { } and {}, corresponding to T and F respectively. Thus

a 0-ary predicate behaves as a propositional atom.

21

if vM (A[x/a]) = T for all a ∈ UM ,

T

7. vM (∀x A) =

if vM (A[x/a]) = F for at least one a ∈ UM .

F

if vM (A[x/a]) = T for at least one a ∈ UM ,

T

8. vM (∃x A) =

if vM (A[x/a]) = F for all a ∈ UM .

F

Proof. The truth value vM (A) is de¬ned by recursion on L-UM -sentences, i.e.,

by induction on the degree of A where A is an arbitrary L-UM -sentence.

De¬nition 2.2.5 (truth and satisfaction). Let M be an L-structure.

1. Let A be an L-UM -sentence. We say that A is true in M if vM (A) = T.

We say that A is false in M if vM (A) = F.

2. Let S be a set of L-UM -sentences. We say that M satis¬es S if all of the

sentences of S are true in M .

Theorem 2.2.6.

1. If M and M are isomorphic L-structures and φ : M ∼ M is an isomor-

=

phism of M onto M , then for all L-UM -sentences A we have vM (A) =

vM (A ) where A = A[a1 /φ(a1 ), . . . , ak /φ(ak )].3 Here a1 , . . . , ak are the

elements of UM which occur in A.

2. If M and M are isomorphic L-structures, then they satisfy the same

L-sentences.

Proof. We omit the proof of part 1. A more general result will be proved later

as Theorem 2.7.3. Part 2 follows immediately from part 1.

De¬nition 2.2.7 (satis¬ability). Let S be a set of L-sentences. S is said to

be satis¬able 4 if there exists an L-structure M which satis¬es S.

Remark 2.2.8. Satis¬ability is one of the most important concepts of mathe-

matical logic. A key result known as the Compactness Theorem5 states that a

set S of L-sentences is satis¬able if and only every ¬nite subset of S is satis¬able.

The following related notion is of technical importance.

De¬nition 2.2.9 (satis¬ability in a domain). Let U be a nonempty set. A

set S of L-U -sentences is said to be satis¬able in the domain U if there exists

an L-structure M such that M satis¬es S and UM = U .

Remark 2.2.10. Let S be a set of L-sentences. Then S is satis¬able (according

to De¬nition 2.2.7) if and only if S is satis¬able in some domain U .

3 We have extended the substitution notation 2.1.8 in an obvious way.

4 Similarly, the notions of logical validity and logical consequence are de¬ned for L-

sentences, in the obvious way, using L-structures. An L-sentence is said to be logically valid

if it is satis¬ed by all L-structures. An L-sentence is said to be a logical consequence of S if

it is satis¬ed by all L-structures satisfying S.

5 See Theorems 2.6.1 and 2.6.2 below.

22

Theorem 2.2.11. Let S be a set of L-sentences. If S is satis¬able in a domain

U , then S is satis¬able in any domain of the same cardinality as U .

Proof. Suppose S is satis¬able in a domain U . Let M be an L-structure M

satisfying S with UM = U . Let U be any set of the same cardinality as U .

Then there exists a one-to-one correspondence φ : U ’ U . Let M be the

L-structure with UM = U , PM = { φ(a1 ), . . . , φ(an ) : a1 , . . . , an ∈ PM } for

all n-ary predicates P of L. Then M is isomorphic to M . Hence, by Theorem

2.2.6, M satis¬es S. Thus S is satis¬able in the domain U .

Example 2.2.12. We exhibit a sentence A∞ which is satis¬able in an in¬nite

domain but not in any ¬nite domain. Our sentence A∞ is (1) & (2) & (3) with

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

(2) ∀x ∀y (Rxy ’ ¬ Ryx)

(3) ∀x ∃y Rxy

See also Example 2.5.9.

2.3 The Tableau Method

De¬nition 2.3.1. Fix a countably in¬nite set V = {a1 , a2 , . . . , an , . . .}. The

elements of V will be called parameters. If L is a language, L-V -sentences will

be called sentences with parameters.

De¬nition 2.3.2. A (signed or unsigned ) tableau is a rooted dyadic tree where

each node carries a (signed or unsigned) L-V -sentence. The tableau rules for

predicate calculus are the same as those for propositional calculus, with the

following additional rules.

Signed:

. .

. .

. .

T ∀x A F ∃x A

. .

. .

. .

| |

T A[x/a] F A[x/a]

where a is an arbitrary parameter

23

. .

. .

. .

T ∃x A F ∀x A

. .

. .

. .

| |

T A[x/a] F A[x/a]

where a is a new parameter

Unsigned:

. .