The uniform Kruskal theorem: between finite combinatorics and strong set existence
Anton Freund, Patrick Uftring · Philosophical Transactions of the Royal Society A Mathematical Physical and Engineering Sciences · 2023
, 108265 (doi:10.1016/j.aim.2022.108265)), it is equivalent to [Formula: see text]-comprehension, over [Formula: see text] with the ascending descending sequence principle ([Formula: see text]). This result provides a connection between finite combinatorics and abstract set existence. The present article sheds further light on this connection. Firstly, 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 [Formula: see text]-comprehension over [Formula: see text] extended by the chain antichain principle ([Formula: see text]). On the other hand, it becomes weak when [Formula: see text] is removed from the base theory. This article is part of the theme issue 'Modern perspectives in Proof Theory'.