Comparing approaches to managing free and bound variables. Corrections:
I originally said $\varphi(x, w_1 \cdots w_n, a)$ was a closed well-formed formula. It is not. I meant to say that within $\varphi$ the only free variables come from $x, w_1 \cdots w_n, a$, i.e. $\text{FV}(\varphi) \subset \{x, w_1 \cdots w_n, a\}$.

Comparing approaches to managing free and bound variables.
What are the different approaches to managing free and bound variables in well-formed formulas? Are there any references that explicitly compare multiple ways of doing it and talk about their advantages and disadvantages?

For example, here is Z(F)(C)'s axiom schema of specification as presented by Wikipedia but with all variables made lowercase and some minor notational changes.
$$ \forall w_1\cdots w_n \mathop. \forall a \mathop. \exists b \mathop. \forall x \mathop. (x \in b) \leftrightarrow (x \in a \land \varphi(x_1, w_1 \cdots w_n, a)) $$
Note that all the variable symbols are bound.
In the convention used in the article, $\varphi$ is a well-formed formula. $\varphi(x_1, w_1 \cdots w_n, a)$ is a well-formed formula and the fact that $b$ does not appear in $(x_1, w_1 \cdots w_n, a) $ is significant. The fact that $b$ does not occur means that $b$ does not occur free in $\varphi$. I'm not sure how to define $\varphi(\vec{v})$ for an arbitrary $\vec{v}$ in this notation ... I usually think of it as a way of declaring dependencies in some sense where the exact interpretation depends on the context.
I think there are some technical advantages when defining syntax to making bound and free variable symbols disjoint. I didn't make up the idea of separating free and bound variables, but I don't remember where I saw it.
Let a lowercase Latin letter be a bound variable symbol and an uppercase Latin letter be a free variable symbol. Let $\psi[M:=\chi]$ be a capture-avoiding substitution replacing $M$ with $\chi$ in the well-formed formula $\psi$.
Using this convention, the above formula can be written as follows.
$$ \exists b \mathop. \forall x \mathop. (x \in b) \leftrightarrow (x \in A \land \varphi[X:=x]) $$
In this case, $\varphi$ is an ordinary well-formed formula with no restrictions placed on it. $A$ might occur in $\varphi$ or might not. $X$ might occur in $\varphi$ or might not. By virtue of being well-formed $b$ cannot occur free in $\varphi$ since it is inherently a bound variable. It is a little weird, though, that the names of free variables in $\varphi$ are not irrelevant; $X$ and $A$ both have special meanings because of the exact phrasing of the axiom schema.
So, in this one particular case, using a distinct collection of symbols for free and bound variables seems to simplify part of my task in defining an axiom schema, but it may not be more convenient in general.
 A: "I think there are some technical advantages when defining syntax to making bound and free variable symbols disjoint. I didn't make up the idea of separating free and bound variables, but I don't remember where I saw it." The device of using different letters for bound variables [i.e. variables which serve to bind quantifier prefixes to places in simple or complex predicates] and for free variables [expressions whose prime use is as parameters/dummy names/"arbitrary" names, however you prefer to put it] is there in Gentzen's original 1930s natural deduction investigations, and then again in Prawitz's 1965 classic book. It is taken up in some later influential logic textbooks, beginning with those by Lemmon and Thomason.
Depending exactly how you set things up, the device -- inter alia -- enables you avoid fussing about unintended capturing of variables. But perhaps the main positive reason for adopting the device is not technical but [in a broad sense] philosophical or conceptual: it cleaves to the very good Fregean principle of perspicuously marking in syntax  important differences of semantic role.
