arXiv2021
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$.