Proof-Theoretic Relations between Higman's and Kruskal's theorem, and Independence Results for Tree-like Structures

TL;DR

This paper explores the proof-theoretic connections between Higman's lemma and Kruskal's theorem within reverse mathematics, and presents independence results for complex tree-like structures that challenge standard arithmetic systems.

Contribution

It clarifies the formal relationship between Higman's and Kruskal's theorems and establishes independence results for certain tree structures from Peano and second-order arithmetic.

Findings

Higman's lemma is a special case of Kruskal's theorem within reverse mathematics.

Certain tree-like structures involving Ackermannian and exponential terms are independent of Peano arithmetic.

The equivalence between Higman's and Kruskal's theorems is formally analyzed in the base system RCA_0.

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.