Wellfoundedness proof with the maximal distinguished set

TL;DR

This paper demonstrates that a specific second-order arithmetic system can prove the wellfoundedness of certain large ordinals, extending the understanding of proof-theoretic bounds within set theory and second-order arithmetic.

Contribution

It shows that $ ext{Σ}^{1-}_{2} ext{-CA}+ ext{Π}^{1}_{1} ext{-CA}_0$ proves wellfoundedness up to certain large ordinals, linking second-order arithmetic with set-theoretic proof bounds.

Findings

Proves wellfoundedness up to $oldsymbol{ ext{ψ}}_{oldsymbol{ ext{Ω}}_1}(oldsymbol{ ext{ε}}_{oldsymbol{ ext{Ω}}_{oldsymbol{ ext{S}}+N+1}})$ for each $N$.

Establishes interpretability of the second-order system in set theory.

Extends proof-theoretic analysis of large ordinals.

Abstract

In arXiv:2208.12944 it is shown that an ordinal $\sup_{N<\omega}\psi_{\Omega_{1}}(\varepsilon_{\Omega_{\mathbb{S}+N}+1})$ is an upper bound for the proof-theoretic ordinal of a set theory ${\sf KP}\ell^{r}+(M\prec_{\Sigma_{1}}V)$. In this paper we show that a second order arithmetic $\Sigma^{1-}_{2}\mbox{-CA}+\Pi^{1}_{1}\mbox{-CA}_{0}$ proves the wellfoundedness up to $\psi_{\Omega_{1}}(\varepsilon_{\Omega_{\mathbb{S}+N+1}})$ for each $N$. It is easy to interpret $\Sigma^{1-}_{2}\mbox{-CA}+\Pi^{1}_{1}\mbox{-CA}_{0}$ in ${\sf KP}\ell^{r}+(M\prec_{\Sigma_{1}}V)$.