# Infinite time Turing machines for elementary proofs on recursive reals

Kenza Benjelloun, Bruno Durand

► To cite this version:

Kenza Benjelloun, Bruno Durand. Infinite time Turing machines for elementary proofs on recursive reals. Journée des Arithmétiques Faibles, Julien Cervelle, Sep 2024, Passau, Germany, Germany. hal-04793621v2

HAL Id: hal-04793621

https://univ-cotedazur.hal.science/hal-04793621v2

Submitted on 3 Feb 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

Public Domain
# Infinite Time Turing Machines for elementary proofs on recursive reals

Kenza Benjelloun<fnref n="1" /> and Bruno Durand<fnref n="2" />

Erratum

We apologize, an error was found in our paper. A corrected version will soon be published. Many thanks to our readers for their understanding.

**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 [2].

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 *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.

# 1 Introduction

Our goal in this paper is to explain with elementary arguments why recursive orders with a non-recursive well ordered initial segment do exist, thus proving Harrison's theorem. In terms of reverse mathematics, our proof resides in the logic system $ACA_0$ – the lowest proof system for proving this theorem. $ACA_0$ is equiconsistent with first order Peano arithmetic. It contains the latter plus the

<footnote n="1">¹ Department of Mathematics and Geoscience University of Trieste, Italy, Laboratoire d'Informatique, Signaux et Systèmes de Sophia-Antipolis (I3S) de l'Université Côte d'Azur, Sophia-Antipolis, France</footnote>

<footnote n="2">² LIRMM, Université de Montpellier, CNRS, Montpellier, France</footnote>
comprehension scheme for arithmetical formulas. Our proof is a construction
from below, and furthermore, we explicitly construct the order by an infinite
time Turing machine using techniques developped in [6,4,5].

In the literature, one can find several proofs of Harrison’s theorem, by Harrison himself [7] and others in textbooks. All these proofs reside in ATR₀ because they require a rather strong theory with arithmetical transfinite recursion – in other terms, they are second order over integers (in Π₁). ATR₀ is a strictly stronger theory than ACA₀ because it proves the consistency of ACA₀.

## 2 Recursive relations, orders and ordinals

We start our contribution by an exploration of the properties of linear orders
which lead us to the crucial Spector's theorem. Our proof uses finite priority
arguments and seems to be new.

In all our paper we deal only with relations, orders and ordinals of *countable support*. We denote by $\langle a, b \rangle$ the classical pairing function which is bijective form $N^2$ to $N$. A real is an infinite sequence of bits indexed by integers and a countable relation (order, ordinal) is encoded by a real $r$ in such a way that $r_{\langle a,b \rangle} = 1$ iff $aRb$ (or $a \prec b$ depending on the context). A relation is total if its support is $N$ and by support we mean those integers that are in relation with another integer.

*An enumerable binary relation can be recursively transformed into a total binary relation.* This precisely means that if there exists an *enumerable real* $r$ representing an infinite binary relation, then there exists an *enumerable real* $r'$ isomorphic to the restriction of $r$ to its support, which encodes a total relation. In other term, we can recursively rename points of the support using all integers and thus keep the relation *enumerable*.

*Enumerable ordinals are recursive.* This also holds in the wider case of anti-symmetric irreflexive binary relations. We first transform the *enumerable ordinal* into a total ordinal as explained above and then we decide this total order – a standard basic recursion theory proof: to decide if $a \prec b$, we enumerate the total order and wait until either $a \prec b$ or $b \prec a$ is enumerated.

*All initial segments of recursive ordinals are also recursive.* If we deal with the initial segment $I_m = \{x, x \prec m\}$ we just have to construct the order defined by $a \prec' b$ iff $a \prec m \land b \prec m \land a \prec b$. This is a recursive construction.

**Theorem 1 (Spector).** Let $\varphi$ be a formula in the arithmetical hierarchy and $\varphi$
characterises an ordinal $\alpha$, then $\alpha$ is a recursive ordinal.

Unlike the original proof, we construct this result from below. We first prove
that if $\varphi$ is in $0'$ then $\alpha < \alpha'$ where $\alpha'$ is an *enumerable ordinal* bounded
by $\alpha.\omega$. This is the difficult part of the proof – we use a finite injury priority
argument. This result is mentioned in [1] as theorem 9.11, but the proof itself
cannot be found. According to above results, $\alpha'$ is also *recursive*, hence $\alpha$ is an
initial segment of $\alpha'$ and is also *recursive*. Then we remark that our proof can
be relativised. Thus, if $\varphi$ is in the *arithmetical hierarchy*, it is also in some set
$O^{(n)}$ and by finite induction, $\alpha$ is recursive.
Please note that this transformation is not effective: we cannot transform
recursively $\varphi$ into a program of a Turing machine that computes $\alpha$.

### 3 Ordinal type of the well-ordered initial segment

**Theorem 2 (Harrison).** *There exists a recursive linear order of which the ordinal type of the well-ordered initial segment is exactly $\omega_1^{CK}$ (the latter being defined as the supremum of recursive ordinals).*

Another formulation of this theorem which is more adapted for proving in our announced proof system ACA₀ is as follows: there exists a recursive order such that any recursive ordinal is a prefix of this order. This formulation may seem weaker than the theorem, but it is not since any initial segment of a recursive order is also recursive. The supremum of the initial recursive ordinals in the Harrison order is thus not a single point and we can deduce that this order consists of $\omega_1^{CK}$ followed by a non-well order (such as $\mathbb{Q}$). The present reasoning requires manipulation of $\omega_1^{CK}$ and thus is of higher order.

To prove this theorem, we need to place our reasoning in a logical framework strong enough to allow sufficient machinery to form sets based on arithmetical properties. Since recursive sets and their properties are arithmetical, the minimum requirement would be a proof sub-system allowing comprehension for arithmetical (first order definable) sets. This is exactly ACA₀.

It is a natural lower bound for proving the existence of such orders, and this is where our proof by infinite time Turing machines (ITTM) resides. Our chosen computation machines, ITTMs, can be much more powerful – when they are allowed long computation times. But when they are run in times bounded by $\omega_1^{CK}$ (recursive ordinal times), then their behaviour is arithmetical.

We design a super-task algorithm by constructing an ITTM that performs a succession of simple algorithmic tasks. Let us first explain the core routine. It takes as input an integer $n$ and considers it as a program number for a (classic) Turing machine (TM). It first simulates this Turing machine and checks that it writes a real (i.e. that it halts in finite time on all integer inputs and outputs either 0 or 1). This task is completed in time $\omega$. Next, it checks that the real encodes an order (antireflective, antisymmetric and transitive relation) which takes an additional time $\omega$. Then the delicate task is to check for well-ordering. This is done by emptying the order from bottom to top and requires a time $\alpha+\omega$ where $\alpha$ is the ordinal type of the well ordered initial segment. Note that if $\alpha$ is recursive then so is the total running time of the routine.

Now let us complete our proof by contradiction. Suppose that all well-orders $\alpha$ associated to different TMs $n$ are recursive. We can ITTM-run all machines $n$ sequentially for all inputs $m$ and then halt. If such a computation by ITTM existed, then this ITTM would halt in time the supremum of recursive ordinals $\omega_1^{CK}$, which is not clockable<fnref n="3" /> because of its admissibility<fnref n="4" />. So such a machine

<footnote n="3">³ An ordinal $\alpha$ is clockable if there exists an ITTM which halts in $\alpha$ steps</footnote>

<footnote n="4">⁴ An ordinal is said to be admissible if it cannot be defined from below by a first-order formula.</footnote>
cannot exist, and *ad absurdum* the $\alpha$'s are not all recursive : they are sometimes
$\omega_1^{CK}$. Harrison's theorem is proved. The last part of our proof is again above
ACA₀. In order to keep our proof in ACA₀, we replace the last argument by the
fact that ITTM computation in time $\beta$ lays in $\Sigma_1(L_\beta)$ and that a $\Sigma_1$ sum of
recursive ordinals is also recursive, contradicting our hypothesis. □

With an extension of our construction<fnref n="5" />, we can describe an ITTM computing
all *Harrison numbers*<fnref n="6" />. It runs all TMs *n* in parallel, flagging the cell number
*n* of its output tape when *n* is a Harrison number. Once we exceed $\omega_1^{CK}$ steps
the indices of cells set at 1 are exactly those numbers. At the smallest clockable
step which follows, $\omega_1^{CK} + \omega$, our ITTM has checked that no new halting of our
process for testing well-ordering has occurred and halts.

References

1. C. J. Ash and J. Knight. *Computable Structures and the Hyperarithmetical Hierarchy*. Elsevier Science B.V., Sara Burgerhartstraat 25 P.O. Box 211, 1000 AE Amsterdam, The Netherlands, 2000.

2. Kenza Benjelloun and Bruno Durand. Infinite time turing machines for elementary proofs on recursive reals. http://hal-lirmm.ccsd.cnrs.fr/lirmm-04509148, 2024.

3. Kenza Benjelloun, Bruno Durand, and Gregory Lafitte. Writability of reals by infinite time turing machines. http://hal-lirmm.ccsd.cnrs.fr/lirmm-04505369, 2024.

4. Merlin Carl, Bruno Durand, Grégory Lafitte, and Sabrina Ouazzani. Admissibles in gaps. In Jarkko Kari, Florin Manea, and Ion Petre, editors, *Unveiling Dynamics and Complexity - 13th Conference on Computability in Europe, CiE 2017, Turku, Finland, June 12-16, 2017, Proceedings*, volume 10307 of *Lecture Notes in Computer Science*, pages 175-186. Springer, 2017.

5. Bruno Durand and Grégory Lafitte. An algorithmic approach to characterizations of admissibles. In Florin Manea, Barnaby Martin, Daniël Paulusma, and Giuseppe Primiero, editors, *Computing with Foresight and Industry - 15th Conference on Computability in Europe, CiE 2019, Durham, UK, July 15-19, 2019, Proceedings*, volume 11558 of *Lecture Notes in Computer Science*, pages 181-192. Springer, 2019.

6. Joel D. Hamkins and Andy Lewis. Infinite time Turing machines. *Journal of Symbolic Logic*, 65(2):567-604, 2000.

7. Joseph Harrison. Recursive pseudo-well-orderings. *Transactions of the American Mathematical Society*, 131:526-543, 1968.

<footnote n="5">⁵ In [3], we have detailed the exact procedures and halting times for writing reals with ITTMs, so this is a nice reference in case the reader is not familiar with these types of algorithms.</footnote>

<footnote n="6">⁶ Harrison numbers are programs of Turing machines that compute a recursive order such that any recursive ordinal is a prefix of this order.</footnote>