Paper Info
Title
What's So Special About Kruskal's Theorem and the Ordinal Gamma0? A Survey of Some Results in Proof Theory
Abstract
This paper consists primarily of a survey of results of Harvey Friedman about some proof-theoretic aspects of various forms of Kruskal's tree theorem, and in particular the connection with the ordinal GAMMA-0. We also include a fairly extensive treatment of normal functions on the countable ordinals, and we give a glimpse of Veblen hierarchies, some subsystems of second-order logic, slow-growing and fast-growing hierarchies including Girard's result, and Goodstein sequences. The central theme of this paper is a powerful theorem due to Kruskal, the 'tree theorem', as well as a 'finite miniaturization' of Kruskal's theorem due to Harvey Friedman. These versions of Kruskal's theorem are remarkable from a proof-theoretic point of view because they are not provable in relatively strong logical systems. They are examples of so-called 'natural independence phenomena', which are considered by most logicians as more natural than the metamathematical incompleteness results first discovered by Godel. Kruskal's tree theorem also plays a fundamental role in computer science, because it is one of the main tools for showing that certain orderings on trees are well founded. These orderings play a crucial role in proving the termination of systems of rewrite rules and the correctness of Knuth-Bendix completion procedures. There is also a close connection between a certain infinite countable ordinal called GAMMA-0 and Kruskal's theorem. Previous definitions of the function involved in this connection are known to be incorrect, in that, the function is not monotonic. We offer a repaired definition of this function, and explore briefly the consequences of its existence.
Year
Venue
DocType
1991
ANNALS OF PURE AND APPLIED LOGIC
Journal
Volume
Issue
ISSN
53
3
0168-0072
Citations 
PageRank 
References 
10
0.95
0
Authors
1
Name
Order
Citations
PageRank
Jean H. Gallier1749111.86