可证明更好的拟序
摘要：强公理系统如$ACA_0$不能证明三元素反链是更好的拟序。在本文中，我们给出了在这种公理系统中可证明是拟序的有限偏序的完全刻画。该结果也将推广到无限序中。作为应用，我们推导出一个版本的最小坏数组引理在$ACA_0$上是弱的。与此形成鲜明对比的是，最近的一项结果表明，相同版本的最小坏数组引理在更强的基础理论$ATR_0$上与$Pi^1_2$-可理解性等价。
作者：Anton Freund, Alberto Marcone, Fedor Pakhomov, and Giovanni Sold`a
论文ID：2305.01066
分类：Logic
分类简称：math.LO
提交时间：2023-05-03