does anyone know of a definition of "bound variable" in the context of lambda calculus or first-order logic that I could cite?