# An equivalence to quantifier elimination

So I am studying the theory of quantifer elimination and have come across the following equivalence. I am defining quantifier elimination as: a theory $$T$$ admits quantifier-elimination (QE) if every formula $$\phi$$ is equivalent to a quantifier-free one.

I then want to prove that $$T$$ admits QE if and only if for any quantifier-free formula $$\phi(x,y_1,y_2,...,y_n)$$ of $$L$$, there exists a quantifier-free formula $$\psi(y_1,...,y_n)$$ such that $$T \models (\forall y_1,...,y_n)(\psi \iff(\exists x)\phi)$$.

I have proved the forward direction I think:

Suppose $$T$$ admits QE, and suppose $$\phi(x,y_1,y_2,...,y_n)$$ is a quantifier-free formula. Consider $$\exists x\phi(x,y_1,y_2,...,y_n)$$. Then as $$T$$ admits QE, $$T \models (\forall y_1,...,y_n)(\psi \iff(\exists x)\phi)$$, where $$\psi$$ is quantifier free formula. I think this is simply by definitions. However, I do not know how to prove the converse, so any help would be hugely appreciated. Thank you.

First note that for any formula $$\phi(x)$$ we have that $$\forall x \phi(x)$$ and $$\neg \exists x \neg \phi(x)$$ are equivalent.

Let $$\zeta(y_1, \ldots, y_n)$$ be any formula. We prove by induction on the structure of $$\zeta$$ that it is equivalent to a quantifier-free formula (modulo $$T$$). By the above we may assume that the only quantifiers that appear in $$\zeta$$ are existential quantifiers. The base case, where $$\zeta$$ is atomic, is trivial. The induction step for the logical connectives ($$\wedge$$, $$\vee$$, $$\neg$$, $$\to$$, $$\bot$$) is also trivial. So we are left with the case where $$\zeta$$ is of the form $$\exists x \phi(x, y_1, \ldots, y_n)$$. By the induction hypothesis we may assume that $$\phi(x, y_1, \ldots, y_n)$$ is equivalent (modulo $$T$$) to a quantifier-free $$\phi'(x, y_1, \ldots, y_n)$$. Then by assumption there is quantifier-free $$\psi(y_1, \ldots, y_n)$$ that is equivalent (modulo $$T$$) to $$\exists x \phi'(x, y_1, \ldots, y_n)$$. Putting things together we get $$T \models \forall y_1 \ldots y_n(\psi(y_1, \ldots, y_n) \leftrightarrow \zeta(y_1, \ldots, y_n)),$$ and so we conclude that $$\zeta$$ is indeed equivalent to a quantifier-free formula (modulo $$T$$). This completes the induction and thus the proof.

• Thank you, this is great! Nov 17, 2020 at 11:43