nLab compactness theorem




The compactness theorem is a fundamental result of model theory on the existence of models of first-order theories.

Historically it goes back to work of Gödel and Mal’cev in the 1930s.

Lindström's theorem uses the compactness and the Löwenheim-Skolem theorem to characterize classical first-order logic. The validity or non-validity of the compactness theorem in logical systems other than first-order logic plays under the name of compactness property an important role in abstract model theory.


Briefly, the compactness theorem states that a set of first-order formulas Φ\Phi has a model precisely iff every finite subset of Φ\Phi has a model.


There are different proofs for the compactness theorem e.g. an entirely ‘semantic’ one using ultraproducts. A particularly transparent one relies on the completeness theorem for first-order logic and the essential finitude of the notion of formal proof1: Suppose Φ\Phi has no model, due to completeness this implies that there is a contradiction φ\varphi with Φφ\Phi\vdash\varphi but such a deduction of φ\varphi can involve only a finite subset Φ 0Φ\Phi_0\subset \Phi hence Φ 0φ\Phi_0\vdash\varphi and Φ 0\Phi_0 would have no model as well.

Despite the intuitive appeal, this approach obliges one to establish the completeness theorem, which depends on fiddly details of formal proofs and deductive systems to make rigorous.

Compactness for propositional logic

The motivation for the terminology stems from the observation that the compactness theorem literally expresses the compactness of a suitable topology on first-order structures.


As the compactness theorem is arguably the most fundamental result of model theory, there are too many examples of its use for us to do it much justice here. But perhaps a few examples here will help illustrate some typical uses.

Total orders


Every set XX can be totally ordered.

Of course this trivially follows from the stronger result that every set can be well-ordered, if we permit the axiom of choice. But part of our point here is that we don’t need the full strength of the axiom of choice: the result can be derived from the weaker “choice principle” called the ultrafilter theorem, on which the compactness theorem depends.


Introduce a language (i.e., signature) with a constant symbol c pc_p for each pXp \in X and a binary relation symbol LL, and for a theory take axioms ¬(c p=c q)\neg (c_p = c_q) whenever pqp \neq q in XX and the usual axioms to make LL a total order (reflexivity, transitivity, antisymmetry, and connectedness). This theory is finitely satisfiable: any finite subset Σ\Sigma of the axioms has a model, by interpreting each c xc_x occurring in an inequality axiom belonging to Σ\Sigma simply as xx, and totally ordering those finitely many xx in some way to interpret LL; the remaining c xc_x can be interpreted as the bottom element of that total order without any harm. By the compactness theorem, this theory has a model YY, and the restriction of the total order on YY to the set of all constants c xc_x in YY is used to totally order all the xXx \in X.

With slightly more effort, a similar argument can be given to show that every partial order can be extended to a total order. We just proved the case where the partial order is discrete.

Choice-like consequences

Again, we assume the ultrafilter principle but do not assume the axiom of choice.


If p:FXp: F \to X is surjective and every fiber is finite, then pp has a section ss.


Use Proposition to totally order FF. Each fiber inherits a total order; being finite, it is well-order. Then choose s(x)s(x) for xXx \in X to be the least element in the fiber F xF_x (which is nonempty because pp is surjective).


A countable disjoint union of finite sets is again countable.


Let F nF_n be the countable family and let FF be the union; again we have a fibering FF \to \mathbb{N} with fiber F nF_n over nn. Using Proposition , totally order FF; each F nF_n inherits an order from FF, and since total orders on finite sets are well-orders, we have chosen a countable family of well-orders. Now put the lexicographic order on the set of pairs F={(n,x):n,xF n}F' = \{(n, x): n \in \mathbb{N}, x \in F_n\}. This is a well-ordering, and clearly the projection FFF' \to F is a bijection, so we obtain a well-ordering of FF by transport of structure (differing, probably, from the original total ordering of FF which has done its job but is of no further use). Then we can define a partial map ϕ:F\phi: \mathbb{N} \to F by induction: ϕ(0)\phi(0) is the bottom of FF, and ϕ(n+1)\phi(n+1) is (if it exists) the bottom of the complement of ϕ([0,n])\phi([0, n]). This defines a bijection from an initial segment of \mathbb{N} onto FF, which is what we wanted.


(Weak König’s lemma) Every infinite tree for which there is finite branching at each node has an infinite branch.


A tree is by definition the category of elements e=(n,xF(n))e = (n, x \in F(n)) of a presheaf F: opSetF: \mathbb{N}^{op} \to Set where \mathbb{N} has its usual order and F(0)F(0) is terminal. A descendant of an element e=(n,xF(n))e = (n, x \in F(n)) is an element that maps to ee, i.e., an element (m,yF(m))(m, y \in F(m)) with mnm \geq n and F(mn)(y)=xF(m \geq n)(y) = x. A child of ee is such a descendant with m=n+1m = n+1.

By the branching hypothesis, the set E nE_n of elements e=(n,x)e = (n, x) is finite. By Proposition , the set of nodes or elements E= nE nE = \sum_n E_n is countable, i.e., is enumerated by some bijection E\mathbb{N} \to E. Then an infinite branch (a global section ss of FF) is given by recursion as follows: s(0)s(0) is the root (the unique element of E 0E_0). The root has infinitely many descendants since the tree is infinite. Given that s(n)F(n)s(n) \in F(n) has infinitely many descendants, let s(n+1)s(n+1) be the first of its children in the enumeration that also has infinitely many descendants (such children exist since s(n)s(n) has only finitely many children by the branching hypothesis).

Weak König’s lemma lends its name to one the so-called Big Five systems of reverse mathematics, namely WKL 0WKL_0, and (over a certain weak fragment of second-order arithmetic) is equivalent to many results in classical elementary analysis.


Actually, the WKL as stated above is stronger than another result that goes by that name, namely that an infinite subtree of the infinite binary tree 2 <ω2^{\lt \omega} (consisting of finite 0-1 sequences or words, where the root is the empty word and the parent of a nonempty word is obtained by leaving off the last binary digit) has an infinite branch. This is provable in ZF without choice or other choice-free forms of set theory; the key point is that 2 <ω2^{\lt \omega}, and subtrees thereof, already have enumerations ready to hand; we don’t need an argument like Proposition to construct one. From there, the recursive construction of a branch in the proof of Corollary can be performed without making choices.


  1. In the German literature the compactness theorem is therefore also called ‘Endlichkeitssatz’.

Last revised on July 26, 2023 at 20:15:41. See the history of this page for a list of all contributions to it.