Compactness theorem

Remarks

One direction is clear, since a model of $\Gamma$ is a model of each subset. For the other, if $\Gamma$ had no model, then by Gödel's completeness theorem it would derive a contradiction. That derivation uses only finitely many sentences of $\Gamma$, and this finite subset would have no model. A second proof builds a model as an ultraproduct of models of the finite subsets. Application: let $\Gamma$ be the true sentences of arithmetic, plus $c > \underline{n}$ for a new constant $c$ and each numeral $\underline{n}$. Each finite subset holds in $\N$ with $c$ a large number, so $\Gamma$ has a model, a non-standard model of arithmetic. In Mathlib the theorem is FirstOrder.Language.Theory.isSatisfiable_iff_isFinitelySatisfiable.

Going deeper

For a student

Compactness is the main tool of model theory. A typical use shows that some property cannot be expressed in first-order logic. If a theory has finite models of every size, then it has an infinite model, so "the domain is finite" is not first-order. The theorem is named after compactness in topology: it says that a certain space of complete theories, the Stone space, is compact. By Lindström's theorem, first-order logic is the strongest logic that has both compactness and the downward Löwenheim–Skolem theorem.