Higher recursion theory and reverse mathematics: What is to $\Pi^1_1-CA_0$ as $RCA_0$ is to $ACA_0$?

There is an extremely rich and well-understood analogy between "recursively enumerable" and "$\Pi^1_1$" - indeed, this is the starting point of metarecursion theory, and $\alpha$-recursion theory in general (see Sacks' wonderful book http://projecteuclid.org/DPubS?verb=Display&version=1.0&service=UI&handle=euclid.pl/1235422632&page=record).

I'm interested in whether there is a straightforward reverse mathematical analogy to be made here, as well. Specifically, we usually think of $RCA_0$ and $ACA_0$ as "recursive comprehension" and "recursively enumerable comprehension," respectively; I'm wondering if there is a theory $T$ such that we can - in a similar way - think of $T$ as "metarecursive comprehension" and $\Pi^1_1-CA_0$ as "metarecursively enumerable comprehension."

A natural candidate for that theory might be $\Delta^1_1-CA_0$, but that's not quite right: in the metarecursive context, $\Delta^1_1$ corresponds to finite (since intuitively everything is relative to Kleene's $\mathcal{O}$). I've been thinking that the right $T$ here is $ATR_0$, but I don't really have any serious reason to back that up.

My instinct is that this is not really the right question - metarecursion theory doesn't live on $\omega$, it lives on $\omega_1^{CK}$, so the right thing to do is formulate a version of reverse math on $\omega_1^{CK}$ (in fact, Richard Shore http://www.math.cornell.edu/~shore/papers/pdf/RMComp7.pdf has already done this for cardinals, and I don't see anything preventing his work extending to arbitrary admissible ordinals - although his theorems might not, of course, since they may require more admissiblity than $\Sigma_1$). But I'm still holding out hope that there's something neat that can happen already on $\omega$.

(I've tagged "descriptive-set-theory" because of the deep connections between higher recursion theory and descriptive set theory, but if anyone feels that that's too much of a reach here, feel free to untag.)

• Since metarecursive + bounded = metafinite, for subsets of $\omega$, $\Delta^1_1$ corresponds to both computable and finite. So I think you're right that to get a real analogy to ACA$_0$/RCA$_0$, we need to work in $\omega_1^{\text{ck}}$. Perhaps a better analogue to $\Pi^1_1$-CA$_0$ (on $\omega$) is not $\Sigma^0_1$-comprehension but $\Sigma^0_1$-induction, in the form of bounded $\Sigma^0_1$-comprehension. Jun 10 '14 at 15:55
• @Denis, good idea. But when you talk about induction, you need a well ordering. My vague ideal is that infinitary logic might be a right way to make this sense.
– 喻 良
Jun 10 '14 at 22:16
• @Liang Yu: What I meant is, forget about induction, and instead think of bounded $\Sigma^0_1$-comprehension, which is equivalent to $\Sigma^0_1$-induction. But yes, it would be nice if there's a way to think of this as actual induction. Jun 10 '14 at 23:15

I am getting the feeling there is some slight miss-match of terminology, or perhaps application of terminology is a better way of putting it? It is true that the (lightface) $\Pi^1_1-CA_0$ sets of integers correspond to the meta-r.e. sets of integers, but as you say, the old meta-recursion theory lies on $\omega_1^{ck}$. So it should really be about sets of ordinals rather than integers. However then one is really talking about $\Delta_1$-recursions over $(L_{\omega_1^{ck}},\in)$, and then the $\omega^{ck}_1$-r.e. sets are those $\Sigma_1(L_{\omega_1^{ck}},\in)$. Using a theorem of Kleene the restriction of the latter to sets of integers are indeed precisely the (lightface) $\Pi^1_1-CA_0$ sets of integers.
I think the link with descriptive set theory comes through Kleene Recursion - not much studied these days but arises as a higher type recursion theory on $\omega$ and $\omega^\omega$. Restricting it to integers, yields that the Kleene-r.e. sets are the $\Pi^1_1$ sets of integers (so again those defined in a $\Sigma_1(L_{\omega_1^{ck}},\in)$ way). Kleene recursive sets of integers correspond to those in $HYP$. Including the reals, and working at the higher type, then Kleene rec. sets corresponds to Borel and Kleene-r.e. to (boldface) co-analytic.
The axioms', $T$, for Kleene recursion are his rules for an equational calculus for recursion on integers and reals, extending his equational calculus for the ordinary general recursive functions. (See, I think P. Hinman, Recursion Theoretic Hierarchies, Springer Omega Series, 1978, but also the chapter about higher type recursions in general by Dag Normann in Turing's Legacy, Ed. R. Downey, ASL Series in Math.Logic,vol 42, May 2104); in my chapter Transfinite Machine Models, in the same volume some particular facts about Kleene Recursion are summarized.)
• Thanks, this looks like it answers my question. One quick question, though: when you talk about Kleene recursion, are you talking about Kleene recursion relative to the equality predicate ${}^2\exists$ for reals, that is, "normal" recursion? Jun 10 '14 at 19:34