A theory has quantifier elimination if every formula (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.

- 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.
- CF, the theory of -adically closed fields, in the Macintyre language—the field language expanded with unary predicates picking out that 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 .)
- 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 -ary relation for each -ary formula , to be interpreted as . This process is sometimes called **Morleyization**.

To prove quantifier elimination, it suffices to show that if is a conjunction of atomic and negated-atomic formulas, and is a single variable, then 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 not involving the variable can be pulled out of the quantifier. So we may assume that every conjunct actually mentions .
- If every atomic and negated-atomic formula is equivalent to a positive boolean combination of atomic and negated atomic formulas in a certain class , then it suffices to consider those which are conjunctions of formulas in . For example, in DLO, we can take to be , , and .
- If one of the conjuncts in is of the form , then is equivalent to the quantifier-free formula . So we may assume that there are no conjuncts of the form .

In the DLO case, one is left proving that is equivalent to a quantifier-free formula in , which is relatively easy.

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

- has quantifier elimination
- If and are models of , extending a common substructure , if is a quantifier-free formula, and if holds for some and , then holds for some .
- If and are models of , extending a common substructure , then the identity map on is a partial elementary map from to . Equivalently, has the same type in as in .

The second condition essentially says that if is an existential formula with one existential quantifier, then the truth of is determined by the quantifier-free type of . 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 determines its full type. Again, by a basic compactness argument, this implies that quantifier elimination holds.

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

If is model complete, then has quantifier elimination if and only if has the amalgamation property. A related fact, not quite a converse, is that if is the model companion of an inductive theory , and has quantifier elimination, then has the amalgamation property.

Quantifier elimination results can be used to show that a theory is complete, or to classify its completions. If has quantifier elimination, and is a sentence (a formula with no free variables), then is equivalent to a quantifier-free sentence. If there are no constants in the language, the only quantifier-free sentences are and , so is complete. In, say, ACF, quantifier-free sentences are boolean combinations of sentences of the form , for . 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 has quantifier elimination in a finite relational language, possibly with constants, then 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 has only finitely many 0-definable sets in each power of the home sort. By Ryll-Nardzewski, this implies that 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 has quantifier elimination, to show that 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 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 are (essentially) of the form , where is parameters. The set of realizations of this formula will be the roots of , which is either a finite set or the entire field, depending on whether is identically 0 or not.

Similarly, in RCF, one is reduced to showing that sets of the form are boolean combinations of points and intervals. The latter set is finite or all of , for reasons just explained. The former set turns out to be a finite boolean combination of intervals with endpoints at the zeros of , 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. ::: ::: :::