Timeline for answer to Examples of proofs using induction or recursion on a big recursive ordinal by Timothy Chow
Current License: CC BY-SA 4.0
Post Revisions
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 31, 2019 at 8:36 | comment | added | Harry Altman | I see! It's smaller so it makes sense. Thanks! | |
| Dec 29, 2019 at 22:33 | comment | added | Timothy Chow | @HarryAltman : Not sure what you mean by the "wrong ordinal." As explained in the paper I mentioned, the validity of induction on $\Gamma_0$ is a natural consequence of Kruskal's theorem. So yes, there is a sense in which Kruskal's theorem is associated with a larger ordinal, but the theorem is also naturally connected with $\Gamma_0$. | |
| Dec 28, 2019 at 22:33 | comment | added | Harry Altman | 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... | |
| Dec 27, 2019 at 5:40 | comment | added | Harry Altman | 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...) | |
| Dec 27, 2019 at 4:11 | comment | added | Timothy Chow | 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. | |
| Dec 27, 2019 at 1:52 | comment | added | QiRenrui | 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. | |
| Dec 26, 2019 at 22:45 | comment | added | cody | 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...) | |
| Dec 26, 2019 at 18:56 | history | answered | Timothy Chow | CC BY-SA 4.0 |