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?
$\begingroup$
$\endgroup$
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
7
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.
answered Sep 9, 2019 at 2:52
-
2$\begingroup$ Incidentally, an even sharper situation holds in arithmetic. By Tennenbaum, no nonstandard model of PA (say) is computable, but the ordertype of any countable nonstandard model of PA (or even vastly less) is exactly $\omega+\zeta\cdot\eta$ where $\zeta$ is the ordertype of the integers. Very little is directly coded into the ordertype, in either set theory or arithmetic. $\endgroup$ Sep 9, 2019 at 2:57
-
$\begingroup$ How hard is it to construct an $\omega$-model of ZF whose well-founded part has order type $\omega_1^{CK}$? Does ZFC prove that the existence of such a model follows from the existence of any $\omega$-model? $\endgroup$ Sep 9, 2019 at 3:01
-
$\begingroup$ @JamesHanson Yes: Gandy basis theorem. (In more detail: GBT says that - assuming there is an $\omega$-model of ZF at all - there is an $\omega$-model of ZF which is low for the hyperjump. But this model cannot have well-founded $\omega_1^{CK}$, or it would be within a couple Turing jumps of $\mathcal{O}$ and hence not low for the hyperjump. The model existence hypothesis is required to say that the relevant tree has a path, or that the relevant $\Sigma^1_1$ class is nonempty.) $\endgroup$ Sep 9, 2019 at 3:03
-
$\begingroup$ I find the contrast with the uncountable model theoretic situation interesting. For uncountable $\lambda$, a model of PA is $\lambda$-saturated if and only if it is $\lambda$-saturated as a linear order. My understanding was that this is roughly true because you can code 'enough' into the order type, in particular into cuts. I wonder if there are similar statements for ZF, ZFC, or ZF + Global Choice? $\endgroup$ Sep 9, 2019 at 3:09
-
2$\begingroup$ @Wojowu I think this question may be useful: mathoverflow.net/questions/30633. $\endgroup$ Sep 9, 2019 at 9:05