Computable models of the ordinal numbers It's known, for example in the answer to this question: Is there a computable model of ZFC? that ZFC has no computable model. My questions is: is there a model of ZFC for which the order relation on the class of ordinals is computable?
 A: Yes, this can happen: if $M$ is a countable $\omega$-model of ZF whose well-founded part has ordertype $\omega_1^{CK}$ (that is: has the shortest well-founded part possible for $\omega$-models), then $Ord^M$ as a linear order is just the Harrison order: $$\omega_1^{CK}+(\omega_1^{CK}\cdot\eta),$$ where $\eta$ is the ordertype of the rationals. This linear order does in fact have a computable copy, and is one of the basic examples/counterexamples in computable structure theory: a computable linear order which is illfounded but has no hyperarithmetic descending sequence (it has other nice properties too).
The key to seeing that this must be the ordertype is the following pair of observations:


*

*Given such an $M$ and an $\alpha\in Ord^M$, there must be an interval in $Ord^M$ beginning with $\alpha$ and isomorphic to $\omega_1^{CK}$.

*No interval in $Ord^M$ can be isomorphic to $\omega_1^{CK}+1$.
As to why such a model exists in the first place, this is trickier; depending how you phrase it, it's an application of either the Gandy basis theorem or the Barwise(-Kreisel) compactness theorem. Unfortunately, this doesn't have a one-line explanation.
