Reverse mathematics of a uniform Kruskal-Friedman theorem

TL;DR

This paper explores the reverse mathematical strength of a uniform version of the Kruskal-Friedman theorem, extending it to recursive data types and linking it to advanced logical principles.

Contribution

It establishes the equivalence of the uniform Kruskal-Friedman theorem with $ ext{Pi}^1_1$-transfinite recursion and a minimal bad sequence principle over RCA_0.

Findings

The uniform Kruskal-Friedman theorem is equivalent to $ ext{Pi}^1_1$-transfinite recursion.

It extends the original theorem from trees to general recursive data types.

Provides insights into the role of infinity in finite combinatorics.

Abstract

The Kruskal-Friedman theorem asserts: in any infinite sequence of finite trees with ordinal labels, some tree can be embedded into a later one, by an embedding that respects a certain gap condition. This strengthening of the original Kruskal theorem has been proved by I. K\v{r}\'i\v{z} (Ann. Math. 1989), in confirmation of a conjecture due to H. Friedman, who had established the result for finitely many labels. It provides one of the strongest mathematical examples for the independence phenomenon from G\"odel's theorems. The gap condition is particularly relevant due to its connection with the graph minor theorem of N. Robertson and P. Seymour. In the present paper, we consider a uniform version of the Kruskal-Friedman theorem, which extends the result from trees to general recursive data types. Our main theorem shows that this uniform version is equivalent both to $\Pi^1_1$-transfinite recursion and to a minimal bad sequence principle of K\v{r}\'i\v{z}, over the base theory $\mathsf{RCA_0}$ from reverse mathematics. This sheds new light on the role of infinity in finite combinatorics.