The uniform Kruskal theorem over RCA$_0$
Patrick Uftring
TL;DR
This work shows that the uniform Kruskal theorem (UKT) is equivalent to $\Pi^1_1$-comprehension over the base system RCA$_0$ without relying on CAC. The authors refine Girard's arithmetical comprehension characterization by isolating a restricted class of well orders for which the exponentiation map $\alpha \mapsto 2^\alpha$ preserves well orders, enabling a direct RCA$_0$ derivation of the equivalence. The approach builds a chain from IPP via a normal WPO-dilator $V_\alpha$, through an exponentiation-based refinement, to a Kruskal fixed point construction that yields the necessary embeddings and well-foundedness results. The paper also clarifies the role of WKL in this framework, showing that no PO-dilator-based characterization of WKL matches UKT within RCA$_0$, thus establishing a sharp separation in the Reverse Mathematics landscape and linking UKT to ACA$_0$-strength in a refined setting. Overall, the results connect uniform Kruskal theory with arithmetical and higher-type comprehension, while solidifying the proof-theoretic position of UKT relative to Bachmann–Howard-type fixed points.
Abstract
Kruskal's theorem famously states that finite trees (ordered using an infima-preserving embeddability relation) form a well partial order. Freund, Rathjen, and Weiermann extended this result to general recursive data types with their uniform Kruskal theorem. They do not only show that this principle is true but also, in the context of reverse mathematics, that their theorem is equivalent to ${Π^1_1}$-comprehension, the characterizing axiom of ${Π^1_1\textsf{-CA}_0}$. However, their proof is not carried out directly over ${\textsf{RCA}_0}$, the usual base system of reverse mathematics. Instead, it additionally requires a weak consequence of Ramsey's theorem for pairs and two colors: the chain antichain principle. In this article, we show that this additional assumption is not necessary and the considered equivalence between the uniform Kruskal theorem and $Π^1_1$-comprehension already holds over ${\textsf{RCA}_0}$. For this, we improve Girard's characterization of arithmetical comprehension using ordinal exponentiation by showing that his result even remains correct if only a certain subclass of well orders is considered.