Compactness and the Compactness Theorem

The compactness theorem can be stated in many ways. It is due to Gödel (1930) and Malcev (1936).

It is an important result for mathematics and computation, as it implies that there are finite proofs available even when dealing with infinite systems.


Proof of the compactness theorem "A set of sentences SS is satisfiable if and only if every finite subset of SS is satisfiable."

Proof one way is easy, the other way is more difficult

If SS is satisfiable,
- then there is a valuation V satisfying all sentences in SS,
- and so every finite subset of SS is satisfied by V.

If every finite subset of SS is satisfiable.
- we take a set DD and show that it is a superset of SS and also satisfiable
- DD is the maximal satisfiable set







Logic Index



Version 1

If all finite subsets of a set of sentences A are satisfiable, then A is satisfiable. (even if A is infinite)


Version 2

a set of first-order sentences is satisfiable, i.e., has a model, if and only if every finite subset of it is satisfiable.


Version 3

Let Ss be a set of sentences of predicate logic. Ss is satisfiable if and only if every finite subset of Ss is satisfiable.


Version 4

A set SS of formulas is satisfiable if and only if every finite subset of SS is satisfiable


Version 5

If each finite subset of a set S of sentences has a model, then the whole set S has a model.


Version 6

A logic is compact iff there are no instances of the logical consequence relation which have an essentially infinite set of premises.


The compactness theorem has been used to show that many interesting properties of models cannot be expressed by a set of first-order sentences -- for instance, there is no set of sentences whose models are precisely all the finite models.

To prove the compactness theorem we must construct a single model in which each sentence of S is true.