Ordinal notations within non-standard models of arithmetic

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.