The nature of variables within proofs

Question

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

Answer 1

universal generalization: "for all odd $m \in \Bbb{Z}$".

existential instantiation: "there exists a $k \in \Bbb{Z}$ such that $m = 2k+1$".

These are both quantified and they are quantified in the way you recite.

It is more accurate to think of variables as variables. A statement with a universally quantified variable may be specialized, removing the universal quantifier, by replacing the occurrences of the variable with a particular member of the set from which that variable is drawn. For instance, in your proof, an equally valid set of statements is produced by replacing every instance of $m$ by "$3$" (an odd integer). Existentially quantified variables can be specialized to the value that satisfies their constraints.

When $m$ is generic (free to range over the odd integers), $k$ must be generic, since the value of $k$ is dependent on the value of $m$. (In a more pedantic setting, the dependence of $k$ on $m$ would be made more apparent by writing, for instance $k(m)$, $k_m$, or some other syntax to indicate dependency. This dependency enforces an order on the quantifiers. Equivalently, the order of the quantifiers, $\forall m \text{ odd}, \exists k \in \Bbb{Z} \dots$.) Even though $k$ is generic, in this case, we can solve for $k$ in terms of $m$: $k = \frac{m-1}{2}$. Consequently, throughout, we may specialize the variable $k$ to the value $\frac{m-1}{2}$.

When $m$ is specialized to a value, we may replace $k$ with the value that is half of one less than the value of $m$. We still end up with a valid set of statements -- this valid set of statements is the explicit proof of the oddness of the square of whatever value $m$ has taken. This last should make it clear: $m$ and $k$ are variables. For each specialization of $m$ and $k$ to (valid) values, we obtain a concrete proof. If we do not specialize, we obtain a proof that is universally quantified over $m$ and existentially quantified over $k$ (which is dependent on $m$).

Answer 2

$m$ is a variable in that its value is not fixed, but due to the relation between $m$ and $k$ once you fix one of them you determine the value of the other (and $m$ must be odd). You are not proving the statement for particular constants but for arbitrary ones, which is to say, variables.

Answer 3

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.

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.

Answer 4

During a proof, there are two things present at any point in time:

• the thing(s) you want to proof right now (which I will call the goal(s) )
• and the things you are assuming right now, the things you can use to continue in your proof (referred to as the context).

Let's go through the proof you want to do, keeping track of both the context on the left and the goal on the right. At the start we have $$ \boxed{\begin{array}{c|c} \text{Context} & \text{Goal} \\ \hline & \hspace{1em} \forall m \, (m \text{ is odd } \Rightarrow m^2 \text{ is odd}) \hspace{1em} \end{array}} $$ So our goal is something of the form $\forall x \, \varphi(x)$. How do we show this in general?

We can conclude $\forall x \, \varphi(x)$ from the context $\Gamma$ if we can show $\varphi(y)$ for a variable $y$ which does not appear as a free variable in either the context $\Gamma$ or $\varphi(x)$.

In our case $y$ would actually satisfy this and thus we get a new goal $$ \boxed{\begin{array}{c|c} \text{Context} & \text{Goal} \\ \hline & \hspace{1em} y \text{ is odd } \Rightarrow y^2 \text{ is odd} \hspace{1em} \end{array}} $$ Why is it fine to simply get rid of the quantification and replace $m$ with $y$? Well, we did not simply get rid of the quantification. We had to make sure that $y$ is not free in the context and the right side! This condition assures that the context can not have any information about the variable $y$ for us. So we are not assuming anything about $y$, we know nothing about it and thus $y$ can truly be considered to be anything/general. And so if we show the right side for a variable we can consider general, the argument is that we have shown $\forall m [\dots]$.

Now let's continue with the proof. To show the implication you assume whats on the left and try to show whats on the right. $$ \boxed{\begin{array}{c|c} \text{Context} & \text{Goal} \\ \hline \hspace{1em} y \text{ is odd } \hspace{1em} & \hspace{1em} y^2 \text{ is odd} \hspace{1em} \end{array}} $$ In order to continue we need to write out the definition of odd $$ \boxed{\begin{array}{c|c} \text{Context} & \text{Goal} \\ \hline \hspace{1em} \exists k \, (y = 2k + 1) \hspace{1em} & \hspace{1em} \exists k \, (y^2 = 2k + 1) \hspace{1em} \end{array}} $$ Now at this point you can apply existential instantiation on the statement $\exists k \, (y = 2k + 1)$ in your context. What happens here is that you are allowed to replace $\exists k \, (y = 2k + 1)$ by $(y = 2z + 1)$ for any variable $z$ that does not appear free in your context and goal. Similarly to before, this now makes sure that the only thing you know about $z$ is that it satisfies $y = 2z + 1$. So we get $$ \boxed{\begin{array}{c|c} \text{Context} & \text{Goal} \\ \hline \hspace{1em} y = 2z + 1 \hspace{1em} & \hspace{1em} \exists k \, (y^2 = 2k + 1) \hspace{1em} \end{array}} $$

---

This explanation is basically a verbalization of some of the rules for natural deduction, which is a formal way of describing proofs. So if you haven't yet and really want to learn more about proofs in detail, this would be a topic to get into; although it's a deep dive.

Answer 5

You say: "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 would say this a little differently. A predicate does not have a truth value until values are assigned to the free variables. But if you assign values to the free variables, then a predicate has a truth value.

Now, let me suggest a slightly different version of Lereau's answer. I like the idea of distinguishing between context and goal, but I would say that the context consists of two things: a specification of which variables are assumed to have values assigned to them, and a specification of which statements are assumed to be true (these are called "givens" in my book). With this modified version of Lereau's idea of context, let me go through the proof. We start with:

• Context: empty; that is, no variables are assumed to have values and no givens are assumed to be true
• Goal: $\forall m(m \text{ is odd} \Rightarrow m^2 \text{ is odd})$

When you write "Let $m \in \mathbb{Z}$ be arbitrary," you change the situation to:

• Context: variables: $m$; givens: none
• Goal: $m \text{ is odd} \Rightarrow m^2 \text{ is odd}$

So now you are assuming that $m$ stands for something (so the goal, which contains $m$ as a free variable, has a truth value), but you are making no assumption about what $m$ stands for, so it could be anything. Now you assume $m$ is odd:

• Context: variables: $m$; givens: $m$ is odd
• Goal: $m^2$ is odd

Writing out the definition of "odd", this means:

• Context: variables: $m$; givens: $\exists k \in \mathbb{Z}(m = 2k+1)$
• Goal: $\exists j \in \mathbb{Z}(m^2 = 2j+1)$

Now since the given is an existential statement, we can introduce the variable $k$ to stand for an integer such that $m = 2k+1$:

• Context: variables: $m$, $k$; givens: $m = 2k+1$
• Goal: $\exists j \in \mathbb{Z}(m^2 = 2j+1)$

Now $m$ and $k$ are both assumed to have values assigned to them, and the statement $m = 2k+1$ is assumed to be true with those values assigned. Now it is just simple algebra to come up with the value of $j$ that demonstrates that the goal is true.