What's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theory

DOI10.1016/0168-0072(91)90022-EzbMath0758.03025OpenAlexW2076972393WikidataQ29030153 ScholiaQ29030153MaRDI QIDQ1182475

Jean H. Gallier

Publication date: 28 June 1992

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0168-0072(91)90022-e

zbMATH Keywords

surveyordinal notationsnormal functionsunprovabilitycompletion procedurecritical ordinalshierarchies of fast- and slow-growing functionsisomorphism of treesKruskal's tree theoremterm orderings

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Grammars and rewriting systems (68Q42) Proof theory in general (including proof-theoretic semantics) (03F03) Recursive ordinals and ordinal notations (03F15)

Related Items (32)

Trees, ordinals and termination ⋮ Equational derivation vs. computation ⋮ An abstract factorization theorem and some applications ⋮ Coq formalization of the higher-order recursive path ordering ⋮ On the modularity of termination of term rewriting systems ⋮ Ordinal arithmetic: Algorithms and mechanization ⋮ Theorems as Constructive Visions ⋮ On some slowly terminating term rewriting systems ⋮ E-Unification based on Generalized Embedding ⋮ Ordinal recursive bounds for Higman's theorem ⋮ A notation for lambda terms. A generalization of environments ⋮ Simple termination of rewrite systems ⋮ The length of an intersection ⋮ A constructive picture of Noetherian conditions and well quasi-orders ⋮ Unnamed Item ⋮ Type-Based Termination with Sized Products ⋮ The Ideal Approach to Computing Closed Subsets in Well-Quasi-orderings ⋮ Strong WQO Tree Theorems ⋮ Well quasi orders in a categorical setting ⋮ A Computation of the Maximal Order Type of the Term Ordering on Finite Multisets ⋮ Well rewrite orderings and well quasi-orderings ⋮ Proof-theoretic investigations on Kruskal's theorem ⋮ Mind change complexity of inferring unbounded unions of restricted pattern languages from positive data ⋮ A Tutorial on Type-Based Termination ⋮ The computable dimension of trees of infinite height ⋮ Simple termination revisited ⋮ Ordinals. I: Basic notions ⋮ Ordinals. II: Some applications and a functorial approach ⋮ From Kruskal’s theorem to Friedman’s gap condition ⋮ Invariants, patterns and weights for ordering terms ⋮ Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\) ⋮ An ordinal calculus for proving termination in term rewriting

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Orderings for term-rewriting systems
• On the recursive decomposition ordering with lexicographical status and other related orderings
• Harvey Friedman's research on the foundations of mathematics
• Termination of rewriting
• Using unavoidable set of trees to generalize Kruskal's theorem
• On multiset orderings
• Well rewrite orderings and well quasi-orderings
• Well quasi-ordered sets
• Proof theory and ordinal analysis
• Konstruktiver Aufbau eines Abschnitts der zweiten Cantorschen Zahlenklasse
• Slow growing versus fast growing
• The slow-growing and the Graegorczyk hierarchies
• Which set existence axioms are needed to prove the Cauchy/Peano theorem for ordinary differential equations?
• Natural well-orderings
• Ordinal numbers and the Hilbert basis theorem
• Proving termination with multiset orderings
• Π12-logic, Part 1: Dilators
• Accessible Independence Results for Peano Arithmetic
• Normal functions and constructive ordinal notations
• Systems of predicative analysis
• Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture
• The Universe of Set Theory
• Ordering by Divisibility in Abstract Algebras
• On the restricted ordinal theorem

This page was built for publication: What's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theory