Understanding Quantifier Elimination

Question

I am struggling to understand Quantifier Elimination as it is treated in Hodges' "A Shorter Model Theory". The relevant definitions are :

Definition: Take $K$ to be a class of $L$-structures, for $L$ a first-order language. An elimination set for $K$ is a set of formulas $\Phi \subseteq L$ such that for every formula $\phi (\bar{x}) \in L$ there is a formula $\phi^{*}(\bar{x}) \in \Phi$ which is a boolean combination of formulas in $\Phi$ and $\phi(\bar{x})$ is equivalent to $\phi^{*}(\bar{x})$ in every structure in K

Definition: Let $T$ be a first-order $L$ theory. $T$ has quantifier elimination if the set of quantifier-free formula in $L$ forms an elimination set for all models of $T$.

Hodges talks about a process where starting with a class $K$ of $L$-structures, a theory $T$ serving as a candidate for axiomatization of $K$, and a set of $L$-formula $\Phi$ that serves as a candidate for an elimination set for $K$. And we build up $T$ and $\Phi$ simultaneously, using the following theorem:

Theorem: Suppose that every atomic formula of $L$ is in $\Phi$, and for every formula $\theta(\bar{x}) \in L$ which is of the form $\exists y \bigwedge_{i < n} \psi_{i}(\bar{x}, y)$ with each $\psi_{i}$ in $\Phi$ or a negation of a formula in $\Phi$, there is a formula $\theta^{*}(\bar{x})$ of $L$ which

(i) is a boolean combination of formulas in $\Phi$ and,

(ii) is equivalent in every structure of $K$

Then $\Phi$ is an elimination set for $K$

But I am not sure what is meant specifically or intuitively. If someone could shed some light on this and help me understand what this process looks like or means, I would greatly appreciate it.

Answer 1

Suppose we have a class $K$ of models. That we have quantifier elimination for $K$ means that for every formula $\varphi(x)$ there is a quantifier-free formula $\psi(x,y)$ such that for every $M\in K$ we have $M\models \varphi(x)\leftrightarrow \psi(x,y)$ (where $x,y$ are tuples of finite length).

It does not, however, mean that the theory itself can be expressed without quantifiers, even if we assume that $K$ is an elementary class. This is not the case for the commonly known complete theories with quantifier elimination, such as $DLO_0$ (dense linear orderings without endpoints), $ACF_p$ (algebraically closed fields of characteristic $p$) or $RCF$ (real closed fields with $\leq$). A theory which has q.e. and is axiomatisable without quantifiers will likely be rather dull, though I don't feel like exploring how dull exactly it would be.

The process in the theorem is as follows:

1. We have a set of formulas $\Phi$ we want to show is an elimination set. This means that any first-order formula in $L$ is equivalent to a boolean combination of elements of $\Phi$.
2. Every first order formula comes from atomic formulas in a finite sequence of alternating two operations: taking a boolean combination and prefixing an existential quantifier. We can do induction with respect to complexity of formulas defined as the length of this finite sequence.
3. So, if $\Phi$ contains an atomic formula (base case of induction), and every boolean combination of formulas in $\Phi$ prefixed by an existential quantifier is equivalent to a boolean combination of formulas without said quantifier then by induction we have...?

Answer 2

The intuition is that, in a model with quantifier elimination, the definable sets are likely to be extremely simple.

The easiest example is the theory of dense linear orderings without endpoints. A set definable by a quantifier-free formula will consist of a finite union of individual points and intervals, by inspection of the formula. Because each model $M$ has quantifier elimination (in a signature with a constant for each element), every definable set will be of that simple form. If we do not add constants for elements, the quantifier-free formulas are all equivalent to $\top$ or to $\bot$, and so there are only two definable sets, $|M|$ and $\emptyset$. This also shows - syntactically - that the theory of dense linear orderings without endpoints is complete.

Quantifier elimination is also helpful for proving that theories are decidable. If the quantifier elimination procedure is effective - meaning there is a computable function mapping arbitrary formulas to quantifier-free equivalent formulas - this often gives a proof that the theory is decidable. This is because the function would have to map arbitrary sentences to equivalent quantifier-free sentences, and in many cases the truth of quantifier-free sentences can be decided algorithmically. This is one way to prove the decidability of the theory of the real numbers as an ordered field, for example: there is effective quantifier elimination, and truth of quantifier-free sentences can be decided algorithmically.