If $\alpha$ is a countable ordinal and $A$ is the set of natural numbers having well-ordering of type $\alpha$, does this mean that $\alpha$-induction (transfinite induction up to $\alpha$) is equivalent to the Well-Ordering Principle on $A$?
For example, if $A=\{0,2,4,6,\ldots,1,3,5,\ldots\}$ (i.e. $1$ is greater than any even number in the well-ordering), what would be a statement about the elements of $A$ that would require induction past $\omega$? Would the following statement work?
$$\exists\, n\in A\,\forall\,m\in A: (n>0)\wedge(n>\rm{S}\overset{m}{\cdots}\rm{S}0)$$
where $\rm{S}$$x$ denotes the successor of $x$ in $A$ (note, if $m=0$ then $\rm{S}\overset{m}{\cdots}\rm{S}0$ is $0$).
Finally, Goodstein's Theorem or the Consistency of PA are a well-kown results which are equivalent to $\varepsilon_{0}$-induction. What is an example of a statement equivalent to $\omega^{\omega}$-induction?
There is something wrong with my statement above. When $m$ is "odd" I cannot think of it as the number I am using to represent it, so the expression $\rm{S}\overset{m}{\cdots}\rm{S}0$ does not make sense.
How about simply the statement $\forall\,n\in A:0+n = n$?
Best Answer
In order to remove the question from the unanswered list I will mention the following ($\alpha$-induction means induction up to $\alpha$, also called induction of length $\alpha$):
The fairly common "double induction" is $\omega^{2}$-induction, and it can occur as explained here. Let's unpack that a bit more to formulate a version of double induction, or $\omega^{2}$-induction:
A simple example of use of $\omega^{2}$-induction is the proof of the statement
Proving that the usual order relation $<$ on $\mathbb{N}$ is a linear ordering uses $\omega^{2}$-induction.
Another example is the proof that $\boldsymbol{\cdot}$ is commutative, where $\boldsymbol{\cdot}$ is simply multiplication defined on the natural numbers (i.e. as a function $\mathbb{N}\times\mathbb{N}\to\mathbb{N}$ such that $i\boldsymbol{\cdot}0=0$, and $i\boldsymbol{\cdot}S(j)=(i\boldsymbol{\cdot}j)+i$, where $S$ is the succesor function). It is worth illustarting the process in this case:
First, we show $0\boldsymbol{\cdot}i=0$ for all $i\in\mathbb{N}$. Next, we prove $i\boldsymbol{\cdot}j=j\boldsymbol{\cdot}i$ using induction on $i$. Later in the proof, we will be assuming $i\boldsymbol{\cdot}j=j\boldsymbol{\cdot}i$ for all $j\in\mathbb{N}$ and will be trying to show that $S(i)\boldsymbol{\cdot}j=j\boldsymbol{\cdot}S(i)$ for all $j\in\mathbb{N}$. In order to do this, we will have to use induction again, this time on $j$.
Additionally, the original proofs of the finite version of Ramsey's theorem (see [Nes1995] below for the proof) and the Hales-Jewett theorem (original proof here) both use $\omega^{2}$-induction. It is important to note that this use is not essential, as it was later shown by Paul Erdős and Saharon Shelah, which used $\omega$-induction.
For more on double, or $\omega^{2}$-induction, see this. It contains several interesting links.
As a final note on $\omega^{2}$-induction, note how the process essentially performs induction on one variable with another induction on the other variable inside the proof. This nested induction idea can be generalized to speak of $\omega^{n}$-induction for $n\ge 2$ in a relatively straightforward manner.
Regarding $\omega^{\omega}$-induction, lemma 3.6 of [Sim1988] shows that well orderedness of $\omega^{\omega}$ (i.e. $\omega^{\omega}$-induction) is equivalent over $\mathsf{RCA}_{0}$ to each of the following statements:
The book Subsystems of Second order Arithmetic, 2nd. ed., by Stephen G. Simpson is an excellent resource containing a plethora of results whose ordinal strength (i.e. to what level of transfinite induction they are equivalent to) is precisely determined.
Another example of use of $\omega^{\omega}$-induction can be found in the usual proof via ordinals of the Weak Goodstein Theorem (see this). Moreover, with a straightforward modification, the usual proof produces, for $n\ge 2$, examples of $(\omega\uparrow\uparrow n)$-induction (where $\omega\uparrow\uparrow n= \underbrace{\omega^{\omega^{^{.^{.^{.^\omega}}}}}}_{n}$) This is achieved by modifying the base-bumping process involved in defining the weak Goodstein sequences by bumping additional exponents:
And so on. Stopping at bumping at level $n+1$ exponents will yield $(\omega\uparrow\uparrow n)$-induction.
It is worth noting that $(\omega\uparrow\uparrow n)$-induction is essential in each case. For example, the $\omega^{\omega}$-induction required by the Weak Goodstein Theorem cannot be reduced to $\omega^{n}$-induction for any $n\in\mathbb{N}$ (See [Cai2007 - p.390]: it is not provable within $\mathsf{PRA}$ or $\mathsf{I\Sigma}_{1}$, both of which have proof theoretic ordinal $\omega^{\omega}$. More generally, the level $n$ modified statement is not provable within $\mathsf{I\Sigma}_{n+1}$, whose proof theoretic ordinal is $\omega\uparrow\uparrow (n+1)$).
[Cai2007] Caicedo, Andrés Eduardo, Goodstein’s function, Rev. Colomb. Mat. 41, No. 2, 381-391 (2007). ZBL1156.03053.
[Nes1995] Nešetřil, J., Ramsey Theory, Handbook of Combinatorics, Vol. 1,2, Elsevier Sci. B. V., Amsterdam, 1995, pp. 1133-1142.
[Sim1988] Simpson, S.G., Ordinal Numbers and the Hilber Basis Theorem, The Journal of Symbolic Logic, Vol. 53 (1988), pp. 961-974.