Take the 2-minute tour ×
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|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|improve this answer

Your Answer

 
discard

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.