# Proof-theoretic ordinals after liberalizing induction to $RCA_0$

This is kind of a follow-up to this question.

For a class $\Gamma$ of second-order formulas (here either $\Sigma_n^0$ or $\Sigma_n^1$), let $X\Gamma$ be a formal theory consisting of $RCA_0$ together with induction schema for formulas in $\Gamma$. In particular, $X\Sigma_0^1$ adds arithmetical induction, and let $RCA$ be $RCA_0$ with induction schema for all formulas.

What are the proof-theoretic ordinals of $X\Gamma$ and $RCA$?

The question linked at the top asks whether these theories have any additional strength comprehension-wise (OP there considers sets $\Sigma_n$, which I suspect meant $\Sigma_n^0$ there). I have asked under one answer what the PTOs of these theories are, and I was told that $X\Sigma_n^0$ has a PTO at least $\omega$ stacked $n+1$ times (which makes sense, because we are allowing "stacked quantifies" in provable part of PA), and I was advised to ask this as a separate question, so here it is.

I highly suspect that this was considered before, but it's hard to find any results.

Let me consider theory $\mathsf{NT}$ which extends $\mathsf{PRA}$ by one unary predicate $X$ and axiom scheme of induction in extended language and weaker theories $\mathsf{NT}_n$ in the same language but with induction scheme restricted to for $\Sigma^0_n(X)$-formulas (here $\Sigma^0_0(X)$-formulas are all the formulas from the language of $\mathsf{NT}$, where all quantifiers are bounded). The proof-theoretic ordinal $|\mathsf{NT}|$of $\mathsf{NT}$ (i.e. the limit of well-ordered order types of primitive-recursive binary relation for which $\mathsf{NT}$ proves transfinite induction for $X$) is equal to $\varepsilon_0$ (essentially it is ordinal analysis of $\mathsf{PA}$ in the terms used by W. Pohlers in his "Proof Theory. The First Step into Impredicativity", Chapter 7; Pohlers considered $\mathsf{NT}$ in the language with countable family of free unary predicates but it can't influence proof-theoretic ordinal).
Clearly, $$|\mathsf{X}\Sigma^0_n|\ge |\mathsf{NT}_n|,$$ $$|\mathsf{RCA}|\ge |\mathsf{X}\Sigma^1_n|\ge |\mathsf{NT}|.$$
Let me consider the interpretation of $\mathsf{RCA}_0$ in $\mathsf{NT}_1$ that encodes $\mathsf{RCA}_0$-sets by $\Delta^0_1(X)$-sets. This interpretation consists of $\Pi^0_2(X)$ definition of set of codes for $\mathsf{RCA}_0$-sets and $\Delta^0_1(X)$-interpretation of $\in$. Clearly, the same syntactical translation gives an interpretation of $\mathsf{X}\Sigma^0_n$ in $\mathsf{NT}_n$ and an interpretation of $\mathsf{RCA}$ in $\mathsf{NT}$.
This interpretations gives the following bounds: $$|\mathsf{X}\Sigma^0_n|\le |\mathsf{NT}_n|,$$ $$|\mathsf{RCA}|\le |\mathsf{NT}|.$$ Thus $|\mathsf{RCA}|=|\mathsf{X}\Sigma^1_n|=\varepsilon_0$. Also, $|\mathsf{X}\Sigma^0_n|= |\mathsf{NT}_n|$. There is natural conjecture that $|\mathsf{NT}_n|=\omega_{n+1}$, where $\omega_m$ is the tower of $\omega$-exponentiation of the height $m$. But I don't know whether it have been proved somewhere; Pohlers in Exercise 7.3.19(f) of the mentioned book asked the question about the upper bound for $|\mathsf{NT}_n|$ without definite conjecture about the answer.
• I don't think your upper bounds are correct: $\sf X\Sigma^1_0$ already includes full arithmetical induction (because $\Sigma^1_0$ is precisely the set of all arithmetical formulas), so $|\sf X\Sigma^1_n|\geq|\sf X\Sigma^1_0|\geq|sf NT|=\varepsilon_0$. – Wojowu Oct 12 '15 at 17:41
• Indeed, I weren't careful about definition of the class $\Sigma^1_n$; with $\Sigma^1_0=\bigcup \Sigma^0_n$ claimed interpretation of $\mathsf{X}\Sigma_n^1$ clearly wouldn't work. With this definition mentioned interpretation actually gives exact bound $\varepsilon_0$ for all the theories $\mathsf{X}\Sigma_n^1$. I'll edit my answer accordingly. – Fedor Pakhomov Oct 12 '15 at 17:59