FOL : Using the same variable in successive quantifiers

Question

1. According to the definition 3.6 of A.G. Hamilton's "Logic for Mathematicians", it looks like the following is a well-formed formula of a first order language: $$ (\forall x_1)(\exists x_1)(x_1<x_1) $$ What is the interpretation of this? Since the last quantifier to be employed is the existential one, is this the same as $$ (\forall x_1)(\exists x_2)(x_2<x_2) $$ which is also the same as $$ (\exists x_2)(x_2<x_2) $$
2. In the same book, the Axiom Scheme of Replacement (one of the axioms for ZF) is written $$ (\forall x_1)(\exists! x_2)\mathscr{A}(x_1,x_2)\to(\forall x_3)(\exists x_4)(\forall x_5)(x_5\in x_4\leftrightarrow(\exists x_6)(x_6\in x_3\wedge\mathscr{A}(x_6,x_5))) $$ and the author says that "$\mathscr{A}(x_1,x_2)$ can be any well-formed formula in which $x_1$ and $x_2$ occur free (and in which, we may suppose without loss of generality, the quantifiers $(\forall x_5)$ and $(\forall x_6)$ do not appear)". Are these restrictions on the well-formed formula $\mathscr{A}(x_1,x_2)$ really necessary? Why do we want such restrictions? Does it have something to do with the kind of example in the part 1. above of this question?

Answer 1

To 1. : YES. A quantifier $\forall x$ acting on a formula $\varphi$ without $x$ free has "no effect"; i.e., in this case, $\forall x \varphi$ is equivalent to $\varphi$.

Thus, as you say, $(∀x_1)(∃x_1)(x_1 < x_1)$ is equivalent to $(∃x_1)(x_1 < x_1)$.

---

For 2. : the antecedent of the axiom $(∀x_1)(∃!x_2)A(x_1,x_2)$ simply states that the formula $A(x_1,x_2)$ "defines" a functional mapping : i.e. a binary relation $R(x,y)$ such that for any value of $x$ there exists exactly one value of $y$ satisfying the relation [e.g. "$x$ is son of $y$" satisfy the functionality condition, while "$x$ is father of $y$" does not].

This has nothing to do with the fact discussed in 1.

In principle, there is no reason to forbid an occurrence of $\forall x_5$ into $A(x_1,x_2)$; if so, this quantifier has as scope a sub-formula of $A(x_1,x_2)$ and thus has no effect outside it, and specifically it does not "interact" with the consequent of the axiom : $(∀x_3)(∃x_4)(∀x_5)(\ldots)$.

It's only a good "hygienical" practice to use distinct quantified variables in the same formula.

For the axiom specifically, we will "apply" it to formulae $A(x_1,x_2)$ satisfying the "functionality" condition expressed by the antecedent (if not, we do not care of them...).

For these formulae, the consequent licenses us to assert, for every set $x_3$, the existence of a set $x_4$ "collecting" all those sets $x_5$ that are "picked up" from $x_3$ by the formula $A$, i.e. such that $A(x_6,x_5)$ holds for $x_6 \in x_3$.

In order to "pick up" the $x_5$, we need that the functionality condition apply.