Consider a First order (FO) formula $\phi = \exists^*\forall^*\exists^* \psi$ where $\psi$ is quantifier free and function free (No n-ary functions, $n \geq 1$) matrix. I am searching for a formula (Example) in the above FO form such that the right most $\exists^*$ cannot be pulled out to the front of the given first oder formula $\phi$. In other words, there is no choice to pull the right most existential quantifier so that that the new formula be in the form of $\phi' = \exists^*\forall^*\psi$.
Consider a formula $\phi = \exists x \forall y \forall z \exists t, P(x,t) \rightarrow Q(y,z)$ and let us pull the right most $\exists t$. So, $\phi' = \exists x \exists t \forall y \forall z , P(x,t) \rightarrow Q(y,z)$. The question is whether $\phi $ and $\phi'$ equivalent? If Yes/No, then why ? What are the conditions in which we can pull the right most existential/universal quantifier so that get aligned in $\exists^*\forall^*\psi$ or $\forall^*\exists^*\psi $ form?
There are rules used to put a formula in prenex normal form that have to do with pulling out quantifiers. For example, $g \rightarrow (\forall x ~.~ f)$ is rewritten as $\forall x ~.~ g \rightarrow f$ and $(\forall x ~.~ f) \rightarrow g$ is rewritten as $\exists x ~.~ f \rightarrow g$.
(Correctness of these transformations depends on variable renaming, which is carried out before their application to guarantee that $x$ does not appear in $g$.)
The order in which the rewriting rules are applied is not fixed, so that expressions in prenex normal form with different prefixes may be derived from the same formula. These different expressions are equivalent, but some are more convenient than others when it comes to reasoning about them. (As a rule of thumb, you try to pull the existential quantifiers out first, so that your Skolem functions may be just Skolem constants.)
Consider, for example,
$$ \phi'' = (\forall x \forall t ~.~ P(x,t))) \rightarrow (\forall y \forall z ~.~ Q(y,z)) \enspace. $$
Using the two rewriting rules mentioned above, you can derive both your $\phi$ and your $\phi'$, which are therefore equivalent.