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.
Best Answer
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.