Infinite Time Turing Machines for elementary proofs on recursive reals - LIRMM - Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier
Conference Papers Year : 2024

Infinite Time Turing Machines for elementary proofs on recursive reals

Abstract

Joseph Harrison published in 1967 a quite famous result in classical recursion theory on recursive reals. It shows the counter-intuitive result that the well-ordered initial segment of a recursive order is not necessarily of recursive ordinal type. This segment can be as long as the supremum of recursive ordinals, hence of non-recursive length, even if the order is itself recursive. In the literature, a few different -- but equivalent -- proofs of this result can be found using arguments strictly in second order arithmetic, more precisely the fact that $\Sigma_1^1 \neq \Pi_1 ^1$. In this article, we sketch a different and more elementary proof of this result, using infinite time Turing machines (ITTMs) -- full proof is in \cite{BD24}. To achieve this, we need to reprove, using elementary arguments only, several results on infinite (countable) binary relations, and more specifically on linear orders. This exploration leads us to an original priority proof of Spector's theorem which exposes the collapse of arithmetically defined ordinals on the recursive ones. In the context of reverse mathematics, we show that our proofs are more \textit{elementary} than those mentioned before, in the sense that they reside in the proof system ACA$_0$, which is not only strictly weaker than ATR$_0$ where all the previous proofs of both theorems reside, but is also a natural lower theory for proving Harrison's theorem.
Fichier principal
Vignette du fichier
jaf_paper.pdf (74.72 Ko) Télécharger le fichier
Origin Files produced by the author(s)
Licence
Copyright

Dates and versions

lirmm-04509148 , version 1 (18-03-2024)
lirmm-04509148 , version 2 (23-07-2024)

Licence

Copyright

Identifiers

  • HAL Id : lirmm-04509148 , version 2

Cite

Kenza Benjelloun, Bruno Durand. Infinite Time Turing Machines for elementary proofs on recursive reals. JAF 2024 - Journées sur les Arithmétiques Faibles, Sep 2024, Passau, Germany. ⟨lirmm-04509148v2⟩
34 View
24 Download

Share

More