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?


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$.

  • $\begingroup$ Could you suggest me a good book/paper/link where I can find information about the quantifier elimination? $\endgroup$ – Mary Star Nov 8 '15 at 2:53
  • $\begingroup$ @MaryStar I would think that this is covered in any of the usual model theory texts, but I don't have any close at hand at the moment. $\endgroup$ – Joel David Hamkins Nov 8 '15 at 2:55
  • $\begingroup$ I saw in your profile that you have answered to questions about decidability. Could you maybe take a look at my question math.stackexchange.com/questions/1516207/… ? $\endgroup$ – Mary Star Nov 8 '15 at 3:01
  • $\begingroup$ I don't know what the "theory of algebraic differential equations" means exactly. This is a first-order theory? What is the language? It seems to me you have some experts over there helping you out, who are also unsure about what you mean. Perhaps you can focus your question more precisely? $\endgroup$ – Joel David Hamkins Nov 8 '15 at 3:19
  • $\begingroup$ The language is $\{+, \cdot , ', 0, 1, t\}$. The formulas in the theory is of the form $tx'=ax$, they are algebraic differential equations (algebraic means that the coefficients are polynomials). So, can we say that this theory in this language is the structure $$(F[t]; +, \cdot , ', 0, 1, t)$$ ? I will try to edit the question to make it more precisely. $\endgroup$ – Mary Star Nov 8 '15 at 3:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.