It is well-known that the order type of any countable non-standard model of arithmetic $\mathfrak{A}$ is $\omega+(\omega^*+\omega)\eta$. My question is what could be said about the order types of ordinal notation systems within non-standard models of arithmetic?

The question is motivated by my answer to the question Order types of models of theories of ordinals about the order types of non-standard models of ordinal arithmetic: some group of this non-standard models corresponded to the ordinal notation systems within non-standard models of arithmetic, and I could say very little about their order types.

Now I'll provide a bit more details. Let us consider some standard computable ordinal notation system, say Cantor ordinal notation for the ordinals $<\varepsilon_0$ (although the same question could be asked for different ordinal notation systems). The ordinal notation system essentially is an arithmetical formula $x\prec y$ such in the standard model it defines a well-ordering with the order type $\varepsilon_0$. For each $\alpha<\varepsilon_0$ let me denote as $\hat\alpha$ the Gödel number for the ordinal $\alpha$ within the ordinal notation system. And for $\alpha<\varepsilon_0$ and a model $\mathfrak{A}\models \mathsf{PA}$ let me denote as $(\alpha)^{\mathfrak{A}}$ the order type in $\mathfrak{A}$ of the arithmetical relation $\prec\upharpoonright_{\hat\alpha}$ that is the restriction of $\prec$ to the elements $\prec \hat\alpha$.

It is easy to see that for each model of arithmetic $\mathfrak{A}\models \mathsf{PA}$ with the order type $A$ and an ordinal $\alpha<\omega^{\omega}$ with the Cantor normal form $\omega^{k_1}+\ldots +\omega^{k_n}$ the order type $(\alpha)^{\mathfrak{A}}$ is precisely $A^{k_1}+\ldots+ A^{k_n}$.

However I have no clue of what happening even with $(\omega^{\omega})^{\mathfrak{A}}$. Does $(\omega^{\omega})^{\mathfrak{A}}$ depends only on the order type of $\mathfrak{A}$? Even if the latter isn't the case, is $(\omega^{\omega})^{\mathfrak{A}}$ the same for all countable non-standard models $\mathfrak{A}$? In the other side of the spectrum of possibilities, one could imagine that $(\omega^{\omega})^{\mathfrak{A}}$ reflects a lot of information about the model $\mathfrak{A}$. Could we recover model $\mathfrak{A}$ from the order type $(\omega^{\omega})^{\mathfrak{A}}$? Could we recover $\mathsf{SSy}(\mathfrak{A})$ from the order type $(\omega^{\omega})^{\mathfrak{A}}$?

Of course I would be interested in the answers to the same kind of questions for other ordinals $\alpha$ and for more restricted classes of models $\mathfrak{A}$ (e.g. models of true arithmetic, or recursively saturated models, etc.).

  • 1
    $\begingroup$ I don’t know that much about the theories of the structures $(\alpha,{<})$, but I assume they do have quantifier elimination down to some class of formulas of bounded quantifier alternation, right? If so, then models of the form $(\alpha)^{\mathfrak A}$ for countable $\mathfrak A\models\mathrm{PA}$ are exactly the recursively saturated countable models of $\mathrm{Th}(\alpha,{<})$. $\endgroup$ Jun 10, 2019 at 16:35
  • $\begingroup$ @Emil Theories $\mathsf{Th}(\alpha,<)$ for $\alpha\ge \omega^{\omega}$ do not enjoy this kind of quantifier elimination. This is due to the fact that $(\omega^n,<)\equiv_{\Pi_n}(\omega^n(1+A),<)$, for any linear order $A$. And that there are first-order formulas distinguishing $(\omega^n,<)$ and $(\omega^{\omega},<)$. $\endgroup$ Jun 10, 2019 at 16:42
  • $\begingroup$ @EmilJeřábek However if all you needed to use for your observation was that over $\mathsf{PA}$ there is a truth definition for $(\alpha,<)$, then it is the case. It is due to the fact that all $\mathsf{Th}(\alpha,<)$ are decidable. $\endgroup$ Jun 10, 2019 at 16:52
  • $\begingroup$ Yes, that is exactly what I need. $\endgroup$ Jun 10, 2019 at 16:53
  • 2
    $\begingroup$ The truth definition is needed to prove that any $(\alpha)^{\mathfrak A}$ is recursively saturated. The converse implication only needs that $\mathrm{Th}(\alpha,{<})$ is (co)interpretable in PA: it follows from the resplendency of countable recursively saturated models. $\endgroup$ Jun 10, 2019 at 17:34

2 Answers 2


I'll provide a description of $(\alpha)^{\mathfrak{A}}$ in the case of countable $\mathfrak{A}$. I base my answer on observations by Emil Jeřábek (see discussion below the initial question), but of course any mistakes here are due to me.

From Cantor's normal form theorem it is easy to conclude that each ordinal $\alpha\ge \omega^{\omega}$ have unique representation in the form $$\omega^{\omega}(1+\alpha')+\omega^{k_1}+\ldots+\omega^{k_n}\text{, where }k_1\ge k_2\ge\ldots\ge k_n.$$ The first claim is that the order types of the form $(\alpha)^{\mathfrak{A}}$, where $\mathfrak{A}$ is countable non-standard model of $\mathsf{PA}$ are precisely the order types $$L+(\omega+(\omega^{\star}+\omega)\eta)^{k_1}+\ldots+(\omega+(\omega^{\star}+\omega)\eta)^{k_n},$$ where $L$ is a recursively saturated linear order that is elementary equivalent to $(\omega^{\omega},<)$. The second claim is that, for given $(\alpha)^{\mathfrak{A}}$ the order type of the corresponding $L$ depends only on $\mathsf{SSy}(\mathfrak{A})$ and that we could recover $\mathsf{SSy}(\mathfrak{A})$ from the order type of $L$.

There is a classical result of A. Tarski and A. Mostowski [1,2] that all theories $\mathsf{Th}(\alpha,<)$ are decidable. A natural formalization of their decision procedure gives us $\Sigma_1$ formula $\mathsf{T}^\alpha(x)$ : "formula with Gödel number $x$ is true in $(\alpha,<)$". Their decidability result have been established via quantifier elimination in extended signature and all the used techniques were fairly elementary. A formalization of their proof in $\mathsf{PA}$ shows that $\mathsf{T}^{\alpha}$ acts as a truth-definition satisfying uniform Tarski's biconditionals: $$\mathsf{PA}\vdash \forall \vec{x}\prec \hat\alpha \;(\prec\upharpoonright_{\hat\alpha}\models\varphi(\vec{x})\mathrel{\leftrightarrow} \mathsf{T}^{\alpha}(\ulcorner\varphi(\dot{\vec{x}})\urcorner)),$$ for all first-order formulas $\varphi(\vec{x})$ of the language of linear orders.

The presence of this truth definition implies that all the order types $(\alpha)^{\mathfrak{A}}$ would be recursively-saturated. If $t(\vec{x})$ is a recursive type in $(\alpha)^{\mathfrak{A}}$ then due to absoluteness of $\Delta_1$ properties for any standard $n$ model $\mathfrak{A}$ thinks that partial type $t(\vec{x})\upharpoonright_n$ is realized in $\prec\upharpoonright_{\hat\alpha}$. By overspill there are $a,\vec{b}\in\mathfrak{A}$ such that $\mathfrak{A}$ thinks that $\vec{b}$ realize the partial type $t(\vec{x})\upharpoonright_a$. But externally, again by absoluteness of $\Delta_1$ properties, tuple $\vec{b}$ is of the type $t(\vec{x})$ in $(\alpha)^{\mathfrak{A}}$.

Since for each $\alpha$, $\mathsf{PA}$ verifies that $\mathsf{T}^{\alpha}$ is $\Delta_1$, we have elementary equivalence $(\alpha)^{\mathfrak{A}}\equiv (\alpha,<)$. Additionally Tarski and Mostowski established that $(\omega^{\omega}\alpha,<)\equiv (\omega^\omega\beta,<)$, for any $1\le \alpha,\beta<\varepsilon_0$. Thus for any non-standar $\mathfrak{A}\models\mathsf{PA}$ and $1\le \alpha< \varepsilon_0$ the linear order $(\omega^{\omega}\alpha)^{\mathfrak{A}}$ is a recursively-saturated linear order elementary equivalent to $\omega^{\omega}$.

Let me now show that for any $1\le \alpha< \varepsilon_0$ and countable recursively-saturated $L\equiv (\omega^{\omega},<)$ there is countable $\mathfrak{A}\models \mathsf{PA}$ such that $L\simeq (\omega^\omega\alpha)^{\mathfrak{A}}$. Indeed, by a well-known result of Barwise and Ressayre [Theorem IV.5.7,3] all countable recursively-saturated models are resplendent and hence the existence of the desired $\mathfrak{A}$ follows from the fact that $\prec\upharpoonright_{\hat{(\omega^\omega\alpha)}}$ is an interpretation of $\mathsf{Th}(L)$ in $\mathsf{PA}$.

This concludes the proof of the first claim: the order $(\alpha)^{\mathfrak{A}}$ is $(\omega^{\omega}(1+\alpha'))^{\mathfrak{A}}+(\omega^{k_1}+\ldots+\omega^{k_n})^{\mathfrak{A}}$, we have already analysed the left summand and the order type of the right summand is trivially expressible from the order type of $\mathfrak{A}$. Now let me briefly sketch the situation with the connection between an order type of $L=(\omega^{\omega}(1+\alpha))^{\mathfrak{A}}$ and $\mathsf{SSy}(\mathfrak{A})$.

The key idea here is to assign to each element $a\in L$ the partial function $s_a\colon \omega\to \omega$. For all $n,m$ there are natural formulas $\varphi_{n,m}(x)$ expressing in all the structures structures $(\beta,<)$ the property of an ordinal $\gamma$ to be in the interval $[\omega^{n+1}\delta+\omega^{n}m,\omega^{n+1}\delta+\omega^{n}(m+1))$ for some $\delta$. We put $s_a(n)=m$ if $L\models \varphi_{n,m}(a)$ and we put $s_a(n)$ to be undefined if $L\not \models \varphi_{n,m}(a)$, for all $m\in \omega$. We define $\mathsf{SF}(L)$ to be the set of all the partial functions $f\colon \omega\to \omega$ that are $s_a$, for some $a\in L$.

It is fairly easy to show that $f\in \mathsf{SF}((\omega^{\omega}\alpha)^{\mathfrak{A}})$ iff $f$ is a partial function which graph lies in $\mathsf{SSy}(\mathfrak{A})$. On the other hand it seems to be easy to show that countable recursively-saturated $L_1,L_2$ with $\mathsf{SF}(L_1)=\mathsf{SF}(L_2)$ are isomorphic (by providing a strategy for the Ehrenfeucht–Fraïssé game). Combining this two facts we prove the second claim.

[1] A. Tarski, A. Mostowski. "Arithmetical classes and types of well ordered systems. Preliminary report." Bull. Amer. Math. Sot., vol. 55 (1949), p. 65.

[2] J.E. Doner, A. Mostowski, and A. Tarski. "The Elementary Theory of Well-Odering—A Metamathematical Study—." Studies in Logic and the Foundations of Mathematics. Vol. 96. Elsevier, 1978. 1-54.

[3] J. Barwise. "Admissible Sets and Structures: An Approach to Definability Theory." Perspectivesin Mathematical Logic. Springer-Verlag, Berlin, 1975.

Update: I learned about a related paper by Harvey Friedman [4], where he studied order types of ordinals in ill-founded countable admissible sets. Unsurprisingly, the order types of ordinals $\mathsf{On}^{\mathfrak{M}}$ in countable admissible sets $\mathfrak{M}$ with ill-founded $\omega^{\mathfrak{M}}$ range precisely over the same order types as $(\omega^\omega)^{\mathfrak{A}}$, for countable non-standard $\mathfrak{A}\models \mathsf{PA}$. Friedman gave an explicit description of $\mathsf{On}^{\mathfrak{M}}$ in terms of $\mathsf{SSy}(\mathfrak{M})$ by giving (in my notations) description of orders $L$ with given $\mathsf{SF}(L)$.

[4] H. Friedman. "Countable models of set theories." Cambridge summer school in mathematical logic. Springer, Berlin, Heidelberg, 1973. 539-573.


I spent some time thinking about order-types of models of arithmetic, and of order-types of structures they interpret (my PhD). I think there are several formulations of your question: (1) about ordinals, (2) about ordinal notations (M-coded), (3) about "provably- (if we are talking of a theory) or satisfied- (if we are in a model of arithmetic) -well-orderededness of systems of ordinal notations", (4) well-orders if your model has a second-order structure (5) constructible or recursive ordinals (as in Turing, Feferman and Sacks's book), from the point of view of a nonstandard model. Also, Kleene's O in a nonstandard model.

Each formulation leads to interesting answers (some known).

I remember being very proud when, at Richard Kaye's hint, I found what a nonstandard model M (the interesting case is uncountable) thinks about the order-type of models of DLO, DIS,.....or PA itself for that matter (using arithmetized completeness inside M).

The answers for DLO and PA are Q(M) and M+Q(M).(M*+M).

It would be nice to see the spectrum of answers to (1)-(5) above.

  • 1
    $\begingroup$ The Friedman technique (see [4] from my answer) covers most of the cases that you mention if we restrict ourselves to countable models. The real requirement is that a model $\mathfrak{A}$ should think that the a representation of an ordinal is isomorphic to a initial segment of some order on Cantor normal form $(\omega^{\mathbb{N}+L})^{\mathfrak{A}}$, where $L$ is any linear order. $\endgroup$ Sep 8, 2019 at 8:17
  • 1
    $\begingroup$ So (for countable models) the cases that aren't covered by this technique are fairly exotic: ordinals in very weak set theories (that couldn't prove Cantor normal form theorem), well-orderings of models of second-order arithmetic $\mathfrak{A}\not\models \mathsf{ATR}_0$ (note that $\mathsf{ATR}_0$ is equivalent to comparability of well-ordering), "bad" ordinal representation systems that couldn't be enriched by structure of Cantor normal forms. $\endgroup$ Sep 8, 2019 at 8:20
  • $\begingroup$ and there's more. $\endgroup$ Sep 9, 2019 at 12:25
  • $\begingroup$ just от балды, here is an arithmetical theory with built-in ordinal notations. Not what you wanted, but in the spectrum of what you could have wanted. home.inf.unibe.ch/~strahm/download/pdf/secord.pdf $\endgroup$ Sep 9, 2019 at 16:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.