论文标题
最小的不良序列对于统一的Kruskal定理是必需的
Minimal bad sequences are necessary for a uniform Kruskal theorem
论文作者
论文摘要
由于纳什·威廉姆斯（Nash-Williams）而引起的最小不良序列参数是对理论计算机科学具有重要意义的组合学工具的强大工具。特别是，它提供了克鲁斯卡定理的非常优雅的证明。同时，众所周知，克鲁斯卡（Kruskal）的定理不需要最小的不良序列论点的全部强度。在反向数学的框架中，可以精确地提出这种说法，在这种框架的框架中，最小不良序列的存在等效于一种称为$π^1_1 $ - comprexension的原则，这比Kruskal的定理强得多。在本文中，我们通过将克鲁斯卡尔定理的统一版本相互关联到良好的部分订单的某些转换。我们表明，$π^1_1 $ -COMPERENIS等同于我们统一的Kruskal定理（超过$ \ Mathbf {rca} _0 $以及链 - 安提卡林原理）。这意味着，统一的克鲁斯卡定理的任何证据都必须需要最小的不良序列。作为我们调查的副产品，我们获得了几种Kruskal型独立性结果的统一证明。
The minimal bad sequence argument due to Nash-Williams is a powerful tool in combinatorics with important implications for theoretical computer science. In particular, it yields a very elegant proof of Kruskal's theorem. At the same time, it is known that Kruskal's theorem does not require the full strength of the minimal bad sequence argument. This claim can be made precise in the framework of reverse mathematics, where the existence of minimal bad sequences is equivalent to a principle known as $Π^1_1$-comprehension, which is much stronger than Kruskal's theorem. In the present paper we give a uniform version of Kruskal's theorem by relativizing it to certain transformations of well partial orders. We show that $Π^1_1$-comprehension is equivalent to our uniform Kruskal theorem (over $\mathbf{RCA}_0$ together with the chain-antichain principle). This means that any proof of the uniform Kruskal theorem must entail the existence of minimal bad sequences. As a by-product of our investigation, we obtain uniform proofs of several Kruskal-type independence results.
