一个理论的 $\Pi^1_2$ 推论

我们为超出序数范围的理论的证明论分析开发了抽象框架，得到了旨在研究复杂度为 $\Pi^1_2$ 的定理的序数分析的类似物。这是通过用线性序范畴中保持良基性的特别一致的函子替代序数的使用来实现的。推广证明论序数的概念，我们定义了理论的函子式 $\Pi^1_2$ 范数，并证明了其对 $\Pi^1_2$-可靠理论的存在性和唯一性。由此，我们进一步抽象出理论的 $\Sigma^1_2$-和 $\Pi^1_2$-可靠性序数的定义；它们分别量化了给定理论的真 $\Sigma^1_2$ 定理的最大强度和假 $\Pi^1_2$ 定理的最小强度。我们研究这些序数，为 $\mathsf{ACA}_0$ 的递归可枚举扩张发展证明论分类理论。利用来自无穷证明论与范畴证明论、广义递归论、可构造性和力迫的技术，我们证明了一个可容许序数是某个 $\mathsf{ACA}_0$ 的递归可枚举扩张的 $\Pi^1_2$-可靠性序数，当且仅当它不是无参数 $\Sigma^1_1$-反射的。我们证明了 $\mathsf{ACA}_0$ 的 $\Sigma^1_2$-可靠性序数是 $\omega_1^{ck}$，并刻画了 $\Pi^1_1{-}\mathsf{CA}_0$ 的递归可枚举、$\Sigma^1_2$-可靠扩张的 $\Sigma^1_2$-可靠性序数。