# Pull Existential Quantifier to front in a FO formula

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?

• Not very clear... Forgetting about the initial $\exists$, we can consider $\forall x \exists y (x=y)$. It is clearly not equiv to $\exists y \forall x (x=y)$. – Mauro ALLEGRANZA Oct 3 '18 at 13:15
• @MauroALLEGRANZA Thankyou for the response. For two quantifiers, it is intuitive and simple. But are there any rule for the pull and push of the n quantifiers. I have edited the question, as it was not clear. – Rituraj Singh Rathore Oct 3 '18 at 18:17
• @RiturajSinghRathore Just have the additional quantifiers be dummy quantifiers. Adding more quantifiers is never going to make things simpler ... – Noah Schweber Oct 3 '18 at 18:30

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$$.)
$$\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.