An equivalence to quantifier elimination

Question

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.

Answer 1

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.