Definable order types without infinity axiom. Denote by $ZF^\times$ the theory of $ZF$ without the axiom of infinity. We know that $V_\omega$, the set of all hereditarily finite sets in a model of $ZF$, is a model of $ZF^\times$.
We further know that $\newcommand{Ord}{\operatorname{Ord}}\Ord^{V_\omega}=\omega$. Consider the following formula: $$\varphi(x,y)=(x \text{ is an ordinal})\land (y\text{ is an ordinal})\land \Big((x\neq0\land x\in y)\lor y=0\Big)$$
It is not hard to see that the class $\{\langle x,y\rangle\mid \varphi(x,y)\}$ is a well-ordering of order type $\omega+1$. Similarly we can define $\omega+2$, even $\omega+\omega$. We can go even further, much further.
However, we can obviously go so far, there are only countably many formulas and countably many parameters so there can only be countably many order types definable.
Questions: 


*

*What is the least ordinal not definable in $V_\omega$ from $ZF^\times$?

*We can push this question into $NBG^\times$, defined as $ZF^\times$. Now we can quantify over classes, surely we can push this even higher?

Vaguely related:


*

*Surreal numbers without the axiom of infinity
 A: To move this off the unanswered queue (actually user 喻良 already posted the correct answer but it was deleted as a link-only answer; also, it only addressed the first question):
The answer is indeed $\omega_1^{CK}$, the least noncomputable ordinal. To see this it's convenient to switch from $V_\omega$ to $\mathbb{N}$; they are bi-interpretable (via e.g. the Ackermann interpretation), so we can basically always switch from one to the other.
By definition, $\omega_1^{CK}$ is the smallest ordinal with no computable copy - that is, the least ordinal $\alpha$ such that there is no computable relation $R$ on $\omega$ such that $R$ defines a well-ordering of $\omega$ of type $\alpha$. Since computable = $\Delta^0_1$, every ordinal with a computable copy in fact has a definable copy. So your ordinal is $\ge\omega_1^{CK}$. But in fact $\omega_1^{CK}$ is gigantic: it is also the smallest ordinal with no hyperarithmetical copy. This is a theorem due to Spector - see Corollary $5.6$ of chapter $1$ of Sacks' book. Since $\mathbb{N}$-definable = arithmetical $\subsetneq$ hyperarithmetical, this shows that your ordinal is $\le\omega_1^{CK}$.
What about bringing classes into the picture? Well, by implementing the $L$-construction in the setting of second-order arithmetic (see the last section of Simpson's reverse math book) this gets us all the reals in $L_\alpha$ for $\alpha$ the smallest "gap ordinal," that is, the smallest $\alpha$ such that $L_{\alpha+1}\cap\mathbb{R}=L_\alpha\cap\mathbb{R}$. This ordinal is absolutely gigantic, certainly vastly bigger than $\omega_1^{CK}$. So yes, things increase at that point.
That's such a big jump that it feels a bit rude. A gentler hike up the countable ordinals goes through looking at the smallest ordinal with no copy definable over $L_\alpha$ for appropriate $\alpha$. This is always at most the next admissibile above $\alpha$, and can be strictly smaller - indeed it usually is, in the sense that this inequality is strict on a club. This is proved similarly to here. One important issue to keep in mind is that, contra the $\omega$-setting, "definable over definable $\not=$ definable" for ordinals over general admissible sets. The robustness of $\omega_1^{CK}$ is rather special.

Incidentally, there's a good "atlas" of countable ordinals here.
