Completeness, compactness and Löwenheim–Skolem

Lens

MotivationH

Truth in every model, and proof

There are two ways to say that a sentence $\varphi$ follows from a set of sentences $\Gamma$ .

Semantically: $\Gamma \models \varphi$ if $\varphi$ is true in every structure in which all the sentences of $\Gamma$ are true. To check this one must, in principle, survey all structures — infinitely many, of every size.
Syntactically: $\Gamma \vdash \varphi$ if there is a formal derivation of $\varphi$ from $\Gamma$ : a finite list of formulas, each an axiom, a member of $\Gamma$ or obtained from earlier lines by a rule.

The lesson on first-order logic proved soundness: if $\Gamma \vdash \varphi$ then $\Gamma \models \varphi$ , so derivations never lead from truths to falsehoods. In 1928 David Hilbert and Wilhelm Ackermann asked whether the converse holds — whether the rules of first-order logic are strong enough to derive every consequence. In his 1929 doctoral thesis, Kurt Gödel proved that they are.

Theorem— Gödel's completeness theorem (1929)

For every set of first-order sentences $\Gamma$ and every sentence $\varphi$ : $\ \Gamma \models \varphi \implies \Gamma \vdash \varphi$ . Equivalently, every consistent set of sentences has a model.

So the two notions of consequence coincide. That alone would make the theorem a cornerstone of logic. But it has consequences that reach far beyond logic, because "has a model" is a statement about mathematical structures, while "is consistent" is a statement about finite objects. This lesson proves the theorem and follows three of its consequences: the compactness theorem, which shows that "finite" cannot be expressed in first-order logic and produces numbers larger than every natural number; and the Löwenheim–Skolem theorems, which show that no first-order theory with an infinite model can pin down the size of its models — not even set theory.

IntuitionH

Building a model out of words

How can one produce a model of a theory knowing only that it is consistent? Leon Henkin's idea (1949) is to build the model out of the language itself. Its elements will be the closed terms — expressions such as $c$ , $f(c)$ , $f(f(c), d)$ — with two terms identified when the theory proves them equal, and a relation holding of terms exactly when the theory says it does.

For this to work the theory must already decide everything (for each sentence, contain it or its negation) and must have witnesses: whenever it contains $\exists x\, \varphi(x)$ , it must contain $\varphi(c)$ for some named constant $c$ . Otherwise the theory might assert that something exists while no term names it. So the proof has three steps: add witnesses, extend to a complete theory, read off the model.

Analogy, not a formal construction

The construction resembles building $\C$ as $\R[x]/(x^2 + 1)$ : one manufactures the new objects from symbols (polynomials, terms) and then identifies two of them when the rules force them to be equal ( $x^2 + 1 = 0$ , or "the theory proves $t = s$ "). This is only an analogy — the Henkin model is built from a theory, not a ring — but in both cases the model is made of syntax up to provable equality.

DefinitionsH

Definitions

Fix a first-order language $L$ (constant, function and relation symbols) and write $|L|$ for the number of its symbols. An $L$ -structure $M$ is a non-empty set with interpretations of the symbols; $M \models \varphi$ means the sentence $\varphi$ is true in $M$ .

Definition— models, consistency, satisfiability

A model of a set of sentences $\Gamma$ is a structure in which every sentence of $\Gamma$ is true. $\Gamma$ is satisfiable if it has a model, and finitely satisfiable if each of its finite subsets has a model. $\Gamma$ is consistent if there is no $\varphi$ with $\Gamma \vdash \varphi$ and $\Gamma \vdash \neg\varphi$ (equivalently, $\Gamma \nvdash \bot$ ).

Definition— complete theories, witnesses

$\Gamma$ is complete if for every sentence $\varphi$ , $\Gamma \vdash \varphi$ or $\Gamma \vdash \neg\varphi$ . A consistent $\Gamma$ is maximal consistent if no proper superset is consistent. $\Gamma$ has the witness property (is a Henkin theory) if for every formula $\varphi(x)$ with one free variable there is a constant $c$ with $(\exists x\, \varphi(x) \to \varphi(c)) \in \Gamma$ .

Definition— elementary substructure

$M$ and $N$ are elementarily equivalent, $M \equiv N$ , if they satisfy the same sentences. If $N \subseteq M$ is a substructure, it is an elementary substructure, $N \preceq M$ , if for every formula $\varphi(\vec x)$ and every tuple $\vec b$ from $N$ : $N \models \varphi(\vec b) \iff M \models \varphi(\vec b)$ .

Note

Two different uses of "complete" meet in this lesson. A proof system is complete if it derives every semantic consequence (Gödel's theorem). A theory is complete if it decides every sentence. The completeness theorem says first-order logic is complete in the first sense; Gödel's incompleteness theorem says that arithmetic has no consistent, effectively axiomatised theory that is complete in the second sense.

For the proof we only need four properties of the derivation relation $\vdash$ , all standard for natural deduction or Hilbert-style systems:

Finiteness. If $\Gamma \vdash \varphi$ then $\Gamma_0 \vdash \varphi$ for some finite $\Gamma_0 \subseteq \Gamma$ (a derivation uses finitely many hypotheses).
Splitting. If $\Gamma \cup \{\varphi\}$ and $\Gamma \cup \{\neg\varphi\}$ are both inconsistent, so is $\Gamma$ (proof by cases).
Constants are generic. If $\Gamma \vdash \psi(c)$ and the constant $c$ occurs neither in $\Gamma$ nor in $\psi(x)$ , then $\Gamma \vdash \forall x\, \psi(x)$ .
Equality and logic. The usual rules for $=$ (reflexivity, symmetry, transitivity, substitution) and for the connectives and quantifiers, e.g. $\psi(t) \vdash \exists x\, \psi(x)$ .

Worked examplesH

Examples: theories and their models

Example— Consistent theories with very different models

The axioms of groups have finite and infinite models, abelian and non-abelian ones; they decide neither " $\forall x\, \forall y\ xy = yx$ " nor its negation, so the theory of groups is consistent but not complete.
The theory DLO of dense linear orders without endpoints has the models $(\Q, <)$ , $(\R, <)$ and $(\Q \cap (0, 1), <)$ . By Cantor's back-and-forth theorem, any two countable models are isomorphic, and (as we will see) this makes DLO complete.
The complete theory of arithmetic $\mathrm{Th}(\N) = \{\varphi \mid (\N, 0, 1, +, \times, <) \models \varphi\}$ is complete by definition. We will show it has models not isomorphic to $\N$ .

Example— Saying 'at least n elements'

The sentence $\sigma_n = \exists x_1 \cdots \exists x_n \bigwedge_{i < j} x_i \neq x_j$ is true in a structure exactly when it has at least $n$ elements. So $\{\sigma_1, \sigma_2, \sigma_3, \dots\}$ is an infinite set of sentences whose models are exactly the infinite structures. Can a set of sentences have exactly the finite structures as its models? The compactness theorem will say no.

Example— A finitely satisfiable set that looks impossible

In the language of arithmetic with one new constant $c$ , let $\Gamma = \mathrm{Th}(\N) \cup \{\, c > \overline{0},\ c > \overline{1},\ c > \overline{2}, \dots \}$ , where $\overline{n}$ is the numeral $1 + 1 + \cdots + 1$ . No natural number is larger than every numeral, so $(\N, c)$ is not a model, whatever $c$ is. But any finite subset mentions only finitely many numerals, and $\N$ with $c$ interpreted as a large enough number is a model of it. So $\Gamma$ is finitely satisfiable.

ProofH

The completeness theorem

Theorem— Theorem 1 (completeness, countable languages)

Let $L$ be a countable language. Every consistent set $\Gamma$ of $L$ -sentences has a model, of cardinality at most $\aleph_0$ . Consequently, if $\Gamma \models \varphi$ then $\Gamma \vdash \varphi$ .

Proof

Step 1: adding witnesses. Let $L_0 = L$ . Given $L_n$ , add a new constant $c_\varphi$ for each $L_n$ -formula $\varphi(x)$ with one free variable, obtaining $L_{n+1}$ , and let $L^* = \bigcup_n L_n$ , still countable. Let $H$ be the set of Henkin axioms $\exists x\, \varphi(x) \to \varphi(c_\varphi)$ , one for each $L^*$ -formula $\varphi(x)$ (each such formula lies in some $L_n$ , and $c_\varphi$ is a constant of $L_{n+1}$ ).

Claim: $\Gamma \cup H$ is consistent. By finiteness it suffices to show $\Gamma \cup H_0$ consistent for finite $H_0 \subseteq H$ . Add the axioms of $H_0$ to $\Gamma$ one at a time, in order of increasing level of their constants. When the axiom for $c_\varphi$ is added to the set $\Delta$ built so far, $c_\varphi$ occurs neither in $\varphi(x)$ nor in $\Delta$ : the axioms already in $\Delta$ involve only constants of lower or equal level, and an axiom of the same level has a different constant and a formula from a lower level. Suppose $\Delta$ is consistent but $\Delta \cup \{\exists x\, \varphi(x) \to \varphi(c)\}$ is not. Then $\Delta \vdash \neg(\exists x\, \varphi(x) \to \varphi(c))$ , so $\Delta \vdash \exists x\, \varphi(x)$ and $\Delta \vdash \neg\varphi(c)$ . By property 3, $\Delta \vdash \forall x\, \neg\varphi(x)$ , i.e. $\Delta \vdash \neg \exists x\, \varphi(x)$ , and $\Delta$ is inconsistent — a contradiction.

Step 2: completing (Lindenbaum's lemma). List all $L^*$ -sentences as $\psi_0, \psi_1, \psi_2, \dots$ . Put $\Gamma_0 = \Gamma \cup H$ and

\Gamma_{n+1} = \begin{cases} \Gamma_n \cup \{\psi_n\} & \text{if this is consistent,} \\ \Gamma_n \cup \{\neg\psi_n\} & \text{otherwise.} \end{cases}

By property 2, each $\Gamma_n$ is consistent. Let $\Gamma^* = \bigcup_n \Gamma_n$ . It is consistent by finiteness (a derivation of $\bot$ would use hypotheses from a single $\Gamma_n$ ), it contains $\psi$ or $\neg\psi$ for every sentence $\psi$ , and it is deductively closed: if $\Gamma^* \vdash \psi$ then $\psi \in \Gamma^*$ , since otherwise $\neg\psi \in \Gamma^*$ and $\Gamma^*$ would be inconsistent.

Step 3: the term model. For closed $L^*$ -terms put $t \sim s$ if $(t = s) \in \Gamma^*$ . By the equality rules and deductive closure, $\sim$ is an equivalence relation compatible with the function symbols and relations. Let $M$ be the set of classes $[t]$ , and interpret: $c^M = [c]$ , $f^M([t_1], \dots, [t_k]) = [f(t_1, \dots, t_k)]$ , and $R^M([t_1], \dots, [t_k])$ iff $R(t_1, \dots, t_k) \in \Gamma^*$ . These are well defined by the substitution rule for equality. Every element of $M$ is named by a closed term, and $M$ is countable.

Step 4: the truth lemma. For every $L^*$ -sentence $\psi$ : $\ M \models \psi \iff \psi \in \Gamma^*$ . By induction on the number of connectives and quantifiers in $\psi$ .

Atomic $\psi$ : by the definition of $M$ (closed terms denote their own classes).
$\neg\psi$ : $M \models \neg\psi \iff M \not\models \psi \iff \psi \notin \Gamma^* \iff \neg\psi \in \Gamma^*$ , the last step because $\Gamma^*$ contains exactly one of $\psi$ and $\neg\psi$ .
$\psi \land \chi$ : by deductive closure, $\psi \land \chi \in \Gamma^*$ iff both $\psi, \chi \in \Gamma^*$ .
$\exists x\, \varphi(x)$ : if $\exists x\, \varphi(x) \in \Gamma^*$ , the Henkin axiom and deductive closure give $\varphi(c_\varphi) \in \Gamma^*$ ; by induction $M \models \varphi(c_\varphi)$ , so $M \models \exists x\, \varphi(x)$ . Conversely, if $M \models \exists x\, \varphi(x)$ , some element $[t]$ is a witness, so $M \models \varphi(t)$ ; $\varphi(t)$ has fewer logical symbols than $\exists x\, \varphi(x)$ , so by induction $\varphi(t) \in \Gamma^*$ , and since $\varphi(t) \vdash \exists x\, \varphi(x)$ , deductive closure gives $\exists x\, \varphi(x) \in \Gamma^*$ .

(The other connectives and $\forall$ are expressible by $\neg$ , $\land$ , $\exists$ .) In particular $M \models \Gamma$ , and forgetting the new constants gives a countable $L$ -structure that is a model of $\Gamma$ .

The second form. If $\Gamma \nvdash \varphi$ , then $\Gamma \cup \{\neg\varphi\}$ is consistent (otherwise $\Gamma \vdash \neg\neg\varphi$ , hence $\Gamma \vdash \varphi$ ), so it has a model, which shows $\Gamma \not\models \varphi$ .

∎

For a language of any cardinality $\kappa$ the same proof works with transfinite lists (or Zorn's lemma in Step 2) and gives a model of cardinality at most $\kappa + \aleph_0$ . The only step that is not purely finitary is Step 2: for countable languages it is an explicit induction, and in general it is exactly the Lindenbaum lemma formalised below.

ProofH

Compactness and what it forbids

Theorem— Theorem 2 (compactness)

A set of first-order sentences has a model if and only if every finite subset of it has a model.

Proof

One direction is trivial. Conversely, suppose $\Gamma$ has no model. By completeness $\Gamma$ is inconsistent, i.e. $\Gamma \vdash \bot$ . The derivation uses only a finite $\Gamma_0 \subseteq \Gamma$ , so $\Gamma_0 \vdash \bot$ , and by soundness $\Gamma_0$ has no model.

∎

The theorem has a direct semantic proof too, by ultraproducts and Łoś's theorem — that is how Mathlib proves it, and it is done in the model theory lesson. Either way, it has striking consequences.

Theorem— Theorem 3 (finiteness is not first-order)

If a set of sentences $T$ has arbitrarily large finite models, then it has an infinite model. In particular, no set of sentences has exactly the finite structures as its models.

Proof

Let $\Gamma = T \cup \{\sigma_1, \sigma_2, \dots\}$ , where $\sigma_n$ says "there are at least $n$ elements". A finite $\Gamma_0 \subseteq \Gamma$ contains only $\sigma_n$ with $n \le N$ for some $N$ , and a model of $T$ with at least $N$ elements is a model of $\Gamma_0$ . By compactness $\Gamma$ has a model, which is a model of $T$ satisfying every $\sigma_n$ — an infinite model. If $T$ 's models were exactly the finite structures, $T$ would have arbitrarily large finite models but no infinite one.

∎

Theorem— Corollary 4 (torsion groups)

The class of torsion groups (every element has finite order) is not first-order axiomatisable.

Proof

Suppose $T$ were a set of sentences in the language of groups whose models are exactly the torsion groups. Add a constant $c$ and let $\Gamma = T \cup \{c^n \neq e \mid n \ge 1\}$ . A finite subset mentions only $c^n \neq e$ for $n \le N$ ; it is satisfied in the torsion group $\Z/(N + 1)$ with $c = 1$ . By compactness $\Gamma$ has a model: a torsion group (it satisfies $T$ ) containing an element $c$ of infinite order. Contradiction.

∎

The same method shows that the classes of connected graphs, of well-orders, of fields of positive characteristic and of finite groups are not first-order axiomatisable (see the exercises). The class of infinite groups is axiomatisable — add $\sigma_1, \sigma_2, \dots$ to the group axioms — but not by finitely many sentences.

Theorem— Theorem 5 (nonstandard models of arithmetic)

There is a structure $M \equiv (\N, 0, 1, +, \times, <)$ that contains an element larger than every numeral $\overline{n}$ . In particular $M \not\cong \N$ , and the same holds for models of Peano arithmetic.

Proof

The set $\Gamma = \mathrm{Th}(\N) \cup \{c > \overline{n} \mid n \in \N\}$ is finitely satisfiable, as shown in the examples. By compactness it has a model $M$ , which satisfies $\mathrm{Th}(\N)$ (so $M \equiv \N$ ; in particular $M$ satisfies the axioms of PA) and contains $c^M > \overline{n}^M$ for every $n$ . An isomorphism $\N \to M$ would have to send $n$ to $\overline{n}^M$ , missing $c^M$ .

∎

Such an $M$ looks like $\N$ followed by further "galaxies": every element has a successor and every non-zero element a predecessor, so $c^M$ sits in a copy of $\Z$ , and between and above these copies there are densely ordered families of others — a countable nonstandard model has order type $\omega + (\omega^* + \omega) \cdot \eta$ , where $\eta$ is the order type of $\Q$ . Its arithmetic is wild: Stanley Tennenbaum (1959) proved that in a countable nonstandard model of PA neither $+$ nor $\times$ is computable.

Example— Infinitesimals

Let $\R^\sharp$ be the structure $\R$ with a symbol for every real number, every subset of $\R^n$ and every function $\R^n \to \R$ . Add a constant $\varepsilon$ and the sentences $0 < \varepsilon < \overline{r}$ for every real $r > 0$ . Every finite subset is satisfied in $\R^\sharp$ by a small enough real $\varepsilon$ , so by compactness there is a structure ${}^*\R \equiv \R^\sharp$ with a positive element smaller than every positive real: an infinitesimal. Because ${}^*\R$ satisfies exactly the same sentences as $\R^\sharp$ , it is an ordered field, and every first-order statement about real functions transfers to it. This is the starting point of Abraham Robinson's nonstandard analysis (1961), in which $f'(x)$ is the standard part of $(f(x + \varepsilon) - f(x))/\varepsilon$ — a rigorous version of Leibniz's infinitesimals.

ProofH

The Löwenheim–Skolem theorems

Compactness says that first-order theories cannot express "finite". The Löwenheim–Skolem theorems say they cannot control infinite size either.

Theorem— Lemma 6 (Tarski–Vaught test)

Let $N$ be a substructure of $M$ . Then $N \preceq M$ if and only if: for every formula $\varphi(x, \vec y)$ and every tuple $\vec b$ from $N$ , if $M \models \exists x\, \varphi(x, \vec b)$ then $M \models \varphi(a, \vec b)$ for some $a \in N$ .

Proof

( $\Rightarrow$ ) If $M \models \exists x\, \varphi(x, \vec b)$ then $N \models \exists x\, \varphi(x, \vec b)$ by elementarity, so some $a \in N$ has $N \models \varphi(a, \vec b)$ , hence $M \models \varphi(a, \vec b)$ . ( $\Leftarrow$ ) Show $N \models \psi(\vec b) \iff M \models \psi(\vec b)$ by induction on $\psi$ . Atomic formulas agree because $N$ is a substructure, and the connective steps are immediate. For $\psi = \exists x\, \varphi(x, \vec y)$ : if $N \models \psi(\vec b)$ , a witness in $N$ is a witness in $M$ by induction; if $M \models \psi(\vec b)$ , the test provides a witness $a \in N$ with $M \models \varphi(a, \vec b)$ , so $N \models \varphi(a, \vec b)$ by induction, and $N \models \psi(\vec b)$ .

∎

Theorem— Theorem 7 (downward Löwenheim–Skolem)

Let $L$ be countable, $M$ an $L$ -structure and $A \subseteq M$ countable. Then there is a countable $N \preceq M$ with $A \subseteq N$ .

Proof

Put $A_0 = A$ . Given a countable $A_n$ , there are countably many pairs $(\varphi, \vec b)$ with $\vec b$ a tuple from $A_n$ ; for each with $M \models \exists x\, \varphi(x, \vec b)$ choose a witness $a \in M$ (this uses countable choice), and let $A_{n+1}$ be $A_n$ together with the chosen witnesses — still countable. Let $N = \bigcup_n A_n$ , which is countable. It is closed under the functions of $M$ (a witness for $\exists x\, (x = f(\vec b))$ is $f(\vec b)$ itself) and contains the constants (witnesses for $\exists x\, (x = c)$ ), so it is a substructure, and it satisfies the Tarski–Vaught test by construction: a formula with parameters from $N$ has its parameters in some $A_n$ , and a witness was added in $A_{n+1}$ . So $N \preceq M$ .

∎

Theorem— Theorem 8 (upward Löwenheim–Skolem)

If a theory $T$ in a countable language has an infinite model, then it has a model of every infinite cardinality $\kappa$ .

Proof

Add $\kappa$ new constants $c_\alpha$ ( $\alpha < \kappa$ ) and let $\Gamma = T \cup \{c_\alpha \neq c_\beta \mid \alpha \neq \beta\}$ . A finite subset mentions finitely many constants, which can be interpreted as distinct elements of an infinite model of $T$ ; so by compactness (for a language of size $\kappa$ ) $\Gamma$ has a model, which has at least $\kappa$ elements. The downward theorem for languages of size $\kappa$ (same proof, with $|A_n| \le \kappa$ ) applied to $A = \{c_\alpha^M\}$ gives an elementary substructure of cardinality exactly $\kappa$ , still a model of $\Gamma$ and hence of $T$ .

∎

So a first-order theory with an infinite model has models of every infinite size, and no first-order theory with an infinite model determines its models up to isomorphism. $\mathrm{Th}(\N)$ has uncountable models; $\mathrm{Th}(\R, +, \times, <)$ has countable ones. The best one can hope for is categoricity in a single cardinality, and the Łoś–Vaught test turns that into completeness: if $T$ has no finite models and all its models of some infinite cardinality $\kappa \ge |L|$ are isomorphic, then $T$ is complete. For instance DLO is $\aleph_0$ -categorical (Cantor), hence complete, so $(\Q, <)$ and $(\R, <)$ satisfy exactly the same sentences.

Skolem's paradox. ZFC is a first-order theory in the countable language $\{\in\}$ . If it is consistent, it has a model, and by Theorem 7 a countable model $(M, E)$ . But ZFC proves that $\mathcal P(\omega)$ is uncountable, so $M$ contains an element $p$ that $M$ believes is $\mathcal P(\omega)$ and believes is uncountable — while $p$ has only countably many $E$ -members, since $M$ itself is countable. There is no contradiction. " $p$ is uncountable" means, inside $M$ , "there is no bijection between $\omega$ and $p$ that is an element of $M$ ". A bijection between the $E$ -members of $\omega^M$ and of $p$ exists outside $M$ , but it is not one of $M$ 's sets. Countability is not absolute: it depends on which functions are available. Thoralf Skolem, who pointed this out in 1922, took it as evidence that set-theoretic notions are relative to a model.

ExplanationH

Completeness versus incompleteness

Gödel proved the completeness theorem in 1929 and the incompleteness theorems in 1931. The names suggest a contradiction; there is none.

Completeness is about all models: if a sentence is true in every model of a theory $T$ , then $T$ proves it.
Incompleteness is about one intended model: for any consistent, effectively axiomatised theory $T$ containing enough arithmetic, such as PA, there is a sentence $G$ that is true in $\N$ but not provable in $T$ (see Gödel's incompleteness theorems).

Put together: since $\mathrm{PA} \nvdash G$ , the completeness theorem says that $\mathrm{PA} \cup \{\neg G\}$ has a model. That model satisfies PA but not $G$ , so it is not $\N$ : it is a nonstandard model, whose existence we already know from compactness. True-in- $\N$ and true-in-every-model-of-PA are different things, and the gap between them is exactly where the incompleteness theorem lives.

The completeness theorem also has a computational meaning. Derivations can be listed mechanically, so the set of sentences valid in all structures is computably enumerable: a machine can confirm validity, eventually, whenever it holds. Alonzo Church and Alan Turing (1936) proved that validity is nevertheless undecidable: no machine can also confirm invalidity in every case (see computability).

Formal mathematicsF

What Lean and Mathlib formalise

Mathlib has first-order syntax and semantics — languages, terms, formulas with bound variables indexed by Fin n, structures, M ⊨ φ, theories and models — and proves the compactness theorem semantically, by an ultraproduct of models of the finite subtheories. It does not yet contain a formal derivation relation $\vdash$ for first-order logic, so Gödel's theorem in the form "consistent implies satisfiable" is not formalised here. What we can formalise is the combinatorial core of the Henkin proof, Lindenbaum's lemma, for an arbitrary finitary notion of consistency:

FinitaryLean 4Formally verified

/-- A notion of consistency `Con` on sets of sentences is **finitary** if a set is consistent
exactly when each of its finite subsets is. Consistency in the sense of proofs is finitary,
because a derivation of a contradiction uses only finitely many hypotheses. -/
def Finitary {S : Type u} (Con : Set S → Prop) : Prop :=
  ∀ Γ : Set S, Con Γ ↔ ∀ Δ : Finset S, (Δ : Set S) ⊆ Γ → Con Δ