Is the order of four quantifiers in a predicate formula relevant? Is the formula:
$$\forall x \exists y \forall z \exists u (F(x) \lor G(y) \to F(z) \lor G(u))$$
Equivalent to formula:
$$\forall z \exists u \forall x \exists y (F(x) \lor G(y) \to F(z) \lor G(u))$$
?
I know that $\forall a \exists b$ is not the same as $\exists b \forall a$. But how about the above formulas? And why?
Thanks.
 A: It looks like you caused even more havoc than with $\forall a\exists b$ becoming $\exists b\forall a$. Yet, your formulae are equivalent!


*

*If $\forall w\,\neg G(w)$, we can simply drop the $G(y)$ and $G(u)$ parts, hence can also drop $\exists y$ and $\exists u$. So in effect we merely swapped two $\forall$, which is allowed.

*If $G(w)$ for some $w$, then both formulae are true because we can always pick $u=w$.

A: The statements are equivalent.
It's easy to see why by noting that they are, respectively, of the form
$$\forall x \exists y \forall z \exists u (P(x,y) \to Q(z,u))$$
and
$$\forall z \exists u \forall x \exists y (P(x,y) \to Q(z,u)).$$
(In this case $P$ and $Q$ are the same predicate, but even they were different, they would still be equivalent as I show below).
Since $z,u$ do not occurr in the the predicate $P(x,y)$, it's possible to distribute the quantifiers of $z$ and $u$ over it. Thus, getting, for instances from the first statement,
$$\forall x \exists y (P(x,y) \to \forall z \exists u (Q(z,u))).$$
By the same token this statement is equivalent to $$\forall x \exists y (P(x,y)) \to \forall z \exists u (Q(z,u)).$$
A similar process shows that the second given statement is also equivalence to this one.
I alluded to the 'why' in a semi-semantical/semi-syntatic way. If you want a different kind of proof, let me know what kind.
A: The order of quantification is irrelevant in this case because each entity is free in all but one atomic predicate, and each bounded in a different atomic predicate.
$$\forall x\; \exists y\; \forall z\; \exists u\; \big(F(x) \lor G(y) \to F(z) \lor G(u)\big)
\\ \equiv
\\\big(\forall x \; \neg F(x) \wedge \exists y\; \neg G(y)\big) \vee \forall z\; F(z) \lor \exists u\;G(u)
\\ \equiv
\\ \forall z\; \exists u\; \forall x\; \exists y\; (F(x) \lor G(y) \to F(z) \lor G(u))
$$
