16
$\begingroup$

Consider the first-order language $\mathcal{L}_{\text{OA}}:=(+,\cdot,0,1)$; in this language, we can formulate statements of ordinal arithmetic. Clearly, the theory $T_{\text{OA}}$ of $(\text{On},+,\cdot,0,1)$ is not recursive, as $\omega$ is definable in $\mathcal{L}_{\text{OA}}$ (as being the only ordinal $\gamma$ different from $0$, not having a predecessor and having no $\alpha$ and $\beta$ different from $0$ such that $\alpha+\beta=\gamma$ with $\alpha$ not having a predecessor) and hence the theory TA (true arithmetic) of $\mathbb{N}$ is computable from $T_{\text{OA}}$. Note that $T_{\text{OA}}$ is absolute between transitive class models of ZFC.

My question is whether the reverse reduction holds: Can we decide $T_{\text{OA}}$, given TA? More precisely, what is the Turing degree of $T_{\text{OA}}$?

Improve this question
$\endgroup$
6
  • 1
    $\begingroup$ Is $\langle L,\in\rangle$ interpretable in $\langle\text{Ord},+,\cdot,0,1\rangle$? I'm not sure, but if it is, then your theory will be complicated. $\endgroup$
    – Joel David Hamkins
    Commented Mar 7, 2016 at 11:34
  • 2
    $\begingroup$ How do you intend to formalize $T_{OA}$? Since the ordinals are a proper class, we don't necessarily have a satisfaction class for this structure, without further explanation. In GBC+ETR, and for example therefore also in KM, we can define first-order truth for the structure $\langle \text{Ord},+,\cdot,0,1\rangle$, but I don't see just yet why we can refer to this theory in ZFC. $\endgroup$
    – Joel David Hamkins
    Commented Mar 7, 2016 at 12:10
  • 3
    $\begingroup$ Addressing @JoelDavidHamkins's comment, it might be best to first consider versions of $T_{OA}$ below fixed ordinals. For instance, via Cantor normal form, I think the version of $T_{OA}$ restricted to ordinals $<\epsilon_0$ is indeed reducible to first-order arithmetic, but I don't see how to push that up to even $\omega_1$ (although we can go past $\epsilon_0$ by using more complicated notation systems of course - the real barrier seems to me to be $\omega_1^{CK}$ . . .). $\endgroup$
    – Noah Schweber
    Commented Mar 7, 2016 at 17:28
  • 1
    $\begingroup$ Vague recollection that I can't check right now since I'm in transit: I think Rosenstein's Linear Orderings contains a proof that this is just $T_{OA}(\alpha)$ for some specific countable indecomposable $\alpha$. On the other hand, with a lot of extra functions, you get Silver machines that encode $L$ as @JoelDavidHamkins suggests. $\endgroup$
    – François G. Dorais
    Commented Mar 7, 2016 at 21:46
  • 2
    $\begingroup$ $T_{OA}$ defined on ordinals less than your favourite recursive ordinal $\alpha$ is decidable from TA, since the relevant subset of Kleene's O is recursively enumerable, and ordinal arithmetic in Kleene's O is recursive. This argument breaks down if you try $\alpha = \omega_1^{CK}$, though. $\endgroup$
    – Adam P. Goucher
    Commented Mar 7, 2016 at 21:50

1 Answer 1

Reset to default
16
$\begingroup$

Using what are now called Ehrenfeucht–Fraïssé Games and extensions thereof, Ehrenfeucht showed that

$$(\mathrm{Ord},{<}) \sim (\omega^\omega,{<})$$ $$(\mathrm{Ord},{<},{+}) \sim (\omega^{\omega^\omega},{<},{+})$$ $$(\mathrm{Ord},{<},{+},{\cdot}) \sim (\omega^{\omega^{\omega^\omega}},{<},{+},{\cdot})$$

where $\sim$ denotes elementary equivalence. Since $(\omega^{\omega^{\omega^\omega}},{<},{+},{\cdot})$ is a computable structure, its first-order theory is computable from $0^{(\omega)}$ ($\equiv_T TA$).

The question omits the relation $<$ but that doesn't matter for the last two results since $x < y$ is definable by $\exists z(x + 1 + z = y)$. [Thanks to Andrés Caicedo for pointing out the correct definition.]

A. Ehrenfeucht, An application of games to the completeness problem for formalized theories, Fund. Math. 49 (1960–1961), 129–141.

Improve this answer
$\endgroup$
10
  • 2
    $\begingroup$ Hm, I just realized that the OP omitted ${<}$. I guess that doesn't matter since $x < y$ can be defined as $\exists z(x + z + 1 = y)$. $\endgroup$
    – François G. Dorais
    Commented Mar 7, 2016 at 22:08
  • 3
    $\begingroup$ Note that the use of games seems to cleverly circumvent the proper class issue with the first-order theory of $(\mathrm{Ord},\ldots)$. However, in ZFC, one must still interpret the result as scheme that, for every $n$, ZFC proves $\sim_n$. $\endgroup$
    – François G. Dorais
    Commented Mar 7, 2016 at 22:20
  • 2
    $\begingroup$ Rather, $\exists z\,(x+1+z=y)$. $\endgroup$
    – Andrés E. Caicedo
    Commented Mar 8, 2016 at 1:06
  • 1
    $\begingroup$ +1. Great answer, François! $\endgroup$
    – Joel David Hamkins
    Commented Mar 8, 2016 at 2:42
  • 1
    $\begingroup$ How does the answer change if we also add ordinal exponentiation? I'd suspect we'll get a structure elementarily equivalent to something like $\varepsilon_\omega$. $\endgroup$
    – Wojowu
    Commented Mar 8, 2016 at 5:45

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .