as a part of a model theory assignment I am asked to prove that if a theory T has quantiier elimination, then it can be axiomatized by sentences of the form $\forall\bar{x}\exists{y}\phi(\bar{x},y)$, where $\phi$ is a quantifier-free formula. I have a sketch for the solution, but I am not too sure about it. I would appreciate some feedback.
For each $\psi\in{T}$: If $\psi$ is quantifier free, it is trivial, as for example $T\vdash\psi\iff \forall{x}\exists{y}\psi$.
For a sentence of the form $Q_1x_1...Q_nx_n\phi(x_1,...x_n)$ where $\phi$ is quantifier free and $Q_i\in${$\forall, \exists$} for each $i\leq{n}$, I use the fact that if a theory has QE then it is model-complete, which implies each formula is T-equivalent to an existential formula.
Therefore, by induction on n: if n=1, i.e $\phi = \forall{x}\psi(x)$, there is some q.f $\psi'(x)$ such that $T\vdash\forall{x} (\psi(x)\iff\exists{y}\psi'(x,y))$, and so $\forall{x}\exists{y}\psi'(x,y)$ is a sentence of the desired form that works. For an existential quantifier, it's similar to the q.f case (we could just take $\forall{x}\exists{y}\psi(y)$ when the original sentence is $\exists{x}\psi(x)$...).
If we assume the claim is true for sentences of the form $Q_1x_1...Q_nx_n\phi(x_1,...x_n)$ for some $n\lt\omega$, and we look at a sentence $\psi$ of the form $\psi = Q_1x_1...Q_{n+1}x_{n+1}\phi(x_1,...x_{n+1})$, we may consider the formula $\phi(y) = Q_2x_1...Q_{n+1}x_{n}\phi(y,x_1,...x_{n+1})$ and repeat the process from the basis of the induction to get a sentence that satisfies the desired conditions.
This proof obviously isn't complete but it fleshes out my general idea - to use a known fact about model-complete theories to get an axiomatization of the desired form. Is this a correct direction? Is there anything I'm missing? I've never really done induction on number of quantifiers so I definitely might be missing something obscenely vital to the proof. Thanks!
I'm not sure I understand your argument... what does it mean for "the claim to be true for sentences of the form..."? "The claim" is not a statement about all sentences, it is a statement about an equivalence of theories. You seem to be showing each sentence in $T$ is equivalent under $T$ to a quantifier-free sentence, but that's clear from the get-go (we have quantifier elimination). And that doesn't work because just because a $\varphi\in T$ is equivalent mod $T$ to some $\psi$ doesn't mean we can replace $\varphi$ with $\psi$ in $T$ and get an equivalent theory... $T$ implies any consequence of $T$ is equivalent with $\varphi,$ no matter how weak.
However, observe that we have, for every quantifier-free formula $\varphi(\vec x,y)$, $$ T\vdash \forall \vec x(\psi_\varphi(\vec x)\leftrightarrow \exists y\varphi(\vec x, y))$$ for some quantifier-free $\psi_\varphi$ (this is just a special case of quantifier eliminiation). Furthermore, this statement of equivalence is itself logically equivalent to a $\forall \exists$ sentence.
Let $T'$ be the collection of all of these sentences, plus all of the quantifier-free consequences of $T.$ By the same inductive argument that shows it suffices to prove quantifier elimination for existential formulas, $T'$ has all the necessary equivalences to prove that any sentence is equivalent to the same quantifier-free sentence $T$ proves it is equivalent to. And then since $T'$ includes all the quantifier-free consequences of $T,$ it will prove any consenquences of $T.$ Thus $T'$ is a $\forall\exists$ theory equivalent to $T.$