# Good examples of double induction

I’m looking for good examples where double induction is necessary. What I mean by double induction is induction on $\omega^2$. These are intended as examples in an “Automatas and Formal Languages” course.

One standard example is the following: in order to cut an $n\times m$ chocolate bar into its constituents, we need $nm-1$ cuts. However, there is a much better proof without using induction.

Another example: the upper bound $\binom{a+b}{a}$ on Ramsey numbers. The problem with this example is that it can be recast as induction on $a+b$, while I want something which is inherently inducting on $\omega^2$.

Lukewarm example: Ackermann’s function, which seems to be pulled out of the hat (unless we know about the primitive recursive hierarchy).

Better examples: the proof of other theorems in Ramsey theory (e.g. Van der Waerden or Hales-Jewett). While these can possibly be recast as induction on $\omega$, it’s less obvious, and so intuitively we really think of these proofs as double induction.

Another example: cut elimination in the sequent calculus. In this case induction on $\omega^2$ might actually be necessary (although I’m not sure about that).

The problem with my positive examples is that they are all quite technical and complicated. So I’m looking for a simple, non-contrived example where induction on $\omega^2$ cannot be easily replaced with regular induction (or with an altogether simpler argument). Any suggestions?

A nice example arises by relativizing Goodstein’s Theorem from $\rm\ \epsilon_0 = \omega^{\omega^{\omega^{\cdot^{\cdot^{\cdot}}}}}$ down to $\rm\ \omega^2\:.\$
$\rm\ \omega^2\$ Goodstein’s Theorem $\$ Given naturals $\rm\ a,\:b,\:c\$ and an arbitrary increasing “base-bumping” function $\rm\ g(n)\$ on $\:\mathbb N\:$ the following iteration eventually reaches $0\$ (i.e. $\rm\ a = c = 0\:$).
$\rm\quad\quad\quad\quad\ \ a\ b + c \ \ \to\quad\quad\ \ a\ \ \ \ \ g(b)\ +\ \ \ c\ \ -\ 1\quad if\quad\ c > 0$
$\rm\quad\quad\quad\quad\ \ \phantom{a\ b + c}\ \ \to\ \ (a-1)\ g(b)\ +\ g(b)-1\quad if\quad \ c = 0$
Note: $\$ The above iteration is really on triples $\rm\ (a,b,c)\$ but I chose the above notation in order to emphasize the relationship with radix notation and with Cantor Normal form for ordinals < $\epsilon_0$. $\ \$ For more on Goodstein’s Theorem see the link in Andres’s post or see my 1995\12\11 sci.math post.