Understanding Universal Quantifiers (Order Matters) I realized I haven't really understood how universal quantifiers work even after doing "serious" mathematics for quite a while. In particular, when can we actually swap universal quantifiers?
For a more specific example, consider the statement of some theorem of the form:
For all $n \in \mathbb{N}$ and all sequence of topological space $\{ (X_i, \mathcal{T}_i)\}_{i = 1} ^n$, some property $P(n, \{ (X_i, \mathcal{T}_i) \}_{i = 1} ^n)$ is true.
Here it seems like we can not make sense of $\{ (X_i, \mathcal{T}_i)\}_{i = 1} ^n$ without letting $n \in \mathbb{N}$ be given first. However, is this not two universal statements and we should be able to swap the universal quantifiers? Now if the swapping is not allowed in this form, is there a way to restate the statement to allow the swapping of orders for the universal quantifiers?
 A: 
For all $n \in \mathbb{N}$ and all sequence of topological space $\{
(X_i, \mathcal{T}_i)\}_{i = 1} ^n$, some property $P(n, \{ (X_i,
\mathcal{T}_i) \}_{i = 1} ^n)$ is true.


Now if the
swapping is not allowed in this form, is there a way to restate the
statement to allow the swapping of orders for the universal
quantifiers?

$$\forall n\; \Big(n \in \mathbb{N}\implies\forall X{\in}S_1\;\forall\mathcal{T}{\in}S_2\;P\big(n, \big\langle (X_i,\mathcal{T}_i) \big\rangle_{i = 1} ^n\big)\Big);$$
in other words,
$$\forall n\:\, \forall X{\in}S_1\;\forall\mathcal{T}{\in}S_2 \;\Big(n \in \mathbb{N}\implies
P\big(n, \big\langle (X_i,\mathcal{T}_i) \big\rangle_{i = 1} ^n\big)\Big).$$
Alternatively,
$$\forall n\; \forall q\;\Big(n \in \mathbb{N}\;\land\;q \in \big\{\big\langle (X_i,\mathcal{T}_i) \big\rangle_{i = 1}^n\mid  X\in S_1,\;\mathcal{T}\in S_2   \big\} \implies 
\;P\big(n, q\big)\Big).$$
Explanation: the notational shorthand $$\forall y{\in}Y\;Q(y)$$ to mean $$\forall y\;\Big(y \in Y\implies Q(y)\Big)$$ obstructs freely "swapping" like quantifiers if there are dependencies among the sets associated with the quantified variables.
A: I believe we have the following:

*

*A $\forall$ statement can never be swapped with an adjacent $\exists$ statement.

*An $\exists$ statement can always be swapped with an adjacent $\exists$ statement, if notation allows this.

*A $\forall$ statement can similarly always be swapped with an adjacent $\forall$ statement, if notation allows this.

With "notation allows this" I mean statements that are not like "$\forall x\in\mathbb{R}\forall y\in\mathbb{R}_{>x} 2x<2y$": Here the second $\forall$ is not "independent" of the first (because $y$ comes from a set that depends on $x$), so notation does not allows us to swap them without thinking.
As Mariano Suárez-Álvarez states in the comments, we can often/always group adjacent $\forall$ respectively adjacent $\exists$ statements into one statement.
e.g. $\forall x\in\mathbb{R}\forall y\in\mathbb{R}_{>x}, 2x<2y$ can be written as $\forall x,y\in\mathbb{R}, x<y\Rightarrow 2x<2y$ or even as $\forall (x,y)\in\{(a,b)\in\mathbb{R}^2\colon a<b\}, 2x<2y$.
Similarly, $\forall x\in A, \forall y\in B_x, \dots$ can be re-grouped as $\forall (x,y)\in\cup_{a\in A}\{a\}\times B_a, \dots$, although this is quite ugly.
Note in particular that the obstruction to swapping the same quantifiers is purely notational. In essence, these can always be swapped.
A: The logic 101 view
In logic the way it's typically taught to mathematicians (and the way it's actually done in a lot of work on logic itself), a universal quantifier only introduces a variable. It doesn't give it a domain. So you don't write things like $\forall n \in \mathbb{N}, P(n)$, but $\forall n, n \in \mathbb{N} \Rightarrow P(n)$ (which is parsed as $\forall n, (n \in \mathbb{N} \Rightarrow P(n))$ — I'll generally leave out these extra parentheses in my answer). In this framework, $\forall n \in \mathbb{N}, P(n)$ is considered an abbreviated notation for $\forall n, n \in \mathbb{N} \Rightarrow P(n)$.
And so if you're quantifying over an integer $n$ and over a sequence of length $n$, you end up with the statement
$$
\forall n, n \in \mathbb{N} \Rightarrow \bigl(
\forall X, X \in \{(X_i, \mathcal{T}_i)_{i=1}^n\} \Rightarrow
P(X)
\bigr)
$$
The universal quantifiers are not adjacent, so you can't swap them using the quantifier commutation rule.
This is very limiting: even in simple cases like $\forall x \in \mathbb{R}, \forall y \in \mathbb{R}, P(x,y)$, you can't swap the quantifications over $x$ and $y$, since the expanded version is $\forall x, x \in \mathbb{R} \Rightarrow (\forall y, y \in \mathbb{R} \Rightarrow P(x,y))$ which is not the same thing as $\forall x, \forall y, x \in \mathbb{R} \Rightarrow (y \in \mathbb{R} \Rightarrow P(x,y))$. It's “obvious” that all of this is equivalent to $\forall (x,y) \in \mathbb{R}^2, P(x,y)$, but things in math are not obvious until proved, so how would we prove it?
The details of the proof would depend on a specific formulation of logic, and I won't go into all the details here. However, there is another important theorem, to add to the theorem “you can swap universal quantifiers”: you can lift a universal quantifier outside the right-hand side of an implication. That is,
$$
P_0 \Rightarrow \forall y, P_1(y)
\quad \text{ is equivalent to } \quad
\forall y, P_0 \Rightarrow P_1(y)
$$
where the variable $y$ can appear in $P_1(y)$, but not in $P_0$.
The reason $y$ may not appear $P_0$ is that in the left-hand side, $P_0$ is outside the scope of the $\forall y$ quantifier. It's a fundamental syntactic property that a variable cannot escape its scope. The scope is what gives a meaning to the variable.
Now we can tackle the simple two-variable example above and transform propositions into equivalent propositions:
$$
\begin{array}{ll}
\forall x \in \mathbb{R}, \forall y \in \mathbb{R}, P(x,y) \\
\forall x, x \in \mathbb{R} \Rightarrow \bigl( \forall y, y \in \mathbb{R} \Rightarrow P(x,y) \bigr) & \text{expanding notation} \\
\forall x, \forall y, x \in \mathbb{R} \Rightarrow (y \in \mathbb{R} \Rightarrow P(x, y)) & \text{by the forall/implication lifting theorem} \\
\forall y, \forall x, x \in \mathbb{R} \Rightarrow (y \in \mathbb{R} \Rightarrow P(x, y)) & \text{by the forall swapping theorem} \\
\forall y, \forall x, y \in \mathbb{R} \Rightarrow (x \in \mathbb{R} \Rightarrow P(x, y)) & \text{by propositional logic} \\
\forall y, y \in \mathbb{R} \Rightarrow \bigl( \forall x, x \in \mathbb{R} \Rightarrow P(x,y) \bigr) & \text{by the forall/implication lifting theorem} \\
\forall y \in \mathbb{R}, \forall x \in \mathbb{R}, P(x,y) & \text{contracting notation} \\
\end{array}
$$
Now let's go back to your example. What goes wrong if we try to apply the reasoning above to $\forall n \in \mathbb{N}, \forall X \in \{(X_i, \mathcal{T}_i)_{i=1}^n\}, P(X)$? Everything is fine until we get to
$$
\forall X, \forall n, X \in \{(X_i, \mathcal{T}_i)_{i=1}^n\} \Rightarrow \bigl( n \in \mathbb{N} \Rightarrow P(x, y) \bigr)
$$
Now we would like to apply the lifting theorem in the converse direction. But the property that we want to “de-lift” $\forall n$ under is $X \in \{(X_i, \mathcal{T}_i)_{i=1}^n\}$, in which $n$ appears. The theorem requires a predicate $P_0$ here where $n$ does not appear. So the lifting theorem does not apply.
Bonus: on universal quantification and implication
There's a notation that combines a universal quantifier with an adjacent implication. There's a theorem that says you can swap adjacent universal quantifiers. There's a theorem that says you can swap a universal quantifier with an adjacent implication. Is there some kind of more general concept where these would all be special cases of a general theorem?
Well, yes. Otherwise I wouldn't have presented things this way. In fact, I'm going to describe two generalizations.
A universal quantifier is a kind of implication from an infinite conjunction. That is, $\forall x, P(x)$ can be seen as the conjunction $\bigwedge_x P(x)$, where the conjunction is over all possible $x$. Now, in general, you can't expect infinite formulas to have all the same properties as finite formulas. But, at least when doing logic over a finite space, propositional logic will definitely apply. And there is a wide range of cases where theorems that apply to all finite models are true of infinite models as well (but I won't get into what this means precisely). Assuming the rules of propositional logic apply:

*

*Forall swap: $\left( \forall x, \forall y, P(x,y) \right) \Longleftrightarrow \left( \bigwedge_x \bigwedge_y P(x,y) \right) \Longleftrightarrow \left( \bigwedge_{x,y} P(x,y) \right) \Longleftrightarrow \left( \bigwedge_y \bigwedge_x P(x,y) \right) \Longleftrightarrow \left( \forall y, \forall x, P(x,y) \right)$ (by re-grouping the terms of the conjunction, since it's associative and commutative)

*Forall/implication lift: $\left( P0 \Rightarrow \forall y, P_1(y) \right) \Longleftrightarrow \left( P0 \Rightarrow \bigwedge_y, P_1(y) \right) \Longleftrightarrow \left( \bigwedge_y (P0 \Rightarrow P_1(y)) \right) \Longleftrightarrow \left( \forall y, P0 \Rightarrow P_1(y) \right)$ (using a distributivity law: $A \Rightarrow (B \wedge C)$ is equivalent to $(A \Rightarrow B) \wedge (A \Rightarrow C)$)

An implication is a kind of universal quantification. “A implies B” can be seen as “no matter how you prove A, B is true”. (But you do have to prove A somehow, otherwise you can't conclude that B is true.) In other words, $A \Rightarrow B$ is equivalent to $\forall \pi \in \mathscr{P}(A), B$ where $\mathscr{P}(A)$ is the class of all proofs of $A$. (Note that here, I'm treating the $\forall x \in S$ notation as primitive, rather than an abbreviation. More on this in the section about types below.) (A “class” is a generalization of a set; the details don't matter here.) So the forall/implication lifting theorem states that $\forall \pi_0 \in \mathscr{P(P0)}, \forall y, P_1(y)$ is equivalent to $\forall y, \forall \pi_0 \in \mathscr{P(P0)}, P_1(y)$ — and this is just a matter of swapping the adjacent universal quantifiers.
The typed view
Above, I presented the way foundational mathematics is traditionally done, with quantifiers applying to a variable. But that's not how day-to-day mathematics is done: we pretty much always write “for all $x$ in a given set”, not just “for all $x$”. Sometimes we don't bother writing the set explicitly, when it's obvious from the context or the notation: for example, when doing real analysis, we write or say “for all $x$” and it's implicit that $x$ is a real number. And we write or say “for all $n$” and it's implicit that $n$ is an integer, or even that it's a non-negative integer. But always, if we take the time to write things down precisely, we'll end up with $\forall x \in \mathbb{R}$ or $\forall n \in \mathbb{N}$.
Intuitively, every variable has a domain. Sometimes this domain is restricted. For example, in real analysis, we might want to say “for any nonzero real number $x$”, and we write $\forall x \in \mathbb{R}^*$. The variable $x$ has an “overall domain”, which is all the real numbers, and a specific domain for this particular proposition, which is the set of nonzero real numbers. Instead of $\forall x \in \mathbb{R}^*, P(x)$, we might write $\forall x \in \mathbb{R}, x \ne 0 \Rightarrow P(x)$.
This notion of overall domain can be formalized in typed logics. Typed logics are mostly taught to computer scientists, because they have a lot of connections with programming. But they're also of interest to logicians, and they explain how everyday mathematical logic works.
In a typed logic, every variable has a type. When a quantifier introduces a new variable, it needs to specify the type of this variable. Intuitively speaking, the type of a variable is the set from which it can be taken. (When you actually study the theory, a type is not necessarily a set — but that aspect is not important here.)
The notation for specifying the type of a variable is $x:T$ where $x$ is the variable and $T$ is the type. So, for example, a universal quantification is $\forall x:T, \ldots$. This is pretty much equivalent to the everyday mathematical notation $\forall x \in T, \ldots$ since for our purposes here, we can pretend that types are sets.
The statement in the question is:
$
\forall n : \mathbb{N},
\forall X : \{(X_i, \mathcal{T}_i)_{i=1}^n\},
P(X)
$
Notice how the type of $X$ uses the variable $n$. The technical term for this is a dependent type — a type where a variable appears.
In a type theory, it is a theorem that you can swap adjacent universal quantifiers, as long as their types are independent. That is,
$$
\left( \forall x:T, \forall y:U, P \right)
\quad \text{is equivalent to} \quad
\left( \forall y:U, \forall x:T, P \right)
$$
provided that $x$ does not appear in $U$ and $y$ does not appear in $T$. The reason for the independence requirement is that if, for example, $x$ appeared in $U$, then the right-hand formula would have $x$ outside the scope of the quantifier that introduces it. And a variable is defined by its scope. It's a syntax error to use a variable outside its scope. (Or, depending on exactly how you model variable scopes, if the variable name $x$ appears outside the scope that defines $x$, then the occurrence of $x$ outside the scope is a different variable, and using the same name for different variables is valid but confusing to the reader.)
In your example, the universal quantifier swap theorem does not apply since the type of $X$ depends on $n$.
I recommend reading up on type theory if you're interested in computer science or programming. If your focus is mathematics (and not specifically logic), type theory won't really help you (it doesn't particularly help with algebra, analysis, geometry, etc. outside of rare advanced intersectionality), but it does provide (in my opinion) better foundational intuition to many aspects of everyday mathematical reasoning than untyped logic.
Bonus: other quantifiers
You can swap adjacent existential quantifiers: $\exists x, \exists y, P(x,y)$ is equivalent to $\exists y, \exists x, P(x,y)$. This is true even with domains or types: $\exists x \in A, \exists y \in B, P(x,y)$ is equivalent to $\exists y \in B, \exists y \in B, P(x,y)$ — provided that $x$ doesn't appear in $B$ and $y$ doesn't appear in $A$ ($x$ and $y$ may not escape their respective scope).
A constraint on a universal quantifier is like an extra implication: $\forall x \in A, P(x)$ is equivalent to $\forall x, x \in A \Rightarrow P(x)$. A constraint on an existential quantifier is like an extra conclusion: $\exists x \in A, P(x)$ is equivalent to $\exists s, P(x) \wedge x \in A$. An existential quantifier is like an infinite disjunction: $\exists x, P(x)$ is like $\bigvee_x P(x)$.
It is not true in general that you can swap quantifiers. It's the case for the two common quantifiers ($\forall$ and $\exists$), but not for more “exotic” quantifiers. For example, some texts define $\exists!$ as the “exists-unique” quantifier: $\exists! x, P(x)$ means that $\exists x, P(x)$ and $\forall x, \forall y, (P(x) \wedge P(y)) \Rightarrow x = y$. The propositions $\exists!x, \exists!y, P(x,y)$ and $\exists!y, \exists!x, P(x,y)$ are not equivalent.
A: The correct general statement is: You can swap adjacent universal quantifiers, provided their domains of quantification are independent.  That is, a statement “$\forall x \in A,\ \forall y \in B, \varphi(x,y)$” is always equivalent to “$\forall y \in B, \forall x \in A, \varphi(x,y)$”.
But in your example, “for all $n \in \mathbb{N}$ and all sequences $\{X_i\}_{i=1}^n$…”, the domain of the second quantifier — sequences of spaces of length n — depends on the variable introduced by the second quantifier.  So, as you observe, you can’t swap these quantifiers — it’s not an instance of the general statement above.
You can always rephrase quantifiers in terms of quantification over fixed/independent domains; sometimes it’s useful, but sometimes it’s quite mathematically unnatural.  A quantification “$\forall x \in A, \varphi(x)$” is equivalent to “$\forall x,\, x \in A \Rightarrow \varphi(x)$” — and indeed, if you reduce mathematics formally to a first-order language such as set theory, then you have to write all universal quantifiers in this form, since standard first-order logic always quantifies over a single fixed domain.  Formally, “for every $n \in \mathbb{N}$” always becomes “for every $n$, if $n$ is a natural number then…”. You can also do this kind of rephrasing with subsets of an ambient set; for instance, “$\forall x \in \mathbb{R}_{\geq 0},\, \varphi(x)$” is equivalent to “$\forall x \in \mathbb{R},\ x \geq 0 \Rightarrow \varphi(x)$“.
This rephrasing lets you rewrite quantifiers into a swappable form.  For instance, “$\newcommand{\R}{\mathbb{R}}\forall x \in \R,\; \forall y \in \R_{\geq x}, \ldots$” can be rewritten as “$\forall x, y \in \R, y \geq x \Rightarrow \ldots$” and then swapped to “$\forall y, x \in \R, y \geq x \Rightarrow \ldots$” — and further if you want to “$\forall y \in \R,\; \forall x \in \R_{\leq y}, \ldots$”.  In an example like this, where the domain of the second quantifier was carved out of some fixed set by a condition involving the first variable, the resulting statement is just as mathematically reasonable as the original one — and in such cases, this kind of rewriting/swapping an be very fruitful.
However, in other cases, the result is very unnatural: for instance, you can swap “for every topological space $X$, and every $x \in X$, …“ to say “for every $x$, and every topological space $X$ containing $x$, …” — but this is very weird and one would never naturally write it: it leaves a long moment where $x$ is an arbitrary object, of a totally unspecified kind.  Such moments are an artefact of reducing mathematics to a fixed first-order language, but they’re alien to normal mathematical practice.  Quantifiers like these, which can only be swapped by breaking them open and prolonging that uncomfortable moment, are best left unswapped.
(I’ve discussed it just in terms of $\forall$, but the version for $\exists$ case is exactly parallel throughout.)
