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:
If $P(i,j)$ is a doubly indexed family of statements, one for each $i\ge a$ and $j\ge b$ such that
- $P(a,b)$ is true,
- $\forall i\ge a$, $P(i,b)\Rightarrow P(i+1,b)$,
- $\forall j\ge b$, we have $\forall i\ge a$, $P(i,j)\Rightarrow P(i,j+1)$,
then $P(i,j)$ is true for all $i\ge a$ and $j\ge b$.
A simple example of use of $\omega^{2}$-induction is the proof of the statement
- $\forall i,j\ge 1$, $(i + 1)\cdot j>i\cdot j$
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:
- Dickson's Lemma - For each $m\in\mathbb{N}$, the $m$-fold Cartesian power $\mathbb{N}^{m}$ is well quasiordered.
- The Hilbert Basis Theorem - For all countable fields $K$ and all $m\in\mathbb{N}$, any ideal in the polynomial ring $K[x_{1},\ldots,x_{m}]$ is finitely generated.
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:
- Bumping the base (call them level $0$ exponents if you may) and the exponents (level $1$) as well will yield $\omega^{{\omega}^{\omega}}$-induction in the usual proof.
- Additionally bumping the exponents of the exponents (level $2$) will get us $(\omega\uparrow\uparrow 4)$-induction.
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.
Best Answer
Re: your first question, this is disappointingly easy: writing "$Con(\mathsf{PA},x)$" for "There is no proof of a contradiction in $\mathsf{PA}$ of length $<x$," consider the relation given by $$a\prec b\quad \equiv \quad (a<b)\leftrightarrow Con(\mathsf{PA}, \min\{a,b\}).$$ Intuitively, this describes the following process: we start listing the natural numbers in their usual order, and if we ever see a contradiction in $\mathsf{PA}$ we shift tactics (so to speak) and build a descending chain. For example, if there were a shortest proof of a contradiction in $\mathsf{PA}$ of length $5$, the $\prec$-order would look like $$0,1,2,3,4, ... ,8,7,6,5$$ and have ordertype $5+\omega^*$ (which is not a well-order, to put it mildly). This is a primitive recursive process, though, and so we have a p.r. "copy" of $\omega$ which $\mathsf{PA}$ can't appropriately analyze.
Note that this trick works with any ("reasonable") theory in place of $\mathsf{PA}$. In particular, your proposal would lead to every proof-theoretic ordinal being just $\omega$.