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

Question

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.)

Answer 1

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.)

This does not say anything about "reverse mathematics" in this context, and indeed I don't see anything resembling it here. I don't know whether Richard Shore's set-up can be made to work here.