Can we move quantifiers $\forall,\exists$ to the front if there aren’t variable collisions

first-order-logiclogic

Let's say I have a formula $\phi$ in First Order Logic, which contains some existential and universal quantifiers quantifiers $\exists, \forall$.

Supposed that in $\phi$ there are no collisions in variables names.

Can we take all the quantifiers of $\phi$, move it on the left (in the same order that appears in $\phi$)?

Example:
$$\phi_1 = \forall x P(x )\rightarrow \exists y T(y) \\
\phi_2 = \forall x\exists y P(x )\rightarrow T(y) \\
\phi_1 \overset{?}{\equiv} \phi_2$$

Obviously, I'm interested in the general case, not in this one, which is shown just to express the question using an example

I looked this up on Google, and I found many material which talks about prenex normal form, which solves this problem using skolemization, however I can't find an answer to this direct question, and skolemization makes it valid for every instance of $\phi$ that I try it on (but obviously trying many times is not a valid proof )

Best Answer

The answer to your general question is very much "no", because moving a quantifier past a connective can change the quantifier. For instance, $\neg \forall x \phi(x)$ is equivalent to $\exists x \neg\phi(x)$ and in the vast majority of cases is not equivalent to $\forall x \neg \phi(x)$.