Bound variable
= Bound variable
A variable occurrence in a <first-order formula> is bound when it lies in the scope of a <quantifier> binding that name. The same name can have both bound and free occurrences in one formula. A <first-order substitution> replaces only free occurrences; a fresh renaming of bound occurrences and their binder preserves the formula up to <alpha equivalence>.