Infinite Time Turing Machines for elementary proofs on recursive reals - LIRMM - Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier Accéder directement au contenu
Communication Dans Un Congrès Année : 2024

Infinite Time Turing Machines for elementary proofs on recursive reals

Résumé

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
Origine Fichiers produits par l'(les) auteur(s)
Licence
Copyright (Tous droits réservés)

Dates et versions

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

Licence

Copyright (Tous droits réservés)

Identifiants

  • HAL Id : lirmm-04509148 , version 2

Citer

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⟩

Collections

CNRS ESCAPE LIRMM
13 Consultations
14 Téléchargements

Partager

Gmail Mastodon Facebook X LinkedIn More