Quantifier elimination

Remarks

For sentences ($n = 0$) one allows the quantifier-free sentences $\top$ and $\bot$ when $L$ has no constant symbols. It suffices to treat formulas of the form $\exists y \, \chi(x_1, \dots, x_n, y)$ with $\chi$ a conjunction of atomic and negated atomic formulas.

Example: the theory of dense linear orders without endpoints, in the signature $\set{<}$, has quantifier elimination. For instance, $\exists y \, (x_1 < y \wedge y < x_2)$ is equivalent to $x_1 < x_2$ by density, and $\exists y \, (x_1 < y)$ is equivalent to $x_1 = x_1$ since there is no greatest element.

Non-example: the theory of $(\R, +, \cdot, 0, 1)$, without the order symbol, does not have quantifier elimination. The formula $\exists y \, (x = y \cdot y)$ defines $[0, \infty)$, which is infinite and co-infinite. A quantifier-free formula in $x$ is a Boolean combination of polynomial equations $p(x) = 0$, so it defines a finite or cofinite subset of $\R$. With the order symbol added, the theory has quantifier elimination; this is Tarski's theorem.