Quantifier elimination vs decidability

Question

Quantifier elimination is used as a technique to get decidability (e.g. $Th( \mathbb{N}, +)$ ) of theories, but typically one has to go over to some expansion. Are there examples of theories which are decidable but there is (provably) no expansion which has (effective) QE?

Answer 1

The answer is no, because in fact every theory $T$ admits quantifier elimination in an expansion, over a theory $\bar T$ that is conservative over $T$. Furthermore, the quantifier elimination procedure in the expansion is computable (assuming the original language has an effective enumeration), regardless of whether $T$ is decidable or even computably axiomatizable.

The idea is simply to add new predicates to represent the old formulas, so that they become quantifier-free. Specifically, if $T$ is a theory in language $\cal L$, then for each formula $\varphi(\vec x)$ in ${\cal L}$ let us add a new predicate symbol $R_{\varphi}$ to form the language $\bar{\cal L}$. We then form the expansion theory $\bar T$ by augmenting the original theory $T$ with the additional axioms $$\forall\vec x\ \left(\varphi(\vec x)\iff R_{\varphi}(\vec x)\right).$$ It is manifest that any model of $T$ can be expanded to a model of $\bar T$ simply by interpreting the $R_\varphi$ according to their definitions, and so $\bar T$ is conservative over $T$. But meanwhile, $\bar T$ has quantifier elimination, because every formula $\bar\varphi$ in the language $\bar L$ can be translated back into an $\cal L$-formula $\varphi$, by expanding all the $R_\psi$ that arise in it according to their definitions, and this formula $\varphi$ is equivalent to $R_\varphi$ in $\bar T$, an atomic formula. Thus, we have quantifier-elimination in the expansion. Furthermore, the procedure $\bar\varphi\mapsto R_\varphi$ is effective, regardless of the decidability of $T$.