# 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?

• I think that the Robertson-Seymour graph minor theorem is an example. The relevant reference is "The metamathematics of the graph minor theorem" by Friedman, Robertson, and Seymour, in 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. – Timothy Chow Dec 8 '19 at 19:57
• @Timothy Chow You can download the paper at this link: libgen.is/book/index.php?md5=E1D065356E31DE3477F05FDD64B453A0 – QiRenrui Dec 9 '19 at 0:22

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$$.
• The proof of the Kruskal's Tree Theorem itself needn't involve such an induction, but arguably Schmidt's proof that its type (maximum linearization) is $\Gamma_0$ does? This relates to another question I've been wondering about -- I'm a little unclear here on the connection between type on the one hand & proof-theoretic ordinal on the other; I'm not sure how well that's understood actually... but I guess that's not something to start a discussion on in the comments; maybe I should ask that as a separate question here...) – Harry Altman Dec 27 '19 at 5:40
• Hold on, wait -- I just realized we've been talking about the wrong ordinal, right? Kruskal's tree theorem is small Veblen ordinal, not $\Gamma_0$, right? May have to go look up this Gallier paper... – Harry Altman Dec 28 '19 at 22:33