J. P. Aguilera, & Pakhomov, F. (2023). The Π1₂ consequences of a theory. Journal of the London Mathematical Society, 107(3), 1045–1073. https://doi.org/10.1112/jlms.12707
We develop the abstract framework for a proof-theoretic analysis of theories with scope beyond the ordinal numbers, resulting in an analog of ordinal analysis aimed at the study of theorems of complexity (Formula presented.). This is done by replacing the use of ordinal numbers by particularly uniform, wellfoundedness preserving functors on the category of linear orders. Generalizing the notion of a proof-theoretic ordinal, we define the functorial (Formula presented.) norm of a theory and prove its existence and uniqueness for (Formula presented.) -sound theories. From this, we further abstract a definition of the (Formula presented.) - and (Formula presented.) -soundness ordinals of a theory; these quantify, respectively, the maximum strength of true (Formula presented.) theorems and minimum strength of false (Formula presented.) theorems of a given theory. We study these ordinals, developing a proof-theoretic classification theory for recursively enumerable extensions of (Formula presented.). Using techniques from infinitary and categorical proof theory, generalized recursion theory, constructibility, and forcing, we prove that an admissible ordinal is the (Formula presented.) -soundness ordinal of some recursively enumerable extension of (Formula presented.) if and only if it is not parameter-free (Formula presented.) -reflecting. We show that the (Formula presented.) -soundness ordinal of (Formula presented.) is (Formula presented.) and characterize the (Formula presented.) -soundness ordinals of recursively enumerable, (Formula presented.) -sound extensions of (Formula presented.) - (Formula presented.).
