Sign up ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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?

share|cite|improve this question

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

share|cite|improve this answer
Could you suggest me a good book/paper/link where I can find information about the quantifier elimination? – Mary Star Nov 8 at 2:53
@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. – Joel David Hamkins Nov 8 at 2:55
Ok... Thank you!! :-) – Mary Star Nov 8 at 2:58
I saw in your profile that you have answered to questions about decidability. Could you maybe take a look at my question… ? – Mary Star Nov 8 at 3:01
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? – Joel David Hamkins Nov 8 at 3:19

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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