In meta-math does the sequence matter for $\bf ∀x$?

Question

For example, if I have an axiom starting with $\bf ∀x∀x'\dots$ , would it still be an axiom if the only difference is that the sequence has changed to $\bf∀x'∀x\dots$?

Answer 1

If adjacent quantifiers of the same kind (both existential or both universal) are swapped, the result is a logically equivalent statement.

Beyond this little can be said. You may find discussions of pre-nex normal form helpful.

In most cases we do not say formally that one statement is an axiom just because it is a logical equivalent of a statement that is an axiom. It is possible however that in one particular circumstance the swapping of two universal quantifiers, just as outlined in the Question, would meet the criterion of being an axiom precisely when the version before swapping quantifiers is an axiom.

That is the case of the Scheme of Generalization of Axioms, often abbreviated AxGen, a provision of many formalizations of predicate calculus:

If $\varphi$ is an axiom of the predicate calculus, then $\forall x \; \varphi$ is an axiom also.

This axiom scheme (as it is not a single axiom, but a rule that allows us to generate many axioms from other axioms) will let us introduce zero or many universal quantifiers onto another axiom of the predicate calculus.

In this specific case (when $\varphi$ is an axiom of the predicate calculus) it is true that $\forall x \forall x'\; \varphi$ and $\forall x' \forall x \; \varphi$ are equally to be considered axioms, and with equal justifications.