Proof-theoretic dilator and intermediate pointclasses
Hanul Jeon
TL;DR
This work reveals a systematic entanglement between Girard's $\Pi^1_2$-proof theory and Pohlers' ordinal analysis via Spector classes, by introducing genedendrons as a bridge between dilators and $R$-recursive well-orders. The main theorem shows that for a $\Pi^1_2$-sound theory $T$ and a recursive locally well-founded genedendron $(D,\varrho)$ generating a $\Sigma^1_2$-singleton $R$, if an $R$-recursive order $\alpha$ renders $D_\alpha$ ill-founded, then $|T|_{\Pi^1_2}(\alpha)$ equals $|T[R] + \mathsf{WO}(\alpha)|_{\Pi^1_1[R]}$, connecting $\Pi^1_2$-dilator data to $\Pi^1_1[R]$-ordinal data. The authors compute the $\Sigma^1_2$-altitude of the hyperjump, showing Alt$_{\Sigma^1_2}(\mathsf{HJ}(\emptyset)) = \omega_1^{\mathrm{CK}}$, and prove Pohlers-type equivalences linking iterated Spector classes to hyperjumps: $\mathsf{SP}^{\xi+1}_\mathbb{N} = \Pi^1_1[\mathsf{HJ}^{\xi}(\emptyset)]$ for $\xi < \text{least recursively inaccessible}$. The framework culminates in a concrete method to derive $\Pi^1_1[R]$ consequences from $\Pi^1_2$ and $\Sigma^1_2$ data, offering a path to higher-level analyses via generalized genedendrons and ${\text{b}}$-logics. Overall, the paper advances the synthesis of two pillars of proof theory, enriching the toolbox for analyzing intermediate pointclasses and their interaction with transfinite constructs.
Abstract
There are two major generalizations of the standard ordinal analysis: One is Girard's $Π^1_2$-proof theory in which dilators are assigned to theories instead of ordinals. The other is Pohlers' generalized ordinal analysis with Spector classes, where ordinals greater than $ω_1^{\mathsf{CK}}$ are assigned to theories. In this paper, we show that these two are systematically entangled, and $Σ^1_2$-proof theoretic analysis has a critical role in connecting these two.