I am studying mathematical logic and metamathematics and I have encountered formalization of number theory as a formal system. There, the following abbreviation is used: $a<b$ stands for $\exists t(b=a+t')$ for some variable $t$. I am concerned with the part "for some variable $t$". As I understand it, for each variable $t$ the given formula can be abbreviated as $(a<b)_t$, which depends on the choice of variable $t$. Why are we allowed to neglect the bound variable? I suppose that the answer lies somehow in the intended interpretation that is independent of bound variable used. But how can this be motivated in metamathematics?
I hope I made my question clear and I would appreciate any suggestions and comments!
Edit: Kleene "Introduction to Metamathematics" 1971, page 187.
The short answer is that, the author is anticipating that all concepts that have been or will be defined on formulas in the entire text, will be independent of renaming bound variables. For example, the truth of a sentence, substitution of a term for a variable, inference rules in the logic, etc., etc. You can check in each and every case that the concept defined doesn't change if bound variables are renamed. If the author is really careful, they might prove this in some cases, but it gets tedious and most likely, it is just left to the reader to verify.
In logic, we are only interested in concepts that are invariant under the symmetry group of renaming bound variables in formulas, just like (for example) Euclidean geometry is only interested in concepts that are invariant under congruence.
Of course, one can artificially construct concepts like "this formula contains the symbol $t$" which will not be invariant if one renames the bound variable $t$ to $u$. But such concepts are not of interest to us in logic. That would be like saying in Euclidean geometry "this point has $x$-coordinate 0".