10
$\begingroup$

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?

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ 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. $\endgroup$ Commented Dec 8, 2019 at 19:57
  • 1
    $\begingroup$ @Timothy Chow You can download the paper at this link: libgen.is/book/index.php?md5=E1D065356E31DE3477F05FDD64B453A0 $\endgroup$ Commented Dec 9, 2019 at 0:22

1 Answer 1

Reset to default
4
$\begingroup$

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$.

Improve this answer
$\endgroup$
7
  • $\begingroup$ I feel like the proof is simply a definition of a WQO, rather than a proof by induction on a WQO. The proof itself is usually in the form of a "minimal bad sequence" argument. I'd also note that it's significantly easier to define and use WQOs and well-founded orders than ordinals, so it might not be quite in the spirit of the question (or maybe it suggests that ordinals are not such useful objects after all...) $\endgroup$ Commented Dec 26, 2019 at 22:45
  • $\begingroup$ Are this proof of Kruskal's tree theorem uses such a wqo, or it just proves that the trees forms a wqo? And I don't think that means ordinals are not such useful. $\endgroup$ Commented Dec 27, 2019 at 1:52
  • $\begingroup$ I don't fully understand the distinction that you're trying to draw. The conclusion of Kruskal's tree theorem is that something is a wqo. The "minimal bad sequence" argument is what I'd call an induction argument. I'd call this proof by induction on a wqo, but maybe you reserve that term for a proof that starts with something that is already known to be a wqo, and uses that fact to prove some statement about the wqo other than "this is a wqo"? Anyway you can read the proof and decide for yourself. $\endgroup$ Commented Dec 27, 2019 at 4:11
  • 1
    $\begingroup$ 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...) $\endgroup$ Commented Dec 27, 2019 at 5:40
  • $\begingroup$ 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... $\endgroup$ Commented Dec 28, 2019 at 22:33

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.