I am confused about how best to view certain kinds of variables that show up in the course of an elementary proof. For example, to prove that the square of every odd integer is odd, I would write:
Let $m \in \mathbf{Z}$ be arbitrary. Suppose $m$ is odd. Choose $k \in \mathbf{Z}$ such that $m = 2k + 1$. Then $m^2 = (2k + 1)^2 = 2(2k^2 + 2k) + 1$, so since $2k^2 + 2k \in \mathbf{Z}$, it follows that $m^2$ is odd.
The symbol $m$ is introduced as part of the technique of universal generalization; Velleman [1] describes this step as "introducing a new variable [$m$] … to stand for an arbitrary object." The symbol $k$ is introduced as part of the technique of existential instantiation; [1] describes this as "introducing a new variable [$k$] to stand for an object for which [the predicate $m = 2k + 1$] is true."
In what sense are $m$ and $k$ variables? They do not seem to be bound variables, as they are in the scope of no quantifier. They also can't be free variables, because if they were, then, for example, the sentence being proved true after the introduction of arbitrary integer $m$ — namely that if $m$ is odd then $m^2$ is odd — would be a predicate and not even have a truth value; I am also obviously not free to substitute values into $m$ and $k$, if for no other reason than $m$ and $k$ are dependent.
Stoll [2] says a variable is free if it is not bound, so there is no third option.
Is it more correct to think of the phrases "let $m \in \mathbf{Z}$ be arbitrary" and "choose $k \in \mathbf{Z}$ such that …" as introducing new constants rather than variables, as their values are fixed despite being unspecified ($m$) or unknown ($k$)? More generally, the idea of a symbol that stands for a particular but arbitrary element of some set seems incompatible with the typical description of a variable as a placeholder as seen in, e.g., Epp [3].
[1] Velleman, D. (2006). How to Prove It: A Structured Approach (2nd ed.). Cambridge: Cambridge University Press.
[2] Stoll, Robert Roth (1963). Set Theory and Logic. W.H. Freeman.
[3] Epp, Susanna S. Variables in Mathematics Education. https://condor.depaul.edu/~sepp/VariablesInMathEd.pdf
Best Answer
Actually every time you say something like "let $m \in \mathbb{Z}$ be arbitrary" the word "arbitrary" is code for an implicit universal quantifier $\forall m \in \mathbb{Z}$, in this case part of the statement
$$\forall m \in \mathbb{Z} : \left( \exists k \in \mathbb{Z} : 2k+1 = m \right) \Rightarrow \left( \exists k' \in \mathbb{Z} : 2k'+1 = m^2 \right)$$
you are trying to prove. So it is a bound variable, bound to a quantifier which is being left implicit. This is a very common convention in mathematics which is usually not described explicitly. Then we appeal to a general principle about how to prove a result involving a universal quantifier, which I guess is called universal generalization: to prove $\forall m, P(m)$ you introduce $m$ as an arbitrary variable and write down a proof where you assume nothing about $m$ except whatever premises might be in the statement $P(m)$ and see if you can deduce the desired conclusion.