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 [Link](https://web.archive.org/web/20200813160253/https://projecteuclid.org/euclid.pl/1235422632)).


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](http://www.math.cornell.edu/%7Eshore/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.)



Higher recursion theory and reverse mathematics: What is to $\Pi^1_1$-$CA_0$ as $RCA_0$ is to $ACA_0$?
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.


