English

The uniform Kruskal theorem over RCA$_0$

Logic 2025-02-07 v1

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 Π11{\Pi^1_1}-comprehension, the characterizing axiom of Π11-CA0{\Pi^1_1\textsf{-CA}_0}. However, their proof is not carried out directly over RCA0{\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 Π11\Pi^1_1-comprehension already holds over RCA0{\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.

Cite

@article{arxiv.2502.03978,
  title  = {The uniform Kruskal theorem over RCA$_0$},
  author = {Patrick Uftring},
  journal= {arXiv preprint arXiv:2502.03978},
  year   = {2025}
}
R2 v1 2026-06-28T21:34:39.626Z