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

arXiv2208.00209MaRDI QIDQ6406535FDOQ6406535

Anton Freund, Patrick Uftring

Publication date: 30 July 2022

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 $P{i}_1^1$-comprehension, over $mathsfRC{A}_0$ with the chain antichain principle ($mathsfCAC$). 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 $P{i}_1^1$-comprehension over $mathsf{RCA}_0+mathsfCAC$. On the other hand, it becomes weak when $mathsfCAC$ is removed from the base theory.

Mathematics Subject Classification ID

Trees (05C05) Combinatorics of partially ordered sets (06A07) Foundations of classical theories (including reverse mathematics) (03B30) Second- and higher-order arithmetic and fragments (03F35)

This page was built for publication: The uniform Kruskal theorem: between finite combinatorics and strong set existence

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6406535)