A theory {\displaystyle T} has quantifier elimination if every formula {\displaystyle \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[]

Important non-examples:

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

Strategies and criteria for proving QE[]

To prove quantifier elimination, it suffices to show that if {\displaystyle \phi (x;y)} is a conjunction of atomic and negated-atomic formulas, and {\displaystyle x} is a single variable, then {\displaystyle \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:

In the DLO case, one is left proving that {\displaystyle \exists x:\bigwedge _{i}x<y_{i}\wedge \bigwedge _{j}x>z_{j}} is equivalent to a quantifier-free formula in {\displaystyle 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:

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

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

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

Applications of Quantifier Elimination[]

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

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