The following theory is a theory of classes of ordinals.
Language: Bi-sorted FOL with identity. First sort in lower case ranging over ordinals. Second sort in upper case ranging over classes of ordinals. We take the sorts to be disjoint.
Primitives: $=, \prec , \epsilon$
Syntactical restrictions: $\epsilon$ from first to second sort, $\prec$ between objects of the second sort.
Axioms: $ \textbf{1. Extensionality: }\forall x \, (x \ \epsilon \ X \leftrightarrow x \ \epsilon \ Y) \to X=Y \\ \textbf{2. Comprehension: }\exists X \forall x \, (x \ \epsilon \ X \leftrightarrow \phi) \\ \textbf { Define: } X=\{x \mid \phi\} \iff \forall x \, (x \ \epsilon \ X \leftrightarrow \phi)\\\textbf {3. Well Ordering}^\dagger\textbf{: } \prec \text{is a well-ordering on } classes \\ \textbf{ Define: } x < y \iff \{x\} \prec \{y\}\\\textbf{4. Infinity: } \exists l: \forall x < l \, \exists y \, ( x < y < l) \\\textbf{5. Replacement: } \phi \text { is 1-1 } \to \exists k \forall y \, ( \exists x < l \, (\phi(x,y)) \to y < k) \\ \textbf { Define:} \lim X = \min l: \forall x \ \epsilon \ X (x < l) \\ \textbf{6. Respective: }\lim X < \lim Y \to X \prec Y \\ \textbf{ Define: } \operatorname {Card}(x) \iff \forall y < x \not \exists F (F: \{z \mid z < y\} \to \{z \mid z < x \}) \\\textbf{7. Successor Cardinals: } \forall x \exists \kappa: \operatorname{Card}(\kappa) \land x < \kappa $
Where $F:X \to Y$, denotes $F$ is a function whose domain is $X$ and whose codomain is $Y$. Where $F$ is a class of Gödel's ordered pairs, satisfying the usual qualifications for functions. $\min l: \phi(l)$, is the minimal $l$ that satisfy $\phi(l)$. $\phi \text{ is 1-1}$, means $\phi$ is a formula that defines a one-to-one relation.
The notable difference between this axiomatic system and the theory "$\sf SO$" of sets of ordinals, (besides existence of big classes here) is actually the last axiom of $\sf SO$, that is the Power set axiom.
Now Chapter 4 of the article about $\sf SO$ defines the $*$-recursive sets, and does establish the result that those are exactly the constructible sets of ordinals.
My question:
Is the $*$-recursive sets definable in this system?
The point is that if we can define the $*$-recursive sets, then we can (using successor cardinals) interpret $\sf ZFC$ via constructing $L$. So, we don't need to add Power set axiom.
$\dagger$ this is the axiom scheme of $\prec$ being areflexic, transitive, connected, and well-founded over classes (well-founded is the schema: if $\phi$ is a formula satisfied by some class, then there is some $\prec$-minimal class satisfying $\phi$).
