\

/

¬ (Ra1 a2 & Ra2 a3 ) Ra1 a3

.

.

\

/ .

¬ Ra1 a2 ¬ Ra2 a3 ¬ Ra3 a1

∃y Ra3 y

Ra3 a4

.

.

.

An in¬nite open path gives rise (via the proof of Hintikka™s Lemma) to an in¬nite

L-structure M with UM = {a1 , a2 , . . . , an , . . .}, RM = { am , an : 1 ¤ m < n}.

Clearly M satis¬es A∞ .

Remark 2.5.10. In the course of applying a tableau test, we will sometimes

¬nd a ¬nite open path which is U -replete for some ¬nite set of parameters

U ⊆ V . In this case, the proof of Hintikka™s Lemma provides a ¬nite L-structure

with domain U .

Example 2.5.11. Let A be the sentence (∀x (P x ∨ Qx)) ’ ((∀x P x) ∨ (∀x Qx)).

34

Testing A for logical validity, we have:

¬A

∀x (P x ∨ Qx)

¬ ((∀x P x) ∨ (∀x Qx))

¬ ∀x P x

¬ ∀x Qx

¬Pa

¬ Qb

P a ∨ Qa

P b ∨ Qb

\

/

Pa Qa

/\

P b Qb

This tableau has a unique open path, which gives rise (via the proof of Hintikka™s

Lemma) to a ¬nite L-structure M with UM = {a, b}, PM = {b}, QM = {a}.

Clearly M falsi¬es A.

2.6 The Compactness Theorem

Theorem 2.6.1 (the Compactness Theorem, countable case). Let S be

a countably in¬nite set of sentences of the predicate calculus. S is satis¬able if

and only if each ¬nite subset of S is satis¬able.

Proof. FIXME

Theorem 2.6.2 (the Compactness Theorem, uncountable case). Let S

be an uncountable set of sentences of the predicate calculus. S is satis¬able if

and only if each ¬nite subset of S is satis¬able.

Proof. FIXME

Exercise 2.6.3. Let L be a language consisting of a binary predicate R and

some additional predicates. Let M = (UM , RM , . . .) be an L-structure such

that (UM , RM ) is isomorphic to (N, <N ). Note that M contains no in¬nite

R-descending sequence. Show that there exists an L-structure M such that:

1. M and M satisfy the same L-sentences.

2. M contains an in¬nite R-descending sequence. In other words, there

exist elements a1 , a2 , . . . , an , . . . ∈ UM such that an+1 , an ∈ RM for all

n = 1, 2, . . ..

Hint: Use the Compactness Theorem.

Exercise 2.6.4. Generalize Exercise 2.6.3 replacing (N, <N ) by an arbitrary

in¬nite linear ordering with no in¬nite descending sequence.

35

2.7 Satis¬ability in a Domain

The notion of satis¬ability in a domain was introduced in De¬nition 2.2.9.

Theorem 2.7.1. Let S be a set of L-sentences.

1. Assume that S is ¬nite or countably in¬nite. If S is satis¬able, then S is

satis¬able in some ¬nite or countably in¬nite domain.

2. Assume that S is of cardinality „µ± . If S is satis¬able, then S is satis¬able

in some domain of cardinality less than or equal to „µ± .

Proof. Parts 1 and 2 follow easily from the proofs of Compactness Theorems

2.6.1 and 2.6.2, respectively.

FIXME

In Example 2.2.12 we have seen a sentence A∞ which is satis¬able in a

countably in¬nite domain but not in any ¬nite domain. Regarding satis¬ability

in ¬nite domains, we have:

Example 2.7.2. Given a positive integer n, we exhibit a sentence An which

is satis¬able in a domain of cardinality n but not in any domain of smaller

cardinality. Our sentence An is (1) & (2) & (3) with

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

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

(3) ∃x1 · · · ∃xn (Rx1 x2 & Rx2 x3 & · · · & Rxn’1 xn )

On the other hand, we have:

Theorem 2.7.3. Let M and M be L-structures. Assume that there exists

an onto mapping φ : UM ’ UM such that for all n-ary predicates P of

L and all n-tuples a1 , . . . , an ∈ (UM )n , a1 , . . . , an ∈ PM if and only if

φ(a1 ), . . . , φ(an ) ∈ PM . Then as in Theorem 2.2.6 we have vM (A) = vM (A )

for all L-UM -sentences A, where A = A[a1 /φ(a1 ), . . . , ak /φ(ak )]. In particular,

M and M satisfy the same L-sentences.

Proof. The proof is by induction on the degree of A. Suppose for example that

A = ∀x B. Then by de¬nition of vM we have that vM (A) = T if and only if

vM (B[x/a]) = T for all a ∈ UM . By inductive hypothesis, this holds if and only

if vM (B[x/a] ) = T for all a ∈ UM . But for all a ∈ UM we have B[x/a] =

B [x/φ(a)]. Thus our condition is equivalent to vM (B [x/φ(a)]) = T for all

a ∈ UM . Since φ : UM ’ UM is onto, this is equivalent to vM (B [x/b]) = T

for all b ∈ UM . By de¬nition of vM this is equivalent to vM (∀x B ) = T. But

∀x B = A , so our condition is equivalent to vM (A ) = T.

Corollary 2.7.4. 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 or larger cardinality.

36

Proof. Suppose S is satis¬able in domain U . Let U be a set of cardinality

greater than or equal to that of U . Let φ : U ’ U be onto. If M is any

L-structure with UM = U , we can de¬ne an L-structure M with UM = U

by putting PM = { a1 , . . . , an : φ(a1 ), . . . , φ(an ) ∈ PM } for all n-ary pred-

icates P of L. By Theorem 2.7.3, M and M satisfy the same L-sentences. In

particular, if M satis¬es S, then M satis¬es S.

Remark 2.7.5. We shall see later8 that Theorem 2.7.3 and Corollary 2.7.4 fail

for normal satis¬ability.

8 See Section 4.1.

37

Chapter 3

Proof Systems for Predicate

Calculus

3.1 Introduction to Proof Systems

De¬nition 3.1.1. An abstract proof system consists of a set X together with a

∞

relation R ⊆ k=0 Xk+1 . Elements of X are called objects. Elements of R are

called rules of inference. An object X ∈ X is said to be derivable, or provable,

if there exists a ¬nite sequence of objects X1 , . . . , Xn such that Xn = X and,

for each i ¤ n, there exist j1 , . . . , jk < i such that Xj1 , . . . , Xjk , Xi ∈ R. The

sequence X1 , . . . , Xn is called a derivation of X, or a proof of X.

Notation 3.1.2. For k ≥ 1 it is customary to write

X1 · · · Xk