What's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theory (Q1182475)

As the subtitle indicates, this is a survey of, mainly, H. Friedman's results on the unprovability of Kruskal's tree theorem and its variations (which says that well-orderedness of a relation among trees is inherited by its ``natural'' extension). The paper begins with the explanation and the proof of the above theorem, and then moves on to discuss ordinal notations and normal functions including Schütte-Feferman \(\Gamma_ 0\). The connection between Kruskal's theorem and the ordinals \(< \Gamma_ 0\) is explained. Then the nature of the paper changes to, mostly, citations of definitions and results. They include formal systems \(\text{ATR}_ 0\), etc., and unprovability results (in them) by Friedman, Simpson, et al.; term orderings [Dershowitz, Okada]; hierarchies of fast- and slow-growing functions [Wainer, Cichoń]; and constructive proof of Higman's theorem about the extension of ordering to finite sequences. This paper is written in lecture note style: the definition of concatenations of finite sequences is given, two pages are devoted to motivational material for critical ordinals, \(\Gamma_ 0\), etc., and the paper abounds with the instructor's comments like ``the key notion is ...'', ``we are already quite dizzy [in connection with ordinal notations]'', and so forth. Hence one should not be intimidated by the length of the paper! The author gives a modified definition of the isomorphism of trees to the ordinals [Def. 9.1.] that surmounts the difficulty in Simpson's and Smoryński's papers.