13
$\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
    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
    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
    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
    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
    Mar 7, 2016 at 21:50

1 Answer 1

Reset to default
12
$\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$
9
  • 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
    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
    Mar 7, 2016 at 22:20
  • 2
    $\begingroup$ Rather, $\exists z\,(x+1+z=y)$. $\endgroup$
    – Andrés E. Caicedo
    Mar 8, 2016 at 1:06
  • 1
    $\begingroup$ +1. Great answer, François! $\endgroup$
    – Joel David Hamkins
    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
    Mar 8, 2016 at 5:45

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.