What's so special about Kruskal's theorem and the ordinal [Gamma]o? A survey of some results in proof theory Export

@article{citeulike:1013469, 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 Verlen 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]o 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.}, author = {Gallier}, citeulike-article-id = {1013469}, citeulike-linkout-0 = {http://dx.doi.org/10.1016/0168-0072(91)90022-E}, citeulike-linkout-1 = {http://www.sciencedirect.com/science/article/B6TYB-45DB1XT-1D/2/cd824c2e2d70c54a1c6241d92912f106}, day = {19}, doi = {10.1016/0168-0072(91)90022-E}, journal = {Annals of Pure and Applied Logic}, keywords = {proof\_theory}, month = {September}, number = {3}, pages = {199--260}, posted-at = {2006-12-25 17:56:23}, priority = {0}, title = {What's so special about Kruskal's theorem and the ordinal [Gamma]o? A survey of some results in proof theory}, url = {http://dx.doi.org/10.1016/0168-0072(91)90022-E}, volume = {53}, year = {1991} }

TY - JOUR ID - citeulike:1013469 L3 - citeulike-article-id:1013469 N2 - 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 Verlen 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]o 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. IS - 3 JF - Annals of Pure and Applied Logic EP - 260 TI - What's so special about Kruskal's theorem and the ordinal [Gamma]o? A survey of some results in proof theory VL - 53 SP - 199 KW - proof_theory AU - Gallier PY - 1991/09/19/ UR - http://dx.doi.org/10.1016/0168-0072(91)90022-E ER -