Generalizations of the Kruskal-Friedman Theorems
Gordeev, L.
J. Symbolic Logic, Tome 55 (1990) no. 1, p. 157-181 / Harvested from Project Euclid
Kruskal proved that finite trees are well-quasi-ordered by hom(e)omorphic embeddability. Friedman observed that this statement is not provable in predicative analysis. Friedman also proposed (see in [Simpson]) some stronger variants of the Kruskal theorem dealing with finite labeled trees under home(e)omorphic embeddability with a certain gap-condition, where labels are arbitrary finite ordinals from a fixed initial segment of $\omega$. The corresponding limit statement, expressing that for all initial segments of $\omega$ these labeled trees are well-quasi-ordered, is provable in $\Pi^1_1$-CA, but not in the analogous theory $\Pi^1_1-CA_0$ with induction restricted to sets. Schutte and Simpson proved that the one-dimensional case of Friedman's limit statement dealing with finite labeled intervals is not provable in Peano arithmetic. However, Friedman's gap-condition fails for finite trees labeled with transfinite ordinals. In [Gordeev 1] I proposed another gap-condition and proved the resulting one-dimensional modified statements for all (countable) transfinite ordinal-labels. The corresponding universal modified one-dimensional statement $UM^1$ is provable in (in fact, is equivalent to) the familiar theory $ATR_0$ whose proof-theoretic ordinal is $\Gamma_0$. In [Gordeev 1] I also announced that, in the general case of arbitrarily-branching finite trees labeled with transfinite ordinals, in the proof-theoretic sense the hierarchy of the limit modified statements $\mathbf{M}_{<\lambda}$ (which are denoted by $LM_\lambda$ in the present note) is as strong as the hierarchy of the familiar theories of iterated inductive definitions (more precisely, see [Gordeev 1, Concluding Remark 3]). In this note I present a "positive" proof of the full universal modified statement UM, together with a short proof of the crucial "reverse" results which is based on Okada's interpretation of the well-established ordinal notations of Buchholz corresponding to the theories of iterated inductive definitions. Formally the results are summarized in $\S5$ below.
Publié le : 1990-03-14
Classification: 
@article{1183743191,
     author = {Gordeev, L.},
     title = {Generalizations of the Kruskal-Friedman Theorems},
     journal = {J. Symbolic Logic},
     volume = {55},
     number = {1},
     year = {1990},
     pages = { 157-181},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183743191}
}
Gordeev, L. Generalizations of the Kruskal-Friedman Theorems. J. Symbolic Logic, Tome 55 (1990) no. 1, pp.  157-181. http://gdmltest.u-ga.fr/item/1183743191/