I am looking for a reference to a textbook on first order logic which works out in detail how capture avoiding term for variable substitution can be defined on formulas up to change in bound variable.
That is, if $ \phi $ is a first order formula, $ t $ is a term and x a variable, if the variables in $ t $ do not occur bound in $ \phi $, $ \phi [t/x] $ can easily be defined so that it replaces each free occurrence of $ x $ in $ \phi$ with $ t $. If some of the variables in $ t $ occur bound in $ \phi $, they may become captured by quantifiers in $ \phi $. In this case, I would like $ \phi[t/x] $ to still be defined. The natural thing seems to be to change the name of the bound variables in $ \phi $ to ``fresh'' ones, and then make the substitution. The issue then it seems is defining equivalence up to change and bound variable and proving that substitution is well-defined operation on the classes independent of the choice of fresh variables.
Thank you very much for your time.