# Does quantifier elimination imply decidability?

I know in some simple cases of quantifier elimination that I have seen, one ends up seeing that the process of quantifier elimination resulted in being able to show decidability. Is this true in general? I read that algebraically closed fields are decidable and in a separate place admits elimination of quantifiers but I don't know if decidability of ACF is due to Q.E. Thanks

-
Indeed, adding new symbols to the language any theory can be conservatively expanded into one which admits quantifier elimination. This conservative expansion is sometimes sknown as Morleyization. Hence, since not every first-order theory is decidiable it follows that the answer to your question is "No". –  boumol Dec 16 '12 at 22:49
You may also find this PDF of interest. –  Brian M. Scott Dec 16 '12 at 22:56

Proving that a first-order theory $T$ admits quantifier-elimination is often a big step toward proving decidability, but it's not the whole story. Once you've proved quantifier-elimination, you know, in particular, that every sentence $S$ in the language of $T$ is equivalent to a quantifier-free sentence $S'$. That suggests the following decision pseudo-algorithm for $T$: Given, as input, a sentence $S$ (so you're supposed to decide whether $S$ is provable in $T$), find the equivalent quantifier-free $S'$ and check whether that's provable in $T$; because of the equivalence, $S$ will be provable in $T$ if and only if $S'$ is. There are two reasons why this pseudo-algorithm might not be a genuine algorithm, namely the words "find" and "check". Let me address them in turn.

To make the pseudo-algorithm into an algorithm, you need to be able to algorithimically compute $S'$ when $S$ is given. This is no problem if you're given a computable (or even just computably enumerable) axiomatization of $T$, because then you can just systematically search through all formal proofs from $T$ until you find one whose conclusion has the form $S\iff S'$ with $S'$ quantifier-free. (Often, there's no need for searching through proofs, because the argument that shows quantifier-elimination may already contain an algorithm converting $S$ to $S'$.) But for totally wild $T$, without a decent axiomatization, it's possible that every $S$ has an equivalent $S'$ but there's no algorithm to find an appropriate $S'$ when $S$ is given. Summary: You need effective quantifier-elimination, meaning that the quantifier-free formula whose existence is assured by quantifier-elimination can be algorithmically found.

Second, once you have the desired quantifier-free sentence $S'$, you need to algorithmically check whether it's provable in $T$. Again, this is no problem in nice cases, because there are usually very few possibilities for $S'$. Note that $S'$ can't contain any variables --- it has no free variables because it's a sentence, and it has no bound variables because it is quantifier-free. In many first-order languages, this drastically limits what $S'$ can be. For example, in the language of fields (constants 0 and 1, binary field operations, and equality), $S'$ has to be a propositional combination of equations between rational expressions built from 0 and 1. In such cases, deciding provability of $S'$ is usually trivial, but for totally wild $T$, there might be no algorithm for this task. Summary: You need a decision algorithm for provability in $T$ of quantifier-free sentences.

If you have quantifier-elimination plus the extra information in the summaries at the end of the preceding paragraphs, then the pseudo-algorithm becomes a genuine decision algorithm.

But without such extra information, quantifier-elimination might not do you any good at all. In fact, given any first-order theory $T$, you can embed it into a quantifier-eliminable theory $T^+$ by adding to the language new predicate symbols, one $n$-ary predicate $P_\phi$ for each formula $\phi(x_1,\dots,x_n)$, with axioms $P_\phi(x_1,\dots,x_n)\iff\phi(x_1,\dots,x_n)$. That makes $T^+$ trivially quantifier-eliminable, but it's no more decidable than the original $T$. (The construction of $T^+$ is sometimes called "Morleyizing" $T$. In addition to the objections some people have to "ize" verbs, this name for such a triviality could be considered an insult to Michael Morley.)

-
great , thank you. –  Jmaff Dec 16 '12 at 22:52
A little less heavy-handed (I think) method of forcing q.e. is by adding a Skolem function, which is called Skolemization. –  tomasz Dec 17 '12 at 8:24