Countability of Church-Kleene ordinal in ZF In the set theory ZFC if we define the Church-Kleene ordinal as usual, it is the least upper bound of a countable set of countable ordinals, then is countable itself because $\aleph_1$ is regular, but if we don't consider the axiom of choiche what happen (i know that $\aleph_1$ is not more necessarily regular)?
It is always true that the Church-Kleene ordinal is countable?
 A: The countability of $\omega_1^{CK}$ has nothing to do with the axiom of choice: consider the map $\omega_1^{CK}\rightarrow\omega$ sending $\alpha$ to the least index of a Turing machine which computes a copy of $\alpha$. This is clearly an injection, hence $\omega_1^{CK}$ is countable.
In general, for any "simple" notion of definability, the least ordinal not definable in that sense is countable, and this is witnessed by the map sending a definable ordinal to the least number representing a definition for that ordinal. If you're interested in such "first undefinable ordinals," you may find this summary of Madore worthwhile.
(Why did I say "simple" in the above? Well, it turns out that we can run into some odd phenomena in general - see for example this article of Hamkins, Linetsky, and Reitz. But this isn't an issue here.)
A: Let me give you a different—and slightly more convoluted—argument than the direct one given by Noah, in hope to present a different way of seeing these type of problems.

Turing machines are absolute between $V$ and $L$. This means that every computable $\alpha$ is also computable in $L$. In particular, every $\alpha<\omega_1^{CK}$ is countable in $L$.
Every computable $\alpha$ in $L$ is also computable in $V$. Therefore the definition of $\omega_1^{CK}$ in $L$ must be the same as in $V$. Since $L$ satisfies choice, this is a countable ordinal in $L$, so it must be countable in $V$.

The key point here is the combination of these two parts:


*

*We have an inner model satisfying choice, which agrees with $V$ on what it means to be computable,

*and being countable is a $\Sigma_1$ property, so it is upwards absolute.
This can be used in a myriad of situations. For example when we want to argue that the diagonal intersection of $\kappa$ closed and unbounded subsets of a regular $\kappa$ form a closed and unbounded subset of $\kappa$, we can do this by checking manually the usual proof works, or we can argue in some inner model of choice that captures our sequence of clubs, and use the fact that you cannot destroy a club subset of a regular cardinal to argue the diagonal intersection in the inner model is still a club in $V$.
