# 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:

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

2. 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:

-
Vague heuristic idea: $ZF^\times$ is very nearly the same thing as $PA$, so this really ought to be the smallest ordinal not definable in $PA$, which I think (?) is $\omega_1^{CK}$. –  Chris Eagle May 8 '12 at 20:26
@Chris: I am not sure it has to be the same ordinal but I think it would have to be at least that. –  Asaf Karagila May 8 '12 at 21:19
I'm not 100% sure about that, but [descriptive-set-theory] seems to make some sense here, perhaps [computability] instead? I'd be glad if someone would take the necessary action if needed. –  Asaf Karagila May 10 '12 at 23:09
Every definable well ordering over $V_{\omega}$ is isomorphic to an arithmetical well ordering of natural numbers. So it must be below $\omega_1^{CK}$. But every recursive well ordering of natural numbers is definable in $V_{\omega}$. So you are right. –  喻 良 May 11 '12 at 2:12
@Liang: So the answer to the first question is indeed $\omega_1^{CK}$? –  Asaf Karagila May 11 '12 at 4:36

$V_{\omega}$ is recursively biinterpretable with $\omega$. So both are $\omega_1^{CK}$.