Is $\omega_1^{CK}$ recursively enumerable? Using the pairing, replacement and union (to take limits) axioms one can effectively produce some recursive ordinals starting from $\omega$ as $\omega+1$, $\omega\cdot 2$, $\omega^2$, $\omega^\omega$, $\varepsilon_0$, $\varphi_{\gamma}(\beta)$, $\Gamma_{\alpha}$, etc. I'm wondered how far we can go this way, i.e. by successively constructing ordinals from already constructed applying pairing, union and replacement a finite number of times? Can we exhaust $\omega_1^{CK}$ this way? If no, is there a recursive enumeration of $\omega_1^{CK}$?
 A: There is no recursive enumeration of $\omega_1^{CK}$. Indeed, there is no hyperarithmetic (or even $\Sigma^1_1$) way to present $\omega_1^{CK}$! This was proved by Spector.
More generally, if a Turing degree ${\bf a}$ computes a copy of an ordinal $\alpha$ and ${\bf a}$ is hyperarithmetic relative to ${\bf b}$, then ${\bf b}$ also computes a copy of $\alpha$. This general property is called "hyperarithmetic-is-recursive," and turns out to have surprising connections with model theory (at least, its more set-theoretic side). We say that a class of structures $\mathbb{K}$ satisfies hyperarithmetic-is-recursive if whenever a Turing degree ${\bf a}$ is hyperarithmetic in ${\bf b}$ and computes a copy of $\mathcal{A}$, then ${\bf b}$ also computes a copy of $\mathcal{A}$, for all $\mathcal{A}\in\mathbb{K}$. Montalban showed that a first-order theory $T$ is a counterexample to Vaught's conjecture if and only if $T$ satisfies "hyperarithmetic-is-recursive on a cone," a slight weakening of "hyperarithmetic-is-recursive."

With regard to the first part of your question, however, it's not entirely clear to me what process you have in mind; specifically, how Replacement is allowed to be used. In the naive sense, we can automatically reach any countable ordinal which has a copy (= ordering of $\omega$ with appropriate ordertype) definable in set theory with a single application of replacement. $\omega_1^{CK}$, and much more, falls into this category. Here is an explicit definable well-ordering of $\omega$ with ordertype $\omega_1^{CK}$:


*

*We define Kleene's set $\mathcal{O}$ of ordinal notations as usual.

*We now define a relation $\triangleleft$ on $\mathcal{O}$ as follows: $m\triangleleft n$ iff $m$ is an index for an ordinal which is smaller than the ordinal $n$ is an index for.

*Finally, we let $$M=\{m\in\mathcal{O}: \forall n\in\mathcal{O}(n<m\implies (m\triangleleft n\vee n\triangleleft m))\}$$ be the set of minimal indices for ordinals. Then $M$, ordered by $\triangleleft$, has ordertype $\omega_1^{CK}$. 

*Now, since $M$ doesn't actually consist of every natural number, we're not technically done, but this is easily fixed: let $M=\{m_0<m_1<m_2< ...\}$ and let $\triangleleft'$ be defined by $x\triangleleft'y\iff m_x\triangleleft m_y$. Then $\triangleleft'$ is a well-ordering of $\omega$ with ordertype $\omega_1^{CK}$. And this doesn't even scratch the surface of ordinals we can build.
So in the process you describe, you probably want to limit attention somehow to "effective" applications of replacement, and it's not entirely clear to me what this means. 
That said, you may be tangentially interested in this paper of Arai, in which he essentially calculates a bound on the $L$-rank of reals (equivalently, hereditarily countable sets) which can be "proved to exist" in ZFC+V=L in a precise sense. I think this overshoots what you want by a huge margin, both because powerset is allowed and because there's no "finite construction" picture going on (as far as I can tell), but you might still find it neat.
