2021/09/23 by Aguilera, Juan P., Pakhomov, Fedor
#FOS: Mathematics #Logic (math.LO)
paper · doi:10.48550/arxiv.2109.11652
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 Π12. 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 Π12 norm of a theory and prove its existence and uniqueness for Π12-sound theories. From this, we further abstract a definition of the Σ12- and Π12-soundness ordinals of a theory; these quantify, respectively, the maximum strength of true Σ12 theorems and minimum strength of false Π12 theorems of a given theory. We study these ordinals, developing a proof-theoretic classification theory for recursively enumerable extensions of ACA0 Using techniques from infinitary and categorical proof theory, generalized recursion theory, constructibility, and forcing, we prove that an admissible ordinal is the Π12-soundness ordinal of some recursively enumerable extension of ACA0 if and only if it is not parameter-free Σ11-reflecting. We show that the Σ12-soundness ordinal of ACA0 is ω1ck and characterize the Σ12-soundness ordinals of recursively enumerable, Σ12-sound extensions of Π11-CA0.