Recursion theory in $\sf HC$ Let $\sf HF$ be the set of hereditarily finite sets. It is well known that one can define a theory of computable/recursive functions on $\sf HF$ (as opposed to working with $\omega^k$): a relation $R\subseteq \sf HF^n$ is decidable iff $R$ is a $\Delta_1$ subset of $(\sf HF,\in)$, and a function $f:\sf HF^n\to \sf HF$ is computable iff it is decidable as a subset of $\sf HF^{n+1}$.
By work of Ackermann, this approach turns out to be equivalent to the usual one, in the sense that one has a (computable) bijection $\Gamma:\sf HF\to \omega$ which can be used to translate between the two notions of computable and see that they are morally the same.
The usual selling point of working with $\sf HF$ is that no coding is necessary, for $\sf HF\times \sf HF\subset \sf HF$ and similarly $\sf HF^{<\omega}\subset \sf HF$.
Can this be reproduced at $\sf HC$, the set of hereditarly countable sets, i.e. get an alternative definition of the projective hierarchy of sets of reals? Two of the problems I see are:

*

*Every set in $\sf HC$ can be coded by a real, but the coding is slightly arbitrary (as opposed to the Ackermann function), since we need to say "fix $x\in \sf HC$, and let $f:\omega\to \text{trcl}(\{x\})$ be a bijection (ignore the finite case), transfer the $\in$-relation on $\text{trcl}(\{x\})$ to $\omega$, take the collapse, etc".

*A set of reals $A$ is $\underset{\sim}{\Sigma}_2^1$ iff it is $\Sigma_1$ definable over $\sf HC$.

So (2) shows that levels of definability are not directly comparable as they are in the $\sf HF$ case, presumably because everything in $\sf HF$ is $\Delta_0$ definable, but no such thing is true of $\sf HC$.
Is there any way of making a theory of computability over $\sf HC$ work, or are things doomed from the get go?
 A: One of the big problems is that $\mathsf{HC}$, unlike $\mathsf{HF}$, is rather underspecified by the usual axioms of set theory.
For example, one possibility is that $\mathsf{HC}=L_{\omega_1}$. Admissible levels of the $L$-hierarchy support a very good analogue of computability theory, namely $\alpha$-recursion theory. Sacks' book Higher recursion theory has a wealth of information on the topic; in particular, most standard priority arguments go through pretty effortlessly in $L_{\omega_1}$ (although there are exceptions, e.g. the existence of maximal c.e. sets). On the other hand, if for example we have large cardinals in our universe then $\mathsf{HC}$ lacks any simply-definable well-ordering, and this stands in the way of any sort of argument which would involve enumerating Turing machines.
I think it's helpful to identify four types of "computability on a transitive set" $T$:

*

*In admissible recursion theory, we assume $T\models\mathsf{KP}$ (= Kripke-Platek set theory). In such a $T$ we have a natural notion of "finite" (= "element of $T$") and "c.e." (= "$\Sigma_1(T)$") which behave not too badly; however, we don't generally have a simple well-ordering of the universe so we can't perform searches or set up priority arguments.


*In $\alpha$-recursion theory, $T=L_\alpha$ for some admissible ordinal $\alpha$. This improves on the previous bulletpoint, and $\alpha$-recursion generalizes classical computability theory rather well.


*In $\beta$-recursion theory, $T=L_\beta$ for some non-admissible ordinal $\beta$. This is the dual situation to admissible recursion theory: we completely sacrifice replacement but require full "search capability." At this point the notion of finiteness becomes rather more nuanced; see Maass' paper, Recursively invariant $\beta$-recursion theory.


*In principle we could keep going and look at transitive sets satisfying very weak set theories. Certainly there is work on such topics (see e.g. various papers of Mathias); however, my opinion is that in the absence of both replacement and searchability there isn't much computability-theoretic character left.
