Is $ \forall x \forall y P(x, y)$ equivalent to $\forall y \forall x P(x, y)$ Question
Is it the case that the statement $ \forall x \forall y P(x, y)$ is equivalent to the statement $\forall y \forall x P(x, y)$ ?
Thoughts
I know that if one of the quantifiers in the original statement was $\exists$, then it wouldn't be equivalent, but if both quantifiers were $\forall$ would this change whether or not the equivalence holds?
 A: Informal Explanation
Yes, they can be used interchangeably.
The easiest way to see this, is to think about everyday examples in English and to see how the quantifiers behave here.
For example:
“for every apple and for every orange, if I pick an apple and an orange, I will prefer the apple”
In regular English, this just says that I always prefer apples to oranges.
This is even easier to see in the special case where two distinct claims are made about the two items. This is the case because we are making two distinct claims that do not interact with one another.
For example: ”for all apples and for all oranges, it is the case that apples can be eaten and oranges are not purple.”
Your question is even true for $n$ variables. So it would apply if we introduced a third object, or a fourth, etc. Again, it is usually fairly intuitive to work out once you set aside the logic and think about constructing English sentences from a given sentence written using FO-Logic / Predicate Logic.
Informal Proof
I'm not sure whether or not you are interested in a proof, but I'll write an informal one based loosely on the principles used in the Fitch Proof System. The reason I am not doing this rigorously is to make it clear exactly what every step means in case you aren't familiar with the system.
Statement: $\forall x \forall y P(x,y)$

*

*Step 1: As this applies for all x, the sentence is true for an arbitrary constant which I will call $\lambda$.


*Step 2: So we know $\forall y P(\lambda, y)$ is true. Because, it's true for any value of x, it must be true when x is lambda.


*Step 3: This statement is true for any value of y, so I can just replace y with an arbitrary constant. Let's call this $\phi$.


*Step 4: Therefore, we now have the statement $P(\lambda, \phi)$. It should make sense that this is true, because we know already that $P(x,y)$ is true for any values of $x$ and $y$.


*Step 5: Since, the choice of $\lambda$ was arbitrary and we could've chosen any value of $x$. Then we know $\forall P(x,\phi)$ is true.


*Step 6: Since $\phi$ was also arbitrary and we could have chosen any value of $y$ instead, the statement in step 5 is true for any $y$. Hence, it is true that $\forall y \forall x P(x,y)$
And then we are done.
A: An intuitive account of this equivalence can be given over a sample domain (a set of numbers, for instance), while we ought to rely first and foremost on derivations. Here is one in axiomatic (Hilbert) style:
$1.\qquad\forall x\forall yP(x, y)\qquad\qquad\qquad\qquad\text{hypothesis}$
$2.\qquad\forall x\forall yP(x, y)\rightarrow\forall yP(x, y)\qquad\,\text{Axiom 4}$
$3.\qquad\forall yP(x, y)\qquad\qquad\qquad\qquad\quad\text{Modus ponens 1, 2}$
$4.\qquad\forall xP(x, y)\rightarrow P(x, y)\qquad\qquad\;\text{Axiom 4}$
$5.\qquad P(x, y)\qquad\qquad\qquad\qquad\qquad\text{Modus ponens 3, 4}$
$6.\qquad\forall xP(x, y)\qquad\qquad\qquad\qquad\quad\text{Generalisation from 5}$
$7.\qquad\forall y\forall xP(x, y)\qquad\qquad\qquad\qquad\text{Generalisation from 6}$
By symmetry, $\forall x\forall yP(x, y)$ is derived from $\forall y\forall xP(x, y)$ as well and we conclude
$$\forall x\forall yP(x, y)\leftrightarrow\forall y\forall xP(x, y)$$
Remark. Each axiomatic system with its axioms and inference rules just as stated should be applied in its entirety; nothing more and nothing less. In the system I've used here, each line (including hypothesis) is accepted as tautology. Thus, line 5 states that $P(x, y)$ is true for arbitrary $x$ and $y$. Hence, generalisation is not an illegitimate binding of a variable.
Axiom 4 of this system is $\forall x\phi(x)\rightarrow\phi(t)$ where $t$ is free for $x$ in $\phi$. Clearly, each variable is free for itself.
A: The informal proof by @FD_bfa is a bit confusing, because it introduces $\lambda$ and $\phi$ in the wrong order.  Here is a version of the proof that I think is clearer.
Suppose that $\forall x\forall yP(x,y)$ is true.  We want to prove that $\forall y\forall xP(x,y)$ is true, so let $\phi$ be an arbitrary object.  If we can prove $\forall xP(x,\phi)$, then, since $\phi$ is arbitrary, we will be able to conclude $\forall y \forall xP(x,y)$.  To prove $\forall xP(x,\phi)$, let $\lambda$ be an arbitrary object.  If we can prove $P(\lambda, \phi)$, then, since $\lambda$ is arbitrary, we will be able to conclude $\forall xP(x,\phi)$.  So our goal now is to prove $P(\lambda,\phi)$.
We started by assuming $\forall x\forall yP(x,y)$.  Since this statement starts with $\forall x$, we can plug in anything we want for $x$.  Plugging in $\lambda$ for $x$, we can conclude that $\forall yP(\lambda, y)$.  Similarly, we can now plug in $\phi$ for $y$ to get $P(\lambda, \phi)$.  Since this was our goal, we are done.
Of course, the proof of the implication in the other direction is similar.
