Proof. Straightforward.

13

De¬nition 1.5.2. A path of a tableau is said to be replete if, whenever it

contains the top formula of a tableau rule, it also contains at least one of the

branches. A replete tableau is a tableau in which every path is replete.

Lemma 1.5.3. Any ¬nite tableau can be extended to a ¬nite replete tableau.

Proof. Apply tableau rules until they cannot be applied any more.

De¬nition 1.5.4. A tableau is said to be open if it is not closed, i.e., it has at

least one open path.

Lemma 1.5.5. Let „ be a replete tableau starting with X1 , . . . , Xk . If „ is

open, then X1 , . . . , Xk is satis¬able.

In order to prove Lemma 1.5.5, we introduce the following de¬nition.

De¬nition 1.5.6. Let S be a set of signed or unsigned formulas. We say that

S is a Hintikka set if

1. S “obeys the tableau rules”, in the sense that if it contains the top formula

of a rule then it contains at least one of the branches;

2. S contains no pair of conjugate atomic formulas, i.e., Tp, Fp in the signed

case, or p, ¬ p in the unsigned case.

Lemma 1.5.7 (Hintikka™s Lemma). If S is a Hintikka set, then S is satis¬-

able.

Proof. De¬ne an assignment M by

T if Tp belongs to S

M (p) =

F otherwise

in the signed case, or

T if p belongs to S

M (p) =

F otherwise

in the unsigned case. It is not di¬cult to see that vM (X) = T for all X ∈ S.

To prove Lemma 1.5.5, it su¬ces to note that a replete open path is a Hin-

tikka set. Thus, if a replete tableau starting with X1 , . . . , Xk is open, Hintikka™s

Lemma implies that X1 , . . . , Xk is satis¬able.

Combining Lemmas 1.5.1 and 1.5.3 and 1.5.5, we obtain:

Theorem 1.5.8 (the Completeness Theorem). X1 , . . . , Xk is satis¬able if

and only if there is no ¬nite closed tableau starting with X1 , . . . , Xk .

Corollary 1.5.9. A1 , . . . , Ak is not satis¬able if and only if there exists a ¬nite

closed signed tableau starting with TA1 , . . . , TAk , or equivalently a ¬nite closed

unsigned tableau starting with A1 , . . . , Ak .

14

Corollary 1.5.10. A is logically valid if and only if there exists a ¬nite closed

signed tableau starting with FA, or equivalently a ¬nite closed unsigned tableau

starting with ¬ A.

Corollary 1.5.11. B is a logical consequence of A1 , . . . , Ak if and only if there

exists a ¬nite closed signed tableau starting with TA1 , . . . , TAk , FB, or equiv-

alently a ¬nite closed unsigned tableau starting with A1 , . . . , Ak , ¬ B.

1.6 Trees and K¨nig™s Lemma

o

Up to this point, our discussion of trees has been informal. We now pause to

make our tree terminology precise.

De¬nition 1.6.1. A tree consists of

1. a set T

: T ’ N+ ,

2. a function

3. a binary relation P on T .

The elements of T are called the nodes of the tree. For x ∈ T , (x) is the level

of x. The relation xP y is read as x immediately precedes y, or y immediately

succeeds x. We require that there is exactly one node x ∈ T such that (x) = 1,

called the root of the tree. We require that each node other than the root has

exactly one immediate predecessor. We require that (y) = (x) + 1 for all

x, y ∈ T such that xP y.

De¬nition 1.6.2. A subtree of T is a nonempty set T ⊆ T such that for all

y ∈ T and xP y, x ∈ T . Note that T is itself a tree, under the restriction of

and P to T . Moreover, the root of T is the same as the root of T .

De¬nition 1.6.3. An end node of T is a node with no (immediate) successors.

A path in T is a set S ⊆ T such that (1) the root of T belongs to S, (2) for each

x ∈ S, either x is an end node of T or there is exactly one y ∈ S such that xP y.

De¬nition 1.6.4. Let P — be the transitive closure of P , i.e., the smallest re-

¬‚exive and transitive relation on T containing P . For x, y ∈ T , we have xP — y

if and only if x precedes y, i.e., y succeeds x, i.e., there exists a ¬nite sequence

x = x0 P x1 P x2 · · · xn’1 P xn = y. Note that the relation P — is re¬‚exive (xP — x

for all x ∈ T ), antisymmetric (xP — y and yP — x imply x = y), and transitive

(xP — y and yP — z imply xP — z). Thus P — is a partial ordering of T .

De¬nition 1.6.5. T is ¬nitely branching if each node of T has only ¬nitely

many immediate successors in T . T is dyadic if each node of T has at most two

immediate successors in T . Note that a dyadic tree is ¬nitely branching.

Theorem 1.6.6 (K¨nig™s Lemma). Let T be an in¬nite, ¬nitely branching

o

tree. Then T has an in¬nite path.

15

Proof. Let T be the set of all x ∈ T such that x has in¬nitely many successors

in T . Note that T is a subtree of T . Since T is ¬nitely branching, it follows by

the pigeonhole principle that each x ∈ T has at least one immediate successor

y ∈ T . Now de¬ne an in¬nite path S = {x1 , x2 , . . . , xn , . . .} in T inductively by

putting x1 = the root of T , and xn+1 = one of the immediate successors of xn

in T . Clearly S is an in¬nite path of T .

1.7 The Compactness Theorem

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

a countable set of propositional formulas. If each ¬nite subset of S is satis¬able,

the S is satis¬able.

Proof. In brief outline: Form an in¬nite tableau. Apply K¨nig™s Lemma to get

o

an in¬nite path. Apply Hintikka™s Lemma.

Details: Let S = {A1 , A2 , . . . , Ai , . . .}. Start with A1 and generate a ¬nite

replete tableau, „1 . Since A1 is satis¬able, „1 has at least one open path. Append

A2 to each of the open paths of „1 , and generate a ¬nite replete tableau, „2 .

Since {A1 , A2 } is satis¬able, „2 has at least one open path. Append A3 to each

of the open paths of „2 , and generate a ¬nite replete tableau, „3 . . . . . Put

∞

„ = i=1 „i . Thus „ is a replete tableau. Note also that „ is an in¬nite, ¬nitely

branching tree. By K¨nig™s Lemma (Theorem 1.6.6), let S be an in¬nite path

o

in „ . Then S is a Hintikka set containing S. By Hintikka™s Lemma, S is

satis¬able. Hence S is satis¬able.

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

be an uncountable set of propositional formulas. If each ¬nite subset of S is

satis¬able, the S is satis¬able.

Proof. We present three proofs. The ¬rst uses Zorn™s Lemma. The second uses

trans¬nite induction. The third uses Tychono¬™s Theorem.

Let L be the (necessarily uncountable) propositional language consisting of

all atoms occurring in formulas of S. If S is a set of L-formulas, we say that

S is ¬nitely satis¬able if each ¬nite subset of S is satis¬able. We are trying to

prove that, if S is ¬nitely satis¬able, then S is satis¬able.

First proof. Consider the partial ordering F of all ¬nitely satis¬able sets of

L-formulas which include S, ordered by inclusion. It is easy to see that any

chain in F has a least upper bound in F. Hence, by Zorn™s Lemma, F has a

maximal element, S — . Thus S — is a set of L-formulas, S — ⊇ S, S — is ¬nitely

satis¬able, and for each L-formula A ∈ S — , S — ∪ {A} is not ¬nitely satis¬able.

/

From this it is straightforward to verify that S — is a Hintikka set. Hence, by

Hintikka™s Lemma, S — is satis¬able. Hence S is satis¬able.

Second proof. Let Aξ , ξ < ±, be a trans¬nite enumeration of all L-formulas.

By trans¬nite recursion, put S0 = S, Sξ+1 = Sξ ∪ {Aξ } if Sξ ∪ {Aξ } is ¬nitely

satis¬able, Sξ+1 = Sξ otherwise, and S· = ξ<· Sξ for limit ordinals · ¤ ±.

Using trans¬nite induction, it is easy to verify that Sξ is ¬nitely satis¬able for

16

each ξ ¤ ±. In particular, S± is ¬nitely satis¬able. It is straightforward to

verify that S± is a Hintikka set. Hence, by Hintikka™s Lemma, S± is satis¬able.

Hence S is satis¬able.

Third proof. Let M = {T, F}L be the space of all L-assignments M : L ’

{T, F}. Make M a topological space with the product topology where {T, F}