Compactness theorem

The compactness theorem for the propositional calculus is a consequence of Tychonoff's theorem (which says that the product of compact spaces is compact) applied to compact Stone spaces,^[1] hence the theorem's name. Likewise, it is analogous to the finite intersection property characterization of compactness in topological spaces: a collection of closed sets in a compact space has a non-empty intersection if every finite subcollection has a non-empty intersection.


The compactness theorem is one of the two key properties, along with the downward Löwenheim–Skolem theorem, that is used in Lindström's theorem to characterize first-order logic. Although there are some generalizations of the compactness theorem to non-first-order logics, the compactness theorem itself does not hold in them, except for a very limited number of examples.^[2]

One can prove the compactness theorem using Gödel's completeness theorem, which establishes that a set of sentences is satisfiable if and only if no contradiction can be proven from it. Since proofs are always finite and therefore involve only finitely many of the given sentences, the compactness theorem follows. In fact, the compactness theorem is equivalent to Gödel's completeness theorem, and both are equivalent to the Boolean prime ideal theorem, a weak form of the axiom of choice.^[10]


Gödel originally proved the compactness theorem in just this way, but later some "purely semantic" proofs of the compactness theorem were found; that is, proofs that refer to truth but not to provability. One of those proofs relies on ultraproducts hinging on the axiom of choice as follows:


Proof: Fix a first-order language ${\displaystyle L,}$ and let ${\displaystyle \Sigma }$ be a collection of ${\displaystyle L}$-sentences such that every finite subcollection of ${\displaystyle L}$-sentences, ${\displaystyle i\subseteq \Sigma }$ of it has a model ${\displaystyle {\mathcal {M}}_{i}.}$ Also let ${\textstyle \prod _{i\subseteq \Sigma }{\mathcal {M}}_{i}}$ be the direct product of the structures and ${\displaystyle I}$ be the collection of finite subsets of ${\displaystyle \Sigma .}$ For each ${\displaystyle i\in I,}$ let ${\displaystyle A_{i}=\{j\in I:j\supseteq i\}.}$ The family of all of these sets ${\displaystyle A_{i}}$ generates a proper filter, so there is an ultrafilter ${\displaystyle U}$ containing all sets of the form ${\displaystyle A_{i}.}$


Now for any sentence ${\displaystyle \varphi }$ in ${\displaystyle \Sigma :}$


Łoś's theorem now implies that ${\displaystyle \varphi }$ holds in the ultraproduct ${\textstyle \prod _{i\subseteq \Sigma }{\mathcal {M}}_{i}/U.}$ So this ultraproduct satisfies all formulas in ${\displaystyle \Sigma .}$