Compactness

Hodges has a proof of compactness for first-order languages in "A Shorter Model Theory" that can be simplified by proving that the set he constructs is maximal consistent, rather than a Hintikka set (which it also is). (He already proves that it's consistent, so it's just a matter of proving maximality instead of a lemma concerning Hintikka sets and then verifying the existential condition for Hintikka sets, which he does. This alternative proof requires validating the universal condition for Hintikka sets if one wishes to prove that T' (below) is indeed a Hintikka set. Hodges lemma allows him to avoid this.)

(I apologize in advance for the ugly notation. I should get/learn LaTeX to HTML (or whatever they call it) but I'm too lazy.)

Let T be a first-order theory in a language L such that every finite subset of T has a model. Let c_1,... be an enumeration of constants new to L and let L' be obtained from L by adding the c_i to L. Let A_1,... be an enumeration of the sentences of L. We construct a maximal consistent (Hintikka) set T' in L' such that T is a subset of T'. Let T_0 = T and suppose that T_n has been defined. Then

T_{n+1} = {T_n ∪ {A_n} if every finite subset of this set has a model, and T_n otherwise.

If at the jth stage of the construction A_j has the form ExB(x) and every finite subset of T_j ∪ {A_j} has a model, then set T'_{j+1} = T_{j+1} ∪ {B(c_i)} for c_i the first constant new to this set. Otherwise T'_{j+1} = T_{j+1}. Let T' = ∪_{i<\omega}T'_i.

We first note that if T_i ∪ {A} is such that not all finite subsets of it have a model, then for all k > i,

(1) T_k ∪ {A} is such that not every finite subset of it has a model,

since T_i ⊆ T_k. Suppose A_i is not in T'. Then T_i ∪ {A_i} is such that not every finite subset of it has a model. (That is the only place in the construction A_i could be added.) But then there exists a finite W ⊆ T_i such that

(2) W ∪ {A_i} |= ~A_i.

Let ~A_i = A_j, and suppose for reductio that T_j ∪ {A_j} is such that not every finite subset of it has a model. (This is the only place in the construction where A_j could enter T', so it is equivalent to saying that A_j is not in T'.) Then there exists a finite W* ⊆ T_j such that

(3) W* ∪ {A_j} |= ~A_j.

By construction, either W ⊆ W* or W* ⊆ W. It doesn't matter which we assume since they both end up at the same conclusion in an analogous way. Assume the former. Then by (1), (2), and (3) (recalling ~A_j = ~~A_i), both W* ∪ {A_i} |= ~A_i & ~~A_i and W* ∪ {~A_i} |= ~A_i & ~~A_i. Whence W* |= ~A_i & ~~A_i, contra the supposition that every finite subset of T_j has a model. This concludes the proof of maximality. (Consistency is easier and Hodges already proves it.)

Technically, one should verify that every finite subset of T'_i has a model when every finite subset of T_i ∪ {A_i} has a model and A_i is existential. It seems too obvious to mention since c_i is new to T_i ∪ {A_i}, and we're lazy. It's Sunday, remember?

To see that T' has a model, we see that T' |= A iff A ∈ T' by maximality. Thus if T' has no model then T' |= A and T' |= ~A. Whence A, ~A ∈ T' contra the consistency of T'. Hence T &subeq; T' has a model.

Is there a faster *purely model-theoretic* way to prove compactness?