Substitution for bound variables in logic 
Let $$ be $(∀  (, , ))$. What is $[( +  + )/]$?

Clearly, if I substitute in $y = x + y + z$ then the issue will be that $x$ will be bound so we cannot directly substitute in.
How does substitution work in this case?
 A: You can directly substitute any term you want for any free variable of any formula. This may cause particular variables in the term to become bound, but that is a separate matter. So, for example, if I substitute $x$ for $y$ in $(\exists x)[x < y]$ I obtain $(\exists x)[x < x]$. Substitution is a purely syntactical operation given by a standard recursive definition. 
On the other hand, we often want to avoid causing the variables in the term that is being substituted from becoming bound. This restriction is necessary for various theorems about provability. But it is not a restriction on what we "can" substitute - it is a restriction on what we are "allowed to" substitute in particular circumstances.
The most careful treatment of this that I know of is in Enderton's logic book.  Enderton defines the word "substitutable" to mean that a term can be substituted into a particular free variable of a formula with no variable in the term becoming bound. This is not the same as "can be substituted" of course - perhaps Enderton could have said "safely substitutable".  The problem in the question and in my example above is that the term being substituted is not substitutable in Enderton's sense for the variable and formula at hand. 
One solution is to rename the quantified variables first. Enderton uses the idiosyncratic term "alphabetical variant", and proves a theorem that for each formula $\phi(y)$ and each term $t$ there is an alphabetical variant $\phi'(y)$ in which $t$ can be substituted for $y$ without any variable in $t$ becoming bound, and so that $\phi$ and $\phi'$ are equivalent. In the example above, one such alphabetical variant is $\phi'(y) \equiv (\exists z)(z< y)$.  (By the way, this is one reason why it is important to assume that a theory/language comes with an infinite collection of variables, while each term only mentions finitely many.) 
You can see one formal definition of an alphabetical variant in these lecture notes by Timothy Carlson, page 7.  The notes have a full treatment of substitution, following Enderton, beginning on page 5.
In many cases, authors will silently assume that, when a substitution is made, a suitable alphabetical variant is also chosen to avoid binding variables in the terms being substituted. However, if they want to be more precise or more pedantic, they will be more explicit about it. 
