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.

Solution 1:

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.