The uniform Kruskal theorem over RCA ₀

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 [Formula: see text]-comprehension, the characterizing axiom of [Formula: see text]. However, their proof is not carried out directly over 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 paper, we show that this additional assumption is not necessary and the considered equivalence between the uniform Kruskal theorem and [Formula: see text]-comprehension already holds over 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.