Does quantifier elimination imply decidability?

Question

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 ii due to Q.E.

Answer 1

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