The uniform Kruskal theorem: between finite combinatorics and strong set existence

TL;DR

This paper explores the uniform Kruskal theorem's extension to recursive data types, revealing its deep connection to strong set existence principles like -comprehension and analyzing its logical strength and variations.

Contribution

It demonstrates the equivalence of the original Kruskal theorem to its uniform version for finitely generated data types and establishes a dichotomy for a variant of the uniform Kruskal theorem.

Findings

Original Kruskal theorem is equivalent to the uniform version for finitely generated data types.

A natural variant of the uniform Kruskal theorem either implies -comprehension or becomes weak without -CA.

The results connect finite combinatorics with strong set existence principles.

Abstract

The uniform Kruskal theorem extends the original result for trees to general recursive data types. As shown by A. Freund, M. Rathjen and A. Weiermann, it is equivalent to $\Pi^1_1$-comprehension, over $\mathsf{RCA_0}$ with the chain antichain principle ($\mathsf{CAC}$). This result provides a connection between finite combinatorics and abstract set existence. The present paper sheds further light on this connection. First, we show that the original Kruskal theorem is equivalent to the uniform version for data types that are finitely generated. Secondly, we prove a dichotomy result for a natural variant of the uniform Kruskal theorem. On the one hand, this variant still implies $\Pi^1_1$-comprehension over $\mathsf{RCA}_0+\mathsf{CAC}$. On the other hand, it becomes weak when $\mathsf{CAC}$ is removed from the base theory.