# How does one determine which variables to do induction on?

I have been struggling with this all day. When one does mathematical induction, how does one choose when to induct with one variable, or with more than one?

I have been working through Tao's Analysis I and got up to Lemma 2.2.3.

At this point, addition of natural numbers is only defined as follows:

• Let $n,m \in \mathbb N$. Then $0+m:=m$, and $(n^{++})+m:=(n+m)^{++}$

("$:=$" means "defined as", and "${}^{++}$" stands for "increment of". At this point in the text basically only Peano's Axioms are defined. Commutativity of addition has not been defined yet.)

Lemma 2.2.3 states:

• if $n,m\in \mathbb N$, then $n+(m^{++})=(n+m)^{++}$

I was able to prove it in the way that was shown in the text, but what puzzled me was the method of induction. In the text, Tao decides to induct on $n$ while leaving $m$ constant, which was great. However, after he finishes this induction, he says that the lemma is proven. I assumed that afterwards he would have to somehow induct on $m$ (two-dimensional induction), but seemingly this isn't needed. Why is this?

edit:

Here is the proof:

Proof: Induct on $n$ (keeping $m$ fixed).

Consider the base case: $0+(m^{++})=(0+m)^{++}$. Applying the Def'n of Addition to each side implies that $m^{++}=m^{++}$, which is true.

Suppose inductively that $n+(m^{++})=(n+m)^{++}$.
We have to prove the inductive step, namely that $(n^{++})+(m^{++})=((n^{++})+m)^{++}$.
Using the Def'n of Addition on both sides gives $(n+(m^{++}))^{++}=((n+m)^{++})^{++}$.
Using the supposition on the left side gives $((n+m)^{++})^{++}=((n+m)^{++})^{++}$, which is true. Thus, whenever $P(n)$ is true, $P(n^{++})$ is true. With the base case established, this proves Lemma 2.2.3.

edit2:

I found this blog post with a good example of 2D induction. It seems in this example, 2D induction is needed only because there are two separate cases: one for $f(m+1,n)$ and another for $f(m,n+1)$. I'm currently searching for (and trying to understand) other examples.

-
Presumably each step in the proof is valid for any $m$, so there is no need to induct over it. But you'd have to reproduce the proof here for me to be sure. –  Alex Becker Dec 21 '12 at 4:03

Formalized in Coq, the proof runs this way:

Lemma plus_n_Sm : forall n m : nat, S (n + m) = n + S m.
Proof. intros n. induction n as [|n' IHn'].
* intros m. reflexivity.
* intros m. simpl. rewrite IHn'. reflexivity.
Qed.


I'm happy to see that this is simply a different notation for the proof that you have.

Either way, there's nothing special about whether m is zero, one, or any other natural number. So there's no call for considering m in separate cases, neither by induction nor by any other method.

In contrast, double induction would be used in order to show that $\forall n,m\in\mathbb N, n + m = m + n$, that is, that addition is commutative. There is certainly something special for commutativity in the case $m = 0$ as well as in the case $n = 0$. Those provide the base cases for the double induction.

-
Thanks! That's the vague thought that I had when doing the proof. I guess I'm just wondering then when it's appropriate to use two-dimensional induction for a proof compared to one like this. What makes the difference? (In the meantime, I'm trying to learn to read Coq) –  matt0089 Dec 21 '12 at 5:42
Thanks again for your answer. I think I'm starting to get what you mean by special... If there are any special cases for a number, then 2D induction is required to verify the base case for each number. However, it turns out the text also proves commutativity with only one var! –  matt0089 Dec 21 '12 at 20:57