---
tag: 484M0TZ1S7
kind: statement
role: theorem
name: Löwenheim–Skolem theorem
msc: [03C07, 03C55]
uses: [WDVVEYD6AT, 983GZBQYT4, 8WZF9SBP39, 0EBACQFAZW]
about: [983GZBQYT4]
sources:
  - url: https://en.wikipedia.org/wiki/Löwenheim–Skolem_theorem
same_as:
  wikidata: Q1068283
  wikipedia: Löwenheim–Skolem theorem
---

## Statement

Let $\sigma$ be a [[signature|WDVVEYD6AT]], and let $\kappa = \max(\abs{\sigma}, \aleph_0)$.
Let $M$ be an infinite $\sigma$-[[structure|983GZBQYT4]], and let $\lambda$ be an infinite [[cardinal|0EBACQFAZW]].

1. Downward: if $\kappa \le \lambda \le \abs{M}$ and $A \subseteq M$ has $\abs{A} \le \lambda$, then $M$ has an [[elementary substructure|8WZF9SBP39]] $N$ with $A \subseteq N$ and $\abs{N} = \lambda$.
2. Upward: if $\lambda \ge \max(\abs{M}, \kappa)$, then $M$ has an elementary extension of cardinality $\lambda$.

## Remarks

The downward part closes $A$ under Skolem functions, which pick witnesses for existential formulas, and uses the [[Tarski–Vaught test|60SA99BER7]].
The upward part adds $\lambda$ new constants that must be pairwise distinct, uses the [[compactness theorem|1NR3HAWG9D]], and then applies the downward part.
For example, the field $\R$ has a countable elementary substructure: the real algebraic numbers form one, by quantifier elimination for real closed fields, the [[Tarski–Seidenberg theorem|3W5JGDZAN0]].
The hypothesis that $M$ is infinite is needed: a finite structure has no elementary extension of a different size.
As a consequence, a countable first-order theory with an infinite model has models of every infinite cardinality.
So no first-order theory with an infinite model determines its models up to isomorphism; [[Skolem's paradox|68QZWDXAQ4]] is one effect of this.
In Mathlib the downward part is `FirstOrder.Language.exists_elementarySubstructure_card_eq`.

## Explanations

### L1 human

First-order logic cannot control the size of an infinite structure.
If some first-order axioms have an infinite model, then they have models of every infinite size, small and large, at least as large as the language.
For example, there are countable structures that satisfy exactly the same first-order sentences as the real numbers.

### L2 human

The theorem is a basic tool of [[model theory|HFTBG5PMXC]].
It shows that categoricity in all infinite cardinalities is impossible, so model theory studies categoricity in one cardinality, as in [[Morley's categoricity theorem|V7N84P60SJ]].
The [[Łoś–Vaught test|ZR7Y5C235P]] combines it with categoricity in one cardinality to prove that a theory is complete.
Second-order logic has no such theorem, since the second-order Peano axioms determine $\N$ up to isomorphism.