The π21$\Pi ∧1_2$ consequences of a theory

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 Pi(1)(2). 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 Pi(1)(2) norm of a theory and prove its existence and uniqueness for Pi(1)(2)-sound theories. From this, we further abstract a definition of the Sigma(1)(2)- and Pi(1)(2)-soundness ordinals of a theory; these quantify, respectively, the maximum strength of true Sigma(1)(2) theorems and minimum strength of false Pi(1)(2) theorems of a given theory. We study these ordinals, developing a proof-theoretic classification theory for recursively enumerable extensions of ACA(0). Using techniques from infinitary and categorical proof theory, generalized recursion theory, constructibility, and forcing, we prove that an admissible ordinal is the Pi(1)(2)-soundness ordinal of some recursively enumerable extension of ACA(0) if and only if it is not parameter-free Sigma(1)(1)-reflecting. We show that the Sigma(1)(2)-soundness ordinal of ACA(0) is omega(CK)(1) and characterize the Sigma(1)(2)-soundness ordinals of recursively enumerable, Sigma(1)(2)-sound extensions of Pi(1)(1)-CA.