42.02.05 · mathematical-logic / model-theory

Quantifier Elimination and Model-Completeness

shipped3 tiersLean: none

Anchor (Master): Marker 2002 *Model Theory: An Introduction* (Springer GTM 217) Ch. 3 (quantifier elimination, the primitive-formula and back-and-forth tests, model-completeness and the Robinson test, model companions and model completions, existentially closed structures, the worked theories DLO, ACF as strongly minimal with the Tarski-Chevalley projection theorem, RCF and the Tarski-Seidenberg theorem, Presburger arithmetic); Chang and Keisler 1990 *Model Theory* 3e (North-Holland) Ch. 3, 5 (the QE tests, model-completeness, model companions); Hodges 1993 *Model Theory* (Cambridge) Ch. 7, 8 (quantifier elimination, the algebra of definable sets, existentially closed models and model companions); Tarski 1948 *A Decision Method for Elementary Algebra and Geometry* (RAND) and Marker, Messmer, Pillay 2006 *Model Theory of Fields* 2e (ASL Lecture Notes in Logic 5)

Intuition Beginner

The previous unit built worlds to order using compactness and diagrams. This unit asks a different question about a single theory: how complicated can a yes-or-no property be? The surprising answer for many important theories is "not complicated at all." Every property, however it is phrased, can be rewritten using only plain comparisons among the named objects, with no hidden search.

A property with a hidden search is one that says "there is some object such that..." To check it directly you would have to hunt through the whole world looking for a witness. Quantifier elimination is the promise that the hunt is never needed. Whatever the property, there is an equivalent way to state it that mentions only the objects you already named, joined by basic relations and the words "and," "or," and "not."

Take the ordered rationals. Ask: "between these two named points, is there a third point?" Phrased that way it asks you to find a witness. But the answer is settled by a single plain comparison: there is a point between them exactly when the two points are different. The buried "there is some object" has been traded for a comparison among the names you started with. That trade, carried out for every property at once, is quantifier elimination.

When a theory permits this trade, its describable regions become simple shapes — cut out by a handful of equations and inequalities rather than by a search. That simplicity is the structural reason such a theory is well-behaved: questions about it can be decided by plain computation, and its geometry stays tame.

Visual Beginner

The picture shows the one move this unit is about: a property stated with a hidden "there is some object" is traded for an equivalent statement using only comparisons among the points already named.

   BEFORE — a buried search
   "is there a point strictly between a and b ?"
        a -------?------- b
            (hunt for a witness)

   AFTER — a plain comparison, no search
   "a and b are different"
        a  ≠  b
            (just compare the names you have)

   WHAT A DESCRIBABLE REGION LOOKS LIKE AFTER THE TRADE

   a region of the line, before:  { x : there is y with ... }   (a search)
   the same region, after:        a < x  AND  x < b             (plain bounds)

       |----------(========)----------|
       a          region              b
       cut out by two comparisons, nothing hidden

phrasing	what it asks you to do	after elimination
"there is a point between a and b"	hunt for a witness	check a is different from b
"x lies in this region"	search for membership	check a few comparisons on x
"for every object, ..."	check all objects	a plain comparison among names

Read left to right: every hidden search is traded for a finite check on the points you already have.

Worked example Beginner

We take the ordered rationals — the fractions with their usual order — and show by hand that one property with a buried search can be rewritten with only comparisons. The property: "the point $x$ has something strictly below it and something strictly above it."

Step 1. Read the property as stated. It says two searches at once: there is a point below $x$ , and there is a point above $x$ . As written, each half asks you to go find a witness somewhere in the line.

Step 2. Look at the line itself. The ordered rationals run on forever in both directions: there is no smallest fraction and no largest fraction. So for any point $x$ you pick, a smaller one always exists and a larger one always exists.

Step 3. Trade the search for a verdict. Because the line has no ends, the first search always succeeds and the second search always succeeds. The property "something below and something above $x$ " is therefore true of every point. Its rewritten, search-free form is simply "always true" — the plainest quantifier-free statement there is.

Step 4. Try a property that is not automatic: "between the named points $a$ and $b$ , with $a < b$ , there is a third point $x$ ." Here the search asks for a point strictly between. The ordered rationals are dense, so whenever $a$ is below $b$ there is always room between them. The verdict: a between-point exists exactly when $a < b$ . Again the buried search became a plain comparison among the names.

What this tells us: in the ordered rationals, the answers to "is there a witness?" never depend on hunting. They depend only on plain comparisons among the points already named — sometimes the comparison is automatic, sometimes it is a single inequality. Carrying out this trade for every property is what it means for the theory to eliminate quantifiers.

Check your understanding Beginner

Formal definition Intermediate+

Fix a first-order language $L$ , the satisfaction relation $⊨$ , the embedding/elementary-embedding hierarchy of 42.02.01 pending, and the diagram machinery $Diag (M)$ , $Diag_{el} (M)$ of 42.02.02 pending. All theories below are consistent first-order $L$ -theories.

A theory $T$ admits quantifier elimination (QE) when for every $L$ -formula $φ (\overset{x}{ˉ})$ there is a quantifier-free $L$ -formula $ψ (\overset{x}{ˉ})$ with $T ⊨ \forall \overset{x}{ˉ} (φ (\overset{x}{ˉ}) \leftrightarrow ψ (\overset{x}{ˉ}))$ ^{[Marker Ch. 3]}. Geometrically, in any model $M ⊨ T$ the $L$ -definable subsets of $M^{n}$ are exactly the boolean combinations of atomic-formula sets; definable sets are as simple as the language can express. The reduction theorem cuts the work to one quantifier: $T$ has QE iff every primitive formula $\exists y (ρ_{1} \land \dots \land ρ_{k})$ , with each $ρ_{i}$ atomic or negated-atomic, is $T$ -equivalent to a quantifier-free formula. Eliminating a single existential over a conjunction of literals suffices, because arbitrary formulas reduce to this case by prenex normal form, distribution, and induction on quantifier depth.

The semantic test runs through embeddings. Call $T$ substructure-complete when $T \cup Diag (A)$ is complete for every $L$ -structure $A$ embeddable in a model of $T$ . The back-and-forth criterion: $T$ has QE iff $T$ is substructure-complete, equivalently iff for all models $M, N ⊨ T$ with a common substructure $A$ , every existential formula over $A$ realized in $M$ is realized in $N$ ^{[Hodges Ch. 7]}.

A theory $T$ is model-complete when every embedding $M ↪ N$ between models of $T$ is elementary, $M ⪯ N$ . Robinson's test gives three equivalents: $T$ is model-complete iff $T \cup Diag (M)$ is complete for every model $M ⊨ T$ , iff every $L$ -formula is $T$ -equivalent to an existential ( $Σ_{1}$ ) formula, iff every embedding of models preserves existential formulas downward ^{[Marker Ch. 3]}. QE implies model-completeness (quantifier-free preservation by any embedding lifts to all formulas once every formula is quantifier-free modulo $T$ ). A model-complete theory with a structure that embeds into every model is complete.

A model $M ⊨ T$ is existentially closed (e.c.) when every existential formula with parameters in $M$ solvable in some extension $N \supseteq M$ with $N ⊨ T$ is already solvable in $M$ . A model companion $T^{*}$ of $T$ is a theory whose models are exactly the e.c. models of $T$ ; it is the unique model-complete theory with the same universal consequences, and a model completion when in addition $T$ has amalgamation over substructures, in which case $T^{*}$ eliminates quantifiers relative to those substructures.

Counterexamples to common slips Intermediate+

"Model-completeness implies completeness." The theory $ACF$ of algebraically closed fields is model-complete but not complete: $ACF_{0}$ and $ACF_{p}$ disagree on $1 + \dots + 1 = 0$ . Completeness needs the extra input of a structure embeddable in every model — here, fixing the characteristic supplies a prime field that embeds everywhere.
"QE depends only on the theory, not the language." QE is language-sensitive. Presburger arithmetic $Th (N; +, 0, 1, <)$ does not eliminate quantifiers in ${+, 0, 1, <}$ — the formula $\exists y (x = y + y)$ defines the even numbers, not a quantifier-free set — but does eliminate quantifiers once the divisibility predicates $D_{n}$ are adjoined. Choosing the right language is part of proving QE.
"Every complete theory eliminates quantifiers." Completeness is far weaker. $Th (N; +, \cdot)$ is complete (it decides every sentence, vacuously, as the theory of a fixed structure) yet defines sets of every arithmetical complexity, so no quantifier-free defining formula exists for most of them. QE is a structural tameness property completeness alone does not supply.

Key theorem with proof Intermediate+

The signature result is Tarski's quantifier-elimination theorem for algebraically closed fields, with its geometric corollary that projections of constructible sets are constructible — the model-theoretic form of the Chevalley elimination theorem. It is the template every later QE theory follows: eliminate one existential from a system of polynomial conditions, then read off model-completeness, completeness, and decidability.

Theorem (Tarski; QE for ACF). The theory $ACF$ of algebraically closed fields admits quantifier elimination in the language of rings ${+, -, \cdot, 0, 1}$ ^{[Marker Ch. 3]}.

Proof. By the reduction theorem it suffices to eliminate one existential over a conjunction of literals. Over a field every atomic formula in the variables $x, \overset{y}{ˉ}$ is a polynomial equation $p (x, \overset{y}{ˉ}) = 0$ , and a negated atomic is $q (x, \overset{y}{ˉ}) \neq = 0$ ; conjoining the inequations into one via $q_{1} \dots q_{m} \neq = 0$ , a primitive formula becomes $$ \exists x,\Big( \textstyle\bigwedge_{i=1}^{n} p_i(x, \bar y) = 0 \ \wedge\ q(x, \bar y) \ne 0 \Big), $$ where each $p_{i}, q$ is a polynomial in $x$ with coefficients that are polynomials in $\overset{y}{ˉ}$ . Use the substructure-completeness criterion: let $M, N ⊨ ACF$ share a common subring $A$ (an integral domain), let $\overset{a}{ˉ}$ be a tuple from $A$ , and suppose the formula holds in $M$ of $\overset{a}{ˉ}$ . We must realize it in $N$ . The witness $b \in M$ satisfies $p_{i} (b, \overset{a}{ˉ}) = 0$ for all $i$ and $q (b, \overset{a}{ˉ}) \neq = 0$ .

If some $p_{i} (\cdot, \overset{a}{ˉ})$ is a nonzero polynomial, $b$ is algebraic over the fraction field $K = Frac (A)$ ; the embedding $K ↪ N$ extends to the algebraic closure of $K$ inside $N$ (every model of $ACF$ contains an algebraic closure of $K$ , and any two are $K$ -isomorphic), so a conjugate root $b^{'} \in N$ of the minimal data realizes the same equations and the inequation $q (b^{'}, \overset{a}{ˉ}) \neq = 0$ . If every $p_{i} (\cdot, \overset{a}{ˉ})$ is the zero polynomial, the equations are vacuous and we need $b^{'}$ with $q (b^{'}, \overset{a}{ˉ}) \neq = 0$ ; since $N$ is infinite and $q (\cdot, \overset{a}{ˉ})$ has finitely many roots, such $b^{'}$ exists. In both cases the existential formula is realized in $N$ , so by the back-and-forth criterion $ACF$ has QE. $□$

Corollary (Tarski-Chevalley; elimination = projection). In any $M ⊨ ACF$ the definable sets are exactly the constructible sets — boolean combinations of Zariski-closed sets. QE says the projection $π : M^{n + 1} \to M^{n}$ of a constructible set is constructible: the image $π (C)$ of the set defined by $θ (x, \overset{y}{ˉ})$ is defined by $\exists x θ (x, \overset{y}{ˉ})$ , which QE rewrites quantifier-free, hence constructible. The Nullstellensatz appears as the completeness/model-completeness face: a finite system of polynomial equations over a field $k$ has a common zero in the algebraic closure iff $1$ is not in the ideal it generates, the embedding $k ↪ \overset{ˉ}{k}$ being existential-formula-preserving by model-completeness ^{[Marker, Messmer, Pillay Ch. 2]} (cross-ref 04.02.07).

Bridge. Tarski's QE for $ACF$ is the foundational reason algebraic geometry's constructible sets are closed under projection: elimination of the existential quantifier is the projection of a constructible set, and this is exactly the Chevalley theorem read through logic. It builds toward the model-completeness and strong-minimality results below, where the same quantifier-free control of definable sets forces every one-variable definable set to be finite or cofinite, and it appears again in the categoricity theory of 42.02.06 pending, where strong minimality drives the uncountable categoricity of $ACF$ . The argument generalises the dense-order back-and-forth of 42.02.01 pending from "match points across a gap" to "match algebraic witnesses across an embedding," and putting these together, the substructure-completeness criterion of 42.02.02 pending is the bridge that turns a one-quantifier elimination into the full structural tameness of the theory. The central insight is that definable sets simple enough to be boolean combinations of atomic ones make the theory decidable, geometrically transparent, and model-complete all at once.

Exercises Intermediate+

Exercise 3 (medium, symbolic).

Prove that $DLO$ (dense linear orders without endpoints) admits quantifier elimination by eliminating the existential from a primitive formula $\exists y (ρ_{1} \land \dots \land ρ_{k})$ whose literals are order/equality comparisons of $y$ with parameters $x_{1}, \dots, x_{n}$ .

Hint

Each literal puts $y$ below, above, or equal to some $x_{i}$ . A consistent conjunction pins $y$ to an open interval or a point; density and no-endpoints decide when such a $y$ exists, by a quantifier-free condition on the $x_{i}$ .

Answer

Each literal is $y < x_{i}$ , $x_{i} < y$ , $y = x_{i}$ , or a negation, which over a linear order rewrites as one of $<, =, >$ . If any literal forces $y = x_{i}$ , substitute $x_{i}$ for $y$ throughout, dropping the quantifier and leaving a quantifier-free condition on the $x_{j}$ . Otherwise the conjunction asserts $L < y$ and $y < U$ where $L$ is the (possibly empty) set of lower parameters and $U$ the upper set; $\exists y$ holds iff every lower parameter is below every upper parameter, i.e. $⋀_{x_{i} \in L, x_{j} \in U} x_{i} < x_{j}$ (with the empty- $L$ or empty- $U$ cases handled by no-endpoints, where existence is automatic). Density supplies the interior witness whenever the bounds are consistent. The resulting condition is quantifier-free in the $x_{i}$ , so the primitive formula is eliminated; by the reduction theorem $DLO$ has QE. Rubric: full credit for the interval analysis, the quantifier-free bound-consistency condition, and explicit use of density and no-endpoints.

Exercise 4 (medium, symbolic).

Use model-completeness to deduce that $ACF_{p}$ is complete and decidable for each prime or zero characteristic $p$ .

Hint

The prime field of characteristic $p$ embeds into every model of $ACF_{p}$ . A model-complete theory with a structure embeddable in all models is complete; a complete recursively axiomatized theory is decidable.

Answer

$ACF$ has QE (Tarski), hence is model-complete. Fix $p$ : the prime field $F_{p}$ (or $Q$ when $p = 0$ ) embeds into every model of $ACF_{p}$ , and its image is determined uniquely. Given any two models $M, N ⊨ ACF_{p}$ , both receive the prime field $P$ ; by model-completeness $P \cap M$ and $P \cap N$ give elementary data, and the completeness criterion (model-complete plus a structure embeddable in all models) yields $M \equiv N$ , so $ACF_{p}$ is complete. Being recursively axiomatized (the field axioms, characteristic $p$ , and the schema "every degree- $n$ monic polynomial has a root") and complete, $ACF_{p}$ is decidable (42.01.10 pending). Rubric: full credit for the prime-field embedding, the model-complete-plus-embeddable completeness step, and the complete-plus-recursive decidability conclusion.

Exercise 5 (medium, symbolic).

State the Tarski-Seidenberg theorem and explain why it is the geometric content of quantifier elimination for real closed fields.

Hint

Semialgebraic sets are the $RCF$ -definable sets. A projection corresponds to prefixing an existential quantifier.

Answer

The Tarski-Seidenberg theorem states that the image of a semialgebraic set $S \subseteq R^{n + 1}$ under the coordinate projection $π : R^{n + 1} \to R^{n}$ is again semialgebraic. Semialgebraic sets are exactly the sets definable in $(R; +, \cdot, <)$ — finite boolean combinations of polynomial inequalities — so a set $S$ defined by $θ (x, \overset{y}{ˉ})$ has projection $π (S)$ defined by $\exists x θ (x, \overset{y}{ˉ})$ . Tarski's QE for $RCF$ rewrites $\exists x θ$ as a quantifier-free formula, which defines a semialgebraic set; thus projection preserves semialgebraicity precisely because the existential quantifier it introduces can be eliminated. The theorem is the $RCF$ analogue of Tarski-Chevalley for $ACF$ . Rubric: full credit for the projection-equals-existential statement, identifying semialgebraic with definable, and reading Tarski-Seidenberg off QE.

Exercise 6 (medium, symbolic).

Show that Presburger arithmetic $Th (N; +, 0, 1, <)$ does not eliminate quantifiers in the language ${+, 0, 1, <}$ , and name the expansion that restores QE.

Hint

Consider $\exists y (x = y + y)$ . Is the set it defines quantifier-free definable in ${+, 0, 1, <}$ ?

Answer

The formula $\exists y (x = y + y)$ defines the even numbers. A quantifier-free formula in ${+, 0, 1, <}$ is a boolean combination of equalities and inequalities between ${+, 0, 1}$ -terms; each such term is $x + c$ or a constant, so its solution set is a finite boolean combination of half-lines and points — an eventually-periodic-with-period-1 (hence cofinitely constant) subset of $N$ . The even numbers are periodic with period $2$ and neither finite nor cofinite, so no quantifier-free ${+, 0, 1, <}$ -formula defines them; QE fails in this language. Adjoining the divisibility predicates $D_{n} (x) \equiv$ " $n ∣ x$ " for each $n \geq 2$ restores QE: $\exists y (x = y + y)$ becomes $D_{2} (x)$ , and the general elimination handles bounded coset conditions. Rubric: full credit for the even-numbers witness, the periodicity obstruction in the base language, and naming the $D_{n}$ expansion.

Exercise 7 (hard, symbolic).

Prove Robinson's test: a theory $T$ is model-complete iff every $L$ -formula is $T$ -equivalent to an existential formula.

Hint

One direction: if every formula is existential modulo $T$ , an embedding preserves existential formulas upward and their negations (also existential modulo $T$ ) too, forcing elementarity. The converse builds, for a given $φ$ , an existential formula by a compactness argument over the class of models and their embeddings.

Answer

( $\Leftarrow$ ) Suppose every formula is $T$ -equivalent to an existential one, and let $M ↪ N$ be an embedding of models. Embeddings preserve existential formulas upward: if $M ⊨ \exists \overset{x}{ˉ} θ (\overset{x}{ˉ}, \overset{a}{ˉ})$ with $θ$ quantifier-free then a witness maps into $N$ , so $N ⊨ \exists \overset{x}{ˉ} θ (\overset{x}{ˉ}, \overset{a}{ˉ})$ . Applying this to an arbitrary $φ$ and to $\neg φ$ (both existential modulo $T$ ) gives $M ⊨ φ [\overset{a}{ˉ}] \Rightarrow N ⊨ φ [\overset{a}{ˉ}]$ and $M ⊨ \neg φ [\overset{a}{ˉ}] \Rightarrow N ⊨ \neg φ [\overset{a}{ˉ}]$ , so the equivalence holds in both directions and the embedding is elementary; $T$ is model-complete.

( $\Rightarrow$ ) Suppose $T$ is model-complete and fix $φ (\overset{x}{ˉ})$ . Let $Φ$ be the set of existential consequences of $φ$ modulo $T$ . Claim $T \cup Φ (\overset{c}{ˉ}) ⊨ φ (\overset{c}{ˉ})$ for new constants $\overset{c}{ˉ}$ ; granting this, compactness yields a finite conjunction $θ \in Φ$ with $T ⊨ θ \to φ$ , and $T ⊨ φ \to θ$ holds since $θ$ is a consequence, giving the existential equivalent $θ$ . For the claim, take $N ⊨ T \cup Φ (\overset{a}{ˉ})$ ; build a model $M ⊨ T \cup {φ (\overset{a}{ˉ})}$ with $⟨ \overset{a}{ˉ} ⟩_{N} ↪ M$ by checking $T \cup Diag (⟨ \overset{a}{ˉ} ⟩_{N}) \cup {φ (\overset{a}{ˉ})}$ is satisfiable (any finite part is realized, else its negation would be an existential consequence of $φ$ in $Φ$ failing in $N$ ). Model-completeness makes $N ↪ M$ elementary along the amalgam, so $N ⊨ φ (\overset{a}{ˉ})$ . Rubric: full credit for the upward-preservation elementarity argument and the compactness extraction of the existential equivalent via the diagram.

Exercise 8 (hard, symbolic).

Prove that $ACF$ is strongly minimal: every definable subset of a model $M ⊨ ACF$ in one free variable (with parameters) is finite or cofinite.

Hint

By QE the set is a boolean combination of zero sets of one-variable polynomials over the parameters. Each nonzero such polynomial has finitely many roots; the zero polynomial gives everything.

Answer

Let $D = {x \in M : M ⊨ φ (x, \overset{a}{ˉ})}$ be definable with parameters $\overset{a}{ˉ}$ . By QE, $φ (x, \overset{a}{ˉ})$ is equivalent to a quantifier-free formula, a boolean combination of atomic conditions $p_{j} (x, \overset{a}{ˉ}) = 0$ where each $p_{j} (\cdot, \overset{a}{ˉ})$ is a one-variable polynomial over the field generated by $\overset{a}{ˉ}$ . For each $j$ , the set ${x : p_{j} (x, \overset{a}{ˉ}) = 0}$ is finite (at most $de g p_{j}$ elements) if $p_{j} (\cdot, \overset{a}{ˉ})$ is a nonzero polynomial, and is all of $M$ if $p_{j} (\cdot, \overset{a}{ˉ})$ is identically zero. Finite sets and the whole set $M$ generate, under finite unions, intersections, and complements, exactly the boolean algebra of finite and cofinite subsets of $M$ (a finite set has cofinite complement; intersections and unions of finite/cofinite sets stay finite/cofinite). Hence $D$ , a boolean combination of such atomic sets, is finite or cofinite. As this holds uniformly across all models, $ACF$ is strongly minimal. Rubric: full credit for the QE reduction to polynomial zero sets, the finite-root bound, and the closure of finite/cofinite sets under boolean operations.

Advanced results Master

Quantifier elimination, model-completeness, and the existentially closed models organize five developments: the QE tests that certify the property from one-quantifier or back-and-forth data, the model-completeness layer with Robinson's test and the route to completeness, the model-companion theory locating QE theories as the e.c. closure of incomplete ones, and the four landmark theories — $DLO$ , $ACF$ , $RCF$ , and Presburger arithmetic — whose elimination delivers decidability and geometric tameness.

Theorem 1 (the QE tests). A theory $T$ has QE iff every primitive formula $\exists y ⋀_{i} ρ_{i}$ over literals is $T$ -equivalent to a quantifier-free formula, and iff $T$ is substructure-complete — $T \cup Diag (A)$ complete for every substructure $A$ of a model ^{[Marker Ch. 3]}. The back-and-forth form: for models $M, N$ sharing a substructure $A$ , every existential formula over $A$ realized in $M$ is realized in $N$ . The one-quantifier reduction localizes a global property to a single elimination step, and the substructure criterion converts it into an amalgamation problem over diagrams — the same diagram machinery of 42.02.02 pending read as a completeness demand on every expansion by a substructure's atomic data.

Theorem 2 (model-completeness and Robinson's test). $T$ is model-complete iff every embedding of models is elementary, iff $T \cup Diag (M)$ is complete for every model $M$ , iff every formula is $T$ -equivalent to an existential ( $Σ_{1}$ ) one ^{[Marker Ch. 3]}. QE implies model-completeness, the converse failing (model-complete theories may keep quantifiers, as the existential normal form is weaker than the quantifier-free one). A model-complete $T$ with a structure embeddable in every model is complete: any two models receive the common structure, whose elementary diagram they share by model-completeness, forcing elementary equivalence. This is the working route to the completeness of $ACF_{p}$ , $RCF$ , and $DLO$ — model-complete by QE, complete by an embeddable prime structure.

Theorem 3 (existentially closed models and model companions). For an inductive theory $T$ (preserved under unions of chains) every model embeds in an existentially closed model ^{[Hodges Ch. 8]}. The class of e.c. models is elementary iff $T$ has a model companion $T^{*}$ — the unique model-complete theory mutually model-consistent with $T$ (same universal consequences, each model of one embedding in a model of the other) — and $T^{*}$ is a model completion when $T$ has amalgamation over substructures, in which case $T^{*}$ eliminates quantifiers relative to the substructures of models of $T$ . The pattern recurs across algebra: $ACF$ is the model companion (indeed completion) of the theory of integral domains, $RCF$ of formally real ordered fields, $DCF_{0}$ of differential fields of characteristic $0$ ; the model companion is the "algebraically closed" hull in which existential algebra has all the solutions it consistently can.

Theorem 4 (ACF: QE, Chevalley, strong minimality, decidability). $ACF$ has QE in the ring language; the definable sets are the constructible sets, and the projection of a constructible set is constructible — the Tarski-Chevalley theorem, elimination read as projection ^{[Marker, Messmer, Pillay Ch. 2]}. Each $ACF_{p}$ is complete (prime field embeds everywhere) and decidable. $ACF$ is strongly minimal: every one-variable definable set is finite or cofinite, since by QE it is a boolean combination of polynomial zero sets; strong minimality supplies a dimension (algebraic-closure rank equal to transcendence degree) and is the engine of the uncountable categoricity of 42.02.06 pending. The Nullstellensatz is the model-completeness face: a polynomial system over a field has a common zero in the algebraic closure iff $1$ avoids the generated ideal, the field-to-closure embedding preserving existential formulas (cross-ref 04.02.07).

Theorem 5 (RCF and Presburger: Tarski's decidability). Tarski's theorem: $RCF$ , the theory of $(R; +, \cdot, <)$ , has QE in the ordered-ring language, so elementary algebra and geometry are decidable ^{[Tarski 1948]}. The definable sets are the semialgebraic sets and the Tarski-Seidenberg theorem is QE in geometric dress — projections of semialgebraic sets are semialgebraic. Presburger arithmetic $Th (N; +, <)$ has QE after adjoining the divisibility predicates $D_{n}$ , and is decidable; the integer order $Th (Z; +, <)$ behaves the same way, as do divisible torsion-free abelian groups (ordered $Q$ -vector spaces, QE in ${+, <}$ ) and atomless boolean algebras ( $ℵ_{0}$ -categorical, QE). Each elimination converts a recursively axiomatized complete theory into a decidable one (42.01.10 pending); $RCF$ 's order-theoretic tameness is abstracted by o-minimality (forward-ref 42.02.08 pending).

Synthesis. Quantifier elimination is the foundational reason a theory is tame, and putting these together it threads all five developments through one demand: definable sets are boolean combinations of atomic ones, so a buried existential is always a projection that lands back inside the definable algebra. This is exactly what Theorem 1's tests certify — the one-quantifier reduction and the substructure-completeness criterion are two faces of the single elimination step — and Theorem 2 shows the immediate dividend: QE generalises to model-completeness, where every embedding is elementary, and model-completeness plus an embeddable prime structure is dual to completeness, the unbounded "decides every sentence" collapsing to "one structure sits inside all." The model-companion theory of Theorem 3 is the central insight that incomplete algebraic theories acquire a quantifier-eliminating completion by passing to their existentially closed models; $ACF$ , $RCF$ , and $DCF_{0}$ are the same construction performed over domains, ordered fields, and differential fields, and this is exactly why algebraic closure, real closure, and differential closure are model-theoretic operations.

Theorems 4 and 5 are the payoff: the Tarski-Chevalley projection theorem and the Tarski-Seidenberg theorem are QE for $ACF$ and $RCF$ in geometric language, the bridge from logic to the geometry of constructible and semialgebraic sets, and the decidability of elementary algebra and geometry is QE feeding the decidability machinery of 42.01.10 pending. The strong minimality of $ACF$ generalises the finite/cofinite dichotomy into the dimension theory that the categoricity of 42.02.06 pending and the o-minimality of 42.02.08 pending erect their classifications upon — quantifier elimination is where geometric tameness, decidability, and structural classification all begin.

Full proof set Master

Proposition 1 (reduction to primitive formulas). A theory $T$ has QE iff every primitive formula $\exists y (ρ_{1} \land \dots \land ρ_{k})$ , each $ρ_{i}$ a literal, is $T$ -equivalent to a quantifier-free formula.

Proof. The forward direction is immediate. For the converse, prove by induction on the number of quantifiers that every formula is $T$ -equivalent to a quantifier-free one. A quantifier-free formula needs nothing. Given $φ$ , put its matrix in prenex form $Q_{1} z_{1} \dots Q_{m} z_{m} χ$ with $χ$ quantifier-free, and induct on the innermost quantifier. If it is $\exists z_{m} χ$ , write $χ$ in disjunctive normal form $⋁_{j} ⋀_{i} ρ_{ij}$ over literals; the existential distributes over the disjunction, $\exists z_{m} ⋁_{j} (\dots) \equiv ⋁_{j} \exists z_{m} ⋀_{i} ρ_{ij}$ , and each disjunct is a primitive formula, replaced by a quantifier-free equivalent by hypothesis. A universal innermost quantifier is $\neg\exists z_{m} \neg χ$ , reduced the same way. This removes one quantifier; the inductive hypothesis on the now-shorter prefix finishes. $□$

Proposition 2 (back-and-forth criterion for QE). $T$ has QE iff for all $M, N ⊨ T$ with a common substructure $A$ and every existential formula $\exists y θ (y, \overset{a}{ˉ})$ ( $θ$ quantifier-free, $\overset{a}{ˉ}$ from $A$ ) realized in $M$ , it is realized in $N$ .

Proof. ( $\Rightarrow$ ) If $T$ has QE, $\exists y θ (y, \overset{a}{ˉ})$ is $T$ -equivalent to a quantifier-free $ψ (\overset{a}{ˉ})$ ; an embedding preserves and reflects $ψ$ , so $M ⊨ ψ (\overset{a}{ˉ})$ iff $A ⊨ ψ (\overset{a}{ˉ})$ iff $N ⊨ ψ (\overset{a}{ˉ})$ , and realization transfers. ( $\Leftarrow$ ) By Proposition 1 it suffices to eliminate one existential $\exists y ⋀_{i} ρ_{i} (y, \overset{x}{ˉ})$ . Let $Δ (\overset{x}{ˉ})$ be the set of quantifier-free formulas $δ (\overset{x}{ˉ})$ with $T ⊨ \exists y ⋀_{i} ρ_{i} \to δ$ . A compactness argument over the back-and-forth hypothesis shows $T \cup Δ (\overset{a}{ˉ}) ⊨ \exists y ⋀_{i} ρ_{i} (y, \overset{a}{ˉ})$ for new constants $\overset{a}{ˉ}$ : any model $N ⊨ T \cup Δ (\overset{a}{ˉ})$ has a substructure $A = ⟨ \overset{a}{ˉ} ⟩$ embeddable, together with the realized type, into a model $M ⊨ T$ of $\exists y ⋀_{i} ρ_{i} (\overset{a}{ˉ})$ (otherwise some quantifier-free consequence lands in $Δ$ and fails in $N$ ), and the hypothesis transfers realization back to $N$ . Compactness extracts a finite quantifier-free $δ \in Δ$ with $T ⊨ \exists y ⋀_{i} ρ_{i} \leftrightarrow δ$ . $□$

Proposition 3 (QE implies model-completeness). If $T$ has QE then $T$ is model-complete.

Proof. Let $M ↪ N$ be an embedding of models of $T$ via $h$ , and let $φ (\overset{x}{ˉ})$ be any formula, $\overset{a}{ˉ}$ from $M$ . By QE there is quantifier-free $ψ$ with $T ⊨ φ \leftrightarrow ψ$ . Embeddings preserve and reflect quantifier-free formulas (42.02.01 pending): $M ⊨ ψ [\overset{a}{ˉ}]$ iff $N ⊨ ψ [h \overset{a}{ˉ}]$ . Composing the two $T$ -equivalences, $M ⊨ φ [\overset{a}{ˉ}]$ iff $N ⊨ φ [h \overset{a}{ˉ}]$ , so $h$ is elementary and $T$ is model-complete. $□$

Proposition 4 (model-complete + embeddable structure implies complete). If $T$ is model-complete and there is an $L$ -structure $A_{0}$ embedding into every model of $T$ , then $T$ is complete.

Proof. Let $M, N ⊨ T$ . Both receive embeddings $A_{0} ↪ M$ and $A_{0} ↪ N$ . By model-completeness each embedding is elementary, so $A_{0}$ 's image is an elementary substructure of each, giving $M ⊨ σ$ iff $A_{0} ⊨ σ$ iff $N ⊨ σ$ for every sentence $σ$ (read off the elementary embeddings at the empty tuple). Hence $M \equiv N$ . As $M, N$ were arbitrary models, $T$ decides every sentence, so $T$ is complete. $□$

Proposition 5 (QE for ACF, with the projection corollary). $ACF$ admits quantifier elimination in ${+, -, \cdot, 0, 1}$ ; consequently the definable sets in a model are the constructible sets and are closed under projection.

Proof. Apply Proposition 2. A primitive formula over the ring language is $\exists x (⋀_{i} p_{i} (x, \overset{y}{ˉ}) = 0 \land q (x, \overset{y}{ˉ}) \neq = 0)$ . Take $M, N ⊨ ACF$ sharing a subring $A$ , $\overset{a}{ˉ}$ from $A$ , with a witness $b \in M$ . If some $p_{i} (\cdot, \overset{a}{ˉ}) \neq = 0$ as a polynomial, $b$ is algebraic over $K = Frac (A)$ ; the algebraic closure of $K$ embeds $K$ -isomorphically into both $M$ and $N$ (uniqueness of algebraic closure), carrying $b$ to a witness $b^{'} \in N$ satisfying the same equations and $q (b^{'}, \overset{a}{ˉ}) \neq = 0$ . If all $p_{i} (\cdot, \overset{a}{ˉ}) = 0$ identically, the equations are vacuous and the infinite field $N$ contains a point off the finite zero set of $q (\cdot, \overset{a}{ˉ})$ . Either way the formula is realized in $N$ , so by Proposition 2 $ACF$ has QE. The definable sets are then boolean combinations of zero sets ${p = 0}$ (Zariski-closed), i.e. constructible; a projection $\exists x θ$ is QE-rewritten quantifier-free, hence constructible — the Tarski-Chevalley theorem. $□$

Proposition 6 (strong minimality of ACF). Every one-variable definable subset of a model $M ⊨ ACF$ , with parameters, is finite or cofinite.

Proof. By Proposition 5 the set is defined by a quantifier-free formula $ψ (x, \overset{a}{ˉ})$ , a boolean combination of atomic conditions $p_{j} (x, \overset{a}{ˉ}) = 0$ . Each atomic set ${x : p_{j} (x, \overset{a}{ˉ}) = 0}$ is finite (a nonzero one-variable polynomial has at most $de g p_{j}$ roots) or all of $M$ (if $p_{j} (\cdot, \overset{a}{ˉ}) \equiv 0$ ). The finite and cofinite subsets of $M$ form a boolean algebra: complements swap finite with cofinite, and finite unions and intersections of finite/cofinite sets stay finite/cofinite. The defined set is a boolean combination of members of this algebra, hence finite or cofinite. $□$

Connections Master

The compactness theorem and the method of diagrams 42.02.02 pending supplies the engine this unit specializes. The substructure-completeness criterion for QE is the demand that $T \cup Diag (A)$ be complete for every substructure $A$ , and Robinson's test for model-completeness is the demand that $T \cup Diag (M)$ be complete for every model — both are diagram-and-compactness conditions read off the consistency-to-embedding dictionary of that unit. The amalgamation arguments certifying QE are elementary-amalgamation instances over shared diagrams. That unit builds models with prescribed substructures; this unit characterizes the theories whose every embedding is thereby elementary.
Types and the omitting types theorem, co-produced as 42.02.03 pending, is the dual axis to quantifier elimination. QE says every formula is quantifier-free modulo $T$ , which collapses every complete type to its quantifier-free part — the isolated, principal types of that unit become the only types, and a QE theory's type spaces are governed by atomic data. The existentially closed models of this unit are exactly those realizing all consistent existential types over substructures, the realization side of the realize/omit dichotomy that unit develops.
Categoricity and Morley's theorem 42.02.06 pending, co-produced, takes the strong minimality of $ACF$ proved here as its central example. The finite/cofinite dichotomy of one-variable definable sets supplies the algebraic-closure dimension equal to transcendence degree, and Morley's theorem upgrades the resulting uncountable categoricity of $ACF$ into the general transfer of categoricity across uncountable cardinals; the QE that makes $ACF$ strongly minimal is the precondition the categoricity classification presupposes.
O-minimality and the tame topology of definable sets, co-produced as 42.02.08 pending, is the order-theoretic refinement of the $RCF$ quantifier elimination established here. Where strong minimality reads finiteness off the one-variable definable sets of $ACF$ , o-minimality reads finite-union-of-intervals-and-points off those of $RCF$ and its expansions; Tarski's QE and the Tarski-Seidenberg theorem of this unit are the base case on which the o-minimal structure theory and the cell-decomposition machinery of that unit are built.
The decision problem for first-order theories and Church's theorem 42.01.10 pending is where the decidability delivered by QE is situated. Each quantifier-eliminating theory of this unit — $DLO$ , $ACF$ , $RCF$ , Presburger arithmetic — is a recursively axiomatized complete theory, hence a decidable island in the sea of undecidability that unit charts; QE is the structural mechanism producing the quantifier-free defining formulas a decision procedure computes on.

Historical & philosophical context Master

Quantifier elimination as a method predates the model-theoretic vocabulary that frames it. Thoralf Skolem and C. H. Langford applied elimination of quantifiers to linear orders in the 1910s and 1920s, and Mojżesz Presburger's 1929 thesis proved the decidability of the additive theory of the integers by eliminating quantifiers after expanding the language with the congruence (divisibility) predicates — the first substantial decidability result obtained by the method ^{[Tarski 1948]}. Alfred Tarski, working through the 1930s and circulating the results in the RAND report eventually published in 1948 and revised in 1951, established quantifier elimination for the real ordered field and so the decidability of elementary algebra and geometry, identifying the definable sets with the semialgebraic sets; the projection theorem now bearing the names of Tarski and Abraham Seidenberg (whose 1954 paper gave an algebraic proof) is the geometric content of that elimination.

The abstraction from particular elimination procedures to the structural notions of model-completeness and model companions is due to Abraham Robinson in the 1950s, who recognized that the algebraists' "algebraically closed" and "real closed" were instances of a uniform model-theoretic phenomenon — existential closure — and proved the test for model-completeness through the diagram method. The reading of Tarski's elimination for algebraically closed fields as the Chevalley constructibility theorem, and of strong minimality as the source of the uncountable categoricity later organized by Michael Morley (1965) and Saharon Shelah, situated quantifier elimination as the foundation of the geometric model theory of fields developed by Angus Macintyre, Anand Pillay, and others ^{[Marker, Messmer, Pillay Ch. 2]}.

Bibliography Master

@book{marker2002modeltheory,
  author    = {Marker, David},
  title     = {Model Theory: An Introduction},
  series    = {Graduate Texts in Mathematics},
  volume    = {217},
  publisher = {Springer},
  year      = {2002}
}

@book{changkeisler1990,
  author    = {Chang, Chen Chung and Keisler, H. Jerome},
  title     = {Model Theory},
  edition   = {3},
  series    = {Studies in Logic and the Foundations of Mathematics},
  volume    = {73},
  publisher = {North-Holland},
  year      = {1990}
}

@book{hodges1993modeltheory,
  author    = {Hodges, Wilfrid},
  title     = {Model Theory},
  series    = {Encyclopedia of Mathematics and its Applications},
  volume    = {42},
  publisher = {Cambridge University Press},
  year      = {1993}
}

@book{hodges1997shorter,
  author    = {Hodges, Wilfrid},
  title     = {A Shorter Model Theory},
  publisher = {Cambridge University Press},
  year      = {1997}
}

@techreport{tarski1948decision,
  author      = {Tarski, Alfred},
  title       = {A Decision Method for Elementary Algebra and Geometry},
  institution = {RAND Corporation},
  number      = {R-109},
  year        = {1948},
  note        = {Second revised edition, University of California Press, 1951}
}

@book{markermessmerpillay2006,
  author    = {Marker, David and Messmer, Margit and Pillay, Anand},
  title     = {Model Theory of Fields},
  edition   = {2},
  series    = {Lecture Notes in Logic},
  volume    = {5},
  publisher = {Association for Symbolic Logic / Cambridge University Press},
  year      = {2006}
}

@phdthesis{presburger1929,
  author = {Presburger, Moj\.{z}esz},
  title  = {\"{U}ber die Vollst\"{a}ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt},
  school = {Sprawozdanie z I Kongresu Matematyk\'{o}w Kraj\'{o}w S\l owia\'{n}skich, Warsaw},
  year   = {1929}
}

@article{seidenberg1954,
  author  = {Seidenberg, Abraham},
  title   = {A new decision method for elementary algebra},
  journal = {Annals of Mathematics},
  volume  = {60},
  year    = {1954},
  pages   = {365--374}
}

@article{morley1965categoricity,
  author  = {Morley, Michael},
  title   = {Categoricity in power},
  journal = {Transactions of the American Mathematical Society},
  volume  = {114},
  year    = {1965},
  pages   = {514--538}
}

@article{robinson1956completetheories,
  author    = {Robinson, Abraham},
  title     = {Complete Theories},
  publisher = {North-Holland},
  year      = {1956}
}

Prerequisites

42.02.02

Tier anchors

beginner: Marker 2002 *Model Theory: An Introduction* (Springer GTM 217) §3.1 (quantifier elimination read informally as 'every yes-or-no question about a list of objects can be settled by a finite check that mentions no hidden objects — no 'there exists' and no 'for all' left to chase down'; the picture of a definable region of the plane being cut out by a handful of plain equations and inequalities rather than by a search; the dense-line example where 'is there something strictly between these two points?' becomes simply 'are the two points different?'); checking by hand that for the ordered rationals every property phrased with a buried 'there exists' can be rewritten with only comparisons among the named points
intermediate: Marker 2002 *Model Theory: An Introduction* §3.1-3.2 (a theory T admits quantifier elimination when every formula is T-equivalent to a quantifier-free one; the reduction to eliminating a single existential over a conjunction of literals, the primitive-formula test; the back-and-forth / substructure-completeness criterion via existentially closed models; model-completeness as the statement that every embedding between models is elementary, the Robinson test, and the implication QE ⟹ model-complete ⟹ (with a structure embedding into all models) complete; the worked theories DLO and ACF); Hodges 1997 *A Shorter Model Theory* (Cambridge) Ch. 7
master: Marker 2002 *Model Theory: An Introduction* (Springer GTM 217) Ch. 3 (quantifier elimination, the primitive-formula and back-and-forth tests, model-completeness and the Robinson test, model companions and model completions, existentially closed structures, the worked theories DLO, ACF as strongly minimal with the Tarski-Chevalley projection theorem, RCF and the Tarski-Seidenberg theorem, Presburger arithmetic); Chang and Keisler 1990 *Model Theory* 3e (North-Holland) Ch. 3, 5 (the QE tests, model-completeness, model companions); Hodges 1993 *Model Theory* (Cambridge) Ch. 7, 8 (quantifier elimination, the algebra of definable sets, existentially closed models and model companions); Tarski 1948 *A Decision Method for Elementary Algebra and Geometry* (RAND) and Marker, Messmer, Pillay 2006 *Model Theory of Fields* 2e (ASL Lecture Notes in Logic 5)

References

Marker, D. — Model Theory: An Introduction · Graduate Texts in Mathematics 217, Springer (2002), Chapter 3. A theory T in a language L has quantifier elimination (QE) if for every L-formula φ(x̄) there is a quantifier-free L-formula ψ(x̄) with T ⊨ ∀x̄ (φ ↔ ψ); geometrically the L-definable subsets of any model are exactly the boolean combinations of sets defined by atomic formulas. The reduction theorem: T has QE iff every primitive formula ∃y (ρ_1 ∧ … ∧ ρ_n), with each ρ_i an atomic or negated-atomic formula, is T-equivalent to a quantifier-free formula; one need only eliminate a single existential quantifier in front of a conjunction of literals. The substructure / back-and-forth criterion (Theorem 3.1.4): T has QE iff for all models M, N of T, every common substructure A ⊆ M, A ⊆ N, and every quantifier-free-satisfiable existential formula realized in M over A is realized in N over A — equivalently, T is 'substructure-complete', T together with the diagram of any substructure being complete. Model-completeness: T is model-complete iff whenever M ⊆ N are models of T the inclusion is elementary, M ≼ N. Robinson's test: T is model-complete iff every embedding A ⊆ M of models is existential-formula-preserving in the reverse direction, equivalently iff for every model M of T the theory T ∪ Diag(M) is complete, equivalently iff every formula is T-equivalent to an existential (Σ_1) formula. QE ⟹ model-complete (quantifier-free preservation upgrades to all formulas). A model-complete theory with a structure that embeds into every model is complete (the Robinson joint-embedding completeness criterion); more generally model-completeness plus the amalgamation/joint-embedding of a 'prime' model gives completeness. Existentially closed (e.c.) models: M is e.c. for a class K if every existential formula with parameters in M solvable in some extension N ⊇ M in K is already solvable in M; a model companion T* of T is a theory whose models are exactly the e.c. models of T (when it exists, it is the unique model-complete T* with the same universal consequences / same ∀∃-completions), and a model completion is a model companion T* such that T ∪ Diag(A) ∪ T* is complete for every substructure A of a model of T (T* eliminates quantifiers over T). Worked theories: DLO (dense linear orders without endpoints) has QE and is ℵ_0-categorical, the QE proved directly by the interval back-and-forth; ACF (algebraically closed fields) has QE in the ring language (Tarski; proof by eliminating ∃x from a system of polynomial equations and inequations via resultants / the fact that a nonconstant polynomial has a root), whence the Tarski-Chevalley theorem that the image of a constructible set under a projection (or any morphism) is constructible — elimination of quantifiers is exactly the projection of a constructible set being constructible; ACF is model-complete, the algebraic closure of the prime field embeds in every model so each ACF_p is complete and (being recursively axiomatized) decidable, and ACF is strongly minimal (every definable subset of a model in one variable is finite or cofinite), the Nullstellensatz appearing as the statement that a system of polynomial equations with no common zero in a field has 1 in the ideal it generates (cross-ref 04.02.07). Real closed fields RCF (Tarski 1948): the theory of (ℝ, +, ·, <, 0, 1) has QE in the ordered-ring language, hence elementary algebra and geometry are decidable; the definable sets are the semialgebraic sets and the Tarski-Seidenberg theorem is the QE statement that a projection of a semialgebraic set is semialgebraic. Presburger arithmetic Th(ℕ, +, 0, 1, <): QE after expanding the language by the family of divisibility-by-n predicates D_n (and constants), decidable; the integer version Th(ℤ, +, <) similarly. Other QE theories: divisible torsion-free abelian groups (= ordered Q-vector spaces, QE in +, <), and atomless boolean algebras (ℵ_0-categorical, QE after adding the predicate counting atoms below an element, here vacuous). QE delivers decidability for a recursively axiomatized complete theory (cross-ref 42.01.10) and is the structural source of model-theoretic tameness; o-minimality (forward-ref 42.02.08) is the order-theoretic refinement for RCF and its expansions.
Tarski, A. — A Decision Method for Elementary Algebra and Geometry · RAND Corporation R-109 (1948; 2nd revised edition 1951), prepared 1930-1948. Tarski's quantifier-elimination decision procedure for the first-order theory of real closed fields, equivalently the elementary theory of the ordered field of real numbers (ℝ, +, ·, −, 0, 1, <). The procedure transforms any formula of elementary algebra into an equivalent quantifier-free formula in the same variables by systematically eliminating existential quantifiers from systems of polynomial equalities and inequalities, using Sturm's theorem and the theory of subresultants to decide when a univariate polynomial has a real root in a prescribed sign configuration. Consequences: the theory of real closed fields is complete and decidable, so every sentence of elementary Euclidean geometry (formalized over the reals) is algorithmically decidable; the definable sets in (ℝ, +, ·, <) are precisely the semialgebraic sets (finite boolean combinations of solution sets of polynomial inequalities p(x̄) > 0), and the Tarski-Seidenberg theorem is the geometric content of QE: the image of a semialgebraic set under a polynomial map (in particular a coordinate projection ℝ^{n+1} → ℝ^n) is again semialgebraic. The decision procedure has nonelementary worst-case complexity in Tarski's original form; later work (Cohen, Collins's cylindrical algebraic decomposition, 1975) gave doubly-exponential procedures, and the existential theory of the reals sits in PSPACE. The same method, stripped of the order, proves QE for algebraically closed fields, and the order-theoretic abstraction of the real case is the theory of o-minimal structures (forward-ref 42.02.08).
Hodges, W. — Model Theory · Cambridge University Press (1993), Chapters 7-8. The systematic treatment of quantifier elimination, the algebra of definable sets, and existentially closed models. Develops QE via the primitive-formula reduction (eliminate ∃ over a conjunction of literals) and the back-and-forth / amalgamation criterion stated as substructure-completeness, with the model-theoretic test that T has QE iff for any two models M, N of T with a common substructure A and any quantifier-free type p over A realized in M, p ∪ {an existential formula} consistent with Diag(A) ∪ T is realized in N. Treats model-completeness through Robinson's test (T model-complete iff T ∪ Diag(M) is complete for every model M iff every formula is equivalent modulo T to an existential one), the chain characterization (T is model-complete iff it is preserved under unions of chains of models AND the reverse, every embedding elementary), and the relation QE ⟹ model-complete ⟹ (with a prime/embeddable model) complete. Existentially closed structures: for an inductive theory T (preserved under unions of chains), every model embeds in an e.c. model; the class of e.c. models is elementary iff T has a model companion T*, characterized as the unique model-complete theory mutually model-consistent with T (same ∀-consequences, every model of one embedding in a model of the other), and T* is a model completion when in addition T has the amalgamation property over substructures, in which case T* has QE relative to the substructures of models of T. Examples worked include DLO, ACF (the model completion of the theory of integral domains / fields), real closed fields as the model completion of formally real ordered fields, divisible ordered abelian groups, and atomless boolean algebras; the algebra of definable sets is identified with the boolean algebra generated by the atomic-formula sets, finite in the strongly minimal and o-minimal cases.
Marker, D., Messmer, M., and Pillay, A. — Model Theory of Fields · Association for Symbolic Logic, Lecture Notes in Logic 5, 2nd edition, Cambridge University Press / A K Peters (2006), Chapters 1-3. The model theory of algebraically closed and other fields organized around quantifier elimination and its geometric content. Proves QE for ACF in the language of rings by the resultant elimination (a single ∃x over polynomial equalities p_i(x, ȳ) = 0 and inequalities q_j(x, ȳ) ≠ 0 reduces to quantifier-free conditions on the coefficients via iterated resultants and the algebraic closure axioms guaranteeing roots), and reads off the Tarski-Chevalley theorem: a constructible set (boolean combination of Zariski-closed sets) has constructible image under a morphism of varieties, equivalently the projection of a constructible set is constructible — the elimination theorem of algebraic geometry. The Nullstellensatz is recovered as the completeness/QE statement (a system of polynomial equations over an algebraically closed field has a common zero iff 1 is not in the generated ideal, the model-theoretic proof using that ACF is the model completion of the theory of fields and the embedding of any field in its algebraic closure; cross-ref 04.02.07). ACF is strongly minimal: every definable subset of a model in one free variable is finite or cofinite, since by QE it is a boolean combination of zero sets of one-variable polynomials, each finite; strong minimality gives a well-defined Morley/algebraic-closure dimension equal to transcendence degree and underlies the categoricity of ACF in uncountable powers (cross-ref 42.02.06). The text develops differentially closed fields DCF_0 as the model companion of differential fields (QE in the differential-ring language) and separably/pseudo-algebraically closed fields as further worked model-complete theories, situating QE and model-completeness as the organizing tools of the subject.

Estimated time

beginner: 22m
intermediate: 56m
master: 94m