Restrictions on universal specification (in first-order logic)? I'm currently working my way through the details of first-order logic (using Suppes' Introduction to Logic), and I have a question about universal specification (US) (aka universal instantiation or elimination).  Specifically, my question has to do with the choosing of a name for the 'ambiguous object' that is used to replace the dropped universally quantified variable (in Suppes' text, he uses the nomenclature 'ambiguous object' when applying either US or ES).  Even more specifically, my question is what, if any, restriction applies to choosing of names of ambiguous objects when dropping / replacing multiple universally quantified variables.
For example, I have no trouble in grappling with an application of US in which the sentence contains but a single quantified variable.  For example, given the following sentence, where $P$ is a 1-place predicate: $(\forall x)(Px)$
And after applying US, choosing $\alpha$ as the ambiguous object (the thing being instantiated), we get: $P\alpha$.  This makes complete sense to me.
But what if we have the following sentence (in which $T$ is a 2-place predicate): $(\forall x)(\forall y)(\forall z)((xTy \bigwedge yTz) \to xTz)$
It's unclear to me if the following application of US is permitted or not:
$((\alpha T\alpha \bigwedge \alpha T\alpha) \to \alpha T\alpha)$
In Suppes' text, I have not come across an example in which an application of US such as this is used.  However, I also cannot find mention of any sort of restriction on US that would not permit this.  Another way to articulate my question is, given the application of US on just $x$, we get the following:
$(\forall y)(\forall z)((\alpha Ty \bigwedge yTz) \to \alpha Tz)$
Is there any such restriction on US that would prevent its application on $y$ such that $\alpha$ cannot legally be used as the object being instantiated?  (For what it's worth, I do understand that $\alpha$ cannot be used if $y$ was existentially quantified, and we wanted to apply ES; I'm unclear if US has the same restriction.)
Thank you in advance for your time and help.
-Paul
 A: Short answer is no, there is no restriction on what you can instantiate a universal quantifier with: you can re-use a term that you have already used to instantiate a quantifier with previously. (The clue is in the name: a universal quantifier applies universally across the domain of quantification.)
A case to think through: Suppose we want to say that a relation $R$ holds between any objects picked from the domain (whether the same or different). We formalize this as $\forall x\forall yRxy$. Think how we would formally derive the evident entailment $\forall xRxx$ in Suppes's system. If we banned re-using the same parameter to instantiate the universals, we wouldn't be able to get there!
A: No, there is no such restriction. When using quantifiers we implicitly invoke some universal domain of discourse, so that
$$\forall x\ \forall y\ \forall z\ (xTy \wedge yTz)\rightarrow xTz$$
is shorthand for
$$\forall x\in U\ \forall y \in U\ \forall z \in U\ (xTy \wedge yTz)\rightarrow xTz$$
Now apply universal specification one quantifier at a time, to get first
$$ \forall y \in U\ \forall z \in U\ (\alpha Ty \wedge yTz)\rightarrow \alpha Tz$$
Now it may be clearer that we can specify $y$ and then $z$ to $\alpha$ as well, or the full sentence would have been false, simply by the fact that $\alpha \in U$. In cases where such restrictions as the one you ask for might apply, we'd have to say 
$$\forall x\ \forall y\ \forall z\ \  x \neq y \wedge x \neq z \wedge y \neq z\rightarrow \varphi(x,y,z)$$
