×

Ein in der reinen Zahlentheorie unbeweisbarer Satz über endliche Folgen von natürlichen Zahlen. (German) Zbl 0591.03041

The following special case of Kruskal’s Theorem is considered. If \(\sigma\) is an infinite sequence of finite strings of natural numbers, then one of the strings will be embeddable (in a rather strong sense) in a string that occurs later in the sequence \(\sigma\). The specialized Kruskal Theorem is represented by a formula K(f) in the system PA(f) of first order Peano arithmetic PA with a free variable f adjoined, and it is proved that K(f) is not derivable in PA(f).
The proof proceeds by means of an embedding of the finite strings, above, in the ordinals less than \(\epsilon_ 0\). To accomplish this embedding, Buchholz’s theory of ordinal notations is developed just to the extent needed to incorporate the regular ordinals up to \(\Omega_{\omega}\). The embedding is not at all trivial but employs ’collapsing’ functions on the notations for the number classes of finite order.
A ’minitiarization’ of the specialized Kruskal Theorem K(f) is obtained by observing that when f is restricted to sequences of linear growth rate, K(f) is a consequence of a \(\Pi^ 0_ 2\)-sentence M (where M is equivalent to \(\forall fK(f)\) under König’s Lemma). Hence M is a true sentence underivable in PA. Of course plenty of such sentences are known, but the paper is of interest, first, because it determines the exact proof-theoretic strength of a reasonably natural special case of Kruskal’s Theorem. The paper has a second, more fundamental interest because of the connections drawn between ordinals, growth rates, and computational complexity.
Reviewer: W.Howard

MSC:

03F30 First-order arithmetic and fragments
03F15 Recursive ordinals and ordinal notations
03D15 Complexity of computation (including implicit computational complexity)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Buchholz, W.: Normalfunktionen und konstruktive Systeme von Ordinalzahlen. Proof Theory Symposion Kiel 1974. Springer Lecture Notes in Math.500, 4–25 (1975). · doi:10.1007/BFb0079544
[2] Buchholz, W.: A new system of proof-theoretical ordinal functions. In Vorbereitung. · Zbl 0655.03038
[3] De Jongh, D., Parikh, R.: Well-partial-orderings and hierarchies. Indig. Math.39, 195–207 (1977). · Zbl 0435.06004
[4] Friedman, H.: Independence results in finite graph theory. Nicht veröffentlichte Manuskripte. Ohio State University 1981.
[5] Friedman, H.: Beyond Kruskal’s theorem. Nicht veröffentlichte Manuskripte. Ohio State University 1982.
[6] Higman, G.: Ordering by divisibility in abstract algebras. Proc. London Math. Soc.2, 326–336 (1952). · Zbl 0047.03402 · doi:10.1112/plms/s3-2.1.326
[7] Schmidt, D.: Well-partial-orderings and their maximal order types. Habilitationsschrift Heidelberg 1979.
[8] Schütte, K.: Proof Theory. Berlin, Heidelberg, New York 1977. · Zbl 0367.02012
[9] Simpson, S.G.: Nichtbeweisbarkeit von gewissen kombinatorischen Eigenschaften endlicher Bäume. Arch. math. Logik25, 45–65 (1985). · Zbl 0598.03045 · doi:10.1007/BF02007556
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.