论文标题
统一的Kruskal定理：有限的组合和强度的存在之间
The uniform Kruskal theorem: between finite combinatorics and strong set existence
论文作者
论文摘要
统一的Kruskal定理将树木的原始结果扩展到一般递归数据类型。如A. Freund，M。Rathjen和A. Weiermann所示，它相当于$π^1_1 $ -COMPREANES，超过$ \ Mathsf {rca_0} $，具有链反式原理（$ \ MATHSF {CAC} $）。该结果提供了有限组合和抽象集存在之间的联系。目前的纸张进一步阐明了这种连接。首先，我们表明原始的Kruskal定理等于有限生成的数据类型的均匀版本。其次，我们证明了统一Kruskal定理的自然变体的二分法结果。一方面，此变体仍然意味着$π^1_1 $ -compreension在$ \ mathsf {rca} _0+\ mathsf {cac} $上。另一方面，当$ \ mathsf {cac} $从基本理论中删除时，它会变得薄弱。
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 $Π^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 $Π^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.
