13 - The Existence of Models

Summary

This chapter is entirely devoted to the proof of the compactness theorem. Section 13.1 outlines the proof, which reduces to establishing two main lemmas. These are then taken up in sections 13.2 through 13.4 to complete the proof, from which the Löwenheim–Skolem theorem also emerges as a corollary. The optional section 13.5 discusses what happens if nonenumerable languages are admitted: compactness still holds, but the Löwenheim–Skolem theorem in its usual ‘downward’ form fails, while an alternative ‘upward’ theorem holds.

Outline of the Proof

Our goal is to prove the compactness theorem, which has already been stated in the preceding chapter (in section 12.3). For convenience, we work with a version of firstorder logic in which the only logical operators are ∼, ∨, and ∃, that is, in which & and ∀ are treated as unofficial abbreviations. The hypothesis of the theorem, it will be recalled, is that every finite subset of a given set of sentences is satisfiable, and the conclusion we want to prove is that the set itself is satisfiable, or, as we more elaborately put it, belongs to the set S of all satisfiable sets of sentences. As a first step towards the proof, we set down some properties enjoyed by this target set S. The reason for not including & and ∀ officially in the language is simply that in this and subsequent lemmas we would need four more clauses, two for & and two for ∀.