Often in logic, you want to define a formula $\phi(x)$ which "says something about $x$". For example, $\phi(x)$ may say that $x$ is a prime. In order to form $\phi$, you may need internal bound variables, for example $\phi(x)$ may have the form $\phi(x) = \exists y \alpha(x,y)$.

Unfortunately, you cannot apply this formula $\phi(x)$ to the variable $y$, as this will create a collision with respect to the internal bound variable $y$. This is really a pain because you want to allow the substitution of any term $t$ to substitute for $x$, and the resulting formula $\phi(t)$ should express some property of $t$. But now you have to worry about whether the term $t$ contains the variable $y$ or not. You would really like $y$ to be a local variable, which is renamed in case the substituted term $t$ contains a copy of $y$.

An analogous situation in computer programming is local vs global namespaces for variables. In most programming languages, a function may have local variables. You can pass any argument, including variables, to the function, and not have to worry about collisions between the local variables and global variables. In the standard treatment of first-order logic, all of the variables are global variables.

Is there any way to define a formula $\phi(x)$, in such a way that any term may be substituted for $x$?