Good examples of double induction

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.

Let me begin with an example of an induction of length $\epsilon_0$: The proof that Goodstein sequences terminate. I mention this because when I decided to understand this result, I began to compute the length of these sequences and eventually came to a conjecture for a general formula (!) for the length of the sequence. It turned out that proving the conjecture was easy, because the proof organized itself as an induction of length $\epsilon_0$. I was both very amused and very intrigued by this. The little paper that came out of this adventure is here.

Now, I also found once a natural example of an induction of length $\omega^2$ when studying a "Ramsey type" problem: the size of min-homogeneous sets for regressive functions on pairs. What I liked about this example is that Ackermann's function injected itself into the picture and ended up providing me with the right rates of growth. The details are in a paper here.

Though you've already dismissed it as 'lukewarm', Ackermann's function (proving totality I think is what is wanted) is your most accessible option (I think it is a great option).

It's not contrived/unnatural because it is motivated by very different concepts. If you want to construct another example (prove $f(x,y) = g(x,y)$), you'd probably want to have x and y very much asymmetric (in the sense that they should be used in syntactically very different ways in the computations). And Ackermann's function does just that.