Generalizations of the Kruskal-Friedman theorems

Journal of Symbolic Logic 55 (1):157-181 (1990)
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 ω. The corresponding limit statement, expressing that for all initial segments of ω these labeled trees are well-quasi-ordered, is provable in Π 1 1 -CA, but not in the analogous theory Π 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 Γ 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}_{ (which are denoted by LM λ 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
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2307/2274960
 Save to my reading list
Follow the author(s)
My bibliography
Export citation
Find it on Scholar
Edit this record
Mark as duplicate
Revision history
Request removal from index
Download options
Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 25,767
Through your library
References found in this work BETA
A New System of Proof-Theoretic Ordinal Functions.W. Buchholz - 1986 - Annals of Pure and Applied Logic 32 (3):195-207.
Proof-Theoretical Analysis: Weak Systems of Functions and Classes.L. Gordeev - 1988 - Annals of Pure and Applied Logic 38 (1):1-121.
An Independence Result for +BI.Wilfried Buchholz - 1987 - Annals of Pure and Applied Logic 33 (2):131-155.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles
Reflections on Concrete Incompleteness.G. Longo - 2011 - Philosophia Mathematica 19 (3):255-280.
A First-Order Axiomatization of the Theory of Finite Trees.Rolf Backofen, James Rogers & K. Vijay-Shanker - 1995 - Journal of Logic, Language and Information 4 (1):5-39.
Predicativism as a Philosophical Position.Geoffrey Hellman - 2004 - Revue Internationale de Philosophie 3:295-312.
An Application of Graphical Enumeration to PA.Andreas Weiermann - 2003 - Journal of Symbolic Logic 68 (1):5-16.
Functional Interpretation and Inductive Definitions.Jeremy Avigad & Henry Towsner - 2009 - Journal of Symbolic Logic 74 (4):1100-1120.
Finitely Constrained Classes of Homogeneous Directed Graphs.Brenda J. Latka - 1994 - Journal of Symbolic Logic 59 (1):124-139.

Monthly downloads

Added to index


Total downloads

12 ( #363,008 of 2,146,897 )

Recent downloads (6 months)

1 ( #385,700 of 2,146,897 )

How can I increase my downloads?

My notes
Sign in to use this feature

There  are no threads in this forum
Nothing in this forum yet.

Other forums