The uniform Kruskal theorem over RCA$_0$

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 ${\Pi^1_1}$-comprehension, the characterizing axiom of ${\Pi^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 $\Pi^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.