Löwenheim–Skolem Theorem

Statement

Let $L$ be a countable first-order language and $T$ an $L$-theory with an infinite model. Then for every infinite cardinal $\kappa \ge |L| + \aleph_0$, there exists a model of $T$ of cardinality exactly $\kappa$:

Visualization

The theory of dense linear orders without endpoints (DLO, e.g. $(\mathbb{Q}, <)$) has a countable model and models of every infinite cardinality:

Cardinality   Example model
-----------   ----------------------------
ℵ₀            (ℚ, <) — rationals
ℵ₁            Dedekind completion + gaps
ℵ₂            further extension
…
κ (any ∞)     Corresponding ordered field extension

All these are elementary extensions of ℚ — they satisfy exactly
the same first-order sentences.

The Skolem paradox: ZFC (if consistent) has a countable model. This does not mean "the reals are countable" inside that model — the internal bijection simply does not exist in the small model, even though the model satisfies the sentence "the reals are uncountable."

Proof Sketch

Downward (Skolem–Löwenheim): Given an infinite model $M$, build the Skolem hull generated by countably many witnesses. Each existential sentence $\exists x \phi(x)$ true in $M$ has a witness added; the resulting substructure is countable and elementary.

Upward: Given infinite $M$ and cardinal $\kappa > |M|$, add $\kappa$ many new constants $\{c_i\}$ to the language. By CompactnessCompactness Theorem (FOL)$$T \text{ satisfiable} \iff \forall T_0 \subseteq_\text{fin} T,\ T_0 \text{ satisfiable}$$A first-order theory has a model if and only if every finite subset has a model.Read more →, the expanded theory (asserting all $c_i$ are distinct) is satisfiable. The model witnesses each $c_i$ distinctly, yielding a model of size $\ge \kappa$; Downward can then trim to exactly $\kappa$.

Connections

Löwenheim–Skolem is a direct corollary of CompactnessCompactness Theorem (FOL)$$T \text{ satisfiable} \iff \forall T_0 \subseteq_\text{fin} T,\ T_0 \text{ satisfiable}$$A first-order theory has a model if and only if every finite subset has a model.Read more → (upward direction). The downward direction uses Skolem functions, which also appear in Gödel's Completeness TheoremGödel's Completeness Theorem$$T \vdash \phi \iff T \models \phi$$A first-order sentence is provable from a theory iff it holds in every model of that theory.Read more →. Both theorems reveal the limits of first-order logic: it cannot pin down a unique model up to isomorphism for infinite structures.

import Mathlib.ModelTheory.Satisfiability

open FirstOrder Language Cardinal

/-- The Löwenheim–Skolem Theorem: any infinite L-structure M and infinite cardinal κ ≥ |L|
    yields a structure of cardinality κ elementarily embedded in or extending M.
    Mathlib: `FirstOrder.Language.exists_elementaryEmbedding_card_eq`. -/
theorem lowenheim_skolem
    {L : Language.{0, 0}} (M : Type*) [L.Structure M] [Infinite M]
    (κ : Cardinal) (h1 : ℵ₀ ≤ κ) (h2 : L.card ≤ κ) :
    ∃ N : CategoryTheory.Bundled L.Structure,
      (Nonempty (N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] N)) ∧ #N = κ :=
  exists_elementaryEmbedding_card_eq L M κ h1 (by simpa using h2)