Compactness

Origin. Gödel completeness theorem (1929) implies compactness. Fundamental model-theoretic property. If every finite subset satisfiable, whole set satisfiable. Fails for many extensions.

Models. Γ is satisfiable iff every finite Γ₀ ⊆ Γ is satisfiable. Equivalently: if Γ ⊨ φ, then Γ₀ ⊨ φ for finite Γ₀. Topological: theory space is compact.

Formalism.

Compactness theorem: For any set Γ of first-order sentences: Γ has a model iff every finite Γ₀ ⊆ Γ has a model.

Equivalent forms:

If Γ ⊨ φ, then Γ₀ ⊨ φ for some finite Γ₀ ⊆ Γ.
If Γ is unsatisfiable, some finite Γ₀ ⊆ Γ is unsatisfiable.

Proof via completeness: Γ ⊨ φ implies Γ ⊢ φ (completeness). Proofs are finite, use only finite Γ₀.

Ultraproduct proof: Direct construction via ultraproducts. Łoś's theorem: ultraproducts preserve truth.

Applications: Nonstandard models: infinite numbers. Transfer principles. Omitting types. Finite satisfiability ≠ satisfiability.

Failures: Second-order logic: fails. Infinitary logics Lω₁ω: fails. Fixed-point logics: fails. Compactness ↔ not too expressive.

Lindström's theorem: FOL is maximal logic with compactness + Löwenheim-Skolem.

Symbols.

Symbol	Unicode	Name	Meaning
Γ	U+0393	Gamma	A set of sentences
⊨	U+22A8	Double turnstile	Semantic consequence and satisfaction
⊢	U+22A2	Turnstile	Derivability, finite by construction
⊆	U+2286	Subset	Γ₀ ⊆ Γ, the finite part
φ	U+03C6	Phi	The consequence being drawn
≠	U+2260	Not equal to	Finite satisfiability ≠ satisfiability
↔	U+2194	Left right arrow	Correspondence between compactness and expressiveness
ℵ	U+2135	Aleph	Cardinal in Löwenheim–Skolem bounds
ω	U+03C9	Omega	Index of the infinitary logic L_{ω₁ω}
Γ₀	—	Finite subset	The finite fragment doing the work
ℵ₀	—	Aleph-null	Countably infinite
BPI	—	Boolean prime ideal theorem	Choice principle equivalent to compactness

Metatheory. Gödel proved compactness for countable languages as a corollary of completeness in 1929–30; Malcev (1936) removed the cardinality restriction, and the general statement is often credited to him. Łoś's theorem (1955) gives a direct ultraproduct proof that uses no proof system at all. Over ZF the compactness theorem for first-order logic is exactly as strong as the Boolean prime ideal theorem — a result of Henkin and of Łoś and Ryll-Nardzewski — hence strictly weaker than the axiom of choice. Topologically it is the compactness of the Stone space of the Lindenbaum–Tarski algebra, and the same fact makes every type space S_n(T) a compact totally disconnected Hausdorff space, which is the foundation of stability theory. Compactness yields upward Löwenheim–Skolem, nonstandard models of arithmetic and of the reals, and the standard non-definability arguments. Lindström (1969) proved that first-order logic is the maximal logic having compactness together with downward Löwenheim–Skolem.

Applies to. Model theory. Nonstandard methods. Database theory. Satisfiability solving. Logic design.

Limitations. Compactness is precisely the reason first-order logic cannot say "finitely many", "well-founded", "torsion", "connected", or "Archimedean": each is refuted by adding a schema whose finite subsets are all satisfiable. It also guarantees the models one did not want — no first-order theory with an infinite model is categorical, so arithmetic, the reals, and every infinite structure come with elementarily equivalent non-isomorphic companions. The theorem is a pure existence principle: it produces a model with no bound on its complexity, and the Henkin construction requires a maximal consistent extension, so the models are not canonical and by Tennenbaum's theorem no countable nonstandard model of PA is even computable. It is vacuous over finite structures, which is why finite model theory has to abandon it, and it fails outright for second-order logic, for L_{ω₁ω}, and for fixed-point logics.