9
$\begingroup$

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.

Thanks in advance.

$\endgroup$
2
$\begingroup$

I don't have complete answer but I think that my remarks still may be useful.

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.

$\endgroup$
2
  • $\begingroup$ 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$. $\endgroup$ – Wojowu Oct 12 '15 at 17:41
  • $\begingroup$ 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. $\endgroup$ – Fedor Pakhomov Oct 12 '15 at 17:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.