Computability and non-monotone induction

Abstract

Non-monotone inductive definitions were studied in the late 1960’s and early 1970’s with the aim of understanding connections between the complexity of the formulas defining the induction steps and the ordinals measuring the rank of the inductive process. In general, any type 2 functional will generate an inductive process, and in this paper we will view non-monotone induction as a functional of type 3. We investigate the associated computation theory of this functional inherited from the Kleene schemes and we investigate the associated companion of sets with codes computable in the functional of non-monotone induction. The interest in this functional is motivated from observing that constructions via non-monotone induction appear to be natural in classical analysis.

There are two groups of results: We establish strong closure properties of the least ordinal without a code computable in the functional of non-monotone induction, and we provide a characterisation of the class of functionals of type 3 computable from this functional, a characterisation in terms of sequential operators working in transfinite time. We will also see that the full computational power of non-monotone induction is required when this principle is used to construct functionals witnessing the compactness of the Cantor space and of closed, bounded intervals.

Keywords

Non-monotone induction Kleene computability sequential procedures reflection properties

1. Introduction

1.1. Motivation and history

With the introduction of set theory in the second half of the 19th century, mathematicians had more tools in their toolbox than before, they had a richer language in which to express mathematical properties, but they also had tools like transfinite recursion and the use of the axiom of choice. One of these tools, inspired from the new ordinal numbers introduced by Cantor, is non-monotone induction over the set of integers, seen as an operator of order four, or of type 3 in the terminology of type theory.

It is worth noticing that the set-theoretical language mostly used at the time is of third order, while coding is needed to capture the same concepts in second order arithmetic (SOA). In a series of papers [16–27], Sam Sanders and the author have investigated the logical and computability strength of some of the results using such tools, when expressed in a language close to how it was originally done. To be more precise, we worked in the framework of Kohlenbach [11] of higher order reverse mathematics combined with Kleene’s [10] model for higher order computability.

Non-monotone inductive definitions were studied in the late 1960’s and early 1970’s, but the general interest has been low since then. Examples of papers on the subject are [1,2,4,29]. The inductive definitions were classified according to the complexity of the formulas defining them, and the key property of interest was the complexity of the corresponding closure ordinals. This could be expressed in terms of reflection properties as in [29] or by comparing classes of closure ordinals as in [1].

In this paper we will study non-monotone inductive definability over $N$ via a functional $I$ of type 3 (Definition 2.1), and investigate the computational strength of $I$ in terms of Kleene’s model for higher order computations. As there is no justifiable Church–Turing thesis for the computability theory of higher order functionals, Kleene computability is just one possible model, but since this model has proved to be fruitful for the analysis of discontinuous functionals of type 2, and for computability relative to the Superjump as defined by Gandy [6], see Harrington [8], Kleene computability is a natural model for the investigation of the computational strength of non-monotone induction. We also aim to characterise the class of functionals of type 3 computable in $I$ in a way that is less model-dependent.

The motivation for bringing up non-monotone induction once again is the observation that this functional represents a natural upper complexity-bound for a number of functionals appearing as realisers for classical theorems, such as the Heine–Borel theorem and the Baire Category theorem, when these theorems are expressed in a higher order language and not within the restricted language of second order arithmetic.

The first application of non-monotone inductive definitions known to the author is due to E. Borel [3]. The motivation of Borel was to give a direct proof of the theorem now known as the Heine–Borel theorem. The assumption was that we are given a way to associate an open neighbourhood $O_{x}$ to each x in a closed interval $[a, b]$ and the claim was that we can then explicitly find a finite sub-covering of this covering. In the terminology of today, Borel constructed a functional taking the map $x \mapsto O_{x}$ as the argument and yielding a finite subcovering as the value. The definition/construction of this functional is by transfinite recursion, building up finite subcoverings of larger and larger closed subintervals, a construction that can be viewed as a simultaneous non-monotone inductive definition of Dedekind cuts for numbers $c ⩽ b$ and finite subcoverings of each closed interval $[a, d]$ for $d < c$ . In [16], a realiser $Θ_{0}$ of the uncountable Heine–Borel theorem ( $HBU$ ) is defined. This realiser selects a finite set $x_{1}, \dots, x_{n}$ such that the corresponding open neighbourhoods form a subcovering. $Θ_{0}$ is essentially the operator constructed by Borel. It is proved in [16] that $Θ_{0}$ , in conjunction with $^{2} E$ , computes the Suslin functional (see below), and in Normann [15, Theorem 1(c)] it is shown that any realiser Θ of $HBU$ as above, in conjunction with the Suslin operator, computes the functional $I$ to be defined below. We will slightly improve this theorem, see Section 6.2.

Realisers Ξ for the Lindelöf lemma for Baire space $N^{N}$ (homeomorphic to the irrationals) is one class of functionals discussed in [15], where it is proved in Theorem 1 that any such realiser will compute $I$ and that there is at least one such realiser computable in $I$ . Thus non-monotone induction reflects the complexity of witnessing the Lindelöf lemma in this special case.

In [20] the aim is to investigate real line topology with the purpose of classifying the complexity of theorems and concepts in terms of their reverse mathematics and computational complexity. Representations of open sets, such as being countable unions of rational neighbourhoods, are based on mathematical insight, and analysing the logical and computational strength of such insight is part of the aim of [20]. Given representations of open sets as in classical reverse mathematics, using second order arithmetic, the Baire Category Theorem is effective in the sense that given (a representation of) a sequence of dense open sets we can compute a fast-converging Cauchy-sequence for a point in the intersection. In [20, Theorem 6.5] it is proved that, using non-monotone induction, we can find a functional ξ taking a sequence ${X_{k}}_{k \in N}$ of subsets of $R$ as arguments and yielding an $x \in R$ as value, such that whenever each $X_{k}$ is dense and open then $\begin{matrix} ξ ({X_{k}}_{k \in N}) \in ⋂_{k \in N} X_{k} . \end{matrix}$ In [20, Theorem 6.6] it is proved that no such functional ξ can be computable in any functional of type 2, but it remains open to decide if the full power of non-monotone induction is needed for obtaining a functional ξ like this.

1.2. Overview and results

In Section 2 we will define the functional $I$ that is our main subject of investigation, and we will define the Kleene-computations via the schemes S1-S9 with $I$ as the one argument of type 3. We observe two interpretations of these schemes, one where we follow Kleene and restrict the application scheme S8 to total inputs and one where we relax on this requirement. We show that the two interpretations lead to the same class of functions of type 1 computable in $I$ . We use this to prove what is known as stage comparison and Gandy selection for the interpretation using partial inputs.

In Section 3 we investigate the least ordinal π not computable in $I$ , and the associated companion $L_{π}$ . We prove that the set of codes $f \in N^{N}$ of π is not computable in $I$ , and thus in particular not a $Π_{1}^{1}$ -set (Corollary 3.8). We also establish a number of closure properties and reflection properties for $L_{π}$ .

Section 4 is a preparation for Section 5. In Section 4 we introduce what we call hyper-sequential procedures and in Section 5 we narrow down this concept to inductive procedures. These procedures model nested systems of non-monotone inductions, using our new concept of blockings to organise the nesting. The inductive procedures can be used to characterise the class of functionals of type 3 computable in $I$ .

In Section 6 we look at some of the functionals serving as realisers for classical theorems in analysis, primarily theorems where the proof in some way depends on the compactness of the unit line or Cantor space. We will see that when such realisers are constructed in a natural way, they implicitly have the full power of non-monotone induction. In conjunction with the Suslin functional S, all realisers of the theorems in question will compute $I$ . We will illustrate how to use compactness for computing $I$ in the proof of Lemma 6.9, a lemma that is a slight improvement of [15, Theorem 1 (c)].

In Section 7 we briefly discuss what it means to relativise these results to functionals of type 2 and in Section 8 we summarise the paper and discuss a few open problems.

2. Non-monotone induction and computability

2.1. Inductive definitions

Mathematically we can identify the Cantor set $C = {0, 1}^{N}$ with the powerset $P (N)$ of the integers, where we identify a set with its characteristic function. In this paper, we will use both notations, as it sometimes is essential that we consider the set $C$ , the compact set of infinite binary sequences, and sometimes more natural to consider the set $P (N)$ where the inclusion ordering is essential. The latter view will be relevant when we define non-monotone induction, but mathematically we use $C$ as the formal definition of the set under consideration, and treat it as $P (N)$ when this is convenient. When elements of $C$ are viewed as characteristic functions, the point-wise ordering ⩽ coincides with the inclusion ordering ⊆.

Definition 2.1.
Let $F : C \to C$ be a functional of type 2.
We view F as an inductive definition, defining the increasing sequence $f_{β}$ in $C$ , where β runs over the countable ordinals, by transfinite recursion as follows:

$f_{0}$ is the constant zero

$f_{β + 1} = max {f_{β}, F (f_{β})}$

If β is a limit ordinal, $f_{β} = {sup}_{γ < β} f_{γ}$ .

There will, for cardinality reasons, be a least countable ordinal $α_{F}$ such that $f_{α_{F}} = f_{α_{F} + 1}$ . Then $α_{F}$ is the least ordinal α such that $F (f_{α}) ⩽ f_{α}$ . We let $I$ be defined by $I (F) = f_{α_{F}}$ , with the notation introduced above.
If we need to point to the functional F, we write $f_{β}^{F}$ .
Remark 2.2.
If $F : C \to C$ is monotone, that is, if $f ⩽ g \to F (f) ⩽ F (g)$ , we say that the corresponding induction is monotone. With our terminology, the class of non-monotone inductive definitions will include the class of monotone ones.
Remark 2.3.
We are not fully in the realm of Kleene-computability, since this is developed for total functionals of pure type only. However, if G is of pure type 2, we may consider G as a code for $\begin{matrix} F_{G} (f) (n) = min {G (n ˆ f), 1}, \end{matrix}$ where $f \in C$ and with the standard concatenation-understanding of $n ˆ f \in N^{N}$ . Using standard coding, we my also consider $I$ as a functional of pure type 3. For the sake of readability, we prefer to use a customised version of Kleene’s definition, as defined in Section 2.2, when we investigate the computational strength of $I$ .1
¹
In [25] we have introduced an alternative, but equivalent, version of Kleene computability. This approach is based on typed λ-calculus and deals directly with mixed types.

Example 1.
We view $C$ as the powerset of $N$ and let $G : C \to N$ . For pure cardinality reasons, there must be $A \neq B \subseteq N$ such that $G (A) = G (B)$ , and by the axiom of choice there will be a functional Φ such that for every G, $Φ (G)$ is such a pair. Now, the axiom of choice is not needed for this, as will be seen from an easy application of $I$ :

Given $G : C \to N$ , let $F_{G}$ be defined by $F_{G} (A) = A \cup {G (A)}$ . We then see that the transfinite iteration of $F_{G}$ will generate a strictly increasing sequence of sets ${A_{β}}_{β ⩽ α}$ exactly until we have an α, and a $β < α$ , such that $G (A_{β}) = G (A_{α})$ .

In [22] the complexity of such functionals Φ witnessing that there is no injection from $C$ to $N$ is studied in more detail, and it is proved that no such functional can be computed from an object of type two.

2.2. Kleene computability

Kleene [10] defined a relation ${e} (\vec{Φ}) = a$ , in the form of a positive inductive definition with nine cases, where e is an index, a natural number that serves as a Gödel number for a generalised algorithm, and $\vec{Φ}$ is a sequence of functionals of pure types in the type-structure of total functionals. The nine cases in the definition are called schemes and are numbered as S1–S9. For a recent introduction to Kleene computability, see Longley and Normann [12, Chapter 5]. For an alternative approach to Kleene computability, see [25].

In this section we will mainly be concerned with computations of the form $\begin{matrix} {e} (I, \vec{F}, \vec{f}, \vec{a}) \end{matrix}$ where $\vec{F}$ is a sequence of functionals of type 2, $\vec{f}$ is a sequence of functions of type 1 and $\vec{a}$ is a sequence from $N$ . In Definition 2.4 we will restrict S1–S9 to this case. In Section 4.2 we will give a more general version of S8, accommodated to the content of that section. Our version of S8 here, when restricted to the use of $I$ as the only object of type 3, will be equivalent to using the version of S8 in Section 4.2 to the functional of pure type 3 that will represent $I$ .

Definition 2.4.
Using transfinite recursion, we define the relation ${e} (I, \vec{F}, \vec{f}, \vec{a}) = c$ , where $I$ is as defined, $\vec{F} = (F_{1}, \dots, F_{m})$ is a sequence from $N^{N} \to N$ , $\vec{f} = (f_{1}, \dots, f_{n})$ is a sequence from $N^{N}$ , $\vec{a} = (a_{1}, \dots, a_{k})$ is a sequence from $N$ and $c \in N$ , as follows.
If $e = ⟨ 1 ⟩$ , then ${e} (I, \vec{F}, \vec{f}, \vec{a}) = a_{1} + 1$ .

If $e = ⟨ 2, q ⟩$ , then ${e} (I, \vec{F}, \vec{f}, \vec{a}) = q$ .

If $e = ⟨ 3 ⟩$ , then ${e} (I, \vec{F}, \vec{f}, \vec{a}) = a_{1}$ .

If $e = ⟨ 4, e_{1}, e_{2} ⟩$ , ${e_{2}} (I, \vec{F}, \vec{f}, \vec{a}) = b$ and ${e_{1}} (I, \vec{F}, \vec{f}, b, \vec{a}) = c$ , then ${e} (I, \vec{F}, \vec{f}, \vec{a}) = c$ .

If $e = ⟨ 6, e_{1}, τ_{1}, τ_{2}, τ_{3} ⟩$ , where $τ_{1}$ , $τ_{2}$ and $τ_{3}$ are (integer codes of) permutations of (the index sets for) the input sequences $\vec{F}$ , $\vec{f}$ and $\vec{a}$ , then ${e} (I, \vec{F}, \vec{f}, \vec{a}) = {e_{1}} (I, {\vec{F}}_{τ_{1}}, {\vec{f}}_{τ_{2}}, {\vec{a}}_{τ_{3}})$ .

If $e = ⟨ 7 ⟩$ , then ${e} (I, \vec{F}, \vec{f}, \vec{a}) = f_{1} (a_{1})$ .

For this scheme there will be subcases, one for each type $> 1$ . For us, there will be two subcases, where the case for type 3 is where we adjust the definition to application of $I$ :

If $e = ⟨ 8, 2, d ⟩$ then ${e} (I, \vec{F}, \vec{f}, b, \vec{a}) = F_{1} (g)$ when $g (a) = {d} (I, \vec{F}, \vec{f}, a, \vec{a})$ is a total function. We write $\begin{matrix} {e} (I, \vec{F}, \vec{f}, \vec{a}) = F_{1} (λ a . {d} (I, \vec{F}, \vec{f}, a, \vec{a})) . \end{matrix}$

If $e = ⟨ 8, 3, d ⟩$ we let ${e} (I, \vec{F}, \vec{f}, b, \vec{a}) = I (F_{G}) (b)$ where $G (f) = {d} (I, \vec{F}, f, \vec{f}, \vec{a})$ .

If $e = ⟨ 9 ⟩$ then ${e} (I, \vec{F}, \vec{f}, d, \vec{a}) = c$ if ${d} (I, \vec{F}, \vec{f}, \vec{a}) = c$ .

Remark 2.5.
We have excluded S5, the scheme of primitive recursion, from our definition. There are two reasons for this. The main reason is that one may prove the recursion theorem on the basis of the other schemes, and thus S5 will be redundant. The other reason is that, since recursion is iterated composition, all arguments involving S5 that we need will be covered by how we deal with S4.

Kleene computability inherits several of the key properties of classical computability, such as the $S_{n, m}$ -theorem and the recursion theorem. The existence of universal algorithms is axiomatised in the form of S9. In the sequel, we will assume familiarity with these basic properties.
2.3. The computability theory of $I$

We first prove that the prototype of discontinuity is computable in $I$ .

Definition 2.6.
We define the functional $^{2} E$ of type 2 by $\begin{matrix} ^{2} E (f) = \{\begin{array}{ll} 0 & if \forall k (f (k) = 0) \\ 1 & if \exists k (f (k) > 0) \end{array} \end{matrix}$
Lemma 2.7.
The functional $^{2} E$ is computable in $I$ .
Proof.
Given $f \in N^{N}$ , we want to decide if $\exists k (f (k) > 0)$ . Let $\begin{matrix} F_{f} (A) = {k : f (k) > 0} \cup {k : k + 1 \in A} . \end{matrix}$ Then $\exists k (f (k) > 0)$ if and only if $0 \in I (F_{f})$ . □
Remark 2.8.
$^{2} E$ is sometimes denoted as $\exists^{2}$ , and is equivalent, within S1–S9, to Feferman’s μ.

The Suslin functional S is defined by $\begin{matrix} S (f) = \{\begin{array}{ll} 0 & if \forall g \exists n (f (\bar{g} (n)) = 0) \\ 1 & if \exists g \forall n (f (\bar{g} (n)) > 0) \end{array} \end{matrix}$ Lemma 2.9.
The Suslin functional S is computable in $I$ .
Proof.
We use that $^{2} E$ is computable in $I$ . Given f, we let $T_{f}$ be the tree of finite sequences $s = (s_{0}, \dots, s_{n - 1})$ such that we for all $m ⩽ n$ have that $f (⟨ s_{0}, \dots, s_{m - 1} ⟩) = 0$ . Then $S (f) = 0$ if and only if $T_{f}$ is well founded. For all f, the subset of $T_{f}$ consisting of all sequences that cannot be extended to an infinite branch in $T_{f}$ can be defined using an arithmetical inductive definition, and we then use $^{2} E$ to decide if this subset is the whole tree $T_{f}$ . □

2.4. Totality vs. partiality

In the original definition of higher order computability via Kleene’s S1–S9, all objects were assumed to be total. This can be considered to be a defect of S8, where the input $λ ξ . {d} (ξ, - - - -)$ has to be defined for all ξ of the type in question in order to accept the termination of $Ψ (λ ξ . {d} (ξ, - - - -))$ , even if Ψ is defined in such a way that it only requires some values of the input functional. In the case of $I$ , we only need F to be total on the set of functions $f_{β}$ for $β ⩽ α_{F}$ in order to identify $I (F)$ , and insisting that F is defined on irrelevant arguments as well may seem as an unnatural restriction on what is considered to be an algorithm relative to $I$ .

Remark 2.10.
A similar phenomenon takes place for Gandy’s Superjump $S$ , introduced in [6]. The superjump is defined by $\begin{matrix} S (F, e) = \{\begin{array}{ll} 1 & if {e} (F, e) ↓ \\ 0 & if {e} (F, e) ↑ \end{array} \end{matrix}$ where ↓ means that there is a value of the computation, while ↑ means the converse. In order to find the value of $S (F, e)$ we only need to know F restricted to the set of f computable in F, the so called 1-section of F. This was used by Harrington [8] in an essential way when he classified the computational strength of $S$ , and was also important in Hartley’s [9] analysis of the countably based functionals (See Section 4 for a further discussion). We will show that loosening up the requirement of totality of the input functional to $I$ does not add to the computational strength of $I$ . This is as it is for $S$ , but not, for instance, as for computations with continuous inputs in general. Then we add considerable strength by relaxing on S8, see e.g. [12, Sections 6.4 and 8.5] for results and further references.
Definition 2.11.
We write ${e}_{t} (I, \vec{F}, \vec{f}, \vec{a}) = b$ if ${e} (I, \vec{F}, \vec{f}, \vec{a}) = b$ according to the original definition, while we write ${e}_{p} (I, \vec{F}, \vec{f}, \vec{a}) = b$ if we interpret S8 according to the following extension of $I$ to partial $F : C \to C$ . We will not accept non-total inputs to F, and for each $f \in C$ we either have that $F (f) \in C$ or $F (f)$ is totally undefined. We stick to the notation from Section 2.1:
By recursion on the ordinal β, $f_{β}^{F}$ is defined if $β = 0$ or $β > 0$ and both $f_{γ}^{F}$ and $F (f_{γ}^{F})$ are defined for all $γ < β$ .

$I (F)$ is defined if there is an ordinal α such that $f_{α + 1}^{F}$ is defined and $f_{α}^{F} = f_{α + 1}^{F}$

If $I (F)$ is defined, and α is as in (ii), $I (F) (n) = f_{α}^{F} (n)$ for each $n \in N$ .

When the context is clear, we will talk about t-computations and p-computations.
Theorem 2.12.
There is a computable (in the sense of Turing) function ρ such that if ${e}_{p} (I, \vec{F}, \vec{f}, \vec{a}) = b$ , then ${ρ (e)}_{t} (I, \vec{F}, \vec{f}, \vec{a}) = b$ .
Proof.
We use the recursion theorem to define ρ, and define it by cases according to S1–S9. It is obvious what to do in all cases except application of $I$ . The final correctness proof will, of course, be by induction on the complexity of the ${e}_{p}$ -computation (we will define the rank or norm of a terminating computation formally below, definitions that do not rely on the correctness of this theorem), but as is common for this kind of argument, we assume that ρ does the job on all subcomputations, and we define ρ by self-reference.

So assume that $\begin{matrix} {e}_{p} (I, \vec{F}, \vec{f}, b, \vec{a}) = I (F_{G_{p}}) (b) \end{matrix}$ where $G_{p} (f) = {d}_{p} (I, \vec{F}, f, \vec{f}, \vec{a})$ , and that the recursion terminates as defined in Definition 2.11. Assume further, as an induction hypothesis, that we can replace $G_{p}$ with the, still partial, $\begin{matrix} G_{t} (f) = {ρ (d)}_{t} (I, \vec{F}, f, \vec{f}, \vec{a}) . \end{matrix}$

We assume familiarity with the concept of a prewellordering R on a domain $D \subseteq N$ . Since $^{2} E$ and S are t-computable in $I$ , we also have that the set of prewellorderings will be t-computable in $I$ .

If R is a prewellordering on D, each element in the domain D will have an ordinal rank, and we let $R_{β}$ be the elements in D with ordinal rank below β. We will construct a total functional H mapping prewellorderings to prewellorderings such that we can decide $b \in I (F_{G_{t}})$ from $I (H)$ . The definition of $H (R)$ is as follows, observing that we only need $^{2} E$ when we know that R is a prewellordering. We let $f_{β}$ be as in the definition of $I (F_{G_{t}})$ , and we identify $f_{β}$ with $A_{β} = {b \in N : f_{β} (b) = 1}$ .

– By R-recursion, compare $R_{α}$ with $A_{α}$ until we either have disagreement or that $R_{α} = A_{α}$ with $F (A_{α}) \subseteq A_{α}$ .

– In the first case, α must be a successor ordinal $β + 1$ . We let $H (R)$ be R restricted to $R_{β} = A_{β}$ , and then end-extended with $F (A_{β}) ∖ A_{β}$ . In the other case we let $H (R)$ be R restricted to $R_{α}$ .

Since we only will ask for values $F (A_{β})$ in the computation of $H (R)$ , our assumption shows that H is total. $I (H)$ will be a prewellordering R, and we will have that it matches the prewellordering induced by $F_{G_{t}}$ . We then have that $\begin{matrix} b \in I (F) \Leftrightarrow b \in dom (I (H)) . \end{matrix}$ It is now a matter of routine to define a suitable candidate for $ρ (⟨ 8, d ⟩)$ in a computable way from d and an alleged index for ρ, so we may define a working ρ by the classical recursion theorem. □

From now on, when we write ${e}$ , we mean ${e}_{p}$ .
2.5. The norm of a computation and Gandy selection

The advantage of using p-computations is that now all computation trees will be countable, and all computations will have a countable ordinal as rank. We give a direct definition of this rank. In order to simplify the readability we introduce the following as a convention: With the expression $λ (g, c) . {d} (I, \vec{F}, g, \vec{f}, c, \vec{a})$ we really mean the function $\begin{array}{r} (*) F (g) (c) = min {1, {d} (I, \vec{F}, c ˆ g, \vec{f}, \vec{a})} . \end{array}$

Definition 2.13.
Let $C_{I}$ be the set of finite sequences $⟨ e, \vec{F}, \vec{f}, \vec{a} ⟩$ such that for some b we have $\begin{matrix} {e} (I, \vec{F}, \vec{f}, \vec{a}) = b . \end{matrix}$ If $⟨ e, \vec{F}, \vec{f}, \vec{a} ⟩ \in C_{I}$ we define the rank or ordinal norm $‖ ⟨ e, \vec{F}, \vec{f}, \vec{a} ⟩ ‖$ by transfinite recursion as follows:
If e corresponds to S1–S3 or S7, we let the norm be zero.

If ${e} (I, \vec{F}, \vec{f}, \vec{a}) = {e_{1}} (I, \vec{F}, \vec{f}, {e_{2}} (I, \vec{F}, \vec{f}, \vec{a}), \vec{a})$ , where ${e_{2}} (I, \vec{F}, \vec{f}, \vec{a}) = c$ , we let $\begin{matrix} ‖ ⟨ e, \vec{F}, \vec{f}, \vec{a} ⟩ ‖ = max {‖ ⟨ e_{2}, \vec{F}, \vec{f}, \vec{a} ⟩ ‖, ‖ ⟨ e_{1}, \vec{F}, \vec{f}, c, \vec{a} ⟩ ‖} + 1 . \end{matrix}$ The cases S6 and S9 are handled in a similar way, and are left for the reader.

If ${e} (I, \vec{F}, \vec{f}, \vec{a}) = F_{1} (g)$ where $g (b) = {d} (I, \vec{F}, \vec{f}, b, \vec{a})$ we let $\begin{matrix} ‖ ⟨ e, \vec{F}, \vec{f}, \vec{a} ⟩ ‖ = sup {‖ ⟨ d, \vec{F}, \vec{f}, b, \vec{a} ⟩ ‖ + 1 : b \in N} \end{matrix}$

If ${e} (I, \vec{F}, \vec{f}, b, \vec{a}) = I (λ (g, c) . {d} (I, \vec{F}, g, \vec{f}, c, \vec{a})) (b)$ , we let F be as in $(*)$ , and we let α and $f_{β}$ for $β ⩽ α$ be as in the definition of $I$ . By the assumption, $f_{β}$ is well defined and total for all $β ⩽ α$ , where $F (f_{α}) ⩽ f_{α}$ . We let $\begin{matrix} ‖ ⟨ e, \vec{F}, \vec{f}, b, \vec{a} ⟩ ‖ = sup {‖ ⟨ d, \vec{F}, c ˆ f_{β}, \vec{f}, \vec{a} ⟩ ‖ + 1 : β ⩽ α \land c \in N} . \end{matrix}$
If $⟨ e, \vec{F}, \vec{f}, \vec{a} ⟩ \notin C_{I}$ we let $‖ ⟨ e, \vec{F}, \vec{f}, \vec{a} ⟩ ‖ = ℵ_{1}$ , the first uncountable ordinal.
Lemma 2.14 (Stage Comparison).

There is a partial functional P in two variables, p-computable in $I$ , such that

$P (⟨ e, \vec{F}, \vec{f}, \vec{a} ⟩, ⟨ d, \vec{G}, \vec{g}, \vec{c} ⟩)$ terminates if at least one of $⟨ e, \vec{F}, \vec{f}, \vec{a} ⟩$ and $⟨ d, \vec{G}, \vec{g}, \vec{c} ⟩$ is in $C_{I}$ and then

$P (⟨ e, \vec{F}, \vec{f}, \vec{a} ⟩, ⟨ d, \vec{G}, \vec{g}, \vec{c} ⟩) = 1$ if $‖ ⟨ e, \vec{F}, \vec{f}, \vec{a} ⟩ ‖ ⩽ ‖ ⟨ d, \vec{G}, \vec{g}, \vec{c} ⟩ ‖$

$P (⟨ e, \vec{F}, \vec{f}, \vec{a} ⟩, ⟨ d, \vec{G}, \vec{g}, \vec{c} ⟩) = 0$ if $‖ ⟨ d, \vec{G}, \vec{g}, \vec{c} ⟩ ‖ < ‖ ⟨ e, \vec{F}, \vec{f}, \vec{a} ⟩ ‖$ .

Proof.
We use the recursion theorem to construct P, and the definition is split into 81 cases, according to the schemes corresponding to e and d. S8 splits into two cases, S8.2 and S8.3 for applications of $F_{1}$ and $I$ , while S5 is redundant and left out. This is why we have $9 \times 9$ cases. Strictly speaking there are 100 cases, because we must say what P does in cases where one or both indices do not correspond to Kleene-indices at all, but we leave these trivial cases for the reader. Fortunately, many other cases are trivial as well, in particular those where one of the indices e or d represents a basic computation via S1–S3 or S6. Moreover, all cases not involving S8.3 are covered by the literature, see e.g. [6].

We will give the details for three cases (S4, S8.3), (S8.2, S8.3) and (S8.3, S8.3). The remaining cases follow by similar, or even simpler, arguments. As is normal practise for this kind of construction/proof we define P by self reference, assuming for each case, as an induction hypothesis, that P works for the immediate subcomputations.

Case (S4, S8.3): Let $\begin{matrix} {e} (I, \vec{F}, \vec{f}, \vec{a}) = {e_{1}} (I, \vec{F}, \vec{f}, {e_{2}} (I, \vec{F}, \vec{f}, \vec{a}), \vec{a}) \end{matrix}$ and let $\begin{matrix} {d} (I, \vec{G}, \vec{g}, b, \vec{c}) = I (G) (b), \end{matrix}$ where $G = λ (g, c) . {d_{1}} (I, \vec{G}, c ˆ g, \vec{g}, \vec{c})$ .

Let $g_{α}$ be element α in the sequence inductively defined from G. We now consider the following induction, that can easily be formalised via an inductive definition:

Use P to compare $‖ ⟨ e_{1}, \vec{F}, \vec{f}, \vec{a} ⟩ ‖$ with the ranks needed to compute $g_{0}$ , $g_{1}$ , … until the first is bounded in norm by one of the latter computations or until the latter induction terminates.

In the first case, let $c = {e_{2}} (I, \vec{F}, \vec{f}, \vec{a})$ and start over again, now comparing the computations involved in computing the $g_{α}$ ’s with $‖ ⟨ e_{1}, \vec{F}, \vec{f}, c, \vec{c} ⟩ ‖$ .

If $‖ ⟨ e, \vec{F}, \vec{f}, \vec{a} ⟩ ‖ ⩽ ‖ ⟨ d, \vec{G}, \vec{g}, \vec{c} ⟩ ‖$ , this will be verified through the two inductions, and the composition will terminate at least as fast as the induction. If $‖ ⟨ d, \vec{G}, \vec{g}, \vec{c} ⟩ ‖ < ‖ ⟨ e, \vec{F}, \vec{f}, \vec{a} ⟩ ‖$ , at least one of the two inductions will result in the full induction induced by G, and we can deduce that this terminates faster than the composition.

Case (S8.2, S8.3): Let $\begin{matrix} {e} (I, \vec{F}, \vec{f}, \vec{a}) = F_{1} (f) \end{matrix}$ where $\begin{matrix} f (a) = {e_{1}} (I, \vec{F}, \vec{f}, a, \vec{a}) \end{matrix}$ and let $\begin{matrix} {d} (I, \vec{G}, \vec{g}, b, \vec{c}) = I (G) (b) \end{matrix}$ where G is as in the previous case.

As in the previous case, we simulate the induction in the second part while, at each step, comparing the length of the computations needed with those of each ${e_{1}} (I, \vec{F}, \vec{f}, a, \vec{a})$ . We use $^{2} E$ in doing this. If we for each a reach a step in the induction where we need a computation that dominates the computation of ${e_{1}} (I, \vec{F}, \vec{f}, a, \vec{a})$ , we know that the left hand side will terminate at most with the same rank as the right hand side. If we are able to complete the induction on the right hand side before termination of all sub-computations on the left hand side, we know that the right hand side terminates first. This stepwise comparison until the value of P is settled can be expressed as an inductive definition.

Case (S8.3, S8.3): Let $\begin{matrix} {e} (I, \vec{F}, \vec{f}, a, \vec{a}) = I (λ (a^{'}, f^{'}) . {e_{1}} (I, \vec{F}, a^{'} ˆ f^{'}, \vec{f}, \vec{a})) (a) \end{matrix}$ and let $\begin{matrix} {d} (I, \vec{G}, \vec{g}, b, \vec{b}) = I (λ (b^{'}, g^{'}) . {d_{1}} (I, \vec{G}, b^{'} ˆ g^{'}, \vec{g}, \vec{b})) (b) . \end{matrix}$ Notice that the norms of these computations will be independent of the choices of a and b. Let F and G be the partial functionals involved in these inductions, where at least one is sufficiently total for the induction to terminate. We now describe a simultaneous inductive definition of two increasing sequences $f_{α}$ and $g_{β}$ of elements of $C$ , where we use $^{2} E$ and P to make all the comparisons involved:
Let $f_{0} = g_{0}$ be the constant zero.

Assume that $f_{0}, \dots, f_{α}$ and $g_{0}, \dots, g_{β}$ are constructed.

Consider all computations involved in computing all $f_{δ} (a)$ for $δ ⩽ α$ and in computing $F (f_{α}) (a)$ for all a, and then consider all computations involved in computing all $g_{γ} (b)$ for $γ ⩽ β$ and in computing $G (g_{β}) (b)$ for all b.

If the norm of each computation in the first set is bounded by the norm of some computation in the second set, we add $f_{α + 1} = max {f_{α}, F (f_{α})}$ and keep $g_{0}, \dots g_{β}$ .

On the other hand, if there is one computation in the first set whose norm strictly bounds all norms of the computations in the other set, we add $g_{β + 1} = max {g_{β}, G (g_{β})}$ and keep $f_{0}, \dots, f_{α}$ .

At least one of these two inductions will terminate through this process, and when it does, we know which one will terminate with lowest ordinal rank.
We leave the formal definition of this inductive definition for the reader. □
Theorem 2.15 (Gandy Selection).

There is a p-computable selection operator ν such that for all e, $\vec{F}$ , $\vec{f}$ and $\vec{a}$ we have $\begin{matrix} \exists n {e} (I, \vec{F}, \vec{f}, n, \vec{a}) ↓ \Rightarrow {e} (I, \vec{F}, \vec{f}, ν (e, \vec{F}, \vec{f}, \vec{a}), \vec{a}) ↓ . \end{matrix}$

Proof.
This is a soft consequence of Lemma 2.14, with an argument well known in the literature, see e.g. [5, Theorem 3.1.6], [13, Theorem 3], [30, Theorem X.4.1] or the original [6]. □

For many of the inductive definitions used, we add at most one new element to the inductively defined set at each stage. Such definitions can be defined by functionals F of pure type 2, identifying $2^{N}$ with the power set of $N$ via characteristic functions: Definition 2.16.
Let $G : 2^{N} \to N$ and let $H_{G} : 2^{N} \to 2^{N}$ be defined by $\begin{matrix} H_{G} (A) = A \cup {G (A)} . \end{matrix}$ An inductive definition F is single valued if it is of the form $H_{G}$ . We let $I_{0} (G) = I (H_{G})$ .
Lemma 2.17.
The functionals $I$ and $I_{0}$ are computationally equivalent modulo $^{2} E$ .
Proof.
$I_{0}$ is trivially, and outright, computable in $I$ . In order to prove the other direction, we let $F : 2^{N} \to 2^{N}$ be given, and we will construct a single valued G that simulates F. We assume that F is nontrivial, i.e. that $F (\emptyset) \neq \emptyset$ . We let G operate on sets B of (sequence numbers of) finite binary sequences, and we totally order these sequences using the standard lexicographical ordering by first comparing the first place where two sequences are different, and if this does not help, by length. This is not a well ordering, but G, as we define it, will only generate well ordered sets of sequences. There will be three cases in the definition of $G (B)$ :
B has no maximal element s. Let A be the set of n such that $s (n) = 1$ for at least one $s \in B$ . If $F (A) \subseteq A$ , let $G (B)$ be the empty sequence. If not, let n be the least number in $F (A) ∖ A$ , and let $G (B) = s$ where s is the binary sequence of length $n + 1$ approximating the characteristic function of $A \cup F (A)$ .

If there are elements $s_{1} < \dots < s_{k}$ in B so that $B_{1} = {s \in B : s < s_{1}}$ has no maximal element and such that $\begin{matrix} B = B_{1} \cup {s_{1}, \dots, s_{k}}, \end{matrix}$ let A be the set of n such that $s (n) = 1$ for at least one s in $B_{1}$ . If the sequences $s_{1}, \dots, s_{k}$ do not approximate the characteristic function of $A \cup F (A)$ , let $G (B) = 0$ (the value does not matter), while otherwise, we let $G (B) = s$ where s is the least proper extension of $s_{k}$ that approximates $A \cup F (A)$ .

Otherwise, let $G (B) = 0$ .
The induction induced by G will, one step at the time, build up approximations to the characteristic functions of the sets appearing in the induction induced by F. If $I (F)$ uses α many steps, $I_{0} (G)$ will use $ω \cdot α$ many steps. Clearly G is computable in F and $^{2} E$ , and the closure set of F is arithmetical in the closure set of G. Thus $I$ is computable in $I_{0}$ and $^{2} E$ . □

3. The companion of $I$

In this section we will analyse the computational power of $I$ in terms of set theory. Recall that a set X is hereditarily countable if the transitive closure $trcl (X)$ is countable. Hereditarily countable sets X will have codes, essentially structures $(D, R, A)$ where $D \subseteq N$ , R is a binary relation on D, $A \subseteq D$ and $(D, R, A)$ is isomorphic to $(trcl (X), \in^{trcl (X)}, X)$ . Such codes can further be coded as functions in $N^{N}$ in a standard way.

Definition 3.1.
The companion $M$ of $I$ is defined as the set of sets X with codes that are computable in $I$ .
Remark 3.2.
The companion of other functionals are defined in analogy with this. For instance, the companion of $^{2} E$ will be $L_{ω_{1}^{CK}}$ , the companion of S (the Suslin functional) is $L_{β}$ for the first recursively inaccessible ordinal β while the companion of $S$ (the Superjump) is $L_{ρ}$ where ρ is the first recursively Mahlo ordinal.
Lemma 3.3.
There is a countable ordinal π such that $M = L_{π}$ .
Proof.
Since ${e}_{p}$ is absolute for $L$ , we have that $M$ is a transitive subset of $L$ . The set of functions computable in $I$ will be closed under a certain map sending a code for an ordinal α to a code for $L_{α}$ (this map is computable in $^{2} E$ ), so $M$ will be an initial segment of $L$ . □
Lemma 3.4.
Let $F : C \to C$ be a partial functional computable in $I$ such that $I (F)$ is defined. Let α be the corresponding closure ordinal for F. Then $α < π$ .
Proof.
For each F there is an $F^{'}$ computable in F and $^{2} E$ such that $F^{'}$ generates a prewellordering R where $R_{β + 1} = F (R_{β}) \cup R_{β}$ for each ordinal β. Then α will be the ordinal rank of the inductively definable prewellordering R so α will be computable in $I$ whenever F is computable in $I$ . □

The aim of this section is to find closure- and reflection-properties of $L_{π}$ . Since S is computable in $I$ we have that the set of codes for hereditarily countable sets is computable in $I$ . Given codes $f_{i}$ for sets $X_{i}$ , $i \in N$ „we only need $^{2} E$ to unify the codes in the form of a code for ${X_{i} : i \in N}$ . Further, given codes $f_{1}, \dots, f_{n}$ for sets $X_{1}, \dots, X_{n}$ , and a $Δ_{0}$ -formula $Φ (x_{1} \dots, x_{n})$ , $^{2} E$ can decide the truth value of $Φ (X_{1}, \dots, X_{n})$ . Finally, if $Φ (x_{1}, \dots, x_{n}, y)$ is a $Δ_{0}$ -formula, $f_{1}, \dots, f_{n}$ are codes computable in $I$ for $X_{1}, \dots, X_{n} \in L_{π}$ and $\begin{matrix} L_{π} ⊧ \exists Y Φ (X_{1}, \dots, X_{n}, Y) \end{matrix}$ then we can use Gandy selection for $I$ to compute (an index for) a code g for a set Y such that $Φ (X_{1}, \dots, X_{n}, Y)$ . This leads to a proof of
Lemma 3.5.
$L_{π}$ is an admissible structure.

Let $WO$ be the set of codes for countable ordinals. This is a $Π_{1}^{1}$ - set, and it is easy to prove that the following sets are $Π_{1}^{1}$ as well:
The set of $f \in WO$ that codes $ω_{1}^{CK}$ .

The set of $f \in WO$ that codes the first recursively inaccessible ordinal.

The set of $f \in WO$ that codes the first recursively Mahlo ordinal.
We say that these ordinals are $Π_{1}^{1}$ -characterisable. Many ordinals of distinction are $Π_{1}^{1}$ -characterisable, for instance all clockable ordinals in the sense of infinite time Turing machines ([7]), see Welch [32] for a survey and further references on such machines.
Definition 3.6.
Let P be a class of ordinals. We say that P is $I$ -decidable if there is an $I$ -computable function $Δ : N^{N} \to N$ such that $Δ (f) = 0$ if and only if f codes an ordinal α and $P (α)$ holds.

That π is not $Π_{1}^{1}$ -characterisable follows from the following much stronger:
Theorem 3.7.
Let P be a property on ordinals that is $I$ -decidable and such that $P (π)$ . Let $X \subset π$ be closed, unbounded and $Σ_{1}$ over $L_{π}$ . Then there is an $α \in X$ such that $P (α)$ .
Proof.
We can code a partially enumerated set ${f_{d} : d \in D}$ of functions as the set of pairs $⟨ d, {\overline{f}}_{d} (n) ⟩$ where $d \in D$ and $n \in N$ . The idea is to construct an inductive definition Γ that is computable in $I$ and such that Γ generates a code for an ordinal both in X and satisfying P. Γ will not be total, but sufficiently total for the induction to terminate. In defining Γ as computable in $I$ , we use that the Suslin functional S is computable in $I$ . We define $Γ (R)$ as follows:
If R does not code an enumerated set ${f_{d} : d \in D}$ of functions, we let $Γ (R) = R$ . Note that the empty set codes the empty set of functions.

Assume that R codes ${f_{d} : d \in D}$ . If $f_{d} \notin WO$ for some $d \in D$ , let $Γ (R) = R$ .

Assume now that $f_{d} \in WO$ codes $α_{d}$ for all $d \in D$ , and use $^{2} E$ to compute a code g for the least upper bound α of ${α_{d} : d \in D}$ . If all $α_{d}$ are in X, then $α \in X$ since X is closed. If $P (α)$ we let $Γ (R) = R$ . This is where we want the induction to close.

Otherwise, we apply Gandy selection for $I$ and search for an index e for a code g of an ordinal $β > α$ such that $β \in X$ . We then let $\begin{matrix} Γ (R) = R \cup {⟨ e, \overline{g} (n) ⟩ : n \in N} . \end{matrix}$
If $α < π$ , we can use the recursion theorem for $I$ to see that $L_{π}$ is closed under the α-iteration of Γ, and that Γ generates codes for an increasing sequence of ordinals $γ_{β}$ for $β < α$ . Since we always use an index e for an ordinal larger than those appearing at earlier stages, we do not risk to mix up codes for different ordinals. Since X is closed, all ordinals obtained during this iteration will be codes for ordinals $γ_{β} \in X$ . Since $P (π)$ and this induction will stop when we hit a $γ_{β}$ with $P (γ_{β})$ , and since by Lemma 3.4 no such induction will stop at π, there must be an ordinal $γ_{β} < π$ such that $P (γ_{β})$ . □
Corollary 3.8.
The closure ordinal π of $I$ is not $Π_{1}^{1}$ -characterisable.

We also have
Corollary 3.9.
The closure-ordinal π of $I$ is recursively Mahlo.
Proof.
We have to prove that if $X \subseteq π$ is π-computable, closed and unbounded, then X contains an admissible ordinal. Since the class of countable, admissible ordinals is $I$ -decidable, this is a direct consequence of Theorem 3.7. □

Since being recursively Mahlo and other even stronger closure properties are also $I$ -decidable, we may extend this argument in order to prove that π satisfies these stronger properties, and that every closed unbounded subset of π that are $Σ_{1}$ over $L_{π}$ also contain elements satisfying these stronger properties. We will not pursue this further here.

We will now consider an alternative way of expressing that π must be a “large” countable ordinal. What is “large” is of course subject to the perspective one is taking.
Definition 3.10.
An ordinal γ is reflecting if for all formulas $Φ (x_{1}, \dots, x_{n})$ and elements $X_{1}, \dots, X_{n}$ in $L (γ)$ , $\begin{matrix} L_{γ} ⊧ Φ (X_{1}, \dots, X_{n}) \Rightarrow \exists β < γ [L_{β} ⊧ Φ (X_{1}, \dots, X_{n}) .] \end{matrix}$

Note that if γ is reflecting, then γ is admissible and recursively inaccessible.
Corollary 3.11.
The closure ordinal π of $I$ is reflecting.
Proof.
If $α < β$ , $X_{1}, \dots, X_{n}$ are in $L_{α}$ and $L_{π} ⊧ Φ (X_{1}, \dots, X_{n})$ , then the set of $γ > α$ such that $L_{γ} ⊧ Φ (X_{1}, \dots, X_{n})$ is $I$ -decidable, contains π and thus, by Theorem 3.7, contains an ordinal β with $α < β < π$ . □

π will not be the least reflecting ordinal: Corollary 3.12.
Let π be the closure ordinal of $I$ . If $α < π$ , then there is a reflecting ordinal γ with $α < γ < π$ .
Proof.
This is also a consequence of Theorem 3.7, since being reflecting is $I$ -decidable. Indeed, if $X \subseteq π$ is closed, unbounded and $Σ_{1}$ over $L_{π}$ , then X contains arbitrarily large reflecting ordinals. □
Remark 3.13.
These results do of course not imply that $L_{π}$ has an elementary substructure, or even a substructure satisfying the same first order sentences. The theory of $L_{π}$ is not $I$ -decidable, so there is no way to unify these arguments to all formulas simultaneously.

4. Classes of functionals of type 3

4.1. Motivation

We introduced the functional $I$ in Section 2 and illustrated its computational strength through an analysis of the companion in Section 3. In this section we will give an analysis of computations relative to $I$ resembling an operational semantics. Our approach is inspired by the success-story of using nested sequential procedures for modelling functionals definable in LCF (Scott, [31]) or equivalently in PCF (Plotkin, [28]) from objects of type 1. For an introduction to nested sequential procedures, see [12, Chapter 6].

Since we are only concerned with functionals of type $⩽ 3$ in this paper, we can forget the qualifier ‘nested’, while we will add the qualifier ‘hyper’ in order to deal with discontinuity. We will aim for more and more restricted concepts of hyper-sequential procedures until we find a characterisation of the functionals of type 3 that are computable in $I$ and some functional of type 2. The gain will mainly be that we obtain a more civilised, and less ad hoc, way of expressing relative computability for certain functionals of type 3 than when we refer to the Kleene schemes directly. We will use this to give mathematical support to the informal claim that if realisers of classical theorems based on compactness arguments are computable in $I$ , then the full power of $I$ is required.

A functional Φ of type 3 is normal if $^{3} E$ is computable in Φ, where $\begin{matrix} ^{3} E (F) = \{\begin{array}{ll} 0 & if \forall f \in N^{N} (F (f) = 0) \\ 1 & if \exists f \in N^{N} (F (f) > 0) \end{array}, \end{matrix}$ and where F is assumed to be total.

The set of functionals of type 3 that are neither normal nor computable in type 2 objects is mainly unexplored with respect to computability-theoretical properties. The classical object of this kind is Gandy’s Superjump $S$ . $S$ is of course a natural functional in the context of higher order computability theory. Recently, examples that are natural from other perspectives have emerged. In [16, §3] we introduced classes of realisers Θ for the general Heine–Borel theorem and a weaker class of functionals Λ that compute realisers for the Vitali Covering theorem. In [15] we also considered functionals Ξ that serve as realisers for the Lindelöf Lemma for Baire Space. In this paper we introduced $I$ , which, under the name IND, was proved in [15] to compute Lindelöf realisers Ξ. This plethora of elements in a so far unexplored class of functionals justifies a more coherent study of this class. We will return to some of these functionals in Section 6.2.

In [25] we consider some other non-normal functionals of type 3, functionals that reflect natural constructions in ordinary mathematics and that are intrinsically partial. As these functionals are not computable in $I$ , they fall out of the scope of this paper, but the alternative to Kleene’s schemes introduced there may serve as an alternative foundation for what we do in Sections 4 and 5.

Hartley [9] investigated the fully typed hierarchy of hereditarily countably based functionals, based on a definition due to Stan Wainer, and he obtained some general results. For instance, he proved that if we assume the Continuum hypothesis together with ZFC, Φ is countably based if and only if $^{3} E$ is not computable in Φ and any functional of type 2.

The original definition of the countably based functionals is by a generalisation of the definition of the continuous functionals e.g. as based on domain theory, see [12, Chapter 10] for a recent introduction. In this paper, we will only be interested in objects of types 0, 1, 2 and 3, and we define the countably based functionals for these cases, suiting our own purposes:

Definition 4.1.
All integers are countably based. Moreover
All total functions $f : N \to N$ are countably based.

All partial functionals F mapping a subset of $N^{N}$ to $N$ are countably based.

Let Φ be a partial functional taking countably based functionals of type 2 as arguments and yielding integers as values. Φ is countably based if we for each F and n such that $Φ (F) = n$ find a countable set $A \subseteq N^{N}$ such that F is total on A and such that for all G of type 2, if G is total on A and agrees with F on A, then $Φ (G) = n$ .
In (3), a base element for Φ will be a countable set A together with the restriction of an F to A with the property described.

$^{3} E$ will not be countably based, since in order to know that $^{3} E (O^{2}) = 0$ we need to know that $O^{2} (f) = 0$ for all $f \in N^{N}$ .

One problem with the countably based functionals Φ is that the base elements of Φ are not well structured as individual sets, and a suitable class of base elements for Φ may not be well structured as a class. Much of the way of thinking inherited from the computability theory of the continuous functionals is useless. The aim of this section is to introduce a more restricted class, the hyper-sequential functionals, where we have added some further structure. Examples of hyper-sequential functionals will be the Superjump and $I$ . However, the first concept we introduce will be too general for our purpose, for instance, all functionals of type 3 computable using an infinite time Turing machine the way suggested by Welch [33] will be hyper-sequential.
4.2. Hyper-sequential functionals

4.2.1. The definitions

In this section we will define what we mean with a hyper-sequential procedure. A transfinite calculation using a functional F as an oracle can be viewed as a sequence of queries of the form “what is $F (f)$ ?”, where the next query will depend on the answers to the previous ones. We will capture such deterministic procedures with our concepts defined in 4.2. Our aim will be to isolate the procedures that will correspond to computations relative to $I$ , and in order to fully capture those, our calculations must also contain some documentation. In a computation ${e} (I, F, \vec{f}, \vec{a})$ , there may be subcomputations with extra arguments g or b of type 1 or 0. Our abstract calculations will contain what we call a LOG, and the use of this LOG will be to show that procedures corresponding to Kleene-computations in $I$ are definable at the level of $Π_{1}^{1}$ . This will be made precise later, and the actual function of the LOG will be easier to grasp when we simulate Kleene-computations as procedures. In order to formally define this LOG we take the liberty to add an extra element ∗ to $N$ , and to claim that sets of objects involving this ∗ will be of a certain complexity, for instance $Π_{1}^{1}$ , without going to the trouble of coding.

Definition 4.2.

A string is a sequence ${(f_{β}, a_{β})}_{β < α}$ where α is a countable ordinal, each $f_{β} \in N^{N}$ and each $a_{β} \in N \cup {}$ . We call $f_{β}$ a query, and sometimes writes it as $F (f_{β}) =$ ?.

A hyper-sequential procedure* is a set Ω of strings where each string will be given an integer value, and such that whenever ${(f_{β}, a_{β})}_{β < α}$ and ${(f_{β}^{'}, a_{β}^{'})}_{β < α^{'}}$ are in Ω they are either equal or there is a $β < min {α, α^{'}}$ such that $f_{β} = f_{β}^{'}$ , $a_{β} \neq a_{β}^{'}$ , $a_{β} \neq $ , $a_{β}^{'} \neq $ and $(f_{γ}, a_{γ}) = (f_{γ}^{'}, a_{γ}^{'})$ for all $γ < β$ . Formally, will let Ω be a set of pairs $(t, b)$ where t is a string and b is the associated value.

If ${(f_{β}, a_{β})}_{β < α}$ is a string and $F \in T p (2)$ , we say that the string matches F if $F (f_{β}) = a_{β}$ for all $β < α$ with $a_{β} \in N$ .

If a string t is in a hyper-sequential procedure Ω, has a value a and matches F, we call t a calculation, calculating $Ω (F) = a$ .

If Ω is a hyper-sequential procedure, then Ω defines (or computes) the partial functional $Φ (F) = Ω (F)$ of type 3. When $Φ (F)$ is defined, the calculation of $Ω (F)$ will be unique.

A total functional of type 3 is hyper-sequential if there is a hyper-sequential procedure that defines it.

If $t = {(f_{β}, a_{β})}_{β < α}$ is a calculation, and $a_{β} = $ we say that $f_{β}$ (or β) is in the LOG of t.

We will from now on use the words procedure* and sequential in the meaning of hyper-sequential procedure and hyper-sequential.
Remark 4.3.
A procedure can be viewed as a strategy for a transfinite game where Player I, the computing device, plays queries and Player II, the input, answers each query using F. In some matches of the games, corresponding to the calculations, Player I wins the match in the sense of providing an output, while in other matches, Player II wins because the match either stops after countably many steps without a value, or it goes on through $ℵ_{1}$ many steps. We will discuss this further when we consider procedures with more structure. If we then still use the picture of games with rules, the LOG will represent places where Player I will enter a sub-game following different rules, and the LOG will help the referee to verify that the whole match is played according to the general, nested, rules of the game.

Note that if t is a string that is an initial segment of several calculations, then the next $f_{β}$ will be the same for all such extensions, and if β is in the LOG of one of them, it will be in the LOG of all extensions.
Definition 4.4.
Let ${(f_{β}, a_{β})}_{β < α}$ be a string.

A sub-string is a sequence ${(f_{γ}, a_{γ})}_{γ < β}$ for some $β ⩽ α$ .

We can concatenate strings in the usual way: If we for each ordinal $γ < γ_{0}$ have a string ${(f_{γ, β}, a_{γ, β})}_{β < α_{γ}}$ we let the concatenation ${(f_{β}, a_{β})}_{β < α}$ be defined by

$α = \sum_{γ < γ_{0}} α_{γ}$

If $β = \sum_{γ < γ_{1}} α_{γ} + β_{1}$ where $γ_{1} < γ_{0}$ and $β_{1} < α_{γ_{1}}$ , then $(f_{β}, a_{β}) = (f_{γ_{1}, β_{1}}, a_{γ_{1}, β_{1}})$ .

We will prove that the class of sequential functionals of type 3 is closed under Kleene-computability as defined through the schemes S1–S9. To be more precise, we will prove that if $\vec{Φ} = (Φ_{1}, \dots, Φ_{n})$ consists of sequential functionals and $\begin{matrix} λ F . {e} (\vec{Φ}, F, \vec{f}, \vec{a}) \end{matrix}$ is total, then it is itself sequential. To make this precise, we need to extend S8 to deal with general inputs of type 3. For the sake of notational simplicity, we assume that the arguments of our computations will be of the form as above, that we drop the scheme S6 of permutation and that we use an alternative indexing for scheme S8 so that we can read out from the index for which of the arguments in the list $\vec{Φ}$ the oracle call is made. (Alternatively we could modify S6 to cater for permutations of the list of inputs of all four types.) We still leave out S5, primitive recursion, partly because it is redundant in the presence of S9, and partly because it can be handled in analogy to composition S4. Thus we add the following scheme to Definition 2.4, while replacing the one occurrence of $I$ with a sequence $\vec{Φ}$ of functionals of type 3:

If $e = ⟨ 8, 3, i, d ⟩$ then $\begin{matrix} {e} (\vec{Φ}, \vec{F}, \vec{f}, \vec{a}) = Φ_{i} (λ f . {d} (\vec{Φ}, \vec{F}, f, \vec{f}, \vec{a})) \end{matrix}$

In the original definition by Kleene, this is only supposed to make sense when ${d} (\vec{Φ}, \vec{F}, f, \vec{f}, \vec{a})$ terminates for all $f \in N^{N}$ , but when we are working with countably based $Φ_{i}$ we normally only require that there is a base element that is a sub-function of $λ f . {d} (\vec{Φ}, \vec{F}, \vec{f}, \vec{a})$ .

As we will see in the sequel, being sequential the way we define it here is quite general, and thus the fact that this class is closed under Kleene computability may be of restricted interest. However, we will later refer to the construction of procedures imbedded in the proof of Lemma 4.7 in situations where we will show that much more restricted classes of functionals still are Kleene closed.

Since we, in this section, are primarily interested in functionals of type 3 computable in a given sequence of sequential functionals of the same type, we restrict the number of arguments of type 2 to one. We can do this because the number of type 2 arguments will not increase as we move down the paths of the computation tree. The number of arguments of type 0 and of type 1 may increase, so we need to consider arbitrarily long finite lists of such input arguments. Definition 4.5.
Let $\vec{Φ} = (Φ_{1}, \dots, Φ_{n})$ be a sequence of sequential functionals defined from the procedures $Ω_{1}, \dots, Ω_{n}$ . Let F be of type 2 and let $\vec{f}$ , $\vec{a}$ be finite sequences of objects of type 1 and 0 resp. Assume that ${e} (\vec{Φ}, F, \vec{f}, \vec{a}) = b$ . By recursion on the length of this computation we define the calculation $t_{e, \vec{Φ}, F, \vec{f}, \vec{a}}$ with value b as follows, where we use $ˆ$ to denote concatenation of strings (recall that calculations are strings that, in the given context, have values):
If e is an index for an initial computation, i.e. for S1, S2, S3 or S7, we let $t_{e, \vec{Φ}, F, \vec{f}, \vec{a}}$ be the empty string, i.e. with $α = 0$ .

If $\begin{matrix} {e} (\vec{Φ}, F, \vec{f}, \vec{a}) = {e_{1}} (\vec{Φ}, F, \vec{f}, {e_{2}} (\vec{Φ}, F, \vec{f}, \vec{a}), \vec{a}), \end{matrix}$ let $c = {e_{2}} (\vec{Φ}, F, \vec{f}, \vec{a})$ . Let $\begin{matrix} t_{e, \vec{Φ}, F, \vec{f}, \vec{a}} = t_{e_{2}, \vec{Φ}, F, \vec{f}, \vec{a}} ˆ t_{e_{1}, \vec{Φ}, F, \vec{f}, c, \vec{a}} . \end{matrix}$

In the case of S9, we just use the calculation for the immediate subcomputation.

Let ${e} (\vec{Φ}, F, \vec{f}, \vec{a}) = F (λ c . {e_{1}} (\vec{Φ}, F, \vec{f}, c, \vec{a}))$ . Let $f (c) = {e_{1}} (\vec{Φ}, F, \vec{f}, c, \vec{a})$ . Then $\begin{matrix} t_{e, \vec{Φ}, F, \vec{f}, \vec{a}} = t_{e_{1}, \vec{Φ}, F, \vec{f}, 0, \vec{a}} ˆ t_{e_{1}, \vec{Φ}, F, \vec{f}, 1, \vec{a}} ˆ \underset{ω}{\underset{︸}{\dots \dots}} ˆ (f, F (f)) . \end{matrix}$

Let ${e} (\vec{Φ}, F, \vec{f}, \vec{a}) = Φ_{i} (λ g . {e_{1}} (\vec{Φ}, F, g, \vec{f}, \vec{a}))$ . Let $H (g) = {e_{1}} (\vec{Φ}, F, g, \vec{f}, \vec{a})$ and let ${(g_{β}, b_{β})}_{β < α}$ be the calculation in $Ω_{i}$ that is matching H.

We let $t_{e, \vec{Φ}, F, \vec{f}, \vec{a}}$ be the concatenation of $\begin{matrix} {(g_{β}, ) ˆ t_{e_{1}, \vec{Φ}, F, g_{β}, \vec{f}, \vec{a}}}_{β < α} . \end{matrix}$
This ends the definition.
Remark 4.6.
We inserted the pairs $(g_{β}, )$ in the LOG in order to remind us of the fact that we at that stage are simulating a subcomputation with an extra argument $g_{β}$ . We need the information about this extra argument in order to say that a string is ‘correct’, in a sense made precise later.
Lemma 4.7.
Let e, $\vec{Φ}$ , $\vec{f}$ and $\vec{a}$ be fixed as in Defintion 4.5 . Then the set $\begin{matrix} {(t_{e, \vec{Φ}, F, \vec{f}, \vec{a}}, b) : {e} (\vec{Φ}, F, \vec{f}, \vec{a}) = b} \end{matrix}$ will be a procedure.
Proof.
Assume that both ${e} (\vec{Φ}, F, \vec{f}, \vec{a})$ and ${e} (\vec{Φ}, G, \vec{f}, \vec{a})$ terminate. We prove by induction on the ordinal ranks of the computations that the corresponding calculations satisfy Definition 4.2(b). The proof is split into cases corresponding to the Kleene schemes.

If e is an index for an initial computation, the claim is trivial, and the induction step is trivial in the case of application of S9.

Let e be an index for composition, and let $e_{1}$ and $e_{2}$ be as in the construction. If the calculations for ${e_{2}} (\vec{Φ}, F, \vec{f}, \vec{a})$ and ${e_{2}} (\vec{Φ}, G, \vec{f}, \vec{a})$ are different, then by the induction hypothesis they split at a first point, and there the f-parts are the same while the a-parts differ. Since these calculations are initial segments of the calculations under consideration, the concatenated calculations also satisfy the definition.

If the calculations for the $e_{2}$ -computation are equal, then, by the indiction hypothesis, the values are the same, c, and then our conclusion follows from the induction hypothesis for ${e_{1}} (\vec{Φ}, F / G, \vec{f}, \vec{a})$ .

Application of $F / G$ : In this case, we construct calculations as the concatenation of $ω + 1$ items, first the corresponding calculations for each $c \in N$ , and at the end, pairs $(f, F (f))$ and $(f^{'}, G (f^{'}))$ respectively. If there is a least c where the corresponding two calculations differ, the f-parts will agree while the a-parts will differ at a minimal location in these calculations, by the induction hypothesis. Then the f-parts will agree and the a-parts will differ at the corresponding minimal location in the concatenated calculation. If the two concatenations of the calculations inherited for each c are equal, it follows from the induction hypothesis that the arguments f and $f^{'}$ for F and G resp. are equal, so at the top pair $(f, F (f))$ and $(f^{'}, G (f^{'}))$ we will have that the query parts are equal.

Application of $Φ_{i}$ : Let ${(g_{β}, b_{β})}_{β < α}$ and ${{(g_{β}^{'}, b_{β}^{'}}}_{β < α^{'}}$ be the two calculations in $Ω_{i}$ matching the corresponding functionals H and $H^{'}$ as in the definition in this case. First we see that if the two concatenated calculations agree as far as they both go, we can use the induction hypothesis, sub-induction on $β < min {α, α^{'}}$ and the fact that $Ω_{i}$ is a procedure to show that $g_{β} = g_{β}^{'}$ and that $H (g_{β}) = H^{'} (g_{β}^{'})$ for all β. Since $Ω_{i}$ is a procedure, it follows that $α = α^{'}$ , that the two concatenated calculations are equal and that the values are the same.

If the two concatenated calculations differ, there will be a least $β < min {α, α^{'}}$ such that they differ in the sections computing $H (g_{β})$ and $H^{'} (g_{β}^{'})$ . Then $g_{β} = g_{β}^{'}$ , so by the induction hypothesis there is a least location in those sections where they differ, and there the f parts are equal while the a-parts differ. So, the calculations constructed will satisfy the definition. □
Theorem 4.8.
The class of hyper-sequential functionals of type 3 is closed under relative Kleene-computability.
Proof.
Immediate from Lemma 4.7. □
Remark 4.9.
We can deduce, from the proof of Theorem 4.8, that all functionals of type 3 computable in functionals of lower types will be hyper-sequential.

4.2.2. Mixed types

Some of the objects we are interested in are of types at level $⩽ 3$ that are not pure, $I$ is one prominent example. There are two natural ways to extend the concept of sequential functionals to objects of such types. One is to identify such types as the fixed points of computable retracts on the corresponding pure types, the retracts being explicitly definable as Kleene-computable where the schemes S5 and S9 are not needed. Then an object will be, by definition, sequential if the representation in the pure type is so.

The other alternative is to extend the intuition of sequentiality to objects of these general types. A type like this will be of the form $\begin{matrix} σ_{1}, \dots, σ_{n} \to N, \end{matrix}$ where each $σ_{i}$ has level $⩽ 2$ . Thus a calculation will be a well-ordered set of queries with answers where each query is of the form $F_{i} (\vec{f}) =$ ? for some i, varying with the query. Each $\vec{f}$ will consist of functions and/or integers, and the functions may be of one or several number variables. To keep track of all this in its full generality will require some heavy notation, but there will be no genuine mathematical problems. Given this, we can define what we mean with a procedure adjusted to each type, and then the sequential objects of that type. It is obvious that the two approaches are equivalent, but not being pressed, we prefer to omit all details. In some of our examples, we will use the latter, intuitive approach.

4.2.3. Examples

Our first example is what motivated us to isolate the concept of hyper-sequential functionals:

Theorem 4.10.
The functional $I$ is hyper-sequential.
Proof.
Let $F : 2^{N} \to 2^{N}$ , $F^{'} (a ˆ f) = F (f) (a)$ and let $f_{0}^{F}$ be the constant 0. We find $f_{1}^{F} = F (f_{0}^{F})$ through the ω-series of queries $F^{'} (a ˆ f_{0}^{F}) =$ ?, then $f_{2}^{F} = F (f_{1}^{F}) \cup f_{1}^{F}$ (identifying a characteristic function with the corresponding set) through the ω-sequence of queries $F^{'} (a ˆ f_{1}^{F}) =$ ? and so on. This is clearly a hyper-sequential procedure. □

In his CiE-2019-paper [33], Philip Welch introduced infinite time Turing machines that can take functionals F of type 2 as oracles. The idea is to have a special oracle tape, and whenever the oracle F is called upon, we consider the oracle tape as the input information, and what the consequence of the oracle call will be will depend on the precise ITTM-model we are using. We have
Theorem 4.11.
Every ITTM-computable functional is sequential.

We leave this theorem without a proof, since the proof is easy, but requires familiarity with the ITTM-model.

Clearly, all sequential functionals are countably based. To what extent the converse is true is unknown, but we do have: Theorem 4.12.
If the continuum hypothesis CH holds, all countably based total functionals will have extensions to partial functionals that are sequential.
Proof.
We work within ZFC + CH. Let ${f_{α}}_{α < ℵ_{1}}$ be an enumeration of $N^{N}$ . Let Φ be countably based and let X be set of base elements for Φ. The elements of X will be triples $(A, ϕ, a)$ where $A \subseteq N^{N}$ is countable, $ϕ : A \to N$ and $a \in N$ . The significance is that whenever F extends ϕ to all of $N^{N}$ , then $Φ (F) = a$ , and that for each F there will be at least one $(A, ϕ, a) \in X$ where F is an extension of ϕ.

The sequential procedure will then be to compute $F (f_{α})$ up to the first $α_{0}$ where there is some $(A, ϕ, a) \in X$ such that
$A \subseteq {f_{α} : α < α_{0}}$ .

For $f_{α} \in A$ we have that $F (f_{α}) = ϕ (f_{α})$ .
We will have that $Φ (F) = a$ independent of which $(A, ϕ, a)$ we chose with this property. □

4.3. Denotation procedures

There is no reason to believe that the continuum hypothesis can be avoided in Theorem 4.12, but the theorem still suggests that the concept of hyper-sequential functional is too general to be of interest, and the intention is to investigate possible refinements of the concept. Now we will consider procedures that will include some extra information, a number or denotation $d_{β}$ for each β in the index ordinal of a calculation. In its full generality, this does not restrict the class of functionals definable from procedures, but it gives us a tool for discussing the complexity of them. Thus, in the theorems of this section, the constructions of the procedures with denotations used to prove them will be as important as the theorems themselves.

Definition 4.13.
A denotation procedure Ω, d-procedure for short, will be a set Ω of calculations with denotations $\begin{matrix} ({(f_{β}, a_{β}, d_{β})}_{β < α}, c) \end{matrix}$ where each $a_{β} \in N \cup {}$ and
The denotations* $d_{β}$ are in $N$ .

The corresponding set of calculations without the denotations is a procedure.

For each $({(f_{β}, a_{β}, d_{β})}_{β < α}, c) \in Ω$ , if $β < γ < α$ , then $d_{β} \neq d_{γ}$ .

By abuse of terminology, we will use Ω both for a d-procedure and for the corresponding procedure, making it clear in each case if we consider the denotations or not. Clearly, all d-procedures will define sequential, partial functionals as well. In fact we have
Observation 1.
By the axiom of choice, all procedures Ω can be extended to d-procedures.

We simply use the axiom of choice to select one enumeration of α for each calculation $({(f_{β}, a_{β})}_{β < α}, c) \in Ω$ and use this to define the additional $d_{β} s$ for each calculation. There is of course no extra knowledge to be harvested from this argument, but it illustrates an aspect that we have to bring under control in the d-procedures that we construct:
Definition 4.14.
Let Ω be a d-procedure, let ${(f_{β}, a_{β}, d_{β})}_{β < α}$ be a calculation in Ω and let $β < α$ . The delay of the denotation of the calculation at point β is the least ordinal γ such that for all other calculations ${(f_{δ}^{'}, a_{δ}^{'}, d_{δ}^{'})}_{δ < α^{'}}$ in Ω, if $(f_{δ}, a_{δ}) = (f_{δ}^{'}, a_{δ}^{'})$ for all $δ < β + γ$ , then $d_{δ} = d_{δ}^{'}$ for all $δ ⩽ β$ .

The delay tells us for how much longer we must run a calculation before we can tell what the denotation will be.

A key property of a d-procedure is that we can use the denotations to code the procedure in a manageable way as a subset of the continuum. Definition 4.15.

Let Ω be a d-procedure. The representation of Ω will be the set of quadruples $(D, ≺, {(f_{d}, a_{d})}_{d \in D}, c)$ derived from calculations $({(f_{β}, a_{β}, d_{β})}_{β < α}, c)$ in Ω as follows:
D is the set of $d_{β}$ for $β < α$ and ≺ is the corresponding ordering on D.

When $d = d_{β}$ , then $f_{d}$ is the $f_{β}$ and $a_{d}$ is the $a_{β}$ of the calculation.

c is the value of the calculation.
We code these items as elements of $N^{N}$ in some standard way.

We say that a d-procedure Ω is $Π_{1}^{1}$ if the representation of Ω is a $Π_{1}^{1}$ -set.

If $(D, ≺, {(f_{d}, a_{d})}_{d \in D}, c)$ is a calculation in a d-procedure and $(D^{'}, ≺^{'}, {(g_{d}, b_{d})}_{d \in D^{'}})$ satisfies that $≺^{'}$ is a well ordering of $D^{'}$ , each $g_{d}$ is of type 1 and each $b_{d}$ is of type 0, we say that $(D^{'}, ≺^{'}, {{(g_{d}, b_{d},}}_{d \in D^{'}})$ is isomorphic to an initial segment of $(D, ≺, {(f_{d}, a_{d})}_{d \in D})$ if there is an order isomorphism ρ from $D^{'}$ to an initial segment of D such that $f_{ρ (d)} = g_{d}$ and $a_{ρ (d)} = b_{d}$ for all $d \in D^{'}$ .

Lemma 4.16.
The functional $I$ is definable from a d-procedure that is $Π_{1}^{1}$ .
Proof.
For each b, we will construct a procedure for the 0–1-valued function $\begin{matrix} λ G . I (F_{G}) (b), \end{matrix}$ where $F_{G} (f) (a) = min {1, G (a ˆ f)}$ is as in Remark 2.3. The only difference between these procedures will be in the value part, the c in each string.

Let G be given. We will describe the calculation with denotation that will match G and conclude with the value $I (F_{G}) (b)$ . Let ${f_{β}}_{β ⩽ α}$ be the sequence constructed while defining $I (F_{G})$ .

For each $β ⩽ α$ , let $g_{a, β} = a ˆ f_{β}$ . We see that in order to “compute” $I (F_{G}) (b)$ we have to evaluate G on all functions $g_{a, β}$ for all $β ⩽ α$ , a sequence of queries of order type $ω (α + 1)$ . So, we define the calculation matching G as $\begin{matrix} ({(h_{γ}, b_{γ}, d_{γ})}_{γ < ω (α + 1)}, c) \end{matrix}$ where
$h_{ω \cdot β + a} = g_{a, β}$ for $β ⩽ α$ and $a < ω$ .

$b_{ω \cdot β + a} = G (g_{a, β})$ for β and a as above.

$d_{ω \cdot α + a} = ⟨ 0, a ⟩$ for $a \in ω$ .

$d_{ω \cdot β + a} = ⟨ x + 1, a ⟩$ , where x is minimal such that $f_{β + 1} (x) = 1$ while $f_{β} (x) = 0$ , if $β < α$ and $a \in ω$ .

$c = f_{α} (b)$ .
It remains to prove that the representation is $Π_{1}^{1}$ . We do this through the following steps:
Since the set of pairs $(D, ≺)$ where $D \subseteq N$ and ≺ is a well ordering of D is $Π_{1}^{1}$ , the set $Ω_{1}$ of quadruples $(D, ≺, {(h_{d}, b_{d})}_{d \in D}, c)$ where $(D, ≺)$ is a well ordering as above is $Π_{1}^{1}$ . We call the elements in $Ω_{1}$ strings.

If $Ω_{2}$ is the set of strings in $Ω_{1}$ where the order type of $(D, ≺)$ equals $ω \cdot (α + 1)$ for some α, we still have a $Π_{1}^{1}$ -set.

Let $Ω_{3}$ be the strings in $Ω_{2}$ that corresponds to a possible evaluation of $I$ on some G. This requires that the calculation is locally correct, i.e. that each $(h_{d}, a_{d})$ is in relation to its $(D, ≺)$ -predecessors as prescribed by the recursion step. This can be decided arithmetically, so $Ω_{3}$ is also $Π_{1}^{1}$ .

For a string in $Ω_{3}$ , we can arithmetically decide if the enumeration $(D, ≺)$ is as in the construction above, so the representation $Ω_{4}$ of the calculations with denotations in the procedure for $I$ will also be $Π_{1}^{1}$ .
□
Remark 4.17.
We introduce delays in this construction. Whenever we simulate one step in the induction, we must wait until we know if we are at the final step or not before we can decide what the denotation will be, and this involves a delay of length ω.
Definition 4.18.
Let Φ be a total functional of type 3. We say that Φ is $Π_{1}^{1}$ -definable if Φ is definable from a $Π_{1}^{1}$ d-procedure.
Lemma 4.19.
The class of $Π_{1}^{1}$ -definable total functionals of type 3 is closed under relative Kleene computability.
Proof.
We build on the proof of Theorem 4.8 and the construction in Definition 4.5. We just have to show how to add the denotations $d_{β}$ to each item in the calculation, and then show that the complexity of the representation is preserved. We define the d-procedure as follows:

In the cases of initial computations there are no ordinals to be denoted, and in the case of S9 we can keep the denotations as they are.

In the case of composition, we can use $d \mapsto ⟨ 0, d ⟩$ to denote the items in the first part and the map $d \mapsto ⟨ 1, d ⟩$ to denote the items in the second part.

When we compute g and then apply F to g, we use the map $d \mapsto ⟨ c + 1, d ⟩$ to denote the items coming from the calculation computing $g (c)$ and end the full subcalculation with $(g, F (g), ⟨ 0, 0 ⟩)$ .

In the case where we apply the procedure $Ω_{i}$ for $Φ_{i}$ to a partial functional H of type 2 for which we have an index, our calculation will be the concatenation of the calculations related to the computations of $H (g_{β}) = a_{β}$ , where we also inserted $(g_{β}, )$ in front of each such local calculation. If the $Ω_{i}$ -denotation for the pair $(g_{β}, a_{β})$ in the calculation evaluating $Φ_{i} (H)$ is $d_{1}$ , we use $⟨ d_{1}, 0 ⟩$ to denote $(g_{β}, )$ in the calculation we construct, and if an item in the calculation defined from the computation of $H (g_{β}) = a_{β}$ is $d_{2}$ , we let $⟨ d_{1}, d_{2} + 1 ⟩$ be the denotation of the corresponding item in the concatenated calculation.

It is clear that if two calculations, as in Definition 4.5 are equal, the denotations will be the same as well. This defines a d-procedure.

It remains to show that the representation of this d-procedure will be $Π_{1}^{1}$ when the representations of the d-procedures for $Φ_{1}, \dots, Φ_{n}$ are $Π_{1}^{1}$ . This will be the hard, technical part of our proof, and we first give a brief explanation of what we aim to do:

We let the $Π_{1}^{1}$ -representations for $\vec{Φ}$ be given. Using the recursion theorem for computing relative to $^{2} E$ , we will design an algorithm that, given e, $\vec{f}$ , $\vec{a}$ and a representation $\begin{matrix} (D, ≺, {(f_{d}, a_{d})}_{d \in D}) \end{matrix}$ of a string with denotations (a d-string for short) will semi-check, in the sense of providing an algorithm relative to $^{2} E$ that terminates when the property holds, if there is some F such that this string matches F and that the d-string gives us the representation of the calculation we constructed for the computation ${e} (\vec{Φ}, F, \vec{f}, \vec{a})$ . In addition, if our algorithm finds the representation $(D, ≺, {(f_{d}, a_{d})}_{d \in D})$ adequate as the representation of a d-calculation, it will produce the value of the computation ${e} (\vec{Φ}, F, \vec{f}, \vec{a})$ , which then will be the same for any F matching the given d-string (which by now is confirmed as a d-calculation). Since termination of $^{2} E$ -algorithms is of complexity $Π_{1}^{1}$ , this will prove the lemma. Without stressing this point everywhere needed, we assume that the given d-string matches itself, in the sense that if both $(f, a)$ and $(f, a^{'})$ occur, maybe at different places, then $a = a^{'}$ .

As usual, our $^{2} E$ -procedure will be defined by cases following S1–S9, where we only focus on the nontrivial cases.

If e is an index for an initial computation, we check if the given string is empty. If so, it is fine as a calculation, and we can read off the value from the index, the given $\vec{f}$ and $\vec{a}$ .

Composition: $\begin{matrix} {e} (\vec{Φ}, F, \vec{f}, \vec{a}) = {e_{1}} (\vec{Φ}, F, \vec{f}, {e_{2}} (\vec{Φ}, F, \vec{f}, \vec{a}), \vec{a}) . \end{matrix}$ First we check if $(D, ≺)$ is of the form $(D_{2}, ≺_{2}) + (D_{1}, ≺_{1})$ where each $d \in D_{2}$ is of the form $⟨ 0, d^{'} ⟩$ and each $d \in D_{1}$ is of the form $⟨ 1, d^{'} ⟩$ .

Let $D_{2}^{'} = {d^{'} : ⟨ 0, d^{'} ⟩ \in D_{2}}$ and consider the corresponding string inherited from the given one. If this is ok for the computation ${e_{2}} (\vec{Φ}, F, \vec{f}, \vec{a})$ , we compute the value $c^{'}$ , and now ask if the $(D_{1}, ≺_{1})$ is ok for ${e_{1}} (\vec{Φ}, F, \vec{f}, c^{'}, \vec{a})$ in the same sense.

Application of F: $\begin{matrix} {e} (\vec{Φ}, F, \vec{f}, \vec{a}) = F (λ c . {e_{1}} (\vec{Φ}, F, \vec{f}, c, \vec{a})) . \end{matrix}$ First we check if the given string has a last element $(g, a, ⟨ 0, 0 ⟩)$ and if what comes before can be seen as an ω-sum of intervals $I_{c}$ where the denotations are of the form $⟨ c + 1, d ⟩$ .

If this is the case, the given string generates, in analogy with the case for composition, strings $t_{c}$ , and we check for each of them if they are ok for the computation ${e_{1}} (\vec{Φ}, F, \vec{f}, c, \vec{a})$ , and with value $g (c)$ .

If they are all ok we accept the given string as a calculation, and see that the value of $F (λ c . {e_{1}} (\vec{Φ}, F, \vec{f}, c, \vec{a}))$ must be a.

Application of $Φ_{i}$ : $\begin{matrix} {e} (\vec{Φ}, F, \vec{f}, \vec{a}) = Φ_{i} (λ g . {e_{1}} (\vec{Φ}, F, g, \vec{f}, \vec{a})) . \end{matrix}$ This is where we need the extra information stored in the LOG. We proceed as follows:

In the given string, first check if $(D, ≺)$ is the union of intervals where the first element of the interval is of the form $⟨ d_{1}, 0 ⟩$ and the rest are of the form $⟨ d_{1}, d_{2} + 1 ⟩$ .

Then check for each of these intervals, where $g = f_{⟨ d_{1}, 0 ⟩}$ , if the rest of this interval, after replacing $⟨ d_{1}, d_{2} + 1 ⟩$ with $d_{2}$ , is ok for ${e_{1}} (\vec{Φ}, F, g, \vec{f}, \vec{a})$ , and if so, compute the value a.

Finally, we collect these pairs $(g, a)$ with denotation $d_{1}$ into a string, and check if this is a calculation in $Ω_{i}$ with some value c. For this, we use Gandy selection, and we then find the correct value as well.

In order to complete the argument we must prove that if this process works, then the computation in question, relative to any F matching the given string, will terminate with the chosen value, and prove that if the computation terminates for a total F, then our process terminates on the corresponding representation of the d-calculation, and again, that it gives the right value. Both arguments are by induction on the length of computations, the first for $^{2} E$ -computations and the latter for the computation of ${e} (\vec{Φ}, F, \vec{f}, \vec{a})$ . The details are trivial. □

5. Inductive procedures

As a consequence of Lemmas 4.16 and 4.19 we see that all total functionals of type 3 computable in $I$ will be definable from a d-procedure that is $Π_{1}^{1}$ , but the converse is not true, see Theorem 6.1.

The aim of this section is to narrow down a subclass of the d-procedures further in order to approach a characterisation of the class we are primarily interested in, the functionals computable in $I$ .

5.1. Computability in $^{2} E$

Matters are trivial if the d-procedure is hyperarithmetical:

Theorem 5.1.
Let Φ be of type 3. Then Φ is computable in $^{2} E$ if and only if Φ is definable from a d-procedure with a $Δ_{1}^{1}$ -representation.
Proof.
First let Φ be definable from the d-procedure Ω, and assume that the representation is $Δ_{1}^{1}$ . By the boundedness theorem for $Σ_{1}^{1}$ -sets of codes for ordinals, see e.g. [30, Exercise II 5.9], there will be a computable ordinal λ such that all calculations in Ω have order-types bounded by λ. Let $(X, ⊲)$ be a computable well-ordering of length λ, and for each $x \in X$ , let $X_{x} = {y \in X : y ⊲ x}$ . For each F, and by recursion on the ⊲-rank of $x \in X$ , we will use F and $^{2} E$ to compute a string indexed by $X_{x}$ that matches F and is, modulo the choice of denotations, isomorphic to the calculation in Ω matching F, until Ω tells us what the value $Φ (F)$ must be. We use the recursion theorem, and explain the step from x to its ⊲-successor $x^{'}$ . So, as an induction hypothesis, we assume that we have constructed the string $t = {(f_{y}, a_{y}, y)}_{y ⊲ x}$ . This string is isomorphic to an initial segment of $((D, ≺, {(f_{d}^{'}, a_{d}^{'})}_{d \in D}, c)$ if there is a $d \in D$ with the same rank as x, and the corresponding isomorphism r from $X_{x}$ to $D_{d}$ will satisfy that $f_{y} = f_{r (y)}^{'}$ and $a_{y} = a_{r (y)}^{'}$ for all $y \in D_{x}$ . Now, the set $Ω_{t}$ of calculations in Ω such that the string t is isomorphic to an initial segment will be $Δ_{1}^{1}$ relative to t.

In order to know what to do next, we first have to split between the two cases: are we able to give out a value for $Φ (F)$ or must we continue the evaluation, that is, identifying, up to isomorphism, a larger part of the calculation matching F? Since Ω has a calculation for $Φ (F)$ , we know that there is at least one calculation in Ω of which t is isomorphic to an initial segment. Moreover, if t is actually isomorphic to a calculation in Ω, this is unique, and Ω provides us with the value. So, in order to decide between the two cases, we ask a “ $Δ_{1}^{1} (t)$ ”-question, i.e. a $Σ_{1}^{1} (t)$ -question and a $Π_{1}^{1} (t)$ -question that are equivalent. Those are: $\begin{array}{r} ‘is t isomorphic to a proper initial segment of some element of Ω_{t} ?’ \end{array}$ and $\begin{array}{r} ‘is t isomorphic to proper initial segments of all elements in Ω_{t} ?’. \end{array}$ In the case the answer is ‘no’, we have constructed a copy of the calculation matching F. Then we can compute the unique value $Φ (F) = c$ from the data. On the other hand, if the answer is ‘yes’, there will be a next query $f_{x}$ that will be unique for all calculations in $Ω_{t}$ . ${f_{x}}$ is a $Δ_{1}^{1}$ -singleton relative to t, and we can compute each $f_{x} (n)$ from t and $^{2} E$ . In both cases, we can rely on Gandy selection. This proves the theorem one way.

Now assume that $Φ (F) = {e} (^{2} E, F)$ . We can construct a d-procedure Ω for Φ in analogy with the one we constructed in the proof of Lemma 4.19, without relativizing the construction to a set of $\vec{Φ}$ with $Π_{1}^{1}$ -procedures. That the result now will be $Δ_{1}^{1}$ can be seen from the following consideration:
Whenever ${e} (^{2} E, F) ↓$ we can compute the corresponding calculation $\begin{matrix} (D, ≺, {(f_{d}, a_{d})}_{d \in D}, c) \end{matrix}$ uniformly in e, F and $\exists^{2}$ , by use of the recursion theorem. It is worth noticing that there will be no delay here, given ${f_{d}, a_{d^{'}}}_{d^{'} ≺ d}$ , we do not only have a unique value for the next f, but also for its denotation d, even if the calculations are matching different $F s$ .

Next we observe that when checking if a representation $(D, ≺, {f_{d}, a_{d}}_{d \in D})$ of a d-string is a real representation of a real calculation of a value, we can relax the requirement that $(D, ≺)$ is a well ordering. The checking the way we did it in the proof of Lemma 4.19 is partially computable by the recursion theorem, and can be proved to terminate for a given e under the assumption that there is at least one total F matching the given d-string such that ${e} (^{2} E, F) ↓$ .
This shows that the d-procedure will be $Δ_{1}^{1}$ in this case. □
Remark 5.2.
We have essentially used that the element of a $Δ_{1}^{1}$ -singleton is itself hyperarithmetical, and this implicitly provides us with a next-function in this case.

There is no delay in the $Δ_{1}^{1}$ -d-procedure constructed in the above argument, the denotations in an initial segment of a calculation is uniquely determined by the segment itself.

5.2. The class $W (I)$

In this section we will give a closer analysis of the class of functionals of type 3 that are computable in $I$ . We will do so by investigating additional properties of the elements in the following class:

Definition 5.3.
Let $W (I)$ be the set of d-procedures for functionals Φ computable in $I$ as constructed in the proofs of Lemma 4.16 and Lemma 4.19.

5.2.1. Tame d-procedures

In this sub-section we will introduce two properties shared by all d-procedures in $W (I)$ .

Definition 5.4.
Let Ω be a procedure defining a total functional.
Let $Ω_{pre}$ be the set of $(D, ≺, {(f_{d}, a_{d})}_{d \in D})$ that are isomorphic to an initial segment of a calculation in Ω.

Let ${NEXT}_{Ω}$ be the function mapping $t \in Ω_{pre}$ to the disjoint union of $N^{N} \times {0, 1}$ and $N$ such that

If t is isomorphic to a calculation $t^{'}$ in Ω, then ${NEXT}_{Ω} (t)$ is the value of this calculation

If t is isomorphic to a proper initial segment $t^{'}$ of a calculation $t^{″}$ in Ω, then ${NEXT}_{Ω} (t) = (f, c)$ where $F (f) =$ ? is the next query after $t^{'}$ in $t^{″}$ (independent of the choice of $t^{″}$ ) and $c \in {0, 1}$ . Moreover, if $c = 0$ , then the next pair in $t^{″}$ after $t^{'}$ will be of the form $(f, )$ while if $c = 1$ , we continue $t^{'}$ with a pair $(f, a)$ in $t^{″}$ for some $a \in N$ .

Definition 5.5.
Let Ω be a d-procedure for a total functional. We say that Ω is tame* if Ω is $Π_{1}^{1}$ , $Ω_{pre}$ is $Π_{1}^{1}$ and ${NEXT}_{Ω}$ is partially computable in $^{2} E$ .
Lemma 5.6.
Let Ω be the d-procedure for $I$ . Then Ω is tame.
Proof.
We need the full complexity of $Π_{1}^{1}$ to formulate that we are dealing with well orderings $(D, ≺)$ , the rest is actually arithmetical. Each step in the underlying recursion takes ω many steps when we evaluate according to Ω. It is clearly arithmetical to decide if any ordered set of pairs $(f, a)$ indexed over $N$ locally satisfies the recursion in $I$ , so checking if a d-string is in $Ω_{pre}$ is arithmetical when we know that the representation is well ordered. If a string is locally correct, the next query is arithmetically defined if there is one, and the value is arithmetically expressible from the list of queries answers if the d-string corresponds to a calculation, so ${NEXT}_{Ω}$ is computable in $^{2} E$ as requested. □
Lemma 5.7.
The class of functionals definable from tame d-procedures Ω is closed under Kleene computability.
Proof.
Let $\vec{Φ} = Φ_{1}, \dots, Φ_{n}$ be defined from the tame d-procedures $Ω_{1}, \dots, Ω_{n}$ . We already know that the d-procedure for any Φ computable in $\vec{Φ}$ is $Π_{1}^{1}$ .

We use the recursion theorem to define, for each index e and extra inputs $\vec{f}$ and $\vec{a}$ , a set $X_{e, \vec{f}, \vec{a}}$ of d-strings $\begin{matrix} ((D, ≺, {(f_{d}, a_{d})}_{d \in D}) \end{matrix}$ that is $Π_{1}^{1}$ uniformly in $e, \vec{f}, \vec{a}$ , together with the function $\begin{array}{r} {NEXT}_{e, \vec{f}, \vec{a}} \end{array}$ defined on $X_{e, \vec{f}, \vec{a}}$ , and show that
If F is of type 2 and ${e} (Φ_{1}, \dots, Φ_{n}, F, \vec{f}, \vec{a}) = c$ and $(D, ≺, {(f_{d}, a_{d})}_{d \in D}, c)$ is the associated d-calculation obtained from the proof of Lemma 4.19, then any string isomorphic to an initial segment of $(D, ≺, {(f_{d}, a_{d})}_{d \in D})$ is in $X_{e, \vec{f}, \vec{a}}$ .

If a string is in $X_{e, \vec{f}, \vec{a}}$ and matches some F for which ${e} (Φ_{1}, \dots, Φ_{n}, F, \vec{f}, \vec{a})$ terminates, then the string is isomorphic to an initial segment of the d-calculation obtained through the proof of Lemma 4.19.

${NEXT}_{e, \vec{f}, \vec{a}}$ is computable in $^{2} E$ uniformly in the parameters and acts as specified.

We define $X_{e, \vec{f}, \vec{a}}$ and ${NEXT}_{e, \vec{f}, \vec{a}}$ by cases according to the scheme e represents. Note that since we are dealing with semi-decidable sets, we cannot take NO for an answer, and search-procedures have to use Gandy selection:

- e is an index for an initial computation given by S1-S3, S7: $X_{e, \vec{f}, \vec{a}}$ will consist of the empty string only. ${NEXT}_{e, \vec{f}, \vec{a}}$ is trivially given in all these cases.

- Composition: $\begin{matrix} {e} (\vec{Φ}, F, \vec{f}, \vec{a}) = {e_{1}} (\vec{Φ}, F, \vec{f}, {e_{2}} (\vec{Φ}, F, \vec{f}, \vec{a}), \vec{a}) . \end{matrix}$ Given $(D, ≺, {(f_{d}, a_{d})}_{d \in D})$ , where $(D, ≺)$ is a well ordering, we use $(D, ≺)$ –recursion to test if the initial segments of $(D, ≺, {(f_{d}, a_{d})}_{d \in D})$ are in $X_{e_{2}, \vec{f}, \vec{a}}$ until we either find an initial segment that is in $X_{e_{2}, \vec{f}, \vec{a}}$ and with a value c or we find that the given string is in $X_{e_{2}, \vec{f}, \vec{a}}$ , and thus in $X_{e, \vec{f}, \vec{a}}$ . If this search fails, the given string is not in $X_{e, \vec{f}, \vec{a}}$ , and non-termination is not a problem. If this search ends with a proper substring that is in $X_{e_{2}, \vec{f}, \vec{a}}$ and with a value c, we compare the rest of the string with $X_{e_{1}, \vec{f}, c, \vec{a}}$ in the same way. The next-function for e will be inherited from the next-functions of $e_{2}$ and $e_{1}, c$ , and these can be used to check that the given string does not go too far, beyond where we should have a valued string.

– We leave the cases for permutation and S9 for the reader, as those cases are even simpler.

– Application of F: $\begin{matrix} {e} (\vec{Φ}, F, \vec{f}, \vec{a}) = F (λ a . {e_{1}} (\vec{Φ}, F, \vec{f}, a, \vec{a})) . \end{matrix}$ This will be in analogy with how we dealt with composition, and technically we use transfinite recursion over $(D, ≺)$ . We first compare the given string poin-by-point with elements in $X_{e_{1}, \vec{f}, 0, \vec{a}}$ . If the given string is in $X_{e_{1}, \vec{f}, 0, \vec{a}}$ , then it is acceptable. If an initial segment of the given string is a maximal element of $X_{e_{1}, \vec{f}, 0, \vec{a}}$ , then we compare the remaining part with $X_{e_{1}, \vec{f}, 1, \vec{a}}$ and so forth. If any of those local comparisons fails, then our global comparison fails. If the comparison is successful, and we find some n and an end segment of our given string in $X_{e_{1}, \vec{f}, n, \vec{a}}$ , we accept the string. The last possibility is that the given string has an initial segment that is a concatenation of maximal strings from each $X_{e_{1}, \vec{f}, n, \vec{a}}$ in increasing order. If this is the full given string, it is also acceptable. If not, we must check that it contains a final $(g, b)$ at the end, and in this case, we must also check for each a if $g (a)$ is the value of the string from $X_{e_{1}, \vec{f}, a, \vec{a}}$ used in the concatenation before accepting the given string. When accepted, we inherit the next-function in the obvious way.

– Application of $Φ_{i}$ : $\begin{matrix} {e} (\vec{Φ}, F, \vec{f}, \vec{a}) = Φ_{i} (λ g . {e_{1}} (\vec{Φ}, F, g, \vec{f}, \vec{a})) . \end{matrix}$ Here it may be useful to look back on Definition 4.5. We explain informally how we, point by point, compare the initial segments of the given string $(D, ≺, {(f_{d}, a_{d})}_{d \in D})$ with the requirements for $Ω_{i}$ and the various sets $\begin{matrix} X_{e_{1}, g, \vec{f}, \vec{a}} \end{matrix}$ where we may assume that we have defined these sets as a part of the induction hypothesis:
If $d_{0}$ is the $(D, ≺)$ -least element, $f_{d_{0}}$ has to be the first query $g_{0}$ in $Ω_{i}$ , given to us by ${NEXT}_{Ω_{i}}$ , with $a_{d_{0}} = *$ .

We check the next segment of $(D, ≺, {(f_{d}, a_{d})}_{d \in D})$ for membership in $X_{e_{1}, g, \vec{f}, \vec{a}}$ until we have reached a value or until we have reached the end of the given string.

In the latter case, the string is in $X_{e, \vec{f}, \vec{a}}$ and in the first case, we let $b_{0}$ be the value, check that the pair $(g_{0}, b_{0})$ is in ${Ω_{i}}_{pre}$ and use the next-function of $Ω_{i}$ to verify that the next query in $Ω_{i}$ will be the next query in $(D, ≺, {(f_{d}, a_{d})}_{d \in D})$ .

By transfinite recursion on $(D, ≺)$ we can continue this comparison until we have reached the end of the given string or until it does not compare with strings in $Ω_{i}$ (whenever we have found a new value there, and can use its next-function to find the new $g_{β}$ ), or with the strings in the sets $X_{e_{1}, g_{β}, \vec{f}, \vec{a}}$ .
It is now routine to verify the properties (i)–(iii). □

5.2.2. Blocking

It is not the case that all functionals definable by a tame d-procedures will be computable in $I$ , see Theorem 6.1. The point with the denotations is that they may make it easier to design non-monotone inductions that are copying evaluations in a procedure, but the obstacle will be that we will not, in general, be able to tell from a part of a calculation what the correct denotation of the next query will be, there may be a delay as defined in 4.14. We find this phenomenon in the procedure for $I$ , where we first must establish, within each in a series of ω-length sub-calculations, if we reached the final fixed point or not before reading off the correct denotation. That the situation would be simpler without this obstacle, is seen from the following lemma:

Lemma 5.8.
Let Ω be a d-procedure for a total functional such that for any sub-string ${(f_{β}, a_{β}, d_{β})}_{β < α}$ of a calculation in Ω, the denotations $d_{β}$ are uniquely given by ${(f_{β}, a_{β})}_{β < α}$ .

If Ω in addition is tame, and the unique choice of $d_{β}$ is computable from ${{(f_{γ}, a_{γ}}}_{γ ⩽ β}$ and $^{2} E$ uniformly at each stage, then the functional defined by Ω is computable in $I$ .
Proof.
We code an entry $(f_{β}, a_{β}, d_{β})$ as the set $\begin{matrix} {⟨ {\bar{f}}_{β} (n), a_{β}, d_{β} ⟩ : n \in N} . \end{matrix}$ These sets will be disjoint, so we may code each initial segment of a string as a pair of sets, where one is the union $X_{β}$ of such single codes and the other is the corresponding ordering of the denotations. We will use that the Suslin functional S is computable in $I$ .

Given F, we design a non-monotone inductive definition $Γ_{F}$ computable in S that simulates the evaluation of the calculation matching F:
Given X, we use S to check if X codes an initial segment of a calculation in Ω as coded above. If not, let $Γ_{F} (X) = X$ , and if it does, continue.

Use ${NEXT}_{Ω}$ to find the next query $f_{α}$ , use F to find $a_{α} = F (f_{α})$ and finally the $^{2} E$ algorithm that gives us the unique denotation $d_{α}$ .

Let $Γ_{F} (X)$ be X extended with the code for $(f_{α}, a_{α}, d_{α})$ in the set to the left and all pairs $⟨ d_{β}, d_{α} ⟩$ for $β < α$ in the set to the right.
It is clear that the set $I (Γ_{F})$ will code the calculation in Ω matching F, together with the ordering of all the denotations used in that calculation, and we can use ${NEXT}_{Ω}$ to compute $Ω (F)$ .

Further details are left for the reader. □

We will now add further structure to d-procedures, blocks. It will be like inserting commands of the form ∖begin{block} and ∖end{block} bracketing blocks and sub-blocks. These imaginary commands must satisfy, for each calculation, the standard rules of bracketing, allowing for infinite branchings in the length, but only finite nesting in depth. Where to put these commands will be determined by the initial segment of the string up to where the command is, and the use will be to mark that there is now an uncertainty to what the denotations will be at the end, and that we have to carry out a sub-procedure, or evaluate the calculation for F a bit further, in order to find the true denotations of the calculation. We will consider two examples before giving the abstract definition of a tame d-procedure with blockings:
Example 2.
Let Ω be the d-procedure for $I$ . Recall that, given G, $Ω (G)$ will iterate the induction given by $F_{G}$ , generating the sequence ${f_{β}}_{β ⩽ α}$ by evaluating G on $0 ˆ f_{0}, 1 ˆ f_{0}, \dots_{ω} 0 ˆ f_{1}, 1 ˆ f_{1} \dots_{ω (α + 1)}$ .

Each ω-sequence will be a block in this case, and after each block we know what the denotation for the query $G (n ˆ f_{β}) =$ ? will be, but not while we are inside a block. However, in order to view the calculation within a block as a sub-procedure, we only need denotations that are unique for queries within this block, and ignore the larger picture. It is not hard to modify the proof of Lemma 5.8 to see that we can simulate the procedure for $I$ using $I$ .
Example 3.
In the case of composition we constructed the calculations as concatenations of strings for the two parts, and when defining the new denotations, we paired the denotations from the first part with 0 and from the second part with 1. We may consider the first part as one block and the other part as another one, but if we know from the larger picture that we are entering a composition, there is no need for this. There is no delay in deciding what the denotations are inherited in the construction of denotations for compositions, as there is for the construction of denotations for transfinite recursions with an unknown end.

We will need the blocking structure on calculations to characterise functionals of type 3 computable in $I$ in terms of procedures.

The blocks will be organised in a nested way, with some blocks being sub-blocks of others. The point is that, within each block, we will define denotations along the way, and when the need of a delay is observed, we enter a sub-block where we form temporary denotations that at the end of the block will be rewritten to the true ones. The nesting of the blocks will reflect that there may be delays within a period of delay, so the rewriting of denotations may go through several levels.

We will now give the full definition: Definition 5.9.
Let Ω be a tame d-procedure.
A block in Ω is an interval $t_{2}$ in a calculation $t_{1} ˆ t_{2} ˆ t_{3}$ in Ω. Blocks $t_{2}$ in $t_{1} ˆ t_{2} ˆ t_{3}$ and $t_{2}^{'}$ in $t_{1}^{'} ˆ t_{2}^{'} ˆ t_{3}^{'}$ are considered to be equal only when $t_{2} = t_{2}^{'}$ and we in addition have that $t_{1} = t_{1}^{'}$ .

A blocking of Ω is a set of blocks for each calculation t in Ω satisfying:
Given two blocks in t, they are either disjoint or one is included in the other.

For each calculation, all chains of blocks totally ordered by inclusion will be finite.

t is one of the blocks in t.

The level of a block $t_{1}$ in t is the number of other blocks in t properly containing $t_{1}$ as a substring.

If $t = t_{1} ˆ t_{2}$ and $t^{'} = t_{1} ˆ t_{2}^{'}$ are two calculations in Ω with a common initial substring $t_{1}$ , and if a block of level m in t starts at the beginning of $t_{2}$ , then a block of level m starts in $t^{'}$ at the beginning of $t_{2}^{'}$ .

Moreover, if the two blocks coincide until one of them ends, they are equal.
(iii) above just makes the rest easier to express.

The blocking is tame if we in addition have

There is a partial function ${BLOCK}_{Ω}$ computable in $^{2} E$ such that for each string t in $Ω_{pre}$ , ${BLOCK}_{Ω} (t)$ decides for each m if there is a block of level m starting at the next query ${NEXT}_{Ω} (t)$ and decides the levels of the blocks, if any, ending before the next query.

For each block $s = {(f_{δ}, a_{δ})}_{γ ⩽ δ < β}$ in a calculation t there is a unique injective denotation ${d_{δ}^{s}}_{γ ⩽ δ < α}$ , where these denotations are computed using the two functions denote and redenote (with subscript Ω if needed) both computable in $^{2} E$ and where

if $t_{1} ˆ (f_{β}, a_{β})$ is an initial substring of the calculation t and s is the block of highest level containing $(f_{β}, a_{β})$ then denote $(t_{1}, a_{β})$ will be the denotation $d_{β}^{s}$ .

If s is a block of level $m > 0$ contained in the calculation $t = t_{1} ˆ s_{1} ˆ s ˆ s_{2} ˆ t_{3}$ , where $t_{2} = s_{1} ˆ s ˆ s_{2}$ is the surrounding block of level $m - 1$ , then redenote with input $t_{1} ˆ s_{1} ˆ s$ and m will give us $d^{t_{2}}$ restricted to $s_{1} ˆ s$ .

Comment 1.
It is (c), (ii) that captures the essence of blocking, a block represents the local delay of deciding what the denotation one level up will be like, and will make it possible to simulate the evaluation of a procedure as a nested application of $I$ .
Definition 5.10.
An Inductive Procedure is a tame $Π_{1}^{1}$ -procedure with a tame blocking.
Theorem 5.11.
A functional Φ of type 3 is definable from an inductive procedure if and only if Φ is computable in $I$ .
Proof.
We first show that if Φ is definable from an inductive procedure, then Φ is computable from $I$ . We use a nested version of the argument in Lemma 5.8, using everywhere that the functions next, block, denote and redenote are computable in $^{2} E$ , and thus in $I$ . We use the recursion theorem for Kleene computations to make the following precise:

Given F, we construct the inductive definition $Γ_{F}$ as in Observation 5.8, using the denotation as it comes, until we hit the beginning of a block s. Then we start the execution of a sub-procedure simulating the evaluation of F along s as an inductive definition $Γ_{F}^{s}$ in the same way. This sub-procedure will come to an end when the full evaluation along s is simulated. At this stage we can describe the next step for $Γ_{F}$ : From the output of $Γ_{F}^{s}$ , $^{2} E$ and the assumption on blocks, we can compute the correct denotations along the string up to the end of s, and $Γ_{F}$ just ads the full simulation of the evaluation of F in Ω using this denotation.

If s has sub-blocks, then $Γ_{F}^{s}$ will have sub-procedures in a similar way, this is why we need the recursion theorem to formally describe this procedure.

In order to prove the other direction we elaborate on the proofs that the class of functionals satisfying our requirements is closed under Kleene computability, and assume that $Φ_{1}, \dots, Φ_{n}$ now are defined from inductive procedures.

The only case we need to consider is that of application of $Φ_{i}$ , $\begin{matrix} {e} (\vec{Φ}, F, \vec{f}, \vec{a}) = Φ_{i} (λ g . {e_{1}} (\vec{Φ}, F, g, \vec{f}, \vec{a})) . \end{matrix}$ Let $G (g) = {e_{1}} (\vec{Φ}, F, g, \vec{f}, \vec{a})$ . Then there is a calculation ${(g_{β}, b_{β})}_{β < α}$ in $Ω_{i}$ matching G. For each $β < α$ , the pair $(g_{β}, b_{β})$ will be replaced by a substring of the composed calculation as follows: $(g_{β}, )$ will just be preserved as it is, while $(g_{β}, b_{β})$ is replaced by a string starting with $(g_{β}, )$ and continued with the calculation of $F (g_{β})$ .

When we defined the denotations for these composed calculations, we gave them directly from the denotations in the $Ω_{i}$ -calculation and from the denotations in the calculations of $G (g_{β})$ without adding any further delay. Thus we can inherit the blocking structure of the $Ω_{i}$ -calculation, and whenever $(g_{β}, a_{β})$ is in one of these blocks before we compose all the substrings, we let all blocks in t, where $(g_{β}, *) ˆ t$ is inserted for $(g_{β}, a_{β})$ and t is the calculation of $G (g_{β})$ , be new blocks of a higher level.

When we constructed the d-procedure in this case, we gave the rules for transforming the denotations in this simulating block to denotations of the corresponding items in the full calculation, and this clearly can be relativised to the blocks in $Ω_{i}$ .

In order to tie the whole thing up showing that the definability and computability requirements of what we construct are satisfied, we need to use the recursion theorem for $^{2} E$ , induction on the ordinal lengths of $\vec{Φ}, F$ -computations and induction/recursion on the level of blocks in a string. The details are tedious, but simple. □

5.3. The $I$ -computable functions revisited

In this section we will consider pure computations $\begin{matrix} {e} (I, \vec{a}), \end{matrix}$ without function and functional parameters.

In our definition of a procedure, we used the parameter F to give values to queries, but at certain points we also inserted elements of the LOG, functions appearing as arguments in sub-computations but not necessarily as arguments in the main computable function or functional we design the procedure for.

When transforming a computation in $I$ without functional arguments to a procedure, this LOG will now be the backbone of the calculation. Since there will be no genuine queries anymore, we can even drop the ∗ for marking element-hood in the LOG. Thus a pure string will be a triple $(D, ≺, {g_{d}}_{d \in D})$ where $(D, ≺)$ is a well ordering and each $g_{d} \in N^{N}$ . We will consider such strings that are $Π_{1}^{1}$ -singletons, where the set of other strings isomorphic to initial segments of the given one is $Π_{1}^{1}$ , where we have a next-function computable in $^{2} E$ and where we have functions block, denote and redenote as before, making this one-point set an inductive procedure. We call this a pure inductive calculation, and these pure inductive calculations will reflect $I$ -computations with integer inputs.

Remark 5.12.
While transforming a computation ${e} (I, \vec{a}) = b$ to a pure inductive calculation we first of all linearised the computation. Then we hid some of the indexing in the function next, and also, in the way we designed the denotations, we actually “hid” all intermediate “Kleene-calculations” that do not involve the scheme S8. However, for transfinite computations, this hiding will not significantly reduce the length of a computation. On the other hand, when we translate a pure inductive calculation to a Kleene-computation, we may add to the length of the computation, partly because it takes time to compute next, block, denote and redenote whenever needed, and partly because we have to add time to the time-span of an induction in order to verify that the induction comes to a halt when it does.

Recall the definition of π as the first ordinal with no code computable in $I$ . We have the following characterisation. Lemma 5.13.
π is the supremum $π^{}$ of the ordinal lengths of the pure inductive calculations.*
Proof.
First, we will prove that $π ⩽ π^{}$ . Let $α < π$ , and let $(X, ≺)$ be $I$ -computable and a well ordering of ordinal length α. We prove this direction by constructing a pure inductive calculation with at least α many steps. We will use the pure inductive calculations deciding $x \in X$ and $x ≺ y$ as building blocks, and with the help of those we simulate, in the form of a grand pure inductive calculation, the induction building up X one point at each step, a process that needs exactly α many steps.

Then we prove that $π^{} ⩽ π$ . Let t be a pure inductive calculation. Using the same strategy we used when showing that a functional definable from an inductive procedure is computable in $I$ , a strategy involving the recursion theorem for $I$ , we can show that there is a nested computation relative to $I$ that computes a code for the ordinal length of t, whenever we enter a block, we compute the length of that block as a subcomputation, and then at the end of the block, ad a copy of this code to the well ordering we are building up. Actually, it will be the denotations with their ordering we compute, and in a block, the local denotations within that block. □
Theorem 5.14.
Let $α < π$ . If α is the rank of a pure inductive calculation t, then α is $Π_{1}^{1}$ -characterisable.
Proof.
If $f \in WO$ has rank β, we can decide if $β = α$ as follows: By recursion on the wellordering coded by f we can use ${NEXT}_{t}$ and the $^{2} E$ -algorithm organising the blockings to compute the corresponding stages in t with full information about where in the blocking structure we are at each step. If this simulation terminates exactly at the end of t, we accept f, otherwise we refute it. The set of $f s$ accepted will be $Π_{1}^{1}$ . □

6. Tracing computations in $I$

6.1. Partial procedures

In order to make constructions of procedures smoother, we have not insisted on the natural requirement that for each f and calculation, there is at most one occurrence of the query $F (f) =$ ?. However, when it does appear several times, the calculation will be based on the same answer everywhere. When we refer to a query $F (f) =$ ? we will always mean the first occurrence. When ${e} (I, F, \vec{f}, \vec{a}) ↓$ for all F, it is clear that the associated procedure will lead to terminating calculations for all F. This means that when f appears in a query $F (f) =$ ? there will be an extension into a calculation for all $a \in N$ . Conversely, we can prove that for every calculation $({(f_{β}, a_{β})}_{β < α}, c)$ constructed in the procedure for $λ F . {e} (I, F, \vec{f}, \vec{a})$ , if F matches this string, then c will be the value of this computation.

We will now discuss what happens if we consider computations ${e_{0}} (I, F)$ that do not terminate for all inputs F. In this case, we can still define a set $Ω_{pre}$ of strings with denotations, in these strings we may enter blocks and sub-blocks, and they behave as required for inductive procedures, since we have established these properties for each e, F, $\vec{f}$ and $\vec{a}$ such that ${e} (I, F, \vec{f}, \vec{a}) ↓$ .

We need to consider parameters $\vec{f}$ and $\vec{a}$ , since such parameters occur in subcomputations, so we reason within this generality.

If we consider the construction of the inductive procedure more carefully, we can observe more closely what we construct in the case of non-termination, again by cases according to what the index e is like:

If e is an index for an initial computation, we constructed a trivial procedure yielding the correct output without any queries made.

In the case of composition, we first constructed the procedure for the inner component, and for the calculations in this procedure (the strings that give us an answer), we concatenated with calculations from the procedure of the corresponding outer component. In the case the composed computation does not terminate, we do construct a string modelling the leftmost non-terminating subcomputation.

In the cases where there will be exactly one subcomputation, what we do is using the string of that one.

In the cases of application of F or application of $I$ , we are doing exactly as above, in case of non-termination we build up the string until we reach the leftmost non-terminating subcomputation, and ending the string in Ω with a copy of a string for this leftmost one.

In the case that e is not an index at all, the procedure will be trivial, but with non-termination as the conclusion.

If ${e} (I, F, \vec{f}, \vec{a}) ↑$ , there will be a leftmost Moschovakis witness, a descending sequence of unsettled computations such that every computation to the left will terminate, and it will be exactly the string corresponding to evaluate ${e} (I, F, \vec{f}, \vec{a})$ along this descending sequence of subcomputations that will be constructed in this case. If Ω is constructed like this, we will simply have some strings where the conclusion must be ⊥ instead of a proper value. However, since being a Moschovakis witness is semi-decidable (this was the original point with them), we see that $Ω_{pre}$ will still be $Π_{1}^{1}$ . We will also have functions next, block, denote and redenote computable in $^{2} E$ . What may be lacking is that blocks may be entered without ever being left, that we may have an infinite descending sequence of blocks (that will then not have end points) and that we will not have a $^{2} E$ -computable way to define the denotations for the blocks unless they have an end. So, the procedure will not be an inductive procedure. This is as it has to be, since we can define the characteristic function of a set of functions of type 2 that is complete semi-computable in $I$ using a procedure like this, replace the value ⊥ with 0 and the value $a \in N$ with 1 as the values of calculations.

These considerations contain the proof of

Theorem 6.1.
There is a total procedure Ω such that $Ω_{pre}$ is $Π_{1}^{1}$ , and such that there is a partial function ${NEXT}_{Ω}$ that is computable in $^{2} E$ , but where the functional defined by Ω is not computable in $I$ .
Proof.
The only property left is that we must be able to decide, using a $^{2} E$ -algorithm, if a string t in $Ω_{pre}$ is maximal or not, and in case it is maximal, if it has a value or not. By recursion on the indexing of t we can follow the points in the computation tree corresponding to the points in t. If this point in the computation tree has an index that is none of the indices of S1–S9, we can conclude that there is no value. If the blocking depth is infinite, we can conclude that the string represents non-termination. This can be checked by $^{2} E$ , using block and calculating the lim sup of the block level of the items of the string. In all other cases, there will be a next query or there will be a value given to us by the original next-function □

We also have Theorem 6.2.
There is a non-terminating computation ${e} (I, \vec{a})$ such that the length of the string simulating the leftmost Moschovakis witness will have length at least $π (= ω_{1}^{I})$ .
Proof.
If this were not the case we can use Gandy selection for $I$ -computations and make $I$ -semidecidable equivalent to $I$ -decidable, obtaining the standard contradiction by diagonalisation. □
Remark 6.3.
Moschovakis witnesses were introduced in [14], and they were significant for the understanding of higher order computing relative to normal functionals and in set recursion. They are also introduced in [12, Section 5.2.2], and they were applied in the proof of [20, Theorem 6.6].

6.2. Functionals computable in $I$

In a series of papers [16–22,27], written jointly with Sam Sanders, we investigate classes of functionals of type 3 that serve as realisers for classical theorems in analysis, and where each class contains elements computable in $I$ . There are unsettled question concerning the relative computability of the elements of these classes. In this section we will see that in the case that elements of these classes are computable in $I$ , we can “almost” compute the Suslin functional from them, and consequently, they will “almost” be computationally equivalent to $I$ itself. We will make the “almost” precise by replacing a functional Φ computable in $I$ with one that traces the history of the computation, not just gives the value. We call this the honest version of Φ

There is an analogue with what we do in complexity theory where the complexity of a set often is measured by the resources required to decide membership in the set and not by what we can decide using small resources combined with the set as an oracle. In a mathematically precise way we will see that if we compute realisers for some classical theorems of analysis from $I$ , we need the full power of $I$ in doing so.

Definition 6.4.
Let $Ω \in W (I)$ be the inductive procedure constructed from a functional Φ as computable in $I$ . We define the honest version $H (Φ)$ as the functional (of mixed type) that sends a functional F of type 2 to the fixed point of the inductive definition $Γ_{F}$ as constructed from Ω in the proof of Theorem 5.11, i.e. as the history of the evaluation of $Φ (F)$ from $I$ .

An open covering of a set X in a topological space $T$ is normally defined as a set $C$ of open sets in $T$ whose union is a superset of X. However, if we make use of the concept of realisers, a realiser of the open covering will be a map sending $x \in X$ to an open set $O_{x} \in T$ such that $x \in O_{x}$ . When Borel [3] gave an attempt of a direct proof of the Heine–Borel theorem, he actually, without knowing the concept, used this idea of a realiser; with free translation he expressed his assumption as follows:
Assume that we have a way of attaching an open neighbourhood $O_{x}$ of x to each $x \in [a, b]$ .
In the papers with Sanders, we have considered coverings and related concepts primarily over the Cantor space $C = {0, 1}^{N}$ and the Baire space $B = N^{N}$ given as functionals F of type 2, where $F (f)$ defines the neighbourhoods $C_{\overline{f} (F (f))}$ and $B_{\overline{f} (F (f))}$ of extensions of $\overline{f} (F (f))$ , depending on which space we consider f to be an element of.

We have been looking at the following three classes:
Definition 6.5.

A strong realiser for the Heine–Borel theorem will be a functional Θ such that whenever $F : C \to N$ , then $Θ (F) = {f_{1}, \dots, f_{n}}$ such that $\begin{matrix} C \subseteq C_{\overline{f_{1}} (F (f_{1}))} \cup \dots \cup C_{\overline{f_{n}} (F (f_{n}))} . \end{matrix}$

A weak realiser for the Heine–Borel theorem will be a functional θ such that whenever $F : C \to N$ then $θ (F) = {s_{1}, \dots, s_{n}}$ where each $s_{i}$ is a finite binary sequence, ${C_{s_{1}}, \dots, C_{s_{n}}}$ is a covering of $C$ and for each $i = 1, \dots, n$ there is an $f_{i} \in C$ such that $\overline{f_{i}} (F (f_{i})) = s_{i}$ .

A Pincherle realiser will be a functional M such that whenever $F : C \to N$ , then $M (F) = N \in N$ and N satisfies:

If $G : C \to N$ satisfies that $G (g) ⩽ F (f)$ whenever $\overline{g} (F (f)) = \overline{f} (F (f))$ (F is considered as a realiser for local boundedness) then G is bounded by N on $C$ .

The following lemma is trivial:
Lemma 6.6.
Every strong realiser for the Heine–Borel theorem computes a weak one, and every weak realiser for the Heine–Borel theorem computes a Pincherle realiser.

The proof is left for the reader.
Lemma 6.7.
Let M be a Pincherle realiser that is countably based. Let $F : C \to N$ be arbitrary, and let $X \subset C$ be countable such that $M (G) = M (F)$ for all G such that F and G are equal when restricted to X. Then ${C_{\overline{f} (F (f))} : f \in X}$ is a covering of $C$ .
Proof.
Assume not, let $M (F) = N$ and define $\begin{matrix} F_{1} (g) = \{\begin{array}{ll} F (g) & if g \in ⋃_{f \in X} C_{\overline{f} (F (f))} \\ N + 1 & if g \notin ⋃_{f \in X} C_{\overline{f} (F (f))} \end{array} \end{matrix}$ Then $M (F) = M (F_{1})$ because the two functions agree on X. However, if we define $\begin{matrix} G (g) = \{\begin{array}{ll} 0 & if g \in ⋃_{f \in X} C_{\overline{f} (F (f))} \\ N + 1 & if g \notin ⋃_{f \in X} C_{\overline{f} (F (f))} \end{array} \end{matrix}$ then G obviously satisfies the boundedness condition induced by $F_{1}$ , but is not bounded by N, contradicting that $N = M (F_{1})$ . □
Theorem 6.8.
Let M be a Pincherle realiser that is computable in $I$ . Then the Suslin functional S is computable in $H (M)$ and $^{2} E$ .
Proof.
In [16, Theorem 5.1] it is proved that there is a functional F computable in $^{2} E$ such that the collection of neighbourhoods defined from F and the hyperarithmetical binary sequences is not a covering of $C$ . The construction easily relativizes to an arbitrary $f \in N^{N}$ so it suffices to show how we can compute a complete $Π_{1}^{1}$ -set from $H (M)$ , F and $^{2} E$ .

For a general procedure Ω and an arbitrary G, the calculation of $Ω (G)$ will form a countable basis for $Ω (G)$ . If F and M are as given, Lemma 6.7 then shows that the calculation of $Ω_{M} (F)$ must contain queries that are not hyperarithmetical. However, in an inductive procedure, if the input functional is computable in $^{2} E$ , then all queries appearing at the level of a computable ordinal must also be computable in $^{2} E$ . This follows from the assumption that the next-function is computable in $^{2} E$ . So, the calculation of $Ω_{M} (F)$ must have a rank that goes beyond $ω_{1}^{C K}$ . The set of (indices for the) computable well-orderings will then be both $Σ_{1}^{1}$ and $Π_{1}^{1}$ in this calculation, and thus computable from this calculation using $^{2} E$ . The calculation itself is computable from F and $H (M)$ , so we are through. □

In [15] it is proved that $I$ (under the name of IND) is computable in the Suslin functional S and any strong realiser for the Heine–Borel theorem. We can improve this as Lemma 6.9.
Let M be a Pincherle realiser. Then $I$ is computable in M and S .
Proof.
Let $F : C \to C$ be given, and consider F as an inductive definition, defining the sequence ${f_{β}}_{β < α}$ . This set is coded as a prewellordering $(A, ⪯)$ where $x ⪯ y$ if $f_{α} (x) = f_{α} (y) = 1$ and we for all $β ⩽ α$ have that $f_{β} (y) = 1 \to f_{β} (x) = 1$ . Identify ⪯ with ${⟨ x, y ⟩ : x ⪯ y}$ . We will see how to compute ⪯ from F, S and M. We let $x, y, z, w, n, m$ etc. range over $N$ .

The idea is, for each $n, x, y$ to construct a functional $G_{n, x, y}$ such that if $x ⪯ y$ then $M (G_{n, x, y}) ⩾ n$ and such that $G_{n, x, y}$ is independent of n otherwise. We will then have that $\begin{matrix} x ⪯ y \leftrightarrow \forall m \exists n (M (G_{n, x, y}) > m) . \end{matrix}$ We will now define $G_{n, x, y} (X)$ in cases, where we in all cases except in the last one have defined $G_{n, x, y} (X)$ independently of n, x and y, and so large that ⪯ will be different from X for at least one argument $z < G_{n, x, y} (X)$ . We rename X to $⪯_{X} = {⟨ z, w ⟩ : ⟨ z, w ⟩ \in X}$ . Let $⟨ z, w ⟩ \in X_{≺}$ if $⟨ z, w ⟩ \in ⪯_{X}$ and $⟨ w, z ⟩ \notin ⪯_{X}$ .

For all cases below, we assume that none of the earlier cases apply.
If $⪯_{X}$ is not a preordering, there is a finite initial binary subsequence s of (the characteristic function of) X such that no extension of s is a preordering. In this case, let $G_{n, x, y} (X)$ be the length of the least such s.

Let $W^{X}$ be the domain of the well founded part of $≺_{X}$ (computable in the data using S), and for each $z \in W^{X}$ let $f_{z}^{X}$ be the characteristic function of ${w \in W^{X} : w ≺_{X} z}$ and $g_{z}^{X}$ be the characteristic function of ${w \in W^{X} : w ⪯_{X} z}$ .

If there is a $≺_{X}$ -least w such that $g_{w}^{X} \neq max {f_{w}^{X}, F (f_{w}^{X})}$ , we know that $⪯_{X}$ differs from ⪯, and we need to find a finite approximation to (the characteristic function of) X where this is manifested. Choose the numerically least such w. There will be two sub-cases:

- There is a z such that $f_{w}^{X} (z) = 0$ , $F (f_{w}^{X}) (z) = 0$ but $g_{w}^{X} (z) = 1$ . Select the numerically least such z. Then we cannot have both $z ⪯ w$ and $w ⪯ z$ , while we have $z ⪯_{X} w$ and $w ⪯_{X} z$ , so we let $\begin{matrix} G_{n, x, y} (X) = max {⟨ z, w ⟩, ⟨ w, z ⟩} + 1 . \end{matrix}$ – There is no such z. Then there is a z such that $f_{w}^{X} (z) = 0$ , $F (f_{w}^{X}) (z) = 1$ , but $g_{w}^{X} (z) = 0$ . Then we do have $z ⪯ w$ and not $z ⪯_{X} w$ , so we let $G_{n, x, y} (X) = ⟨ z, w ⟩ + 1$ for the numerically least such z.

If we get to this point, the well-founded part of $⪯_{X}$ is an initial segment of ⪯, and we want to decide if this initial segment is proper or not. This is tested by letting g be the characteristic function of $W^{X}$ : the initial segment is proper unless $F (g) ⩽ g$ . If the initial segment is proper, we can find z such that $z ⪯ z$ but $z \notin W^{X}$ , recognised by $g (z) < F (g) (z)$ . If $⟨ z, z ⟩ \notin X$ , we let $G_{n, x, y} (X) = ⟨ z, z, ⟩ + 1$ . If $⟨ z, z ⟩ \in X$ , z is still not in the well founded part of $≺_{X}$ so there will be a w such that $w ≺ z$ and w is not in the well founded part of $≺_{X}$ . Since z is of minimal rank in ≺ outside $X^{W}$ , we cannot have that $w ≺ z$ when $w \notin X^{W}$ . We can find such z and w using $^{2} E$ and search over $N$ , and we let $G_{n, x, y} (X) = max {⟨ z, w ⟩, ⟨ w, z ⟩} + 1$ .

So far, we have defined $G_{n, x, y} (X)$ independently of n, x and y. If we have reached this far, we know that $I (F) = W^{X}$ , and we let

$G_{n, x, y} (X) = n$ if $x \in W^{X}$ , $y \in W^{X}$ and $x ⪯_{X} y$

$G_{n, x, y} (X) = 0$ otherwise.
Through items (1)–(3) above, we have constructed $G_{n, x, y}$ such that unless X is a preordering with ⪯ as its well founded part, $G_{n, x, y} (X)$ is such that ⪯ is not in the neighbourhood of X induced by $G_{n, x, y} (X)$ . Moreover $G_{n, x, y} (X)$ is independent of n (and of x and y) in this case. We further have that $G_{n, x, y}$ is independent of n if we do not have $x ⪯ y$ , while the function $\begin{matrix} F_{n, x, y} (X) = \{\begin{array}{ll} n & if X = ⪯ \\ 0 & otherwise \end{array} \end{matrix}$ will satisfy the bounding condition induced by $G_{e, x, y}$ if $x ⪯ y$ . In this case we must have that $M (F_{e, x, y}) ⩾ n$ . This is what we aimed to obtain. □
Corollary 6.10.
Let M be a Pincherle realiser that is computable in $I$ . Then $I$ and $(H (M),^{2} E)$ are computationally equivalent.

7. Relativisations

It is a matter of routine to relativise concepts of computability to functions $f : N \to N$ or to subsets of $N$ . Our characterisation of the functionals of type 3 computable in $I$ using inductive procedures do relativise directly to objects of type 1. We even had to do so in order to cope with inductive procedures themselves, since there will be function parameters in subcomputations of the form ${e} (I, \vec{a})$ .

In this section we will briefly discuss how the concept of an inductive procedure relativises to parameters $\vec{F}$ of type 2, without going into any technical details. The key observation is that we can easily extend the definition of procedures to cope with multiple inputs $\vec{F}$ , or, if we are interested in functionals of type 3 computable in a fixed functional G of type 2, to input pairs $F, G$ . We only have to add the coordinate of each query when asked during a calculation.

Given a partial functional $λ (F, H) {e} (I, F, H)$ there will be a procedure Ω as before, where Ω and $Ω_{pre}$ are $Π_{1}^{1}$ , there are functions next, block, denote and redenote computable in $^{2} E$ . The calculations/strings corresponding to terminating computations will have a blocking accepting the axioms we gave, respecting the rules of bracketing and with no infinitely deep chains of blocks. Our main problem in describing what we mean with an inductive G-procedure for a total functional $λ F . {e} (F, G)$ is to find the right relativisation of $Π_{1}^{1}$ to G. Another, minor problem is that we must allow information about G in the LOG of a calculation, or in some other way, see Remark 7.4.

Definition 7.1.
Let G be a functional of type 2.
For $g \in N^{N}$ , let ${g_{i}^{p}}_{i \in N}$ be an enumeration of the set of functions primitive recursive in g, where the enumeration is uniformly computable in g.

A weakly arithmetical formula $Φ (g, G)$ is a formula that is arithmetical in g and $λ i . G (g_{i}^{p})$ .

$X \subseteq N^{N}$ is weakly arithmetical in G if it is defined by $\begin{matrix} g \in X \leftrightarrow Φ (g, G) \end{matrix}$ for some weakly arithmetical formula Φ.

$X \subseteq N^{N}$ is $Π_{1}^{1} [G]$ if X is the intersection of a $Π_{1}^{1}$ -set and a set that is weakly arithmetical in G.

Definition 7.2.
Let Ω be a procedure for a total functional $Φ (F)$ . Let G be of type 2. Ω is an inductive G-procedure if the following are satisfied:
Ω and $Ω_{pre}$ are $Π_{1}^{1} [G]$ .

There is a function ${NEXT}_{Ω}$ partially computable in $^{2} E$ and terminating on $Ω_{pre}$ .

The calculations in Ω have blockings, and the blocking structure is guided by the partial functions bloc, denote and redenote, computable in $^{2} E$ and with the standard properties.

Theorem 7.3.
Let G be of type 2 and Φ of type 3. Then Φ is computable in $I$ and G if and only if Φ is definable by an inductive G-procedure.
Proof.
One way is proved exactly in the same way that we proved that if Φ is definable by an inductive procedure, then Φ is computable in $I$ .

For the other direction, let $Φ (F) = {e} (I, F, G)$ . We consider the procedure $Ω^{+}$ for the partial functional $λ F, H . {e} (I, F, H)$ , where both $Ω^{+}$ and $Ω_{pre}^{+}$ are $Π_{1}^{1}$ and where the functions next, block, denote and redenote are computable in $^{2} E$ . Intersecting with a set that is weakly arithmetical in G we get the procedures in $Ω^{+}$ and the strings in $Ω_{pre}^{+}$ that are matching G. Those will be our Ω and $Ω_{pre}$ . □
Remark 7.4.
Pairs $(g, G (g))$ will still be present in the calculations. They may be considered to be elements of the LOG of the G-calculations. This would actually require a re-definition of our concepts of procedure and calculation, but we leave how to do it for the reader in case of interest.

It may be possible to avoid appearances of pairs $(g, G (g))$ in the procedure for $λ F . {e} (F, G)$ , but then at the cost of the complexity of the next-function and the other functions guiding the blockings. These will then have to be computed by $I$ and G, and not just by $^{2} E$ .

8. Summary and open problems

In this paper2

The paper was written in 2020, and has, since then, only undergone cosmetic changes and updates of the bibliography.

we have investigated non-monotone induction as given by a functional

I

of type 3 from the perspective of higher order computability theory. We have established strong closure properties for the companion

L_{π}

of the set of functions computable in

I

, and we have represented computations relative to

I

and parameters of type 2 in the form of inductive procedures and sequential calculations. Computations relative to

I

can be linearised in a natural way, since application of

I

can be seen as the result of a linear process indexed by some ordinal, and the ordinal rank of a calculation reflects the length of a computation seen as a linear process. We have shown that the length of any terminating computation, with integer inputs in addition to

I

, is

Π_{1}^{1}

-characterisable. There are two open problems related to this:

Problem 1.

Are all ordinals $α < π$ $Π_{1}^{1}$ -characterisable?

Problem 2.

Are there ordinals computable in $I$ that are not the length of any computation ${e} (I, \vec{a})$ ?

A positive solution to Problem 1 would give us a nice characterisation of the closure ordinal π, but we conjecture that the answer is negative. We also believe that when the two problems are solved, the solution will show that they are connected.

Problem 2 asks if there is a gap-structure for computing with $I$ as it is for infinite time Turing machines, see Hamkins and Lewis [7] or Welch [33], and for recursion in $^{3} E$ , and not as for computing relative to the Superjump $S$ . In case there are gaps, it will be of interest to see how the gap structure coincides with the gap structure of infinite time Turing machines computing in time bounded by π.

This problem also suggests that there is a distinction between various functionals of type 3 similar to the one between predicative and non-predicative arguments in mathematics: in order to compute $S (F)$ we need to generate the 1-section of F, the set of functions computable in F, and we need that F is total on its own 1-section, and then we have enough information to deduce what $S (F)$ will be. This will also work when F is partial, as long as it is not so partial that it is undefined for an input it is able to compute. In order to compute $I (F)$ for a partial F we need that F is total on functions computable from F and $I$ , including the final product of the ‘computation’. In our main theorem for establishing closure properties of π, it is essential for the argument that we construct an induction where π tells us to stop, and that we thus must stop before π. We can only consider partial inductive definitions computable in $I$ when they also make sense in the case when the recursion lasts π steps in order to deduce that they must stop at an earlier stage. This is a kind of non-predicativity.

We will end this paper with an example of a partial functional $F : C \to C$ that is computable in $I$ and total on the set of $f \in C$ that are computable in $I$ , but where the closure set X of the associated inductive definition is not computable in $I$ because $F (X)$ is undefined.

Example 4.

We define F as a partial function from $P (N \times N)$ to $P (N \times N)$ :

If X is a well ordering, use Gandy selection for $I$ to find an index e for a well ordering $Y \subseteq N \times N$ with domain B and of length extending that of X, and let $\begin{matrix} F (X) = X \cup {(a, ⟨ e, b ⟩) : a \in X \land b \in B} \cup {(⟨ e, b ⟩, ⟨ e, c ⟩) : (b, c) \in Y} . \end{matrix}$

If X is not a well ordering, we let $F (X) = X$ .

During the induction, a new index e must be found each time, so

F (X_{β})

will be an end-extension of

X_{β}

with a well ordering of the order-type of some

Y_{β}

with index

e_{β}

for all

β < π

. The recursion will stop after π steps because then

F (X_{π})

is undefined. Clearly,

X_{π}

is not computable in

I

Footnotes

Acknowledgements

I thank Sam Sanders for involving me in the project this paper is a spin-off from, for reading a preliminary version of this paper, and for giving valuable feedback on the exposition. Our joint project started with him asking me if I could say anything about the computational properties of some weird-looking functionals of type 3, of which $Θ_{0}$ is one example. The rest is history.

I am grateful to John Hartley for his comments on the exposition.

I am grateful to editors and anonymous referees of other papers from our joint project, their sharp comments often helped me think more clearly about how to present higher order computability in the context of those papers, and then of this one.

I also thank the participants of the seminar on mathematical logic at the University of Oslo for attending my informal talks on the subjects of this paper, and giving valuable feedback.

References

S.O.

Aanderaa, Inductive definitions and their closure ordinals, in: Generalized Recursion Theory,

J.E.

Fenstad and

P.G.

Hinman, eds, North-Holland, 1974, pp. 207–220.

Aczel and

Richter, Inductive definitions and analogues of large cardinals, in: Conference in Mathematical Logic, London’70, Springer Verlag, 1971, pp. 1–10.

Borel, Sur quelques points de la théorie des fonctions, Ann. Sci. École Norm. Sup. 12(3) (1895), 9–55. doi:10.24033/asens.406.

Cenzer, Ordinal recursion and inductive definitions, in: Generalized Recursion Theory,

J.E.

Fenstad and

P.G.

Hinman, eds, North-Holland, 1974, pp. 221–264.

J.E.

Fenstad, Generalized Recursion Theory, Springer Verlag, 1980.

R.O.

Gandy, General recursive functionals of finite type and hierarchies of functions, Ann. Fac. Sci. Univ. Clermont-Ferrand No. 35 (1967), 5–24.

J.D.

Hamkins and

Lewis, Infinite time Turing machines, The Journal of Symbolic Logic 65(2) (2000), 567–604. doi:10.2307/2586556.

Harrington, The superjump and the first recursively Mahlo ordinal, in: Generalized Recursion Theory,

J.E.

Fenstad and

P.G.

Hinman, eds, North-Holland, 1974, pp. 43–52.

J.P.

Hartley, The countably based functionals, Journal of Symbolic Logic 48 (1983), 458–474. doi:10.2307/2273562.

10.

S.C.

Kleene, Recursive functionals and quantifiers of finite types I, Trans. Amer. Math. Soc. 91 (1959), 1–52.

11.

Kohlenbach, Higher Order Reverse Mathematics 2001, Lecture Notes in Logic, Vol. 211, Association of Symbolic Logic, 2005, pp. 281–295.

12.

J.R.

Longley and

Normann, Higher Order Computability, Spinger Verlag, 2015.

13.

Moldestad, Computations in Higher Types, Lecture Notes in Mathematics, Vol. 574, Springer Verlag, 1977.

14.

Y.N.

Moschovakis, Hyperanalytic predicates, Transactions of the American Mathematical Society 129(2) (1967), 249–282. doi:10.1090/S0002-9947-1967-0236010-2.

15.

Normann, Functionals of type 3 as realisers of classical theorems in analysis, in: Sailing Routes in the World of Computation,

Manea,

R.G.

Miller and

Nowotka, eds, Lecture Notes in Computer Science, Vol. 10936, Springer Verlag, 2018, pp. 318–327. doi:10.1007/978-3-319-94418-0_32.

16.

Normann and

Sanders, Computability theory, nonstandard analysis and their connections, Journal of Symbolic Logic 84(4) (2019), 1422–1465. doi:10.1017/jsl.2019.69.

17.

Normann and

Sanders, The strength of compactness in computability theory an nonstandard analysis, Annals of Pure and Applied Logic 170(11) (2019), 1–42. doi:10.1016/j.apal.2019.05.007.

18.

Normann and

Sanders, On the mathematical and foundational significance of the uncountable, Jour. Math. Log. 19(1) (2019). doi:10.1142/S0219061319500016.

19.

Normann and

Sanders, Pincherle’s theorem in reverse mathematics and computability theory, Annals of Pure and Applied Logic 171(5) (2020). doi:10.1016/j.apal.2020.102788.

20.

Normann and

Sanders, Open sets in reverse mathematics and computability theory, Journal of Logic and Computation 30(8) (2020), 1639–1676. doi:10.1093/logcom/exaa049.

21.

Normann and

Sanders, The axiom of choice in computability theory and reverse mathematics, with a cameo for the continuum hypothesis, Journal of Logic and Computation 31(1) (2021), 297–325. doi:10.1093/logcom/exaa080.

22.

Normann and

Sanders, On the uncountability of

R

, Journal of Symbolic Logic 87(4) (2022), 1–45. doi:10.1017/jsl.2022.27.

23.

Normann and

Sanders, Betwixt Turing and Kleene, in: Logical Foundations of Computer Science, Lecture Notes in Computer Science,

Artemov and

Nerode, eds, Vol. 13137, 2022, pp. 236–252. doi:10.1007/978-3-030-93100-1_15.

24.

Normann and

Sanders, On robust theorems due to Boltzano, Weierstrass, Jordan and Cantor, Journal of Symbolic Logic (2022). doi:10.1017/jsl.2022.71.

25.

Normann and

Sanders, On the computational properties of basic mathematical notions, Journal of Logic and computation 32(8) (2022), 1747–1795. doi:10.1093/logcom/exaa075.

26.

Normann and

Sanders, The biggest five of reverse mathematics, Journal of Mathematical Logic (2022). doi:10.1142/S021119061324500077.

27.

Normann and

Sanders, Representations in measure theory: Between a non-computable rock and hard to prove place, submitted arXiv:1902.02756.

28.

G.D.

Plotkin, LCF considered as a programming language, Theoretical Computer Science 5(3) (1977), 223–255. doi:10.1016/0304-3975(77)90044-5.

29.

Richter and

Aczel, Inductive definitions and reflecting properties of admissible ordinals, in: Generalized Recursion Theory,

J.E.

Fenstad and

P.G.

Hinman, eds, North-Holland, 1974, pp. 301–381.

30.

G.E.

Sacks, Higher Recursion Theory, Perspectives in Mathematical Logic, Springer-Verlag, Berlin-Heidelberg, 1990.

31.

D.S.

Scott, A type-theoretical alternative to ISWIM, CUCH, OWHY, unpublished note (1969). Edited version in: A collection of contributions in honor of Corrado Böhm on the occasion of his 70th birthday, Theoretical Computer Science 121(1–2) (1993), 411–440. doi:10.1016/0304-3975(93)90095-B.

32.

P.D.

Welch, Transfinite machine models, in: Turing’s Legacy, Developments from Turing’s Ideas in Logic,

Downey, ed., Lecture Notes in Logic, Vol. 42, Cambridge University Press, 2014, pp. 493–529. doi:10.1017/CBO9781107338579.015.

33.

P.D.

Welch, Higher type recursion for transfinite machine theory, in: Computing with Foresight and Industry,

Manea,

Martin,

Paulusma and

Primeiro, eds, Springer Lecture Notes in Computer Science, Vol. 11558, 2019, pp. 72–83. doi:10.1007/978-3-030-22996-2_7.

Computability and non-monotone induction

Abstract

Keywords

1. Introduction

1.1. Motivation and history

1.2. Overview and results

2. Non-monotone induction and computability

2.1. Inductive definitions

4.1. Motivation

4.2.1. The definitions

4.2.3. Examples

5.1. Computability in 2 E

Definition 5.3. Let W ( I ) be the set of d-procedures for functionals Φ computable in I as constructed in the proofs of Lemma 4.16 and Lemma 4.19. 5.2.1. Tame d-procedures

6.1. Partial procedures

Footnotes

Acknowledgements

References

5.1. Computability in $^{2} E$

Definition 5.3.
Let $W (I)$ be the set of d-procedures for functionals Φ computable in $I$ as constructed in the proofs of Lemma 4.16 and Lemma 4.19.

5.2.1. Tame d-procedures