Examples of proofs using induction or recursion on a big recursive ordinal There are many proofs use induction or recursion on $\omega$, or on an arbitary (may be uncountable) ordinal. Are there some good examples of proofs which use a big but computable ordinal?
The original proof of Ramsey theorem and Hales-Jewett theorem use induction on $\omega^2$, but the using is not essential, because Erdos and Shelah have given better bounds by using induction just on $\omega$. And further more $\omega^2$ shouldn't be considered big.
A typical use of big ordinal induction is proving the consistence of axiom systems, for example, using $\varepsilon_0$-induction to prove the consistence of PA. This is one kind of examples.
The existence of Goodstein function uses the induction on $\varepsilon_0$, and I think it's just a directly explaining of how do recursion on ordinal works.
Are there more examples?
 A: This is an expanded version of my comment.  There are examples from wqo (well quasi-order) theory, if you accept that induction on a wqo is "induction on an ordinal" (specifically, the ordinal of the tree of "finite bad sequences" of the wqo).  Kruskal's tree theorem can be proved by induction on a certain wqo whose ordinal is bigger than $\Gamma_0$, which is much bigger than the ordinals you mentioned.  This is explained in detail in "What's so special about Kruskal's theorem and the ordinal $\Gamma_0$? A survey of some results in proof theory," by Jean H. Gallier, Ann. Pure Appl. Logic 53 (1991), 199–260.
Related to this is Friedman's extension of Kruskal's theorem; let's call it EKT.  In "The metamathematics of the graph minor theorem" by Friedman, Robertson, and Seymour, it is explained that EKT is equivalent (over RCA$_0$) to a weak version of the Graph Minor Theorem that they call the "bounded Graph Minor Theorem," i.e., the Graph Minor Theorem restricted to graphs of bounded tree-width.  The relevant ordinal here is $\alpha_n$, the ordinal of the wqo of graphs of tree-width at most $n$, partially ordered by minor inclusion.
I believe that the exact ordinal corresponding to the full Graph Minor Theorem is still unknown, but is conjectured to exceed $\lim_n \alpha_n$, which is the proof-theoretic ordinal of $\Pi_1^1$-CA$_0$.
