Wellfoundedness proof with the maximal distinguished set
Toshiyasu Arai · arXiv (Cornell University) · 2022
In arXiv:2208.12944 it is shown that an ordinal $\sup_{N<ω}ψ_{Ω_{1}}(\varepsilon_{Ω_{\mathbb{S}+N}+1})$ is an upper bound for the proof-theoretic ordinal of a set theory ${\sf KP}\ell^{r}+(M\prec_{Σ_{1}}V)$. In this paper we show that a second order arithmetic $Σ^{1-}_{2}\mbox{-CA}+Π^{1}_{1}\mbox{-CA}_{0}$ proves the wellfoundedness up to $ψ_{Ω_{1}}(\varepsilon_{Ω_{\mathbb{S}+N+1}})$ for each $N$. It is easy to interpret $Σ^{1-}_{2}\mbox{-CA}+Π^{1}_{1}\mbox{-CA}_{0}$ in ${\sf KP}\ell^{r}+(M\prec_{Σ_{1}}V)$.