Proof-Theoretic Relations between Higman's and Kruskal's theorem, and Independence Results for Tree-like Structures
Gabriele Buriola, Andreas Weiermann
TL;DR
This work clarifies the proof-theoretic relationships between Higman’s and Kruskal’s theorems within reverse mathematics, establishing over RCA$_0$ the equivalence between the finite versions HT$(n)$ and KT$_\ell(n)$ and between the infinite versions HT$(\omega)$ and KT$_\ell(\omega)$. By formalizing ordered algebras and labelled trees, the authors bridge the algebraic and tree-embedding viewpoints, and derive nontrivial separations such as KT$_\ell(\omega)$ not implying $\forall n\ KT_\ell(n)$ within RCA$_0$. The paper also analyzes the Higman–Dickson relationship, providing strong ordinal analyses (e.g., $\varepsilon_0$ and beyond) and presents independence results for tree-like structures built from Ackermannian and exponential terms, showing certain well-foundedness properties are unprovable in PA or ATR$_0$. Collectively, these results map the logical strength of core wqo principles and illuminate the landscape of reverse mathematics, ordinal analysis, and foundational aspects of termination and proof theory. The work also points to future directions including labelled Kruskal variants and deeper PN$^1_2$RFNBI$_0$-style classifications.
Abstract
Higman's lemma and Kruskal's theorem are two of the most celebrated results in the theory of well quasi-orders. In his seminal paper G. Higman obtained what is known as Higman's lemma as a corollary of a more general theorem, dubbed here Higman's theorem. While the lemma deals with finite sequences over a well quasi-order, the theorem is about abstract operations of arbitrary high arity. J.B. Kruskal was fully aware of this broader framework: in his seminal paper, he not only applied Higman's lemma at crucial points of his proof but also followed Higman's proof schema. At the conclusion of the paper, Kruskal noted that Higman's theorem is a special case, restricted to trees of finite degree, of his own tree theorem. Although he provided no formal reduction, he included a glossary translating concepts between the tree and algebraic settings. The equivalence between these versions was later clarified by D. Schmidt and M. Pouzet. In this work, we revisit that equivalence to illuminate the proof-theoretical relationships between the two theorems within the base system $RCA_0$, of reverse mathematics. Moreover, some independence results over first- and second-orders are treated. In particular, tree-like structures, involving either Ackermannian terms or exponential expressions, are studied unveiling well-foundedness properties that are independent from Peano arithmetic and relevant fragments of second-order arithmetic.