Infinite Time Turing Machines for elementary proofs on recursive reals
Résumé
A famous theorem of recursion theory by Joseph Harrison published in 1967 states the existence of sneaky recursive non-well-orders of which the well-ordered initial segment is longer than any recursive ordinal. This result is quite intriguing because it proves that some recursive orders are quite good at hiding their infinite descending chains.
The proofs given by J. Harrison and others from the 60s reside typically in $\text{ATR}_0$ (second order logic on integers). With the development of transfinite computational models, namely Infinite Time Turing Machines in the 2000s, and the evolution of ordinal computability theory over the past 23 years, we seized the opportunity of giving this result a more elementary proof using ITTMs. From a reverse mathematics perspective, it is interesting to present a proof assuming as little logical requirements of the arithmetical hierarchy as possible and our proof is in $ \text{ACA}_0$. Moreover, our work paves the way for an explicit construction of such orders.
Domaines
Informatique [cs]Origine | Fichiers produits par l'(les) auteur(s) |
---|