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?

Logic and Combinatorics(edited by Stephen Simpson, Amer. Math. Soc. 1987), but unfortunately I don't have a copy of that paper ready to hand. $\endgroup$ – Timothy Chow Dec 8 '19 at 19:57