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?
from Hot Weekly Questions - Mathematics Stack Exchange
Post a Comment