理论的$Π^1_2$结果
The $Π^1_2$ Consequences of a Theory
摘要：
我们开发了一个抽象的框架，证明理论分析的范围超出序数的理论，从而在一个模拟的序数分析，旨在研究定理的复杂性$Π^1_2$。这是通过在线性序范畴中用特别一致的、良好基保持函子来取代序数的使用来实现的。推广了证明论序数的概念，我们定义了一个理论的函子$Π^1_2$范数，并证明了它的存在性和唯一性$Π^1_2$ -健全的理论。由此，我们进一步抽象出一个定义的$Σ^1_2$ -和$Π^1_2$ -健全序数的理论，这些量化，分别是最大强度的真正的$Σ^1_2$定理和最小强度的假$Π^1_2$定理的一个给定的理论。我们研究这些序数，发展一个证明理论的分类理论的递归可扩展的$\mathsf{ACA}_0$使用技术从无穷大和范畴的证明论，广义递归论，构造性，和强迫，我们证明了一个允许的序数是$Π^1_2$ -健全序数的一些递归可扩展的$\mathsf{ACA}_0$当且仅当它不是参数自由的$Σ^1_1$ -反映。我们证明了$\mathsf{ACA}_0$的$Σ^1_2$ -健全序数是$ω_1^{ck}$，并刻画了$Π^1_1{-}\mathsf{CA}_0$的递归可列、$Σ^1_2$ -健全扩展的$Σ^1_2$ -健全序数.
英文摘要：
We develop the abstract framework for a proof-theoretic analysis of theories with scope beyond ordinal numbers, resulting in an analog of Ordinal Analysis aimed at the study of theorems of complexity $Π^1_2$. This is done by replacing the use of ordinal numbers by particularly uniform, wellfoundedness preserving functors in the category of linear orders. Generalizing the notion of a proof-theoretic ordinal, we define the functorial $Π^1_2$ norm of a theory and prove its existence and uniqueness for $Π^1_2$-sound theories. From this, we further abstract a definition of the $Σ^1_2$- and $Π^1_2$-soundness ordinals of a theory; these quantify, respectively, the maximum strength of true $Σ^1_2$ theorems and minimum strength of false $Π^1_2$ theorems of a given theory. We study these ordinals, developing a proof-theoretic classification theory for recursively enumerable extensions of $\mathsf{ACA}_0$ Using techniques from infinitary and categorical proof theory, generalized recursion theory, constructibility, and forcing, we prove that an admissible ordinal is the $Π^1_2$-soundness ordinal of some recursively enumerable extension of $\mathsf{ACA}_0$ if and only if it is not parameter-free $Σ^1_1$-reflecting. We show that the $Σ^1_2$-soundness ordinal of $\mathsf{ACA}_0$ is $ω_1^{ck}$ and characterize the $Σ^1_2$-soundness ordinals of recursively enumerable, $Σ^1_2$-sound extensions of $Π^1_1{-}\mathsf{CA}_0$.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
