Proof theory for higher pointclasses
Various logicians observed that the consistency strength comparison is well-ordered and coincides with comparing arithmetical and projective consequences for natural theories. The primary goal of my dissertation is to establish results that justify this observation and to produce results suggesting that various methods for comparing the strength of theories are instances of a single, general framework. Walsh (“An incompleteness theorem via ordinal analysis”. In: The Journal of Symbolic Logic (2022), pp. 1–17.) proved that comparing $\Pi^1_1$-consequences modulo true $\Sigma^1_1$-sentences is equivalent to comparing proof-theoretic ordinals and comparing the $\Pi^1_1$-version of consistency comparison, namely, $\Pi^1_1$-reflection comparison. In Chapter 1, I will prove that $\Sigma^1_2$-consequence comparison is equivalent to comparing the $\Sigma^1_2$-proof-theoretic ordinal $s^1_2(T)$ introduced by Aguilera-Pakhomov (“The $\Pi^1_2$ consequences of a theory”. In: J. Lond. Math. Soc. (2) 107.3 (2023), pp. 1045–1073.) and $\Sigma^1_2$-reflection comparison. This will be further generalized in Chapter 5 by showing that assuming Projective Determinacy, for a projective pointclass $\Gamma$ admitting the prewellordering property (i.e., $\Gamma = \Pi^1_3,\Sigma^1_4$, etc.), $\Gamma$-consequence comparison modulo true $\check{\Gamma}$-sentences is prewellordered and is equivalent to the $\Gamma$-reflection comparison. In Chapter 3, I will prove how Pohlers' performance ordinal is associated with Girard's $\Pi^1_2$-proof theory. Briefly, Pohlers' characteristic ordinal is a generalized proof-theoretic ordinal computed over expansions of $\mathbb{N}$ with definable reals, typically a $\Sigma^1_2$-singleton real. Girard's $\Pi^1_2$-proof theory computes a proof-theoretic dilator $|T|_{\Pi^1_2}$ encoding the $\Pi^1_2$-consequences of the theory. I will prove in this chapter that Pohlers' characteristic ordinals are instances of Girard's proof-theoretic dilator. Inner model theorists use mice to gauge the strength of theories, which are transitive models with an additional structure indicating how to iterate the model. Chapters 2 and 4 correspond to the first step towards a larger program of ranking theories via mice. We will examine how to rank theories via their well-founded models or $\beta$-models in Chapter 2. In Chapter 4, I will construct a measurable dilator by analyzing Martin's proof of $\mathbf{\Pi}^1_2$-determinacy from a rank-into-rank cardinal, which isolates a large-cardinal object encapsulating $\mathbf{\Pi}^1_2$-determinacy. Its construction is suspected to be related to the construction of higher versions of transitive models, or EM models, introduced by Ressayre (“$\Pi^1_2$-logic and uniformization in the analytical hierarchy”. In: Arch. Math. Logic 28.2 (1989), pp. 99–117.), corresponding to sharps. This dissertation makes extensive use of the theory of dilators and ptykes. Hence, I will also provide the development of the basic theory of dilators and ptykes.