A theory $T$ has quantifier elimination if every formula $\phi (x)$ (without parameters) is equivalent to a quantifier-free one (without parameters). This is a stronger condition than model completeness. It depends on the choice of the language–for example, RCF has quantifier elimination in the language of ordered rings, but not in the language of rings.

Quantifier elimination is a fundamental tool in model theory, because it allows one to get some control over definable sets. When analyzing a theory, quantifier elimination is usually (but not always) the first step.

Theories with Quantifier Elimination[]

ACF, the theory of algebraically closed fields, in the language of rings.
DLO, the theory of dense linear orders, in the language of ordered sets.
RCF, the theory of real closed fields, in the language of ordered rings.
$p$ CF, the theory of $p$ -adically closed fields, in the Macintyre language—the field language expanded with unary predicates $P_{n}$ picking out that $n$ th powers.
ACVF, the theory of algebraically closed valued fields (with non-trivial valuation), in the one-sorted language with the ring language and with a binary predicate for divisibility (that is, for the condition $val(x)\leq val(y)$ .)
ACVF in some specific two-sorted and three-sorted languages.
DCF, the theory of differentially closed fields of characteristic 0.
The Random Graph. More generally, any Fraïsse limit in a finite relational language. For example, the Henson triangle-free graph.
Ax-Kochen-Ershov examples…

Important non-examples:

ACFA
Pseudo-finite and PAC fields
RCF in the language of rings.

Any theory can be (trivially) made to have QE by a definitional expansion, by adding a new $n$ -ary relation $R_{\phi }$ for each $n$ -ary formula $\phi (x_{1},\ldots ,x_{n})$ , to be interpreted as $\phi$ . This process is sometimes called Morleyization.

Strategies and criteria for proving QE[]

To prove quantifier elimination, it suffices to show that if $\phi (x;y)$ is a conjunction of atomic and negated-atomic formulas, and $x$ is a single variable, then $\exists x:\phi (x;y)$ is equivalent to a quantifier-free formula. This strategy is useful in cases where there are few function symbols, like DLO. Certain optimizations can be made in this approach, for example:

Conjuncts in $\phi (x;y)$ not involving the variable $x$ can be pulled out of the quantifier. So we may assume that every conjunct actually mentions $x$ .
If every atomic and negated-atomic formula is equivalent to a positive boolean combination of atomic and negated atomic formulas in a certain class $\Delta$ , then it suffices to consider those $\phi (x;y)$ which are conjunctions of formulas in $\Delta$ . For example, in DLO, we can take $\Delta$ to be $x<y$ , $x>y$ , and $x=y$ .
If one of the conjuncts in $\phi (x;y)$ is of the form $x=y_{i}$ , then $\exists x:\phi (x;y)$ is equivalent to the quantifier-free formula $\phi (y_{i};y)$ . So we may assume that there are no conjuncts of the form $x=y_{i}$ .

In the DLO case, one is left proving that $\exists x:\bigwedge _{i}x<y_{i}\wedge \bigwedge _{j}x>z_{j}$ is equivalent to a quantifier-free formula in $y_{i},z_{j}$ , which is relatively easy.

There are also more semantic approaches to proving quantifier elimination. For example, the following conditions are equivalent:

$T$ has quantifier elimination
If $M$ and $N$ are models of $T$ , extending a common substructure $S$ , if $\phi (x;y)$ is a quantifier-free formula, and if $\phi (m;s)$ holds for some $m\in M$ and $s\in S$ , then $\phi (n;s)$ holds for some $n\in N$ .
If $M$ and $N$ are models of $T$ , extending a common substructure $S$ , then the identity map on $S$ is a partial elementary map from $M$ to $N$ . Equivalently, $S$ has the same type in $M$ as in $N$ .

The second condition essentially says that if $\psi (z)$ is an existential formula with one existential quantifier, then the truth of $\psi (s)$ is determined by the quantifier-free type of $s$ . By a simple compactness argument, this ensures that every existential formula with one quantified variable is equivalent to a quantifier-free formula. Iterating this yields full quantifier elimination.

The third condition essentially says that the quantifier-free type of an element of a model of $T$ determines its full type. Again, by a basic compactness argument, this implies that quantifier elimination holds.

If $T$ is a complete theory, quantifier elimination is equivalent to the following condition: for every model $M$ , if $S$ and $T$ are substructures of $M$ , and $f:S\to T$ is an isomorphism of structures, then there is an elementary extension $N$ of $M$ and an automorphism $\sigma$ of $N$ which extends $f$ . This condition is easy to check for ACF, if one believes in the existence of transcendence bases.

If $T$ is model complete, then $T$ has quantifier elimination if and only if $T_{\forall }$ has the amalgamation property. A related fact, not quite a converse, is that if $T$ is the model companion of an inductive theory $T'$ , and $T$ has quantifier elimination, then $T'$ has the amalgamation property.

Applications of Quantifier Elimination[]

Quantifier elimination results can be used to show that a theory $T$ is complete, or to classify its completions. If $T$ has quantifier elimination, and $\phi$ is a sentence (a formula with no free variables), then $\phi$ is equivalent to a quantifier-free sentence. If there are no constants in the language, the only quantifier-free sentences are $\top$ and $\bot$ , so $T$ is complete. In, say, ACF, quantifier-free sentences are boolean combinations of sentences of the form $n=m$ , for $n,m\in \mathbb {Z}$ . The truth of these sentences depends only on the characteristic, so models of ACF are classified up to elementary equivalence by their characteristic.

QE can also be used to see that a theory is countably categorical (via the Ryll-Nardzewski theorem). If a complete theory $T$ has quantifier elimination in a finite relational language, possibly with constants, then $T$ is countably categorical. The lack of function symbols ensures that there are only finitely many atomic formulas in any finite number of variables. There are only finitely many boolean combinations of these, so $T$ has only finitely many 0-definable sets in each power of the home sort. By Ryll-Nardzewski, this implies that $T$ is countably categorical.

Control over definable sets is also useful for proving that theories are strongly minimal, o-minimal, or C-minimal. If a theory $T$ has quantifier elimination, to show that $T$ is strongly minimal, it suffices to show that every subset of the home sort cut out by an atomic formula is finite or co-finite. Similarly, to show that $T$ is o-minimal, it suffices to show that every subset of the home sort cut out by an atomic formula is a disjoint union of points and intervals.

For example, to see that ACF is strongly minimal, note that the only atomic formulas in one variable $x$ are (essentially) of the form $P(x;a)=0$ , where $a$ is parameters. The set of realizations of this formula will be the roots of $P(x;a)=0$ , which is either a finite set or the entire field, depending on whether $P(X;a)$ is identically 0 or not.

Similarly, in RCF, one is reduced to showing that sets of the form $\{x\in R:P(x;a)>0\}$ $\{x\in R:P(x;a)=0\}$ are boolean combinations of points and intervals. The latter set is finite or all of $R$ , for reasons just explained. The former set turns out to be a finite boolean combination of intervals with endpoints at the zeros of $P(x;a)$ , essentially because the intermediate value theorem holds for polynomials in models of RCF. So o-minimality holds in RCF.

More generally, conditions like stability, NIP, and NSOP can be verified using quantifier elimination. Quantifier elimination often allows one to get a handle on types, and stability can be proven by counting types. For example, in DCF, types correspond to prime differential ideals, and there is some way to count these. Something similar happens in SCF. ::: ::: :::