Model theory · The Lumenary

MotivationH

One sentence, many worlds

Here is a theorem about complex polynomials:

Ax–Grothendieck. If a polynomial map $f : \C^n \to \C^n$ is injective, then it is surjective.

For $n = 1$ this is easy (a non-constant polynomial in one variable takes every value). For $n \ge 2$ it is not at all obvious. Yet over a finite set it is trivial: an injective map from a finite set to itself is surjective, by counting. The proof we will give runs: the statement, for maps of bounded degree, is a single first-order sentence; it is true over the algebraic closure of every finite field because those are unions of finite fields; and any first-order sentence in the language of rings that is true in algebraically closed fields of every prime characteristic is true in $\C$ . Each step is a theorem of model theory.

Or take two familiar orders, the rationals $(\Q, <)$ and the reals $(\R, <)$ . They are not isomorphic — one is countable, the other is not — and $\R$ is complete while $\Q$ is full of gaps. Yet no sentence of first-order logic that talks only about $<$ can tell them apart. Model theory explains why, and turns that blindness into a powerful method.

Model theory studies the relationship between theories (sets of sentences) and their models (structures in which the sentences are true): what a theory determines about its models, which sets are definable in a structure, and how structures that satisfy the same sentences can be built and compared. This lesson assumes first-order logic and the completeness, compactness and Löwenheim–Skolem theorems.

IntuitionH

Sentences cut out classes of structures

Fix a language $L$ — a list of function, relation and constant symbols. For a set $T$ of $L$ -sentences and a class $K$ of $L$ -structures put

\mathrm{Mod}(T) = \{\, M \mid M \models \varphi \text{ for all } \varphi \in T \,\}, \qquad \mathrm{Th}(K) = \{\, \varphi \mid M \models \varphi \text{ for all } M \in K \,\}.

Both maps reverse inclusions, and $K \subseteq \mathrm{Mod}(T) \iff T \subseteq \mathrm{Th}(K)$ : they form an antitone Galois connection. By the completeness theorem, $\mathrm{Th}(\mathrm{Mod}(T))$ is exactly the set of consequences of $T$ . A single structure $M$ has a complete theory $\mathrm{Th}(M)$ : for each sentence $\varphi$ , exactly one of $\varphi$ , $\neg\varphi$ belongs to it.

Analogy, not a formal construction

In algebraic geometry, polynomial equations cut out varieties, and a set of points determines the ideal of polynomials vanishing on it; the maps $I \mapsto V(I)$ and $X \mapsto I(X)$ form a Galois connection of exactly the same shape. Model theory's "geometry" is the study of definable sets: subsets of $M^n$ of the form $\{\bar a \mid M \models \varphi(\bar a, \bar b)\}$ . For algebraically closed fields the analogy becomes literal — the definable sets are the constructible sets of algebraic geometry. In general it is only an analogy: definable sets need not look like varieties at all.

Three tools do most of the work in a first course:

Ultraproducts average a family of structures; Łoś's theorem says a sentence holds in the average iff it holds in "most" of the factors.
Quantifier elimination shows that, in a good theory, every definable set is defined without quantifiers — so definable sets can be understood concretely.
Back and forth builds isomorphisms, and its finite version — Ehrenfeucht–Fraïssé games — shows exactly what first-order logic can and cannot see.

DefinitionsH

Definitions

Throughout, structures are nonempty, and $\bar a$ denotes a finite tuple.

Definition— elementary equivalence

$L$ -structures $M$ and $N$ are elementarily equivalent, written $M \equiv N$ , if they satisfy the same $L$ -sentences: $\mathrm{Th}(M) = \mathrm{Th}(N)$ .

Definition— elementary embedding and elementary substructure

A map $j : M \to N$ is an elementary embedding if for every formula $\varphi(x_1, \dots, x_n)$ and every $\bar a \in M^n$ ,

M \models \varphi(\bar a) \iff N \models \varphi(j\bar a).

If $M \subseteq N$ and the inclusion is elementary, $M$ is an elementary substructure of $N$ and $N$ an elementary extension of $M$ , written $M \preceq N$ .

Taking $n = 0$ shows that $M \preceq N$ implies $M \equiv N$ . The converse fails, and the difference is parameters: $(\N_{\ge 1}, <)$ is a substructure of $(\N, <)$ isomorphic to it, hence elementarily equivalent, but the formula $\forall y\,(x \le y)$ holds of $x = 1$ in the substructure and not in $\N$ .

Theorem— Tarski–Vaught test

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

Proof

( $\Rightarrow$ ) If $N \models \exists x\,\varphi(x, \bar a)$ then $M \models \exists x\,\varphi(x, \bar a)$ by elementarity; pick $b \in M$ with $M \models \varphi(b, \bar a)$ ; by elementarity again $N \models \varphi(b, \bar a)$ .

( $\Leftarrow$ ) We show $M \models \psi(\bar a) \iff N \models \psi(\bar a)$ for all formulas $\psi$ and tuples $\bar a$ from $M$ , by induction on $\psi$ (built from atomic formulas with $\neg$ , $\wedge$ , $\exists$ ). Atomic formulas are preserved because $M$ is a substructure: terms are evaluated the same way in $M$ and $N$ . The cases $\neg$ and $\wedge$ are immediate from the induction hypothesis. If $M \models \exists x\,\varphi(x, \bar a)$ , choose a witness $b \in M$ ; by induction $N \models \varphi(b, \bar a)$ , so $N \models \exists x\,\varphi(x, \bar a)$ . Conversely, if $N \models \exists x\, \varphi(x, \bar a)$ , the hypothesis gives $b \in M$ with $N \models \varphi(b, \bar a)$ , and by induction $M \models \varphi(b, \bar a)$ .

∎

Note that the test only ever evaluates formulas in $N$ : it asks whether $M$ contains enough witnesses.

Definition— complete theory, categoricity

A consistent theory $T$ is complete if for every sentence $\varphi$ , either $T \models \varphi$ or $T \models \neg \varphi$ . For an infinite cardinal $\kappa$ , $T$ is $\kappa$ -categorical if any two models of $T$ of cardinality $\kappa$ are isomorphic.

Definition— quantifier elimination

A theory $T$ has quantifier elimination (QE) if every formula $\varphi(\bar x)$ is $T$ -equivalent to a quantifier-free formula $\psi(\bar x)$ with the same free variables: $T \models \forall \bar x\,(\varphi \leftrightarrow \psi)$ . (We count $\top$ and $\bot$ as quantifier-free, so that sentences can be equivalent to quantifier-free sentences even in a language without constants.)

Definition— ultrafilter and ultraproduct

An ultrafilter on a set $I$ is a family $U$ of subsets of $I$ with $\emptyset \notin U$ , closed under finite intersections and supersets, and such that for every $A \subseteq I$ exactly one of $A$ and $I \setminus A$ is in $U$ . It is principal if it consists of all sets containing a fixed $i_0$ . Every family of subsets with the finite intersection property extends to an ultrafilter (by Zorn's lemma); in particular, non-principal ultrafilters on $\N$ exist (extend the cofinite sets).

Given $L$ -structures $(M_i)_{i \in I}$ and an ultrafilter $U$ on $I$ , the ultraproduct $\prod_i M_i / U$ is the set $\prod_i M_i$ modulo $f \sim g \iff \{i \mid f(i) = g(i)\} \in U$ , with functions and constants interpreted coordinatewise and

R([f_1], \dots, [f_n]) \iff \{\, i \mid M_i \models R(f_1(i), \dots, f_n(i)) \,\} \in U .

If all $M_i = M$ , this is the ultrapower $M^I / U$ , and $d(a) = [i \mapsto a]$ is the diagonal map $M \to M^I/U$ .

Closure of $U$ under intersections and supersets makes $\sim$ an equivalence relation and makes the interpretations independent of representatives. Think of $U$ as deciding which sets of indices are "large": a property holds in the ultraproduct when it holds on a large set of coordinates.

Definition— types

Let $M$ be a structure and $A \subseteq M$ . A complete $n$ -type over $A$ is a set $p(\bar x)$ of formulas in $n$ free variables with parameters from $A$ that is maximal subject to $p \cup \mathrm{Th}(M_A)$ being satisfiable, where $M_A$ is $M$ with names for the elements of $A$ . The set of these is $S_n^M(A)$ . A type is realised in an elementary extension $N \succeq M$ by $\bar b$ if $N \models \varphi(\bar b)$ for all $\varphi \in p$ .

Worked examplesH

Examples and non-examples

Example— Elementarily equivalent, not isomorphic

$(\Q, <) \equiv (\R, <)$ , and in fact $(\Q, <) \preceq (\R, <)$ ; both statements are proved below, from quantifier elimination for dense linear orders. They are not isomorphic, since $\Q$ is countable and $\R$ is not. "Every bounded nonempty set has a supremum" is not first-order: it quantifies over sets.

Example— Distinguished by one sentence

$(\N, <) \not\equiv (\Z, <)$ : the sentence $\exists x\, \forall y\, (x \le y)$ ("there is a least element") separates them.
$(\Z, <) \not\equiv (\Q, <)$ : density, $\forall x\,\forall y\,(x < y \to \exists z\,(x < z \wedge z < y))$ , separates them. So $(\Z, <) \subseteq (\Q, <)$ is a substructure that is not elementary.
Finite structures of different sizes are never elementarily equivalent: "there are exactly $n$ elements" is a sentence. But sentences of bounded quantifier depth see only a bounded amount: the computation section shows that sentences with at most $k$ nested quantifiers cannot tell a linear order with $2^k - 1$ elements from one with $2^k$ .

Example— A theory without quantifier elimination

In $(\Z, <)$ the formula $\varphi(a, b) = \exists x\,(a < x \wedge x < b)$ is not equivalent to a quantifier-free formula in $a, b$ . A quantifier-free formula in two variables is a Boolean combination of $a < b$ , $a = b$ , $b < a$ , so it has the same truth value at $(0, 1)$ and $(0, 2)$ ; but $\varphi(0, 1)$ is false and $\varphi(0, 2)$ is true. (Enlarging the language by successor and predecessor functions restores quantifier elimination for $\mathrm{Th}(\Z, <)$ .)

Similarly, the ordered field $\R$ has QE in the language $\{+, -, \cdot, 0, 1, <\}$ (Tarski), but not in the ring language $\{+, -, \cdot, 0, 1\}$ : there $\exists y\,(y \cdot y = x)$ defines $[0, \infty)$ , while a quantifier-free formula in one variable defines a finite or cofinite set.

Example— Hyperreals and nonstandard natural numbers

Let $U$ be a non-principal ultrafilter on $\N$ . In ${}^*\R = \R^\N/U$ , the element $\varepsilon = [(1, \tfrac12, \tfrac13, \dots)]$ satisfies $0 < \varepsilon < r$ for every real $r > 0$ : the set $\{n \mid 1/n < r\}$ is cofinite, hence in $U$ . Likewise in $\N^\N/U$ the class of $(0, 1, 2, \dots)$ lies above every standard natural number — proved in Lean below. By Łoś's theorem the diagonal maps $\R \to {}^*\R$ and $\N \to \N^\N/U$ are elementary, so these new elements live in structures with exactly the same first-order theory as the old ones.

ProofH

Łoś's theorem and compactness

Theorem— Łoś's theorem

Let $(M_i)_{i\in I}$ be nonempty $L$ -structures, $U$ an ultrafilter on $I$ and $M = \prod_i M_i / U$ . For every formula $\varphi(x_1, \dots, x_n)$ and $f_1, \dots, f_n \in \prod_i M_i$ ,

M \models \varphi([f_1], \dots, [f_n]) \iff \{\, i \in I \mid M_i \models \varphi(f_1(i), \dots, f_n(i)) \,\} \in U.

Proof

Write $\|\varphi(\bar f)\| = \{i \mid M_i \models \varphi(\bar f(i))\}$ . First, for every term $t$ , the value $t^M([f_1], \dots, [f_n])$ is the class of $i \mapsto t^{M_i}(f_1(i), \dots, f_n(i))$ : this is an induction on $t$ , using that functions are interpreted coordinatewise. Now induct on $\varphi$ , built from atomic formulas by $\neg$ , $\wedge$ and $\exists$ .

Atomic. For $t_1 = t_2$ this is the definition of $\sim$ , and for $R(t_1, \dots, t_k)$ the definition of $R^M$ , combined with the statement about terms.
Negation. $M \models \neg\varphi(\bar f)$ iff $\|\varphi(\bar f)\| \notin U$ (induction) iff $I \setminus \|\varphi(\bar f)\| = \|\neg\varphi(\bar f)\| \in U$ . This is the only step that uses that $U$ is an ultrafilter.
Conjunction. $\|\varphi \wedge \psi\| = \|\varphi\| \cap \|\psi\|$ , and a filter contains $A \cap B$ iff it contains both $A$ and $B$ .
Existential. Suppose $M \models \exists x\, \varphi(x, \bar f)$ , witnessed by $[g]$ . By induction $\|\varphi(g, \bar f)\| \in U$ , and this set is contained in $\|\exists x\,\varphi(x, \bar f)\|$ , which is therefore in $U$ . Conversely, suppose $B = \|\exists x\,\varphi(x, \bar f)\| \in U$ . For $i \in B$ choose $g(i) \in M_i$ with $M_i \models \varphi(g(i), \bar f(i))$ , and for $i \notin B$ let $g(i)$ be any element of $M_i$ (nonempty). Then $\|\varphi(g, \bar f)\| \supseteq B$ is in $U$ , so by induction $M \models \varphi([g], \bar f)$ , hence $M \models \exists x\,\varphi(x, \bar f)$ .

∎

The existential step uses the axiom of choice to pick $g$ — this is where all the witnesses are assembled into one element.

Theorem— Corollary — the diagonal embedding is elementary

For every structure $M$ and ultrafilter $U$ on $I$ , the diagonal map $d : M \to M^I/U$ is an elementary embedding.

Proof

For $\bar a \in M^n$ , Łoś gives $M^I/U \models \varphi(d\bar a)$ iff $\{i \mid M \models \varphi(\bar a)\} \in U$ . That set is $I$ or $\emptyset$ according as $M \models \varphi(\bar a)$ or not, and $I \in U$ , $\emptyset \notin U$ .

∎

Theorem— Compactness theorem — second proof

If every finite subset of a theory $T$ has a model, then $T$ has a model.

Proof

Let $I$ be the set of finite subsets of $T$ , and for each $\Delta \in I$ choose a model $M_\Delta \models \Delta$ . For $\varphi \in T$ let $A_\varphi = \{\Delta \in I \mid \varphi \in \Delta\}$ . These sets have the finite intersection property, since $\{\varphi_1, \dots, \varphi_k\} \in A_{\varphi_1} \cap \dots \cap A_{\varphi_k}$ . Extend them to an ultrafilter $U$ on $I$ , and let $M = \prod_\Delta M_\Delta / U$ . For $\varphi \in T$ , every $\Delta \in A_\varphi$ has $M_\Delta \models \varphi$ , so $\{\Delta \mid M_\Delta \models \varphi\} \supseteq A_\varphi$ belongs to $U$ , and $M \models \varphi$ by Łoś.

∎

This proof is purely semantic: it does not pass through the completeness theorem or any proof system. It is the proof Mathlib formalises.

An ultraproduct of models of finite fragments. Coordinate Δ satisfies the sentences in Δ; each φ ∈ T holds on the large set of Δ containing φ, so Łoś's theorem makes φ true in the ultraproduct.

ProofH

Dense linear orders: quantifier elimination and back and forth

Let $\mathrm{DLO}$ be the theory, in the language $\{<\}$ , of dense linear orders without endpoints: the axioms of a strict linear order, together with $\forall x\,\exists y\,(x < y)$ , $\forall x\,\exists y\,(y < x)$ and $\forall x\,\forall y\,(x < y \to \exists z\,(x < z \wedge z < y))$ . Its models include $\Q$ , $\R$ , $\Q \cap (0, 1)$ and the real algebraic numbers.

We first reduce QE in general to a single quantifier applied to a conjunction.

Theorem— Lemma — reduction to primitive formulas

Suppose that for every conjunction $\theta(x, \bar y)$ of atomic and negated atomic formulas, $\exists x\,\theta$ is $T$ -equivalent to a quantifier-free formula in $\bar y$ . Then $T$ has quantifier elimination.

Proof

By induction on formulas we show each is $T$ -equivalent to a quantifier-free one. Atomic formulas are quantifier-free, and the class of formulas with quantifier-free equivalents is closed under $\neg$ and $\wedge$ . For $\exists x\,\varphi$ , replace $\varphi$ by a quantifier-free equivalent and put it in disjunctive normal form $\theta_1 \vee \dots \vee \theta_m$ , each $\theta_j$ a conjunction of literals. Since $\exists x\,(\theta_1 \vee \dots \vee \theta_m)$ is logically equivalent to $\exists x\,\theta_1 \vee \dots \vee \exists x\,\theta_m$ , the hypothesis applies to each disjunct.

∎

The heart of the matter is the following lemma, formalised in Lean below as dlo_elim_core.

Theorem— Key lemma

Let $M \models \mathrm{DLO}$ and let $A, B \subseteq M$ be finite. There is $x \in M$ with $a < x$ for all $a \in A$ and $x < b$ for all $b \in B$ if and only if $a < b$ for all $a \in A$ , $b \in B$ .

Proof

The forward direction is transitivity. Conversely, assume $a < b$ for all $a \in A$ , $b \in B$ . If $A$ and $B$ are both nonempty, then $\max A < \min B$ , and density gives $x$ with $\max A < x < \min B$ . If only $B$ is nonempty, take $x < \min B$ (no least element); if only $A$ is nonempty, take $x > \max A$ (no greatest element); if both are empty, take any $x$ ( $M$ is nonempty).

∎

Theorem— Theorem — DLO has quantifier elimination

Every formula in the language $\{<\}$ is $\mathrm{DLO}$ -equivalent to a quantifier-free formula.

Proof

By the reduction lemma it suffices to treat $\exists x\,\theta$ with $\theta$ a conjunction of literals. In a linear order, $\neg(s < t) \leftrightarrow (t < s \vee s = t)$ and $\neg(s = t) \leftrightarrow (s < t \vee t < s)$ ; substituting and redistributing, $\theta$ becomes a disjunction of conjunctions of atomic formulas, and $\exists$ distributes over $\vee$ . So let $\theta$ be a conjunction of atomic formulas. Conjuncts not mentioning $x$ can be moved outside the quantifier. A conjunct $x < x$ makes $\theta$ equivalent to $\bot$ ; a conjunct $x = x$ can be dropped. If some conjunct is $x = c$ (or $c = x$ ) with $c$ a variable other than $x$ , then $\exists x\,(x = c \wedge \theta'(x)) \leftrightarrow \theta'(c)$ . Otherwise $\theta$ has the form $\bigwedge_{a \in A} a < x \wedge \bigwedge_{b \in B} x < b$ for finite sets of variables $A$ and $B$ , and by the key lemma $\exists x\,\theta$ is equivalent to $\bigwedge_{a \in A, b \in B} a < b$ — the empty conjunction being $\top$ .

∎

Theorem— Corollary — completeness and model completeness

(1) $\mathrm{DLO}$ is complete; in particular $(\Q, <) \equiv (\R, <)$ . (2) Every embedding between models of $\mathrm{DLO}$ is elementary; in particular $(\Q, <) \preceq (\R, <)$ .

Proof

(1) The language has no constant symbols, so a quantifier-free sentence is a Boolean combination of $\top$ and $\bot$ . By QE every sentence is $\mathrm{DLO}$ -equivalent to $\top$ or to $\bot$ , so $\mathrm{DLO}$ decides it; and $\mathrm{DLO}$ is consistent because $\Q$ is a model. (2) Embeddings preserve quantifier-free formulas, and every formula is $\mathrm{DLO}$ -equivalent to a quantifier-free one.

∎

There is a second, older route to completeness, through categoricity.

Theorem— Cantor's theorem — DLO is ℵ₀-categorical

Any two countable models of $\mathrm{DLO}$ are isomorphic.

Proof

Let $A$ , $B$ be countable models of DLO; they are infinite (a finite nonempty linear order has a greatest element). Enumerate $A = \{a_0, a_1, \dots\}$ and $B = \{b_0, b_1, \dots\}$ . Call a finite order-preserving bijection $p$ between a finite subset of $A$ and a finite subset of $B$ a partial isomorphism.

Extension property: if $p$ is a partial isomorphism and $a \in A$ , there is $b \in B$ with $p \cup \{(a, b)\}$ a partial isomorphism. If $a \in \mathrm{dom}\,p$ take $b = p(a)$ . Otherwise let $A_- = \{a' \in \mathrm{dom}\,p \mid a' < a\}$ and $A_+ = \{a' \in \mathrm{dom}\,p \mid a < a'\}$ . Every element of $p(A_-)$ is below every element of $p(A_+)$ , since $p$ preserves order, so the key lemma (applied in $B$ ) gives $b$ above $p(A_-)$ and below $p(A_+)$ ; then $b \notin \mathrm{ran}\,p$ and $p \cup \{(a, b)\}$ preserves order. By symmetry, for every $b \in B$ there is a matching $a \in A$ .

Start with $p_0 = \emptyset$ . At step $2n + 1$ extend so that $a_n$ is in the domain ("forth"); at step $2n + 2$ extend so that $b_n$ is in the range ("back"). The union $\bigcup_n p_n$ is an order-preserving map defined on all of $A$ and onto all of $B$ : an isomorphism.

∎

Back and forth: alternately add the next point of A (forth) and the next point of B (back), each time choosing a partner in the same position relative to the points already matched. Density and the absence of endpoints guarantee a partner always exists.

Theorem— Łoś–Vaught test

Let $T$ be a consistent theory in a language $L$ with no finite models, and suppose $T$ is $\kappa$ -categorical for some infinite cardinal $\kappa \ge |L|$ . Then $T$ is complete.

Proof

If $T$ decided neither $\varphi$ nor $\neg\varphi$ , both $T \cup \{\varphi\}$ and $T \cup \{\neg \varphi\}$ would have models, necessarily infinite. By the upward and downward Löwenheim–Skolem theorems each has a model of cardinality $\kappa$ . These two models of $T$ are isomorphic by categoricity, yet one satisfies $\varphi$ and the other $\neg\varphi$ — a contradiction.

∎

With Cantor's theorem ( $\kappa = \aleph_0$ , $L$ finite) this gives a second proof that DLO is complete. Mathlib proves completeness exactly this way.

ProofH

Algebraically closed fields, Lefschetz and Ax–Grothendieck

Work in the language of rings $\{+, -, \cdot, 0, 1\}$ . Let $\mathrm{ACF}$ be the theory of algebraically closed fields — the field axioms plus, for each $n \ge 1$ , the sentence $\forall a_0 \dots \forall a_{n-1}\, \exists x\, (x^n + a_{n-1}x^{n-1} + \dots + a_0 = 0)$ . For $p$ prime, $\mathrm{ACF}_p$ adds $p \cdot 1 = 0$ ; and $\mathrm{ACF}_0$ adds $p \cdot 1 \neq 0$ for every prime $p$ .

Theorem— Theorem (Tarski) — ACF has quantifier elimination

Every formula in the language of rings is $\mathrm{ACF}$ -equivalent to a quantifier-free formula.

We do not prove this here; a complete proof (by the same reduction lemma, with a careful elimination of $\exists x$ from systems $f_1(x) = \dots = f_k(x) = 0 \wedge g(x) \neq 0$ using polynomial division) is in Marker, Model Theory: An Introduction, Theorem 3.2.2. Its consequences are what matter for us.

Constructible sets. In $K \models \mathrm{ACF}$ , a quantifier-free formula with parameters defines a finite Boolean combination of zero sets of polynomials — a constructible set. So the definable subsets of $K^n$ are exactly the constructible ones. Since an existential quantifier is a coordinate projection, QE implies that the projection $K^{n+1} \to K^n$ of a constructible set is constructible: this is Chevalley's theorem for affine space over $K$ . (Conversely, a sufficiently uniform form of Chevalley's theorem yields QE; the two are closely related rather than literally the same statement.)
Completeness of $\mathrm{ACF}_p$ . A quantifier-free sentence is a Boolean combination of atomic sentences $t_1 = t_2$ between closed terms, that is, of statements $n \cdot 1 = m \cdot 1$ with $n, m \in \Z$ . These are decided by the characteristic. Hence $\mathrm{ACF}_p$ is complete for $p = 0$ and for every prime $p$ . In particular $\overline{\Q} \equiv \C$ , and by QE again $\overline{\Q} \preceq \C$ .

Theorem— Lefschetz principle

For a sentence $\varphi$ in the language of rings, the following are equivalent:

$\C \models \varphi$ ;
$\mathrm{ACF}_0 \models \varphi$ ;
$\mathrm{ACF}_p \models \varphi$ for all sufficiently large primes $p$ ;
$\mathrm{ACF}_p \models \varphi$ for infinitely many primes $p$ .

Proof

(1)⇔(2): $\C \models \mathrm{ACF}_0$ , which is complete. (2)⇒(3): $\mathrm{ACF}_0 \cup \{\neg\varphi\}$ has no model, so by compactness some finite subset has none; such a subset lies in $\mathrm{ACF} \cup \{p \cdot 1 \ne 0 \mid p < N\} \cup \{\neg\varphi\}$ for some $N$ , so every algebraically closed field of characteristic at least $N$ satisfies $\varphi$ . (3)⇒(4) is trivial. (4)⇒(2): if $\mathrm{ACF}_0 \not\models \varphi$ , completeness gives $\mathrm{ACF}_0 \models \neg\varphi$ , so by (2)⇒(3) $\mathrm{ACF}_p \models \neg\varphi$ for all large $p$ ; since each $\mathrm{ACF}_p$ is consistent, $\varphi$ fails in $\mathrm{ACF}_p$ for all large $p$ , contradicting (4).

∎

Theorem— Ax–Grothendieck theorem

Let $K$ be an algebraically closed field. Every injective polynomial map $f : K^n \to K^n$ is surjective.

Proof

Fix $n$ and a degree bound $d$ . "Every polynomial map $K^n \to K^n$ whose coordinates have degree at most $d$ and which is injective is surjective" is a single first-order sentence $\Phi_{n,d}$ : quantify universally over the finitely many coefficients $\bar c$ of $n$ polynomials of degree $\le d$ , and write

\forall \bar c\, \Big[ \forall \bar x\, \forall \bar y\, \big(f_{\bar c}(\bar x) = f_{\bar c}(\bar y) \to \bar x = \bar y\big) \;\to\; \forall \bar z\, \exists \bar x\; f_{\bar c}(\bar x) = \bar z \Big].

Step 1: $\Phi_{n,d}$ holds in $\overline{\mathbb F}_p$ for every prime $p$ . Let $f$ have coefficients in $\overline{\mathbb F}_p$ , be injective, and let $\bar z \in \overline{\mathbb F}_p^{\,n}$ . The finitely many coefficients of $f$ and coordinates of $\bar z$ are algebraic over $\mathbb F_p$ , so they generate a finite subfield $F$ . Then $f$ maps $F^n$ to $F^n$ and is injective there; as $F^n$ is finite, $f|_{F^n}$ is surjective, so $\bar z = f(\bar x)$ for some $\bar x \in F^n$ .

Step 2: transfer. As $\mathrm{ACF}_p$ is complete and $\overline{\mathbb F}_p \models \mathrm{ACF}_p$ , Step 1 gives $\mathrm{ACF}_p \models \Phi_{n,d}$ for every prime $p$ . By the Lefschetz principle $\mathrm{ACF}_0 \models \Phi_{n,d}$ . So every algebraically closed field, of any characteristic, satisfies $\Phi_{n,d}$ . Every polynomial map has some degree $d$ .

∎

The algebraic closure matters: over $\Q$ , the map $x \mapsto x^3$ is injective but $2$ is not a cube; over $\mathbb F_p(t)$ , the Frobenius $x \mapsto x^p$ is injective but $t$ is not a $p$ -th power.

Note

Ultraproducts give another view of the Lefschetz principle. If $U$ is a non-principal ultrafilter on the set of primes, then $\prod_p \overline{\mathbb F}_p / U$ is algebraically closed (Łoś, axiom by axiom) of characteristic $0$ (each sentence $q \cdot 1 \ne 0$ holds in all factors with $p \ne q$ ), and it has cardinality $2^{\aleph_0}$ . Since $\mathrm{ACF}_0$ is categorical in every uncountable cardinal (an algebraically closed field is determined by its characteristic and transcendence degree — Steinitz), this ultraproduct is isomorphic to $\C$ .

ExplanationH

Types and the Stone space

Types record how a new element could sit over a set of parameters. For $\mathrm{DLO}$ , quantifier elimination says a complete 1-type over $A \subseteq M$ is determined by which atomic formulas $x < a$ , $x = a$ , $a < x$ ( $a \in A$ ) it contains. Over $A = \Q$ inside $(\Q, <)$ , the complete 1-types are therefore:

$x = q$ for each $q \in \Q$ (realised in $\Q$ );
for each irrational $r$ , the type $\{q < x \mid q \in \Q,\ q < r\} \cup \{x < q \mid q \in \Q,\ q > r\}$ (not realised in $\Q$ , realised in $\R$ by $r$ );
for each $q \in \Q$ , a type $q^+$ "infinitely close to $q$ from above" ( $q < x$ and $x < r$ for all rationals $r > q$ ), and similarly $q^-$ ;
$+\infty$ ( $q < x$ for all $q$ ) and $-\infty$ .

So $|S_1(\Q)| = 2^{\aleph_0}$ . The types $q^\pm$ and $\pm\infty$ are realised in neither $\Q$ nor $\R$ . All of these types are realised in the ultrapower $\Q^\N/U$ , an elementary extension of $\Q$ by Łoś's theorem: $q^+$ by $[(q + 1/n)_n]$ , $q^-$ by $[(q - 1/n)_n]$ , $\pm\infty$ by $[(\pm n)_n]$ , and the cut of an irrational $r$ by the class of any sequence of rationals converging to $r$ .

The set $S_n(T)$ of complete $n$ -types of a complete theory $T$ (over $\emptyset$ ) carries the Stone topology, with basic open sets $[\varphi] = \{p \mid \varphi \in p\}$ . These sets are also closed (their complements are $[\neg\varphi]$ ), so $S_n(T)$ is totally disconnected and Hausdorff; and it is compact precisely because of the compactness theorem: a cover by basic open sets with no finite subcover would give a set of formulas $\{\neg\varphi_j\}$ , finitely satisfiable with $T$ but not satisfiable. A type is an isolated point iff it is generated by a single formula modulo $T$ .

Formal mathematicsF

Model theory in Lean and Mathlib

Mathlib has a substantial model theory library: languages, structures, terms and formulas whose bound variables are indexed by Fin n (FirstOrder.Language.BoundedFormula), satisfaction M ⊨ φ, theories, elementary embeddings and substructures, ultraproducts, compactness, Löwenheim–Skolem, Fraïssé limits, and the theories of orders and algebraically closed fields. Here is what this lesson proves and what it applies.

The key lemma of quantifier elimination, proved here, following the proof above case by case. The statement uses finite sets of parameters L and U:

dlo_elim_coreLean 4Proved here from basic factsFormally verified

/-- **The key lemma of quantifier elimination for DLO.** In a nonempty dense linear order
without endpoints, a point `x` strictly above every element of the finite set `L` and strictly
below every element of the finite set `U` exists **if and only if** every element of `L` is
below every element of `U`. So the formula `∃x (⋀ aᵢ < x ∧ ⋀ x < bⱼ)` is equivalent to the
quantifier-free formula `⋀ᵢⱼ aᵢ < bⱼ`.

The proof follows the lesson: if both sets are nonempty, density gives a point between
`max L < min U`; if one is empty, "no endpoints" gives a point beyond the other; if both are
empty, nonemptiness gives any point. -/
theorem dlo_elim_core {α : Type*} [LinearOrder α] [DenselyOrdered α] [NoMinOrder α]
    [NoMaxOrder α] [Nonempty α] (L U : Finset α) :
    (∃ x, (∀ a ∈ L, a < x) ∧ ∀ b ∈ U, x < b) ↔ ∀ a ∈ L, ∀ b ∈ U, a < b := by
  constructor
  · rintro ⟨x, hL, hU⟩ a ha b hb
    exact (hL a ha).trans (hU b hb)
  · intro h
    rcases L.eq_empty_or_nonempty with rfl | hL
    · rcases U.eq_empty_or_nonempty with rfl | hU
      · -- no constraints at all: any point will do
        obtain ⟨x⟩ := ‹Nonempty α›
        exact ⟨x, by simp, by simp⟩
      · -- only upper bounds: go below the least of them (no least element)
        obtain ⟨x, hx⟩ := exists_lt (U.min' hU)
        exact ⟨x, by simp, fun b hb => hx.trans_le (U.min'_le b hb)⟩
    · rcases U.eq_empty_or_nonempty with rfl | hU
      · -- only lower bounds: go above the greatest of them (no greatest element)
        obtain ⟨x, hx⟩ := exists_gt (L.max' hL)
        exact ⟨x, fun a ha => (L.le_max' a ha).trans_lt hx, by simp⟩
      · -- both: `max L < min U` by hypothesis, and density puts a point in between
        have hlt : L.max' hL < U.min' hU := h _ (L.max'_mem hL) _ (U.min'_mem hU)
        obtain ⟨x, hx₁, hx₂⟩ := exists_between hlt
        exact ⟨x, fun a ha => (L.le_max' a ha).trans_lt hx₁,
          fun b hb => hx₂.trans_le (U.min'_le b hb)⟩