Why is quantifier elimination desirable for a given theory?

Question

We say that a given theory $T$ admits QE in a language $\mathcal{L}$ if for every $\mathcal{L}$-formula, there is an equivalent quantifier free $\mathcal{L}$-formula. That is for every $\mathcal{L}$-formula $\phi(x)$, where $x$ is a free variable, there is an $\mathcal{L}$-formula $\psi(x)$ so that $T\vDash\forall x\left(\phi(x)\iff\psi(x)\right)$.

The way I interpret this is that for any formula which $T$ implies, there is an equivalent q-free formula which $T$ imples. In other words, all the logical consequences of $T$ are expressible q-free.

My question is then:

Why is this advantageous? What is the benefit of having every logical consequence of a theory being q-free expressible?

Wikipedia says something along the lines that admitting QE makes the decidability problem simpler. But doesn't every theory admit QE in a sufficienctly complex language? Why is it desirable to be decidable with respect to a small (simpler) language?

Answer 1

You're quite right that we can "shoehorn in" quantifier elimination to any theory we want, by adding new predicates for all old formulas (this is called Morleyization if I recall correctly). So considered in a vacuum, there's nothing particularly special about quantifier elimination.

Quantifier elimination is useful in the context of theories whose quantifier-free fragments already have nice properties - that is, it forms half of an argument, with the other half being the analysis of the quantifier-free fragment of the theory in question to begin with. For a good example of this, look at the model-theoretic proof of the Nullstellensatz: quantifier elimination on its own doesn't do anything, but in combination with what we already know (e.g. per the fundamental theorem of algebra) about quantifier-free formulas in algebraically closed fields it gives us something nontrivial.

Answer 2

I'm going to write this answer from a model theoretic perspective and focus a bit more on why forcing quantifier elimination via Morleyization may not aid our understanding of the theory in question.

Given a particular theory $T$, one of the key steps in understanding $T$ is to understand the definable subsets of $T$. Having quantifier elimination in this context is extremely useful. Instead of looking at extremely complicated formulas you simply look at quantifier free formulas.

For example the theory of the random graph (in the language $L=\{E\}$) has quantifier elimination. So instead of attempting to understand an extremely complicated formula $\varphi(\overline{x})$, say a formula with a billion alternation of quantifiers, we can replace it with a quantifier free formula, which in this case simply ends up describing some finite graph. So checking to see if $\varphi(\overline{x})$ is satisfied by the tuple $\overline{a}$ from a model $M$ of the random graph simply boils down to checking whether $\overline{a}$ has the proper graph structure, essentially ignoring the billion quantifiers.

This example also leads nicely in to your question about forcing quantifier elimination via Morleyization. It can be done. But the quantifier free formulas obtained this way may not have a nice representation that aids in our understanding of the theory. For example, if we carry out Morleyzation for the theory here we obtain that there is some new relation symbol $R_{\varphi}((\overline{x}))$ such that for any tuple $\overline{a}$ from a model $M$ of the random graph $M\models\varphi(\overline{a})$, if and only if $M\models R_{\varphi}\overline{a}$. This doesn't really increase our understanding of how $\varphi$ behaves or how to evaluate it.