Compactness Theorem

The compactness theorem is a fundamental result in first-order logic: a set of sentences can be satisfied simultaneously if every finite subset can be satisfied simultaneously. It connects finite collections of logical requirements with potentially infinite theories and is a central tool of model theory. The theorem concerns the existence of models, not their uniqueness or an effective procedure for constructing them. (math.berkeley.edu)

Statement and interpretation

Let $L$ be a first-order language, and let $T$ be a set of $L$-sentences, called a theory. A sentence is a formula with no free variables. A model of $T$ is an $L$-structure in which every sentence belonging to $T$ is true. The compactness theorem states:

The right-hand condition is called finite satisfiability. The model satisfying one finite subset need not satisfy another; compactness guarantees a single model satisfying the entire theory. The forward implication is immediate, whereas the reverse implication is the substantive result. The theorem applies to arbitrary set-sized languages, including uncountable ones. (math.berkeley.edu)

Two equivalent formulations are particularly useful:

• If a theory has no model, some finite subset already has no model.
• If $T\models\varphi$, then $T_0\models\varphi$ for some finite $T_0\subseteq T$.

Here $T\models\varphi$ denotes semantic consequence: every model of $T$ satisfies $\varphi$. Thus even a consequence of infinitely many assumptions follows semantically from finitely many of them. The equivalence follows by applying compactness to $T\cup\{\neg\varphi\}$. (math.berkeley.edu)

Proof methods

From the completeness theorem

Gödel’s completeness theorem identifies semantic consequence with formal derivability. Suppose $T$ is unsatisfiable. Completeness gives a formal proof of a contradiction from $T$. Because a proof is finite, it uses only finitely many assumptions, forming a subset $T_0$. By soundness, this subset is itself unsatisfiable. Taking the contrapositive establishes compactness. (math.berkeley.edu)

This argument distinguishes two kinds of finiteness: individual first-order formulas are finite expressions, and ordinary formal proofs contain finitely many steps. A theory, however, may contain infinitely many sentences. (math.berkeley.edu)

Henkin construction

A direct proof uses a Henkin construction. The language is enlarged by adding constants that provide witnesses for existential assertions. The finitely satisfiable theory is extended so that sentences are decided consistently and existential assertions have witnesses. A model is then built from closed terms, identifying terms when the extended theory asserts their equality. An induction on formulas establishes that this term model satisfies the original theory. (math.berkeley.edu)

Ultraproduct proof

A model-theoretic proof uses ultraproducts and Łoś’s theorem. Index structures $M_F$ by the finite subsets $F\subseteq T$, choosing each $M_F$ to satisfy $F$. For every sentence $\sigma\in T$, consider

These sets have the finite intersection property and can be included in an ultrafilter $U$. Łoś’s theorem then implies that

satisfies every sentence of $T$: the indices at which each sentence holds form a set belonging to $U$. (personalpages.manchester.ac.uk)

Principal applications

Infinite and larger models

Suppose a theory $T$ has arbitrarily large finite models. Introduce constants $c_0,c_1,\ldots$ and add all sentences

Every finite subset of the enlarged theory is satisfiable in a sufficiently large finite model of $T$. Compactness produces a model interpreting all the constants as distinct elements, so its domain is infinite. (people.math.sc.edu)

More generally, if $T$ has an infinite model, constants indexed by any prescribed infinite cardinal can be required to be pairwise distinct. Compactness gives a model of at least that cardinality. Together with the Löwenheim–Skolem theorem, this yields models of every infinite cardinality at least as large as the language. (people.math.sc.edu)

Nonstandard arithmetic

A standard application constructs nonstandard models of arithmetic. Add to the Peano axioms a new constant $c$ and the sentences

where $\overline n$ is the numeral denoting the ordinary natural number $n$. Any finite collection is satisfiable in ordinary arithmetic by interpreting $c$ as a sufficiently large number. Compactness therefore gives a model containing an element larger than every standard numeral. Such a model cannot be isomorphic to the ordinary natural-number structure. The same argument works with the complete first-order theory of that structure, not merely the Peano axioms. (plato.stanford.edu)

Graph coloring

In graph theory, compactness establishes a finite-to-infinite coloring principle: for a fixed positive integer $k$, a graph is $k$-colorable if every finite subgraph is $k$-colorable. Encode the possible colors of each vertex using sentences of propositional logic, requiring exactly one color per vertex and different colors at adjacent vertices. Every finite collection of constraints concerns finitely many vertices and is satisfiable by hypothesis. Propositional compactness supplies a coloring of the whole graph. (math.berkeley.edu)

Connection with topological compactness

The name reflects a connection with topology. For a set $P$ of propositional variables, truth assignments form the space

with the product topology, where $\{0,1\}$ is discrete. A formula involves only finitely many variables, so its satisfying assignments form a set that is both open and closed. Finite satisfiability says that these sets have the finite intersection property. Compactness of the assignment space then implies that their total intersection is nonempty. This is precisely the logical compactness theorem for propositional logic. (iep.utm.edu)

A related first-order formulation uses spaces of complete theories: sentences determine basic open-and-closed sets, and logical compactness corresponds to compactness of the resulting topological space. (pages.jh.edu)

Scope and limitations

Compactness applies to first-order logic with its usual semantics; it does not assert compactness for every stronger logical system. For example, second-order logic with full semantics can express that a domain is finite. Combining such a sentence with assertions that there are at least $n$ elements, for every positive integer $n$, gives a finitely satisfiable but unsatisfiable set. (iep.utm.edu)

Even within first-order logic, restricting attention to finite models destroys compactness. The sentences asserting “there are at least $n$ elements” have finite models for every finite subset, but their totality has only infinite models. Consequently, no first-order theory can have exactly all finite structures as its models, although infinitude can be axiomatized by this infinite collection of sentences. (math.berkeley.edu)

The theorem also need not produce a model inside a specified structure. In the arithmetic example, every finite collection is satisfiable in the ordinary natural numbers, but the entire collection requires a different structure. (plato.stanford.edu)

Historical development

Kurt Gödel obtained compactness for countable languages in work associated with his 1929 dissertation and published it in 1930 alongside his completeness theorem. Anatoly Mal’cev extended compactness to arbitrary languages in 1936 and developed applications in algebra. Leon Henkin subsequently introduced a model-building proof that became a standard approach to completeness and compactness. These developments helped establish compactness as a principal method of model theory. (people.math.sc.edu)

References

1. Math 225A – Model Theory, Lecture 16: Compactnessmath.berkeley.edu
2. Mathematical Logic for Mathematicians, Part Imath.berkeley.edu
3. Model Theory — George F. McNultypeople.math.sc.edu
4. The Compactness Theorem and Ultraproducts — Mike Prestpersonalpages.manchester.ac.uk
5. Math 225A – Model Theory, Lecture 17: Compactness Continuedmath.berkeley.edu
6. Kurt Gödel — Stanford Encyclopedia of Philosophyplato.stanford.edu
7. The Compactness Theorem — Internet Encyclopedia of Philosophyiep.utm.edu