The Π21$\Pi ^1_2$ consequences of a theory
Juan P. Aguilera, Fedor Nikolaevich Pakhomov · Journal of the London Mathematical Society · 2022
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 . 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 norm of a theory and prove its existence and uniqueness for -sound theories. From this, we further abstract a definition of the - and -soundness ordinals of a theory; these quantify, respectively, the maximum strength of true theorems and minimum strength of false theorems of a given theory. We study these ordinals, developing a proof-theoretic classification theory for recursively enumerable extensions of . Using techniques from infinitary and categorical proof theory, generalized recursion theory, constructibility, and forcing, we prove that an admissible ordinal is the -soundness ordinal of some recursively enumerable extension of if and only if it is not parameter-free -reflecting. We show that the -soundness ordinal of is and characterize the -soundness ordinals of recursively enumerable, -sound extensions of -.