Second order theories with ordinals and elementary comprehension (Q1908814): Difference between revisions

We study elementary second-order extensions of the theory \(\text{ID}_1\) of noniterated inductive definitions and the theory \(\text{PA}_\Omega\) of Peano arithmetic with ordinals. We determine the exact proof-theoretic strength of those extensions and their natural subsystems, and we relate them to subsystems of analysis with arithmetic comprehension plus \(\Pi^1_1\) comprehension and bar induction without set parameters.