The Compactness Theorem — Mathematics Knowledge System

Overview

The compactness theorem is a cornerstone result of first-order model theory: a set of first-order sentences Σ has a model if and only if every finite subset of Σ has a model. The forward direction is trivial (a model of all of Σ is automatically a model of any finite piece of it); the substance is the converse — that satisfiability can be verified 'locally,' one finite piece at a time, and this automatically guarantees a single model exists for the entire, possibly infinite, set. It follows immediately from Gödel's completeness theorem (a set is satisfiable iff it is consistent, and any proof of a contradiction from Σ can only use finitely many sentences of Σ), though it can also be proved directly via ultraproducts. Compactness is the key tool behind many striking existence results: it shows that if a first-order theory has arbitrarily large finite models, it must have an infinite model; it produces nonstandard models of arithmetic containing 'infinite' numbers; and it underlies the construction of the hyperreal numbers in nonstandard analysis.

Intuition

Compactness says that an infinite 'wish list' of first-order requirements is simultaneously satisfiable exactly when no finite sub-list of it is already self-contradictory — you never need to check the whole infinite list at once, only ask 'could a contradiction be hiding in some finite chunk?' A vivid application: suppose a theory T has models of every finite size (size 1, size 2, size 3, ...) but you want a model of infinite size. Add to T infinitely many new constants c₁, c₂, c₃, ... together with sentences cᵢ ≠ cⱼ for every i ≠ j, forcing at least ω many distinct elements. Any FINITE subset of this expanded theory only mentions finitely many of the cᵢ, so it can be satisfied by simply reusing one of T's large-enough finite models (assign the finitely many mentioned constants to distinct elements, which is possible since T has arbitrarily large finite models). Since every finite subset is satisfiable, compactness guarantees the WHOLE infinite expanded theory is satisfiable — producing a model of T with infinitely many elements, seemingly out of nothing.

Formal Definition

Definition

For a set Σ of first-order sentences in some fixed language:

\Sigma \text{ is satisfiable} \iff \text{every finite } \Sigma_0 \subseteq \Sigma \text{ is satisfiable}

Compactness theorem

\Sigma \vdash \bot \implies \exists\, \Sigma_0 \subseteq \Sigma \text{ finite with } \Sigma_0 \vdash \bot

Proofs are finite (used in the proof of compactness)

\text{(if } n \text{ has arbitrarily large finite models)} \implies \text{(} n \text{ has an infinite model)}

Typical compactness application schema

Worked Examples

Extend the language with new constant symbols c₁, c₂, c₃, ... and let Σ = T ∪ {cᵢ ≠ cⱼ : i ≠ j}.
$\Sigma = T \cup \{c_i \ne c_j : i \ne j\}$
Any finite Σ₀ ⊆ Σ mentions only finitely many constants, say c₁,...,cₖ. Since T has a model of size ≥ k, interpret c₁,...,cₖ as k distinct elements of that model, satisfying Σ₀.
$\Sigma_0 \subseteq \Sigma \text{ finite} \implies \Sigma_0 \text{ satisfiable (using a size-} \ge k \text{ model of } T)$
Every finite subset of Σ is satisfiable, so by compactness Σ itself is satisfiable. A model of Σ satisfies T and interprets infinitely many cᵢ as pairwise distinct, so it must be infinite.
$\Sigma \text{ satisfiable} \implies \exists\, \mathcal{M} \models T,\ |\mathcal{M}| \ge \aleph_0$

Answer: T has an infinite model — this is exactly how compactness proves that the theory of, e.g., finite graphs cannot pin down finiteness, and is the standard route to nonstandard models of arithmetic.

Practice Problems

Difficulty 6/10

Why is the 'only if' direction of the compactness theorem (satisfiable ⟹ every finite subset satisfiable) considered the 'easy' direction?

Difficulty 7/10

How does the compactness theorem follow from Gödel's completeness theorem?

Difficulty 8/10

Sketch how compactness is used to build a nonstandard model of arithmetic containing an element larger than every standard natural number.

Quiz

Summary

Compactness: Σ is satisfiable iff every finite subset of Σ is satisfiable — infinite satisfiability reduces to a finite check.
It follows from the completeness theorem together with the fact that formal proofs, being finite, can only draw on finitely many premises.
Its signature use is manufacturing infinite or nonstandard models: adding infinitely many 'largeness' constraints one finite piece at a time, then invoking compactness to satisfy them all simultaneously.

References

WebsiteWikipedia — Compactness theorem