关于Nash-Williams超限序列定理的逻辑强度
On the logical strength of Nash-Williams' theorem on transfinite sequences
摘要：
我们证明了Nash-Williams定理，即由可嵌入性排序的更好拟序的元素的可数超限序列形成更好拟序，在二阶算术Pi^1_1-CA_0的子系统中是可证明的，但不等价于Pi^1_1-CA_0.我们在较弱子系统ATR_0中获得了该定理证明的一些部分结果，并且我们表明wqo和bqo理论典型的极小性引理隐含Pi ^1_1-CA_0，因此不能用于这样的证明。
英文摘要：
We show that Nash-Williams' theorem asserting that the countable transfinite sequences of elements of a better-quasi-ordering ordered by embeddability form a better-quasi-ordering is provable in the subsystem of second order arithmetic Pi^1_1-CA_0 but is not equivalent to Pi^1_1-CA_0. We obtain some partial results towards the proof of this theorem in the weaker subsystem ATR_0 and we show that the minimality lemmas typical of wqo and bqo theory imply Pi^1_1-CA_0 and hence cannot be used in such a proof.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
