The Gandy–Hyland functional and a computational aspect of Nonstandard Analysis

Abstract

In this paper, we highlight a new computational aspect of Nonstandard Analysis relating to higher-order computability theory. In particular, we prove that the Gandy–Hyland functional equals a primitive recursive functional involving nonstandard numbers inside Nelson’s internal set theory. From this classical and ineffective proof in Nonstandard Analysis, a term from Gödel’s system T can be extracted which computes the Gandy–Hyland functional in terms of a modulus-of-continuity functional and the special fan functional. We obtain several similar relative computability results not involving Nonstandard Analysis from their associated nonstandard theorems. By way of reversal, we show that certain relative computability results, called Herbrandisations, also imply the nonstandard theorem from whence they were obtained. Thus, we establish a direct two-way connection between the field Computability (in particular theoretical computer science) and the field Nonstandard Analysis.

Keywords

Gandy–Hyland functional Nonstandard Analysis higher-order computability theory

1. Introduction

Our aim is to highlight a new computational aspect of Nonstandard Analysis relating to (higher-order) computability theory. We study the Gandy–Hyland functional, which was introduced in [10] as an example of a higher-type functional not computable, in the sense of Kleene’s S1-S9 (see [17], 1.10 or [15], 5.1.1), in the fan functional over the total continuous functionals (see [17], 4.61 or [15], 8.3.3). The Gandy–Hyland functional Γ is defined as: $\begin{matrix} (GH) & (\exists Γ^{3}) (\forall Y^{2} \in C, s^{0}) [Γ (Y^{2}, s^{0}) = Y (s * 0 * (λ n^{0}) Γ (Y, s * (n + 1)))], \end{matrix}$ where ‘ $Y^{2} \in C$ ’ is the definition of continuity on Baire space as in (1.1); All notations are introduced in Section 2.2. $\begin{matrix} (1.1) & (\forall f^{1}) (\exists N^{0}) (\forall g^{1}) (\overline{f} N =_{0} \overline{g} N \to Y (f) =_{0} Y (g)) . \end{matrix}$ The functional Γ from ( GH ) apparently exhibits non-well-founded self-reference: Indeed, in order to compute Γ at $s^{0}$ , one needs the values of Γ at all child nodes of $s^{0}$ , as is clear from the right-hand side of ( GH ). In turn, to compute the value of Γ at the child nodes of s, one needs the value of Γ at all grand-child nodes of s, and so on. Hence, repeatedly applying the definition of Γ seems to result in a non-terminating recursion. By contrast, primitive recursion is well-founded as it reduces the case for $n + 1$ to the case for n, and the case for $n = 0$ is given.

In Section 4.2, we show that in Nelson’s internal set theory (see Section 2.1), the primitive recursive1

¹
The functional G is primitive recursive in the sense of Gödel’s system $T$ ; See Section 2.2.

functional

\begin{matrix} (1.2) & G (Y, s, M) = \{\begin{matrix} Y (s * 00 \dots) & | s | ⩾ M \\ Y (s * 0 * (λ n^{0}) G (Y, s * (n + 1), M)) & otherwise \end{matrix} \end{matrix}

equals the Γ-functional from ( GH ) for standard input and any nonstandard number

M^{0}

. Note that one need only apply the definition of G at most M times to terminate in the first case of (1.2). In other words, the extra case ‘

| s | ⩾ M

’ provides a nonstandard stopping condition which ‘unwinds’ the non-terminating recursion in Γ to the terminating one in G. Or: one can trade in self-reference for nonstandard numbers. Thus, we shall refer to G as the canonical approximation of Γ.

We work in $P$ , a fragment of Nelson’s internal set theory based on Gödel’s $T$ , both introduced in Section 2. The proof in Section 4 that $G (\cdot, M)$ and $Γ (\cdot)$ are equal for standard inputs and nonstandard $M^{0}$ , takes place in P augmented with a nonstandard continuity axiom NPC and a nonstandard bar induction axiom STP . This is a natural setting for Γ, as it is modified bar recursion in disguise ([4], Section 4).

From the aforementioned proof in $P$ regarding Γ and G, we show how to extract a term t from Gödel’s $T$ and a proof in higher-order Peano arithmetic that t computes the Gandy–Hyland functional in terms of a special case of the fan functional and a modulus-of-continuity functional. Conceptually, it is important to note that this final proof, as well as the term t, does not involve Nonstandard Analysis, and that the extraction of the term t from the proof proceeds via an algorithm. In Sections 4.4 to 4.6, we obtain further nonstandard results from which we extract related relative computability results. In particular, the relative computability results in Section 4.4 and 4.5 are ‘pointwise’ versions of previous results in this paper, and these results witness the robustness of our approach. Furthermore, in Section 4.5 and 4.6, we prove some Reverse Mathematics² results (both nonstandard and effective). In particular, we work with associates of continuous functionals in Section 4.6, leading to particularly elegant results.

Finally, it is a natural ‘Reverse Mathematics2

For Friedman’s foundational program Reverse Mathematics, we refer to Simpson’s monograph [24], which provides an excellent overview.

style’ question if from a relative computability result, obtained via Nonstandard Analysis, the ‘original’ nonstandard theorem can be re-obtained. In answer to this question, we show in Section 4.3 that (a proof of) the original nonstandard theorem (that the Gandy–Hyland functional

Γ (\cdot)

equals

G (\cdot, M)

for all standard inputs and nonstandard

M^{0}

) follows from (a proof of) a certain natural relative computability result, called the Herbrandisation of the original nonstandard theorem.

In conclusion, while these relative computability results are not necessarily deep or surprising in and of themselves, the methodology by which we arrive at them constitutes the real surprise of this paper, namely a new computational aspect of Nonstandard Analysis: From a classical-logic proof in which no attention to computability is given at all, and in which Nonstandard Analysis is freely used, we obtain a relative computability result in a straightforward way. With some attention to detail, a natural relative computability result, called the Herbrandisation, allows us to re-obtain the original nonstandard theorem. In this way, we establish a direct two-way connection between the field Computability (in particular theoretical computer science) and Nonstandard Analysis. As such, our results differ significantly from known applications of Nonstandard Analysis in Computability, as discussed in Section 2.5.

2. About and around internal set theory

In this section, we introduce the system $P$ in which we will work. In a nutshell, $P$ is a conservative extension of Gödel’s system $T$ with certain axioms from Nelson’s Internal Set Theory $IST$ [16] based on the approach from [27,28].

2.1. Nelson’s internal set theory $IST$

In this section, we discuss Nelson’s internal set theory $IST$ , first introduced in [16]. In Nelson’s syntactic approach to Nonstandard Analysis, as opposed to Robinson’s semantic one [21], a new unary predicate ‘st(x)’, read as ‘x is standard’, is added to the language of ZFC, the usual foundation of mathematics. In other words, $L_{IST} = L_{ZFC} \cup {st}$ is the language of $IST$ if $L_{ZFC}$ is the language of $ZFC$ . The notations $(\forall^{st} x) (\dots)$ and $(\exists^{st} y) (\dots)$ are short for $(\forall x) (st (x) \to \dots)$ and $(\exists y) (st (y) \land \dots)$ . A formula of $IST$ is called internal if it does not involve ‘st’, and external otherwise. The external axioms Idealisation, Standard Part, and Transfer govern ‘st’; They are defined3

³
The superscript ‘fin’ in (I) means that x is ‘finite’, i.e. the set is in one-to-one correspondence with some subset ${0, 1, \dots, N}$ of the natural numbers. A finite set x is standard in $IST$ if (and only if) the associated number N is, in light of [16], Theorem 1.1.

as follows:

Definition 2.1 (Axioms of

IST

$(\forall^{st fin} x) (\exists y) (\forall z \in x) φ (z, y) \to (\exists y) (\forall^{st} x) φ (x, y)$ , for internal φ.

$(\forall x^{st}) (\exists^{st} y) (\forall^{st} z) ((z \in x \land φ (z)) \leftrightarrow z \in y)$ , for any formula φ.

$(\forall^{st} t) [(\forall^{st} x) φ (x, t) \to (\forall x) φ (x, t)]$ , where $φ (x, t)$ is internal and only has free variables $x, t$ .

The system IST consist of the aforementioned three external axioms, plus the internal system ZFC, i.e. the latter does not involve ‘st’. Now, $IST$ is a conservative extension of ZFC for the internal language $L_{ZFC}$ , as proved in [16]. Of course, the step from $ZFC$ to $IST$ can be done for fragments of $IST$ too; we shall make use the system $P$ , a fragment of $IST$ based on Gödel’s system $T$ , introduced in Section 2.3. Before that, we briefly introduce system $T$ in Section 2.2. The system $P$ was first introduced in [27] and is exceptional in that it has a ‘term extraction procedure’ with a very wide scope (see Corollary 2.9). We discuss this in more detail in Remark 3.5.

2.2. Gödel’s system $T$

In this section, we briefly introduce Gödel’s system $T$ and the associated systems ${E-PA}^{ω}$ and ${E-PA}^{ω *}$ .

In his Dialectica paper [11], Gödel defines an interpretation of intuitionistic arithmetic into a quantifier-free calculus of functionals. This calculus is now known as ‘Gödel’s system T’, and is essentially just primitive recursive arithmetic ([5], Section 1.2.10) with the schema of recursion expanded to all finite types. Firstly, the set of finite types $T$ is: $\begin{matrix} (i) 0 \in T and (ii) If σ, τ \in T then (σ \to τ) \in T, \end{matrix}$ where 0 is the type of natural numbers, and $σ \to τ$ is the type of mappings from objects of type σ to objects of type τ. Gödel’s system $T$ includes ‘recursor’ constants $R^{ρ}$ for every finite type $ρ \in T$ , defining primitive recursion: $\begin{matrix} (PR) & R^{ρ} (f, g, 0) : = f and R^{ρ} (f, g, n + 1) : = g (n, R^{ρ} (f, g, n)), \end{matrix}$ for $f^{ρ}$ and $g^{0 \to (ρ \to ρ)}$ . The system ${E-PA}^{ω}$ is a combination of Peano arithmetic and system $T$ , and the full axiom of extensionality ( E ). The detailed definition of ${E-PA}^{ω}$ may be found in [14], Section 3.3; We do introduce the notion of equality and extensionality in ${E-PA}^{ω}$ , as these notions are needed below.

Definition 2.2 (Equality).

The system ${E-PA}^{ω}$ includes equality between natural numbers ‘ $=_{0}$ ’ as a primitive. Equality ‘ $=_{τ}$ ’ for type τ-objects $x, y$ is then: $\begin{matrix} (2.1) & [x =_{τ} y] \equiv (\forall z_{1}^{τ_{1}} \dots z_{k}^{τ_{k}}) [x z_{1} \dots z_{k} =_{0} y z_{1} \dots z_{k}] \end{matrix}$ if the type τ is composed as $τ \equiv (τ_{1} \to \dots \to τ_{k} \to 0)$ . The usual inequality predicate ‘ $⩽_{0}$ ’ between numbers has an obvious definition, and the predicate ‘ $⩽_{τ}$ ’ is just ‘ $=_{τ}$ ’ with ‘ $=_{0}$ ’ replaced by ‘ $⩽_{0}$ ’ in (2.1). The axiom of extensionality is the statement that for all $ρ, τ \in T$ , we have: $\begin{matrix} (E) & (\forall x^{ρ}, y^{ρ}, φ^{ρ \to τ}) [x =_{ρ} y \to φ (x) =_{τ} φ (y)] . \end{matrix}$

Next, we introduce ${E-PA}^{ω *}$ , a definitional extension of ${E-PA}^{ω}$ with a type for finite sequences; The set $T^{*}$ is: $\begin{matrix} (i) 0 \in T^{*}, (ii) If σ, τ \in T^{*} then (σ \to τ) \in T^{*}, and (iii) If σ \in T^{*}, then σ^{*} \in T^{*}, \end{matrix}$ where $σ^{*}$ is the type of finite sequences of objects of type σ. The system ${E-PA}^{ω *}$ includes ( PR ) for all $ρ \in T^{*}$ , as well as dedicated ‘list recursors’ to handle finite sequences for any $ρ^{*} \in T^{*}$ . A detailed definition of ${E-PA}^{ω *}$ may be found in [27], Section 2.1. We now introduce some notations specific to ${E-PA}^{ω *}$ , as also used in [27].

Notation 2.3 (Finite sequences).

The system ${E-PA}^{ω *}$ has a dedicated type for ‘finite sequences of objects of type ρ’, namely $ρ^{*}$ . Since the usual coding of pairs of numbers goes through in ${E-PA}^{ω *}$ , we shall not always distinguish between 0 and $0^{*}$ ; See e.g. the definition $(GH)$ of the Gandy–Hyland functional in Section 1. Similarly, we do not always distinguish between ‘ $s^{ρ}$ ’ and ‘ $⟨ s^{ρ} ⟩$ ’, where the former is ‘the object s of type ρ’, and the latter is ‘the sequence of type $ρ^{*}$ with only element $s^{ρ}$ ’. The empty sequence for the type $ρ^{*}$ is denoted by ‘ ${⟨ \cdot ⟩}_{ρ}$ ’, usually with the typing omitted. Furthermore, we denote by ‘ $| s | = n$ ’ the length of the finite sequence $s^{ρ^{*}} = ⟨ s_{0}^{ρ}, s_{1}^{ρ}, \dots, s_{n - 1}^{ρ} ⟩$ , where $| ⟨ \cdot ⟩ | = 0$ , i.e. the empty sequence has length zero. For sequences $s^{ρ^{*}}, t^{ρ^{*}}$ , we denote by ‘ $s * t$ ’ the concatenation of s and t, i.e. $(s * t) (i) = s (i)$ for $i < | s |$ and $(s * t) (j) = t (| s | - j)$ for $| s | ⩽ j < | s | + | t |$ . For a sequence $s^{ρ^{*}}$ , we define $\overline{s} N : = ⟨ s (0), s (1), \dots, s (N) ⟩$ for $N^{0} < | s |$ . For a sequence $α^{0 \to ρ}$ , we also write $\overline{α} N = ⟨ α (0), α (1), \dots, α (N) ⟩$ for any $N^{0}$ . By way of shorthand, $q^{ρ} \in Q^{ρ^{*}}$ abbreviates $(\exists i < | Q |) (Q (i) =_{ρ} q)$ . Finally, we shall use $\underline{x}, \underline{y}, \underline{t}, \dots$ as short for tuples $x_{0}^{σ_{0}}, \dots, x_{k}^{σ_{k}}$ of possibly different type $σ_{i}$ .

Finally, we discuss an alternative way of formulating Gödel’s system $T$ .

Remark 2.4 (Alternatives to primitive recursion).

In [8], Cor. 20, it is shown that $T$ can be equivalently defined using finite product of selection functions operators $P^{ρ}$ , rather than the usual recursor constants $R^{ρ}$ as in ( PR ). The definition of $P^{ρ}$ is rather complicated, and therefore omitted, but we do point out that in the proof of [8], Theorem 18, the operator $P^{ρ}$ is defined explicitly in terms of the recursor constants $R^{ρ}$ . In other words, $P^{ρ}$ is primitive recursive in the sense of Gödel’s $T$ .

Intuitively speaking, the operator $P^{ρ}$ is such that $P^{ρ} (i, m, \dots)$ is defined in terms of $P^{ρ} (i + 1, m, \dots)$ for $i ⩽ m$ , and the constant-zero-functional if $i > m$ . In other words, $P^{ρ}$ can call itself, but only m many times before defaulting to a fixed output, namely the constant-zero-functional. In light of the definition of $P^{ρ}$ in [8], Def. 10, it is immediate that G from (1.2) can be expressed in terms of the operator $P^{ρ}$ , and G is therefore primitive recursive (in the sense of system $T$ ). Indeed, $G (Y, s, M)$ can only call itself at most M times before defaulting to the first case of (1.2): Since $G (Y, s, M)$ is defined in terms of $G (Y, s * (n_{1} + 1), M)$ , which is defined in terms of $G (Y, s * (n_{1} + 1) * (n_{2} + 1), M)$ , and so on, we have that: $G (Y, s * (n_{1} + 1) * (n_{2} + 1) * \dots * (n_{M} + 1), M) = Y (s * (n_{1} + 1) * (n_{2} + 1) * \dots * (n_{M} + 1) * 00 \dots)$ , which is the first case of (1.2), i.e. $G (Y, s, M)$ defaults to the first case in (1.2) after M applications of its definition.

2.3. The classical system $P$

In this section, we introduce the system $P$ . We first discuss some of the external axioms studied in [27].

Firstly, as in [27], Def. 6.1, we have the following definition of ${E-PA}_{st}^{ω *}$ . The language of the latter is the language of ${E-PA}^{ω *}$ extended with a new predicate ‘ ${st}_{σ}$ ’ for every finite type $σ \in T^{*}$ . Just as in [27], the typing is omitted.

Definition 2.5 (The system ${E-PA}_{st}^{ω *}$ ).

The set $T^{*}$ is defined as the collection of all the constants in the language of ${E-PA}^{ω *}$ . The system ${E-PA}_{st}^{ω *}$ is defined as ${E-PA}^{ω *} + T_{st}^{*} + {IA}^{st}$ , where $T_{st}^{*}$ consists of the following axiom schemas:

The schema $st (x) \land x = y \to st (y)$ ,

The schema providing for each closed term $t \in T^{*}$ the axiom $st (t)$ .

The schema $st (f) \land st (x) \to st (f (x))$ .

The external induction axiom IA^st is as follows, for any formula Φ:

\begin{matrix} (IA^{st}) & (Φ (0) \land (\forall^{st} n^{0}) (Φ (n) \to Φ (n + 1))) \to (\forall^{st} m^{0}) Φ (m) . \end{matrix}

Secondly, to guarantee that $P$ be a conservative extension of Peano arithmetic, Nelson’s axiom Standard part needs to be weakened to ${HAC}_{int}$ as follows, for any internal formula φ: $\begin{matrix} ({HAC}_{int}) & (\forall^{st} x^{ρ}) (\exists^{st} y^{τ}) φ (x, y) \to (\exists^{st} F^{ρ \to τ^{*}}) (\forall^{st} x^{ρ}) (\exists y^{τ} \in F (x)) φ (x, y) . \end{matrix}$ Note that $F (x)$ provides a finite sequence of witnesses to $(\exists^{st} y)$ , explaining its name Herbrandized Axiom of Choice.

Thirdly, Nelson’s axiom Idealisation requires no weakening and appears in [27] as follows: $\begin{matrix} (I) & (\forall^{st} x^{σ^{*}}) (\exists y^{τ}) (\forall z^{σ} \in x) φ (z, y) \to (\exists y^{τ}) (\forall^{st} x^{σ}) φ (x, y), \end{matrix}$ where φ is again an internal formula. Intuitively speaking, (the contraposition of) idealisation $I$ allows us to ‘push all standard quantifiers to the front’.

Fourth, we introduce the system $P$ , for which we need a fragment of the axiom of choice. Note that $P$ does not include any fragment of Transfer, as the latter translates to non-constructive axioms by Section 3.1.2.

Definition 2.6 (The classical system $P$ ).

For internal and quantifier-free $φ_{0}$ , we have $\begin{matrix} ({QF-AC}^{σ, τ}) & (\forall x^{σ}) (\exists y^{τ}) φ_{0} (x, y) \to (\exists F^{σ \to τ}) (\forall x^{σ}) φ_{0} (x, F (x)) . \end{matrix}$

The system $P$ is defined as ${E-PA}_{st}^{ω *} + {QF-AC}^{1, 0} + {HAC}_{int} + I + {IA}^{st}$ .

The system $P$ is a conservative extension of Peano arithmetic; in particular $P$ is connected to ${E-PA}^{ω *}$ by Theorem 2.8. The superscript ‘ $S_{st}$ ’ in the latter is the syntactic translation from [27], Def. 7.1 and is defined as:

Definition 2.7.
Assume $Φ (\underline{a})$ and $Ψ (\underline{b})$ in the language of $P$ have interpretations $\begin{matrix} (2.2) & Φ {(\underline{a})}^{S_{st}} \equiv (\forall^{st} \underline{x}) (\exists^{st} \underline{y}) φ (\underline{x}, \underline{y}, \underline{a}) and Ψ {(\underline{b})}^{S_{st}} \equiv (\forall^{st} \underline{u}) (\exists^{st} \underline{v}) ψ (\underline{u}, \underline{v}, \underline{b}), \end{matrix}$ where $ψ, φ$ are internal. Then we have the folllowing:
$ψ_{0}^{S_{st}} : = ψ_{0}$ for atomic internal $ψ_{0}$ .

${(st (z))}^{S_{st}} : = (\exists^{st} x) (z = x)$ .

${(\neg Φ)}^{S_{st}} : = (\forall^{st} \underline{Y}) (\exists^{st} \underline{x}) (\forall \underline{y} \in \underline{Y} [\underline{x}]) \neg φ (\underline{x}, \underline{y}, \underline{a})$ .

${(Φ \lor Ψ)}^{S_{st}} : = (\forall^{st} \underline{x}, \underline{u}) (\exists^{st} \underline{y}, \underline{v}) [φ (\underline{x}, \underline{y}, \underline{a}) \lor ψ (\underline{u}, \underline{v}, \underline{b})]$ .

${((\forall z) Φ)}^{S_{st}} : = (\forall^{st} \underline{x}) (\exists^{st} \underline{y}) (\forall z) (\exists {\underline{y}}^{'} \in \underline{y}) φ (\underline{x}, {\underline{y}}^{'}, z)$ .

Theorem 2.8.
Let $Φ (\underline{a})$ be a formula in the language of ${E-PA}_{st}^{ω }$ and suppose* $Φ {(\underline{a})}^{S_{st}} \equiv \forall^{st} \underline{x} \exists^{st} \underline{y} φ (\underline{x}, \underline{y}, \underline{a})$ . If $Δ_{int}$ is a collection of internal formulas and $\begin{matrix} (2.3) & P + Δ_{int} ⊢ Φ (\underline{a}), \end{matrix}$ then one can extract from the proof a sequence of closed terms t in $T^{}$ such that* $\begin{matrix} (2.4) & {E-PA}^{ω } + {QF-AC}^{1, 0} + Δ_{int} ⊢ \forall \underline{x} \exists \underline{y} \in \underline{t} (\underline{x}) φ (\underline{x}, \underline{y}, \underline{a}) . \end{matrix}$
Proof.
Immediate by [27], Theorem 7.7. □

The proofs of the soundness theorems in [27], Sections 5–7 actually provide an algorithm* to obtain the term t from the theorem. In other words, one can just ‘read off’ the term t from the proof mentioned in (2.3).

The following corollary is only mentioned in [27] for Heyting arithmetic, but it also turns out to be valid for Peano arithmetic. The proof of the corollary takes place in the same meta-theory as Theorem 2.8.
Corollary 2.9 (Term extraction).

For internal ψ and $Φ (\underline{a}) \equiv (\forall^{st} \underline{x}) (\exists^{st} \underline{y}) ψ (\underline{x}, \underline{y}, \underline{a})$ , we have ${[Φ (\underline{a})]}^{S_{st}} \equiv Φ (\underline{a})$ . Hence, if $Δ_{int}$ is a collection of internal formulas and $\begin{matrix} P + Δ_{int} ⊢ (\forall^{st} \underline{x}) (\exists^{st} \underline{y}) ψ (\underline{x}, \underline{y}, \underline{a}), \end{matrix}$ then one can extract from the proof a sequence of closed terms t in $T^{*}$ such that $\begin{matrix} {E-PA}^{ω *} + {QF-AC}^{1, 0} + Δ_{int} ⊢ (\forall \underline{x}) (\exists \underline{y} \in t (\underline{x})) ψ (\underline{x}, \underline{y}, \underline{a}) . \end{matrix}$

Proof.
A tedious but straightforward verification using (i)-(v) from Definition 2.7 establishes that ${[Φ (\underline{a})]}^{S_{st}} \equiv Φ (\underline{a})$ for $Φ (\underline{a}) \equiv (\forall^{st} \underline{x}) (\exists^{st} \underline{y}) ψ (\underline{x}, \underline{y}, \underline{a})$ and internal ψ. This verification is in [22], Section 2 and [23], Section 2.1. □

With regard to notation, for the rest of this paper, a normal form refers to a formula of the form $(\forall^{st} x) (\exists^{st} y) φ (x, y)$ for φ internal. Thus, one can say that normal forms are ‘invariant under $S_{st}$ ’ in the sense of the previous corollary.

Finally, the previous corollary is central to this paper. Indeed, a large number of theorems in Nonstandard Analysis can be brought into a normal form (see also Remark 3.5), and therefore fall within the scope of Corollary 2.9.
2.4. Notations

We finish this section with remarks on notation in $P$ . First of all, we mostly follow Nelson, as sketched now.

Remark 2.10 (Nonstandard Analysis).

We write $(\forall^{st} x^{τ}) Φ (x^{τ})$ and $(\exists^{st} x^{σ}) Ψ (x^{σ})$ for $(\forall x^{τ}) [st (x^{τ}) \to Φ (x^{τ})]$ and $(\exists x^{σ}) [st (x^{σ}) \land Ψ (x^{σ})]$ . We write $(\forall x \in Ω) Φ (x^{0})$ and $(\exists x \in Ω) Ψ (x^{0})$ as symbolic4

⁴
As suggested by its name, Nelson’s internal set theory deals with internal sets, i.e. sets can only be formed in $IST$ from internal formulas. In particular, external formulas cannot be used to define sets in $IST$ , and a violation of this rule is called illegal set formation by Nelson (see [16]). Thus, our use of ‘ $x \in Ω$ ’ is purely symbolic, as there is no set of all nonstandard numbers in $IST$ .

abbreviations for

(\forall x^{0}) [\neg st (x^{0}) \to Φ (x^{0})]

and

(\exists x^{0}) [\neg st (x^{0}) \land Ψ (x^{0})]

. Furthermore, we write ‘

x^{0} \in Ω

’ for

\neg st (x)

. A formula A is ‘internal’ if it does not involve ‘

st

’;

A^{st}

is defined from A by appending ‘st’ to all quantifiers (except bounded number quantifiers).

Secondly, we introduce an ‘approximate’ notion of equality.

Remark 2.11 (Approximate quality).

We define ‘approximate equality $\approx_{τ}$ ’ as: $\begin{matrix} (2.5) & [x \approx_{τ} y] \equiv (\forall^{st} z_{1}^{τ_{1}} \dots z_{k}^{τ_{k}}) [x z_{1} \dots z_{k} =_{0} y z_{1} \dots z_{k}] \end{matrix}$ if the type τ is composed as $τ \equiv (τ_{1} \to \dots \to τ_{k} \to 0)$ . Now, the system $P$ includes the axiom of extensionality ( E ), but not the following version: $\begin{matrix} (2.6) & (\forall^{st} x^{ρ}, y^{ρ}, φ^{ρ \to τ}) [x \approx_{ρ} y \to φ (x) \approx_{τ} φ (y)], \end{matrix}$ which is just ( E )^st, and we shall refer to (2.6) as the axiom of standard extensionality. As noted in [27], p. 1973, ( E )^st is problematic and cannot be included in $P$ . Finally, we need an explicit version of the axiom of extensionality: $\begin{matrix} (EXT (Ξ, Y)) & (\forall f^{1}, g^{1}) (\overline{f} Ξ (f, g) =_{0} \overline{g} Ξ (f, g) \to Y (f) =_{0} Y (g)) . \end{matrix}$ We say that $Ξ^{2}$ is an extensionality functional for the functional $Y^{2}$ .

Finally, we introduce the following (strictly speaking ‘abuse of’) notation.

Remark 2.12 (Set-theoretic notation).

As in [27], we sometimes use intuitive set-theoretic notation, although $P$ strictly speaking only involves functionals. First of all, we assume that ‘sets of numbers $X^{1}$ ’ are given by their characteristic functions $f_{X}^{1}$ , i.e. $(\forall x^{0}) [x \in X \leftrightarrow f_{X} (x) = 1]$ .

Secondly, the notation ‘ $Y^{2} \in C$ ’ means that $Y^{2}$ is continuous on Baire space ‘as usual’ given by (1.1). A formula $(\forall^{st} Y^{2} \in C) (\dots)$ is thus shorthand for $(\forall Y^{2}) ([st (Y) \land Y \in C] \to \dots)$ ; Note in particular that no mention whatsoever of (1.1)^st is made, or will be made in the rest of this paper.

Thirdly, we sometimes block quantifiers together to save space; In this way, the formula $(\forall (Y^{2} \in C, Z^{2}) \in Ψ) (\dots)$ for some functional $Ψ^{2^{*}}$ , is an abbreviation for $\begin{matrix} (\forall Z^{2}) (\forall Y^{2}) ([Y \in C \land (\exists j < | Ψ |) (Ψ (j) =_{2} Y) \land (\exists i < | Ψ |) (Ψ (i) =_{2} Z)] \to \dots), \end{matrix}$ which saves considerable space, as will become clear below.

2.5. Applications of Nonstandard Analysis in computability

We discuss known applications of Nonstandard Analysis in Computability, in particular [18–20].

First of all, as suggested by its title, the main goal of [18] is characterising the continuous functionals in highly elementary nonstandard terms in Robinson’s semantic approach to Nonstandard Analysis. In particular, Normann defines a class $F_{k}$ of so-called finitary operators mapping $F_{k - 1}$ into $N$ . In the nonstandard model, $^{*} F_{k}$ is the corresponding nonstandard extension, consisting of the so-called hyper-finitary functionals, and Normann proves that $Ct (k)$ is isomorphic to the standard part of $^{*} F_{k}$ .

While Normann’s approach is similar in spirit to ours (representing complicated objects via elementary nonstandard ones), his nonstandard proofs do not obviously carry computational content. In particular, the use of Standard Part is problematic, as discussed in the final paragraph of this section.

Secondly, as again suggested by its title, the main goal of [19] is also the characterisation of a certain type structure in terms of elementary nonstandard objects. The authors state the following:

The novelty [compared to [18]] here is that we use a constructive version of hyperfinite functionals and also generalise the method to transfinite types. Many of the results of this paper are constructive, though not the characterisation theorems themselves. (See [19], p. 1216)

Hence, the approach from [19] is again similar in spirit to ours (representing complicated objects via elementary nonstandard ones), but the nonstandard proofs again do not obviously carry computational content. In particular, the use of standard extensionality is problematic, as explicitly mentioned in [19], p. 1218.

Thirdly, the author and Dag Normann explore the connection between higher-order computability theory and Nonstandard Analysis in [20]. The special fan functional Θ from Section 3.1.1 (and related functionals based on ${WWKL}_{0}$ from [24, Ch. X]) is shown to have quite ‘non-standard’ computational properties: On one hand, no type two functional (including $(\exists^{2})$ and $(S^{2})$ ) can compute the special fan functional, but both $(\exists^{3})$ and $MUC$ can.

Thus, the special fan functional exhibits extreme computational hardness compared to its first-order strength, but applying the so-called ECF-translation (see [26], Section 2.6) converts the existence of the former into ${WKL}_{0}$ . Higher-type generalisations of $STP$ (and hence of the special fan functional) give rise to even more extreme computational hardness. Furthermore, the combination $Π_{1}^{0} - TRANS + STP$ allows one to derive ${ATR}_{0}$ relative to ‘st’, i.e. the proofs in [18] (and hence [19]) seem to take place in highly non-constructive systems. In particular, it seems difficult to (directly) recover computational content from the proofs in [18,19], in contrast to the proofs in this paper.

3. Preliminaries

In this section, we prove some preliminary results needed below. In particular, we study useful fragments of Standard Part and Transfer from $IST$ in Section 3.1. Furthermore, in Section 3.2, we derive a version of so-called bar induction for external formulas from these fragments of $IST$ .

The theme of this paper is the extraction of relative computability results from theorems of Nonstandard Analysis. To further understanding, we will treat in Corollary 3.4 a very simple example of this theme. We also formulate a template for later term extraction results based on this corollary.

3.1. Fragments of standard part and transfer

In this section, we discuss several useful fragments of Standard Part and Transfer from $IST$ . To this end, we first introduce underspill and overspill, which will be used a lot below. Intuitively speaking, overspill and underspill express that no internal formula can capture the ‘st’ predicate exactly.

Theorem 3.1.
The system $P$ proves overspill and underspill, i.e. $\begin{matrix} (\forall^{st} x^{ρ}) φ (x) \to (\exists y^{ρ}) [\neg st (y) \land φ (y)] and (\forall x^{ρ}) [\neg st (x) \to φ (x)] \to (\exists^{st} y^{ρ}) φ (y), \end{matrix}$ for any internal formula φ.
Proof.
Immediate by [27], Prop. 3.3 and Section 5. □

We apply underspill often as follows: From $(\forall M \in Ω) ψ (M)$ for internal ψ, we conclude $(\forall K^{0}) [\neg st (K) \to (\forall M ⩾ K) ψ (M)]$ . Applying underspill for $φ (K) \equiv (\forall M ⩾ K) ψ (M)$ , we obtain $(\exists^{st} K^{0}) (\forall M ⩾ K) ψ (M)$ .
3.1.1. The nonstandard counterpart of weak König’s lemma

In this section, we study the following fragment of the Standard part principle of $IST$ : $\begin{matrix} (STP) & (\forall f^{1} ⩽_{1} 1) (\exists^{st} g^{1} ⩽_{1} 1) (f \approx_{1} g) . \end{matrix}$ The function $g^{1}$ from STP is called a standard part of $f^{1}$ . By the following theorem, $STP$ is a nonstandard version of weak König’s lemma ( $WKL$ ). The latter is the statement that a infinite binary tree has a path (see e.g. [24], IV).

Theorem 3.2.
The system $P$ proves that STP is equivalent to $\begin{array}{l} (3.1) & (\forall T^{1} ⩽_{1} 1) [(\forall^{st} n) (\exists β^{0}) (| β | = n \land β \in T) \to (\exists^{st} α^{1} ⩽_{1} 1) (\forall^{st} n^{0}) (\overline{α} n \in T)], \end{array}$ where ‘ $T ⩽_{1} 1$ ’ means that T is a binary tree. Over $P$ , STP is also equivalent to $\begin{matrix} (3.2) & (\forall f^{1}) (\exists^{st} g^{1}) ((\forall^{st} n^{0}) (\exists^{st} m^{0}) (f (n) = m) \to f \approx_{1} g) . \end{matrix}$
Proof.
Assume STP and apply overspill to $(\forall^{st} n) (\exists β^{0}) (| β | = n \land β \in T)$ to obtain $β_{0}^{0} \in T$ with nonstandard length $| β_{0} |$ . Now apply STP to $β^{1} : = β_{0} * 00 \dots$ to obtain a standard $α^{1} ⩽_{1} 1$ such that $α \approx_{1} β$ and hence $(\forall^{st} n) (\overline{α} n \in T)$ . For the reverse direction, let $f^{1}$ be a binary sequence, and define a binary tree $T_{f}$ which contains all initial segments of f. Now apply (3.1) for $T = T_{f}$ to obtain STP .

For the final equivalence, $(3.2) \to STP$ is trivial, and for the reverse implication, fix $f^{1}$ such that $(\forall^{st} n) (\exists^{st} m) f (n) = m$ and let $h^{1}$ be such that $(\forall n, m) (f (n) = m \leftrightarrow h (n, m) = 1)$ . Applying ${HAC}_{int}$ to the former, there is standard $Φ^{0 \to 0^{}}$ such that $(\forall^{st} n) (\exists m \in Φ (n)) f (n) = m$ , and define $Ψ (n) : = {max}_{i < | Φ (n) |} Φ (n) (i)$ . Now define $α_{0} ⩽_{1} 1$ as: $α_{0} (0) : = h (0, 0)$ , $α_{0} (1) : = h (0, 1), \dots, α_{0} (Ψ (0)) : = h (0, Ψ (0))$ , $α_{0} (Ψ (0) + 1) : = h (1, 0)$ , $α_{0} (Ψ (0) + 2) : = h (1, 1), \dots, α_{0} (Ψ (0) + Ψ (1)) : = h (1, Ψ (1))$ , et cetera. Now let $β_{0}^{1} ⩽_{1} 1$ be the standard part of $α_{0}$ provided by STP and define $g (n) : = (μ m ⩽ Ψ (n)) [β_{0} (\sum_{i = 0}^{n - 1} Ψ (i) + m) = 1]$ . By definition, $g^{1}$ is standard and $f \approx_{1} g$ . □

The function $g^{1}$ from (3.2) is also called a standard part* of $f^{1}$ . We now show that STP follows from the nonstandard uniform continuity of all type two functionals on Cantor space. Note that the principle NUC in the theorem contradicts classical mathematics, as the latter involves discontinuous functionals.
Theorem 3.3.
The axiom STP can be proved in $P$ plus the axiom $\begin{matrix} (NUC) & (\forall^{st} Y^{2}) (\forall f^{1}, g^{1} ⩽_{1} 1) (f \approx_{1} g \to Y (f) =_{0} Y (g)) . \end{matrix}$
Proof.
First of all, note that NUC implies by Remark 2.11 that $\begin{matrix} (3.3) & (\forall^{st} Y^{2}) (\forall f^{1}, g^{1} ⩽_{1} 1) (\exists^{st} N^{0}) (\overline{f} N =_{0} \overline{g} N \to Y (f) =_{0} Y (g)) . \end{matrix}$ Applying idealisation I to (3.3), we obtain that $\begin{matrix} (3.4) & (\forall^{st} Y^{2}) (\exists^{st} x^{0^{}}) (\forall f^{1}, g^{1} ⩽_{1} 1) (\exists N^{0} \in x) (\overline{f} N =_{0} \overline{g} N \to Y (f) =_{0} Y (g)), \end{matrix}$ which immediately yields that $\begin{matrix} (3.5) & (\forall^{st} Y^{2}) (\exists^{st} N_{0}^{0}) (\forall f^{1}, g^{1} ⩽_{1} 1) (\overline{f} N_{0} =_{0} \overline{g} N_{0} \to Y (f) =_{0} Y (g)), \end{matrix}$ by taking $N_{0}$ in (3.5) to be ${max}_{i < | x |} x (i)$ for x as in (3.4). This implies that for Y and $N_{0}$ as in (3.5), we have $\begin{matrix} (3.6) & (\forall f^{1} ⩽_{1} 1) (Y (f) ⩽ max_{σ ⩽_{0^{}} 1 \land | σ | = N_{0}}) Y (σ * 00 \dots), \end{matrix}$ i.e. Y attains a standard maximum on Cantor space. In this light, consider the contraposition of (3.1) for some fixed $T ⩽_{1} 1$ , and assume $(\forall^{st} α^{1} ⩽_{1} 1) (\exists^{st} n^{0}) (\overline{α} n \notin T)$ . Applying ${HAC}_{int}$ yields a standard functional $Y_{0}^{1 \to 0^{}}$ such that $(\forall^{st} α^{1} ⩽_{1} 1) (\exists i \in Y_{0} (α)) (\overline{α} i \notin T)$ . Now define $Y_{1}^{2}$ by $Y_{1} (α) : = {max}_{i < | Y_{0} (α) |} Y_{0} (α) (i)$ and note that $(\forall^{st} α^{1} ⩽_{1} 1) (\exists n^{0} ⩽ Y_{1} (α)) (\overline{α} n \notin T)$ by definition. By the previous, $Y_{1}$ has a standard upper bound on Cantor space as in (3.6), yielding $(\exists^{st} k^{0}) (\forall β^{1} ⩽_{1} 1) (\exists i ⩽ k) (\overline{β} i \notin T)$ , and STP follows from Theorem 3.2. □

The following is a more direct proof of Theorem 3.3, not requiring Theorem 3.2.
Proof.
Working in $P + NUC$ , suppose there is some $g_{0} ⩽_{1} 1$ such that $(\forall^{st} f^{1} ⩽_{1} 1) (f ≉_{1} g_{0})$ . The latter implies $(\forall^{st} f^{1} ⩽_{1} 1) (\exists^{st} n^{0}) (\overline{f} n \neq \overline{g_{0}} n)$ , and applying ${HAC}_{int}$ yields standard* $Y_{0}^{1 \to 0^{}}$ such that $(\forall^{st} f^{1} ⩽_{1} 1) (\exists n^{0} \in Y_{0} (f)) (\overline{f} n \neq \overline{g_{0}} n)$ . Define standard $Y_{1}^{2}$ by $Y_{1} (f) : = {max}_{i < | Y_{0} (f) |} Y_{0} (f) (i)$ and note that $(\forall^{st} f^{1} ⩽_{1} 1) (\overline{f} Y_{1} (f) \neq \overline{g_{0}} Y_{1} (f))$ . By the above, $NUC \to (3.5)$ , which yields $(\forall^{st} Y^{2}) (\forall g^{1} ⩽_{1} 1) (\exists^{st} K^{0}) (Y (g) ⩽ K)$ by taking $K = Y (\overline{g} N_{0} 00 \dots)$ for $N_{0}$ as in (3.5). Note that $\overline{g} N_{0}$ is standard by [27], Cor. 2.19. Applying idealisation I, we obtain the formula $(\forall^{st} Y^{2}) (\exists^{st} k^{0^{}}) (\forall g^{1} ⩽_{1} 1) (\exists K^{0} \in k) (Y (g) ⩽ K)$ , and the maximum of k yields the existence of a standard upper bound for any standard $Y^{2}$ on Cantor space. In particular, $Y_{1}$ has a standard upper bound on Cantor space, say $m_{1}$ . Then define the sequence $g_{1}^{1}$ as $\overline{g_{0}} m_{1} 00 \dots$ , and note that $\overline{g_{0}} m_{1}$ is standard by [27], Cor. 2.19, and hence $g_{1}$ is also standard. By the definition of $Y_{1}$ , we have $\overline{g_{1}} Y_{1} (g_{1}) \neq \overline{g_{0}} Y_{1} (g_{1})$ , which yields a contradiction. □

As explained in the Introduction, the theme of this paper is the extraction of relative computability results from theorems of Nonstandard Analysis. We now provide the first example of this theme in Corollary 3.4, based on the proof of $NUC \to STP$ in the previous theorem. The following definitions are relevant. $\begin{array}{l} (MUC (Ω)) & (\forall Y^{2}) (\forall f^{1}, g^{1} ⩽_{1} 1) (\overline{f} Ω (Y) = \overline{g} Ω (Y) \to Y (f) = Y (g)), \\ (\forall g^{2}, T^{1} ⩽_{1} 1) \\ (SCF (Θ)) & [(\forall α^{1} \in Θ (g) (2)) (α ⩽_{1} 1 \to \overline{α} g (α) \notin T) \to (\forall β ⩽_{1} 1) (\exists i ⩽_{0} Θ (g) (1)) (\overline{β} i \notin T)] . \end{array}$ The functional $Ω^{3}$ as in $MUC (Ω)$ is the (intuitionistic) fan functional and yields a conservative extension of $WKL$ for the second-order language (see [13], Prop. 3.15). By Corollary 3.4, Θ as in $SCF (Θ)$ is a ‘special case’ of Ω and we refer to Θ as the special fan functional (although Θ is strictly speaking not unique).

The computational properties of Θ have been studied in [20] and are briefly sketched in Section 2.5. From a computability theoretic perspective, the main property of Θ is the selection of $Θ (g) (2)$ as a finite sequence of binary sequences $⟨ f_{0}, \dots, f_{n} ⟩$ such that the neighbourhoods defined from $\overline{f_{i}} g (f_{i})$ for $i ⩽ n$ form a cover of Cantor space; almost as a by-product, $Θ (g) (1)$ can then be chosen to be the maximal value of $g (f_{i}) + 1$ for $i ⩽ n$ . We stress that $g^{2}$ in $SCF (Θ)$ may be discontinuous and that Kohlenbach has argued for the study of discontinuous functionals in higher-order RM (see [13], Section 1). In the absence of discontinuous functionals, Θ behaves as follows.
Corollary 3.4.
From the proof in $P$ that $NUC \to STP$ , a term $t^{3 \to 3}$ can be extracted such that ${E-PA}^{ω } + {QF-AC}^{1, 0}$ proves* $(\forall Ω^{3}) [MUC (Ω) \to SCF (t (Ω))]$ .
Proof.
By the proof of the theorem, $NUC$ is equivalent to the normal form (3.5), which we abbreviate as $(\forall^{st} Y^{2}) (\exists^{st} N^{0}) A (Y, N)$ . The contraposition of (3.1) is $\begin{array}{l} (3.7) & (\forall T^{1} ⩽_{1} 1) [(\forall^{st} α ⩽_{1} 1) (\exists^{st} n^{0}) (\overline{α} n \notin T) \to (\exists^{st} k^{0}) (\forall β ⩽_{1} 1) (\exists i ⩽ k) (\overline{β} i \notin T)] . \end{array}$ Since standard functionals have standard output for standard input, (3.7) implies: $\begin{array}{l} (3.8) & (\forall T^{1} ⩽_{1} 1) (\forall^{st} g^{2}) [(\forall^{st} α ⩽_{1} 1) (\overline{α} g (α) \notin T) \to (\exists^{st} k^{0}) (\forall β ⩽_{1} 1) (\exists i ⩽ k) (\overline{β} i \notin T)] . \end{array}$ Pushing all standard quantifiers outside, we obtain that $\begin{matrix} (\forall^{st} g^{2}) (\forall T^{1} ⩽_{1} 1) (\exists^{st} k^{0}, α^{1} ⩽_{1} 1) [(\overline{α} g (α) \notin T) \to (\forall β ⩽_{1} 1) (\exists i ⩽ k) (\overline{β} i \notin T)] . \end{matrix}$ Applying idealisation $I$ , we pull the standard quantifiers to the front as follows: $\begin{array}{l} (3.9) & (\forall^{st} g^{2}) (\exists^{st} w^{1^{}}) (\forall T^{1} ⩽_{1} 1) (\exists (α^{1} ⩽_{1} 1, k^{0}) \in w) [(\overline{α} g (α) \notin T) \to (\forall β ⩽_{1} 1) (\exists i ⩽ k) (\overline{β} i \notin T)], \end{array}$ which we abbreviate as $(\forall^{st} g^{2}) (\exists^{st} w^{1^{}}) B (g, w)$ . Hence, the proof of $NUC \to STP$ yields a proof of $(\forall^{st} Y^{2}) (\exists^{st} N^{0}) A (Y, N) \to (\forall^{st} g^{2}) (\exists^{st} w^{1^{}}) B (g, w)$ , which yields $\begin{matrix} (3.10) & [(\exists^{st} Ω^{3}) (\forall Y^{2}) A (Y, Ω (Y)) \to (\forall^{st} g^{2}) (\exists^{st} w^{1^{}}) B (g, w)], \end{matrix}$ by strengthening the antecedent. Bringing all standard quantifiers up front: $\begin{matrix} (3.11) & (\forall^{st} Ω^{3}, g^{2}) (\exists^{st} w^{1^{}}) [(\forall Y^{2}) A (Y, Ω (Y)) \to B (g, w)] . \end{matrix}$ Applying Corollary 2.9 to ‘ $P ⊢ (3.11)$ ’, we obtain a term $t^{3 \to 3}$ such that $\begin{matrix} (3.12) & (\forall Ω^{3}, g^{2}) (\exists w \in t (Ω, g)) [(\forall Y^{2}) A (Y, Ω (Y)) \to B (g, w)] \end{matrix}$ is provable in ${E-PA}^{ω } + {QF-AC}^{1, 0}$ . Bringing all quantifiers inside again, (3.12) yields $\begin{matrix} (3.13) & (\forall Ω^{3}) [(\forall Y^{2}) A (Y, Ω (Y)) \to (\forall g^{2}) (\exists w \in t (Ω, g)) B (g, w)] . \end{matrix}$ Clearly, the antecedent of (3.13) expresses that $Ω^{3}$ is the fan functional. To define a functional Θ as in $SCF (Θ)$ from $t (Ω, g)$ , note that the latter is a finite sequence of numbers and binary sequences by (3.9); Using basic sequence coding, we may assume that $t (Ω, g) = t_{0} (Ω, g) * t_{1} (Ω, g)$ , where the first (resp. second) part contains the binary sequences (resp. numbers). Now define $Θ (g) (1)$ as ${max}_{i < | t_{1} (Ω, g) |} t_{1} (Ω, g) (i)$ and $Θ (g) (2) : = t_{0} (Ω, g)$ , and note that Θ indeed satisfies $SCF (Θ)$ . □

In the following remark, we discuss how the proof of Corollary 3.4 provides a template for the rest of the term extraction results in this paper. We will apply this template to another basic example in Section 3.1.2. Remark 3.5 (Template for term extraction).

Bring antecedent and consequent in normal form (see (3.5) and (3.9)).

Introduce a standard witnessing functional in the antecedent, and drop the remaining ‘st’ (see (3.10)).

Bring all standard quantifiers up front to obtain a normal form (see (3.11)). Use idealisation I when encountering ‘ $(\forall x) (\exists^{st} y)$ ’ (Irrelevant for Corollary 3.4).

Apply Corollary 2.9 to the proof in $P$ of the normal form to obtain a term t and a proof in ${E-PA}^{ω *}$ (see (3.12)).

Bring all quantifiers inside again to obtain the sought-after relative computability result (see (3.13)).

All further term extraction results follow this template, but often in less detail. It is interesting to note that the nonstandard definitions of e.g. continuity, Riemann integration, compactness, differentiability, etc., have normal forms in (fragments of)

P

; Furthermore, normal forms are ‘closed under modus ponens’ in the sense that an implication between two normal forms can be brought into a normal form too (As is done in items (ii) and (iii) above). Thus, the template seems to apply to any theorem which only involves nonstandard definitions. This is explored in the context of Reverse Mathematics and its ‘zoo’ in [22,23].

3.1.2. Nonstandard arithmetical comprehension

In this section, we apply the template from Remark 3.5 to another instructive example, involving the following fragment of Nelson’s axiom Transfer: $\begin{matrix} (Σ_{2}^{0} -TRANS) & (\forall^{st} f^{1}) [(\exists m^{0}) (\forall n^{0}) f (m, n) = 0 \to (\exists^{st} k^{0}) (\forall l^{0}) f (k, l) = 0] . \end{matrix}$ and the following nonstandard continuity principle: $\begin{matrix} (NPC) & (\forall^{st} Y^{2} \in C, f^{1}) (\forall g^{1}) (f \approx_{1} g \to Y (f) =_{0} Y (g)) . \end{matrix}$ By Corollary 3.7, $Σ_{2}^{0} -TRANS$ is a nonstandard ‘precursor’ to ${ACA}_{0}$ . We have the following theorem.

Theorem 3.6.
The system $P$ proves that $Σ_{2}^{0} -TRANS \to NPC$ .
Proof.
We make essential use of the proof of [12], Prop. 4.7. In the latter, it is shown that a continuous functional on Baire space has a modulus of continuity, assuming arithmetical comprehension. With our notations and for $Y^{2} \in C$ , the aforementioned proof amounts to weakening (1.1) to: $\begin{matrix} (3.14) & (\forall f^{1}) (\exists N^{0}) [(\forall τ^{0^{}}, σ^{0^{}}) (Y (\overline{f} N * σ * 00 \dots) =_{0} Y (\overline{f} N * τ * 00 \dots))], \end{matrix}$ and using arithmetical comprehension to obtain the characteristic function $χ^{2}$ of the formula in square brackets in (3.14). The latter then yields $(\forall f^{1}) (\exists N^{0}) (χ (f, N) = 1)$ , and ${QF-AC}^{1, 0}$ and quantifier-free induction are applied to the former to obtain $H^{2}$ such that $H (f)$ is the least such N. The functional $H^{2}$ is then shown to be the modulus of continuity for $Y^{2} \in C$ .

Applying $Σ_{2}^{0} -TRANS$ to (3.14) for standard $f^{1}$ and standard $Y^{2} \in C$ , yields: $\begin{matrix} (\forall^{st} f^{1}) (\exists^{st} N^{0}) [(\forall τ^{0^{}}, σ^{0^{}}) (Y (\overline{f} N * σ * 00 \dots) =_{0} Y (\overline{f} N * τ * 00 \dots))] . \end{matrix}$ Hence, by the leastness of $H (f)$ from the previous paragraph, the latter is standard for standard $f^{1}$ . Since H is a modulus of pointwise continuity, we thus obtain $\begin{matrix} (\forall^{st} f^{1}) (\exists^{st} N^{0}) (\forall g^{1}) (\overline{f} N =_{0} \overline{g} N \to Y (f) =_{0} Y (g)), \end{matrix}$ which immediately implies that $Y^{2}$ is nonstandard continuous, and $NPC$ follows. □

To apply term extraction to Theorem 3.6, the following principles are needed. $\begin{array}{l} (MPC (Ψ)) & (\forall Y^{2} \in C, f^{1}, g^{1}) (\overline{f} Ψ (Y, f) = \overline{g} Ψ (Y, f) \to Y (f) = Y (g)), \\ (MU (μ)) & (\forall f^{1}) [(\exists n^{0}) f (n) = 0 \to f (μ (f)) = 0] . \end{array}$ Note that $MPC (Ψ)$ states that $Ψ^{3}$ is a modulus-of-continuity functional, while $MU (μ)$ states that $μ^{2}$ is Feferman’s search operator (see e.g. [13] for the latter). One usually abbreviates ‘ $(\exists μ^{2}) MU (μ)$ ’ by $(μ^{2})$ , and the latter provides arithmetical comprehension in the sense of (3.24) below.
Corollary 3.7.
From the proof in $P$ that $Σ_{2}^{0} -TRANS \to NPC$ , a term t can be extracted such that ${E-PA}^{ω } + {QF-AC}^{1, 0}$ proves* $(\forall μ^{2}) [MU (μ) \to MPC (t (μ))]$ .
Proof.
First of all, a normal form for $Σ_{2}^{0} -TRANS$ is: $\begin{matrix} (3.15) & (\forall^{st} f^{1}) (\exists^{st} k^{0}) [(\exists m^{0}) (\forall n^{0}) f (m, n) = 0 \to (\exists i ⩽ k) (\forall l) f (i, l) = 0], \end{matrix}$ where $A (f, k)$ is the internal formula in square brackets. A normal form for $NPC$ is $\begin{matrix} (3.16) & (\forall^{st} Y^{2} \in C, f^{1}) (\exists^{st} N_{0}^{0}) [(\forall g^{1}) (\overline{f} N_{0} =_{0} \overline{g} N_{0} \to Y (f) =_{0} Y (g))], \end{matrix}$ which can be obtained in exactly the same way that (3.5) is derived from NUC . Let $B (Y, f, N_{0})$ be the formula in square brackets in (3.16). The implication $Σ_{2}^{0} -TRANS \to NPC$ thus implies $\begin{matrix} (3.17) & (\forall^{st} f^{1}) (\exists^{st} k^{0}) A (f, n) \to (\forall^{st} Y^{2} \in C, g^{1}) (\exists^{st} N_{0}^{0}) B (Y, g, N_{0}) . \end{matrix}$ As standard functionals yield standard outputs for standard inputs, we may strengthen the antecedent of (3.17) as follows: $\begin{matrix} (3.18) & (\forall^{st} ν^{2}) [(\forall^{st} f^{1}) A (f, ν (f)) \to (\forall^{st} Y^{2} \in C, g^{1}) (\exists^{st} N_{0}^{0}) B (Y, g, N_{0})] . \end{matrix}$ We may also strengthen the antecedent by dropping the ‘st’ to obtain $\begin{matrix} (3.19) & (\forall^{st} ν^{2}) [(\forall f^{1}) A (f, ν (f)) \to (\forall^{st} Y^{2} \in C, g^{1}) (\exists^{st} N_{0}^{0}) B (Y, g, N_{0})] . \end{matrix}$ Brining all standard quantifiers to the front, we obtain the normal form $\begin{matrix} (3.20) & (\forall^{st} ν^{2}, Y^{2} \in C, g^{1}) (\exists^{st} N_{0}^{0}) [(\forall f^{1}) A (f, ν (f)) \to B (Y, g, N_{0})] . \end{matrix}$ Apply Corollary 2.9 to ‘ $P ⊢ (3.20)$ ’ to obtain a term t s.t. ${E-PA}^{ω } + {QF-AC}^{1, 0}$ proves $\begin{matrix} (3.21) & (\forall ν^{2}, Y^{2} \in C, g^{1}) (\exists N_{0}^{0} \in t (ν, Y, g)) [(\forall f^{1}) A (f, ν (f)) \to B (Y, g, N_{0})] . \end{matrix}$ Now define the term s by $s (ν, Y, g) : = {max}_{i < | t (ν, Y, g) |} t (ν, Y, g) (i)$ and note that $\begin{matrix} (3.22) & (\forall ν^{2}, Y^{2} \in C, g^{1}) [(\forall f^{1}) A (f, ν (f)) \to B (Y, g, s (ν, Y, g))] . \end{matrix}$ Bringing all quantifiers inside again, we obtain that $\begin{matrix} (3.23) & (\forall ν^{2}) [(\forall f^{1}) A (f, ν (f)) \to (\forall Y^{2} \in C, g^{1}) B (Y, g, s (ν, Y, g))], \end{matrix}$ where the consequent is clearly $MPC (u (ν))$ for $u (ν) (Y, g) : = s (ν, Y, g)$ .

Finally, it is easy to define ν as in $(\forall f^{1}) A (f, ν (f))$ from (3.23) explicitly in terms of $μ^{2}$ as in $MU (μ)$ ; Indeed, for such $μ^{2}$ we have: $\begin{matrix} (3.24) & (\forall h^{1}) [(\forall k^{0}) (h (k) \neq 0) \leftrightarrow h (μ (h)) \neq 0], \end{matrix}$ i.e. $μ^{2}$ as in $MU (μ)$ allows us to decide universal formulas. Thus, $(\exists m^{0}) (\forall n^{0}) f (m, n) = 0$ is equivalent to $(\exists m^{0}) f (m, μ ((λ n) \tilde{f} (m, n))) = 0$ , where for $\tilde{k}$ is defined as $\begin{matrix} \tilde{k} (n) : = \{\begin{matrix} 1 & k (n) = 0 \\ 0 & otherwise . \end{matrix} \end{matrix}$ Applying the definition of $μ^{2}$ to $(\exists m^{0}) f (m, μ ((λ n) \tilde{f} (m, n))) = 0$ , we observe that $(\exists m^{0}) (\forall n^{0}) f (m, n) = 0$ yields $(\forall n^{0}) f (μ ((λ m) μ ((λ n) \tilde{f} (m, n))), n) = 0$ , and $ν (f) : = (λ f) μ ((λ m) μ ((λ n) \tilde{f} (m, n)))$ is as required for $(\forall f^{1}) A (f, ν (f))$ , and we are done. □

As is clear from the last part of the proof, $Σ_{2}^{0} -TRANS$ is the nonstandard precursor of the search functional: $\begin{matrix} ({MU}_{2} (ν)) & (\forall f^{1}) [(\exists m^{0}) (\forall n^{0}) f (m, n) = 0 \to (\forall l^{0}) f (ν (f), l) = 0], \end{matrix}$ but by the previous proof, two applications of Feferman’s search operator μ yields ν as in ${MU}_{2} (ν)$ . We refer to the latter as ‘Feferman’s second* search functional’, which will be needed in Section 4.3.
3.1.3. A ‘computable’ fragment of the standard part principle

In this section, we discuss the Standard Part principle $Ω -CA$ , a very practical consequence of ${HAC}_{int}$ . Intuitively speaking, $Ω -CA$ expresses that we can obtain the standard part (in casu G) of Ω-invariant nonstandard objects (in casu $F (\cdot, M)$ ), defined as follows.

Definition 3.8 (Ω-invariance).

Let $F^{(σ \times 0) \to 0}$ be standard and fix $M^{0} \in Ω$ . Then $F (\cdot, M)$ is Ω-invariant if $\begin{matrix} (3.25) & (\forall^{st} x^{σ}) (\forall N^{0} \in Ω) [F (x, M) =_{0} F (x, N)] . \end{matrix}$

Principle 3.9 (Ω-CA).

Let $F^{(σ \times 0) \to 0}$ be standard and fix $M \in Ω$ . For Ω-invariant $F (\cdot, M)$ , there is standard $G^{σ \to 0}$ such that $\begin{matrix} (3.26) & (\forall^{st} x^{σ}) (\forall N^{0} \in Ω) [G (x) =_{0} F (x, N)] . \end{matrix}$

In line with $STP$ , we also refer to $G (\cdot)$ as ‘a standard part of $F (\cdot, N)$ ’. Intuitively speaking, Ω-CA provides a standard part for a nonstandard object, if the latter is independent of the choice of nonstandard number used in its definition.

Theorem 3.10.
The system $P$ proves $Ω - CA$ .
Proof.
Assume $F (\cdot, M^{0})$ is Ω-invariant, i.e. we have $\begin{matrix} (3.27) & (\forall^{st} x^{σ}) (\forall N^{0}, M^{0} \in Ω) [F (x, M) =_{0} F (x, N)], \end{matrix}$ and underspill (see Theorem 3.1) implies that $\begin{matrix} (3.28) & (\forall^{st} x^{σ}) (\exists^{st} k^{0}) (\forall N^{0}, M^{0} ⩾ k) [F (x, M) =_{0} F (x, N)] . \end{matrix}$ Now apply ${HAC}_{int}$ to (3.28) to obtain standard $Φ^{σ \to 0^{*}}$ such that $\begin{matrix} (\forall^{st} x^{σ}) (\exists k^{0} \in Φ (x)) (\forall N^{0}, M^{0} ⩾ k) [F (x, M) =_{0} F (x, N)] . \end{matrix}$ Define standard $Ψ (x) : = {max}_{i < | Φ (x) |} Φ (x) (i)$ and note that $\begin{matrix} (3.29) & (\forall^{st} x^{σ}) (\forall N^{0}, M^{0} ⩾ Ψ (x)) [F (x, M) =_{0} F (x, N)] . \end{matrix}$ Finally, define $G (x) : = F (x, Ψ (x))$ and note that the latter is as in $Ω -CA$ . □

We finish this section with two remarks on the above results. Remark 3.11 (Extensions of $Ω -CA$ ).

It is straightforward to verify that Theorem 3.10 also holds if the quantifier ‘ $(\forall^{st} x^{σ})$ ’ in (3.25) and (3.26) is restricted as in ‘ $(\forall^{st} x^{σ}) (C (x) \to \dots)$ ’, where C is any internal formula. We shall also refer to this slight extension as $Ω -CA$ . The axiom $Ω -CA$ can also be generalised to $F^{(σ \times 0) \to τ}$ using the approximate equality ‘ $\approx_{τ}$ ’ defined in Remark 2.11. However, the above version suffices for our purposes.

Remark 3.12 (Using ${HAC}_{int}$ and $I$ ).

The axiom ${HAC}_{int}$ produces a functional of type $σ \to τ^{*}$ which outputs a finite sequence of witnesses. Now, in the proof of Theorem 3.10, ${HAC}_{int}$ is applied to (3.28) to obtain $Φ^{σ \to 0^{*}}$ , and from the latter, the functional $Ψ^{σ \to 0}$ is defined as follows: $Ψ (x) : = {max}_{i < | Φ (x) |} Φ (x) (i)$ . In particular, Ψ satisfies (3.29), and provides a witnessing functional, due to the ‘monotone’ nature of the internal formula in (3.28). In general, ${HAC}_{int}$ provides a witnessing functional assuming (i) $τ = 0$ in ${HAC}_{int}$ and (ii) the formula φ from ${HAC}_{int}$ is ‘sufficiently monotone’ as in: $(\forall x^{σ}, n^{0}, m^{0}) ([n ⩽_{0} m \land φ (n, x)] \to φ (m, x))$ .

A similar observation applies to idealisation I; Indeed, consider (3.3) and note that the internal formula in the latter is monotone as above. Taking the maximum of x from (3.4) as $N_{0} : = {max}_{i < | x |} x (i)$ , one can drop the quantifier $(\exists N \in x)$ in (3.4) to obtain (3.5). To save space in proofs, we will sometimes skip the (obvious) step involving the maximum of the finite sequences, when applying ${HAC}_{int}$ and $I$ .

3.2. External bar induction

In this section, we derive various versions of bar induction inside extensions of $P$ studied in the previous section. Now, bar induction can be viewed as ‘induction down a tree’, and we consider the following example.

Principle 3.13 ( ${BI}_{0}$ ).

For internal quantifier-free $Q (x^{0})$ , if $\begin{matrix} (3.30) & (\forall α^{1}) (\exists n^{0}) Q (\overline{α} n) \land (\forall t^{0}) [(\forall x^{0}) Q (t * ⟨ x ⟩) \to Q (t)] \end{matrix}$ then we have $Q (⟨ \cdot ⟩)$ .

Intuitively speaking, bar induction ${BI}_{0}$ expresses that we may conclude $Q (x)$ for $x = ⟨ \cdot ⟩$ from the fact that Q is implied ‘downwards’ from child nodes to parent nodes (second conjunct of (3.30)) and that Q holds eventually along any path (first conjunct of (3.30)). On a technical note, ${BI}_{0}$ is essentially ${BI}_{qf}$ from [26, p. 78] for $P (n) \equiv Q (n)$ quantifier-free. We now prove ${BI}_{0}^{st}$ form STP .

Theorem 3.14.
In $P + STP$ , we have ${BI}_{0}^{st}$ .
Proof.
Assume (3.30)^st and suppose we have $\neg Q (⟨ \cdot ⟩)$ . Now define $F (x, M) : = (μ m ⩽ M) \neg Q (x * ⟨ m ⟩)$ and put $G (0) : = F (⟨ \cdot ⟩, M)$ and $G (n + 1) : = F (G (0) * \dots * G (n), M)$ . By (3.30)^st for $t = ⟨ \cdot ⟩$ and the assumption $\neg Q (⟨ \cdot ⟩)$ , $G (0)$ is standard. Furthermore, we also have that $G (n + 1)$ is standard if $G (k)$ is standard, for standard n and $k ⩽ n$ , by (3.30)^st for $t = G (0) * \dots * G (n)$ . Hence, $G (n)$ is standard for all standard n by external induction IA^st. This in turn implies that $\neg Q (G (0) * \dots * G (k))$ for standard k, by quantifier-free induction and (3.30)^st. Now consider the sequence $β^{1} = G (0) * G (1) * G (2) * \dots$ and let $γ^{1}$ be its standard part via $STP$ . Finally, apply (3.30)^st for $α = γ$ to obtain a contradiction. □

The theorem is not that surprising: STP is the nonstandard version of $WKL$ by Theorem 3.2, the latter lemma is equivalent to a version of dependent choice (see [24, VIII.2.5]), and bar induction is a version of the latter.

Nonstandard Analysis also has a ‘distinct’ kind of induction, called external induction, as follows:
Principle 3.15 (ExInd).

For standard $F^{(0 \times 0) \to 0}$ and $M \in Ω$ , if $\begin{matrix} (3.31) & st (F (0, M)) \land (\forall^{st} n) [st (F (n, M)) \to st (F (n + 1, M))], \end{matrix}$ then $(\forall^{st} n) (st (F (n, M)))$ .

Intuitively speaking, (ExInd) tells us that we may use induction on the new standardness predicate along the standard numbers (and obviously not along all the numbers). Although seemingly more general than normal induction, we now derive (ExInd) from the standardness of the recursor constants in $P$ . We consider this theorem as its proof is similar to the proof of Theorem 3.18.

Theorem 3.16.
The system $P ∖ {{IA}^{st}}$ proves (ExInd).
Proof.
Consider (3.31) and replace ‘st’ as follows: $\begin{matrix} (\forall^{st} n) [(\exists^{st} k^{0}) (F (n, M) ⩽ k) \to (\exists^{st} l^{0}) (F (n + 1, M) ⩽ l)] . \end{matrix}$ Now bring all standard quantifiers outside to obtain: $\begin{matrix} (3.32) & (\forall^{st} n, k) (\exists^{st} l) [F (n, M) ⩽ k \to F (n + 1, M) ⩽ l] . \end{matrix}$ Recall Remark 3.12 and apply ${HAC}_{int}$ to (3.32) to obtain standard $g^{1}$ such that $\begin{matrix} (\forall^{st} n, k) [F (n, M) ⩽ k \to F (n + 1, M) ⩽ g (n, k)] . \end{matrix}$ Now use primitive recursion to define the standard function $h^{1}$ such that $h (0) : = F (0, M)$ and $h (k + 1) : = g (k, h (k))$ . By the definition of h, we have $F (n, M) ⩽ h (n)$ for standard n, proved by quantifier-free induction (of the non-external variety). As $h (n)$ is standard for standard n, (3.31) implies the consequent of (ExInd). □

Note that the same proof goes through for variations of (ExInd), e.g. if the induction hypothesis involves $(\forall k ⩽ n) (st (F (k, M)))$ instead of $st (F (n, M))$ . Note that (ExInd) also follows directly from ${IA}^{st}$ , but the latter cannot be included in fragments of $P$ based on ${E-PRA}^{ω}$ (see [13], Section 2).

We now formulate external bar induction, which is bar induction on the (external) standardness predicate.
Principle 3.17 (EBI).

For standard $F^{(0 \times 0) \to 0}$ and $M \in Ω$ , if $\begin{array}{l} (3.33) & (\forall^{st} α^{1}) (\exists^{st} n^{0}) [st (F (\overline{α} n, M))] \\ (3.34) & \land (\forall^{st} t^{0}) [(\forall^{st} x^{0}) (st (F (t * ⟨ x ⟩, M))) \to st (F (t, M))] \end{array}$ then $st (F (⟨ \cdot ⟩, M))$ .

Finally, we prove external bar induction from $STP$ and the following fragment of Nelson’s axiom Transfer: $\begin{matrix} (Π_{1}^{0} - TRANS) & (\forall^{st} f^{1}) [(\forall^{st} n^{0}) f (n) \neq 0 \to (\forall m^{0}) f (m) \neq 0] . \end{matrix}$

Theorem 3.18.
The system $P + STP + Π_{1}^{0} - TRANS$ proves EBI .
Proof.
First of all, we use $Π_{1}^{0} - TRANS$ to obtain standard $μ^{2}$ such that ${[MU (μ)]}^{st}$ . To this end, define $ν^{2}$ as follows: $\begin{matrix} ν (f, N) : = \{\begin{matrix} (μ n ⩽ N) f (n) = 0 & (\exists n ⩽ N) (f (n) = 0) \\ 0 & otherwise . \end{matrix} \end{matrix}$ Assuming $Π_{1}^{0} - TRANS$ , we have $(\forall^{st} f^{1}) (\forall N, M \in Ω) (ν (f, M) =_{0} ν (f, N))$ , i.e. $ν (\cdot, N)$ is Ω-invariant. Now let $μ^{2}$ be the standard part of $ν (\cdot, N)$ provided by $Ω -CA$ , and note that ${[MU (μ)]}^{st}$ , i.e. $μ^{2}$ is Feferman’s search operator relative to ‘st’.

Secondly, consider (3.34), and bring the latter in the form: $\begin{matrix} (3.35) & (\forall^{st} t^{0}) (\exists^{st} x^{0}, m^{0}) (\forall^{st} l^{0}) [F (t * ⟨ x ⟩, M) ⩽ l \to F (t, M) ⩽ m] . \end{matrix}$ Let $f^{1} ⩽_{1} 1$ be the characteristic function of the formula in square brackets in (3.35), and let standard $h^{1} ⩽_{1} 1$ be the standard part of $f^{1}$ as provided by $STP$ . Hence, (3.35) implies that $\begin{matrix} (3.36) & (\forall^{st} t^{0}) (\exists^{st} x^{0}, m^{0}) (\forall^{st} l^{0}) (h (t, x, m, l) = 1) . \end{matrix}$ Similar to the proof of Corollary 3.7, $μ^{2}$ from ${[MU (μ)]}^{st}$ can be used to define a standard characteristic function $χ^{1}$ for $(\forall^{st} l^{0}) (h (t, x, m, l) = 1)$ from (3.36), i.e. $\begin{matrix} (\forall^{st} x, m, l) [(\forall^{st} l^{0}) (h (t, x, m, l) = 1) \leftrightarrow χ (x, m, l) = 1] . \end{matrix}$ Applying $μ^{2}$ as in ${[MU (μ)]}^{st}$ to $(\forall^{st} t^{0}) (\exists^{st} x^{0}, m^{0}) (χ (x, m, l) = 1)$ then yields standard $g^{1}$ such that $(\forall^{st} t^{0}) (\forall^{st} l^{0}) (h (t, g (t) (1), g (t) (2), l) = 1)$ , which implies: $\begin{matrix} (3.37) & (\forall^{st} t^{0}, l^{0}) [F (t * ⟨ g (t) (1) ⟩, M) ⩽ l \to F (t, M) ⩽ g (t) (2)] . \end{matrix}$ Finally, we derive EBI using g from (3.37). Thus, assume (3.33) and (3.34) and consider the standard $α^{1}$ defined by $α (0) : = g (⟨ \cdot ⟩) (1)$ and $α (n + 1) : = g (\overline{α} n) (1)$ . By (3.33), there is standard n such that $F (\overline{α} n, M)$ is standard. However, then there is standard l such that $F (\overline{α} n, M) = F (\overline{α} (n - 1) * ⟨ g (\overline{α} (n - 1)) (1) ⟩, M)$ satisfies the antecedent of (3.37) for $t = \overline{α} (n - 1)$ . Hence, $F (\overline{α} (n - 1), M)$ is also standard by (3.37), as the latter yields $F (\overline{α} (n - 1), M) ⩽ g (\overline{α} (n - 1)) (2)$ . Applying (3.37) for $t = \overline{α} (n - 2)$ and $l = g (\overline{α} (n - 1)) (2)$ , we obtain $F (\overline{α} (n - 2), M) ⩽ g (\overline{α} (n - 2)) (2)$ . Applying the same procedure at most n times, we obtain $F (⟨ \cdot ⟩, M) ⩽ g (⟨ \cdot ⟩) (2)$ , i.e. $F (⟨ \cdot ⟩, M)$ is standard, and EBI follows. □

4. The Gandy–Hyland functional in Nonstandard Analysis

4.1. Introduction

In this section, we prove our main results concerning the Gandy–Hyland functional Γ from ( GH ) and its so-called canonical approximation G, defined as follows: $\begin{matrix} (4.1) & G (Y, s, M) = \{\begin{matrix} Y (s * 00 \dots) & | s | ⩾ M \\ Y (s * 0 * (λ n) G (Y, s * (n + 1), M)) & otherwise . \end{matrix} \end{matrix}$ As to its provenance, we recall that the Γ-functional was introduced in [10] as an example of a functional not Kleene-S1-S9-computable over the total continuous functionals, even with the fan functional as an oracle (see [17, Section 4] or [15], Section 8). By contrast, G is primitive recursive, as discussed in Section 2.2.

Using the results from the previous section, we prove in Section 4.2 that the Gandy–Hyland functional $Γ (\cdot)$ equals $G (\cdot, M)$ for all standard inputs and nonstandard M; This proof takes place in an extension of the system $P$ from Section 2.3. From this nonstandard proof, we extract a term from Gödel’s T expressing Γ in terms of the special fan functional (see Corollary 3.4) and a modulus-of-continuity functional. This final result does not involve Nonstandard Analysis.

In Section 4.4 to 4.6, we obtain similar nonstandard theorems, from which we extract the associated relative computability results. In particular, in Sections 4.4 and 4.5, we prove ‘pointwise’ versions of the above results, not involving a modulus-of-continuity functional. We introduce the well-known notion of associate of a continuous functional in Section 4.6, and use it to obtain particularly elegant results. In our opinion, the aforementioned variations of the main result establish the robustness of our approach.

Finally, we show in Section 4.3 that one can re-obtain the original nonstandard theorem (that the Gandy–Hyland functional $Γ (\cdot)$ equals $G (\cdot, M)$ for all standard inputs and nonstandard M) from the proof of a certain natural relative computability result, called the Herbrandisation of the original nonstandard theorem. In this way, the latter is seen to have the same computational content as its Herbrandisation. Based on the results in Section 4.3, one can easily obtain the Herbrandisation for any nonstandard theorem in this paper. The observed connection between a nonstandard theorem and its ‘highly constructive’ Herbrandisation, provides us with a two-way street between the fields Nonstandard Analysis and Computability.

4.2. From Nonstandard Analysis to relative computability

In this section, we prove that the functionals $G (\cdot, M)$ and $Γ (\cdot)$ are equal for standard inputs and nonstandard $M^{0}$ , inside an extension of $P$ . From this proof, we extract a term from Gödel’s system $T$ which computes Γ in terms of a modulus-of-continuity functional and the special fan functional (see Corollary 3.4).

As noted in the first section, the Γ-functional corresponds to modified bar recursion of type 0 (see [4, Section 4]). Since bar recursion holds in the model of all total continuous functionals (see [3,7]), the easiest way of obtaining Γ from G seems to be adding the continuity axiom $NPC$ to $P$ , which was defined above as: $\begin{matrix} (NPC) & (\forall^{st} Y^{2} \in C, f^{1}) (\forall g^{1}) (f \approx_{1} g \to Y (f) =_{0} Y (g)), \end{matrix}$ where ‘ $Y^{2} \in C$ ’ is the (internal) definition of continuity as in (1.1). As discussed in Remark 4.6, NPC without the restriction ‘ $Y^{2} \in C$ ’ is inconsistent, while NPC easily5

⁵
Fix a standard $Y^{2}$ and standard $f^{1}$ in (1.1), and apply (the contraposition of) Transfer.

follows from the

IST

axiom Transfer (see Theorem 3.6).

Furthermore, according to [4, p. 167], the role of the continuity principle and bar induction in [4, Theorem 2.5] is to verify the correctness of the [bar recursive] witnessing functional. As was proved in Section 3.2, the principles STP and $Σ_{2}^{0} -TRANS$ from Section 3.1 yield a version of bar induction and a nonstandard continuity principle $NPC$ . Hence, we arrive at the following theorem.

Theorem 4.1.

In $P$ + Σ 2 0 -TRANS + STP , we have $\begin{matrix} (4.2) & (\forall^{st} Y^{2} \in C, s^{0}) (\forall M, N \in Ω) (G (Y, s, N) =_{0} G (Y, s, M)), \end{matrix}$ i.e. the canonical approximation of Γ is Ω-invariant.

Proof.

We sketch the proof of the theorem and then provide a detailed version.

First of all, EBI and nonstandard continuity $NPC$ may be used in light of Theorem 3.6 and Theorem 3.18. Secondly, one uses this bar induction to prove that $G (Y, s, M)$ is standard for standard $Y^{2} \in C, s^{0}$ and nonstandard $M^{0}$ . Thirdly, one applies bar induction again to prove that (4.2) holds for fixed inputs. In both cases, nonstandard continuity is used to establish (3.33) and (3.34) in external bar induction. We now provide a detailed proof.

We first prove that $G (\cdot, M)$ is standard for standard input and nonstandard M using EBI. To this end, fix standard $Y^{2} \in C, s^{0}$ and $M \in Ω$ , and define $F (x^{0}, M) : = G (Y, s * x, M)$ . To prove (3.33), fix standard $γ^{1}$ and $N \in Ω$ . We have $\begin{array}{l} F (\overline{γ} N, M) & = G (Y, s * \overline{γ} N, M) \\ (4.3) & = Y (s * \overline{γ} N * 0 * (λ n) G (Y, s * \overline{γ} N * (n + 1), M)) \\ (4.4) & = Y (s * γ), \end{array}$ where the final step follows by nonstandard continuity NPC as $s * γ \approx_{1} ζ$ , where the latter is the sequence in (4.3). We have proved that $(\forall K \in Ω) F (\overline{γ} K) = Y (s * γ)$ and underspill yields $(\exists^{st} k^{0}) (\forall K ⩾ k) F (\overline{γ} K) = Y (s * γ)$ , from which it is immediate that $(\forall^{st} γ^{1}) (\exists^{st} m) (\forall n ⩾ m) (st (F (\overline{γ} n, M)))$ , and hence (3.33).

To prove (3.34), assume the antecedent of the latter for standard t, and consider $\begin{array}{l} F (t, M) & = G (Y, s * t, M) \\ = Y (s * t * 0 * (λ n) G (Y, s * t * (n + 1), M)) \\ (4.5) & = Y (s * t * 0 * (λ n) F (t * (n + 1), M)) \end{array}$ which follows by the definitions of F and G. However, the antecedent of (3.34) tells us that $F (t * ⟨ m ⟩, M)$ is standard for standard m. Hence, the sequence $\begin{matrix} (4.6) & s * t * 0 * F (t * 1, M) * F (t * 2, M) * F (t * 3, M) * \dots \end{matrix}$ has a standard part by STP , say $γ^{1}$ , and NPC yields $F (t, M) = Y (γ)$ , which is standard. Hence, we obtain (3.34), and $F (⟨ \cdot ⟩, M) = G (Y, s, M)$ is standard by $EBI$ , for any standard $Y^{2} \in C$ and standard $s^{0}$ .

Secondly, we prove (4.2) using the previous part of the proof and EBI. Thus, define the function $F (x, M)$ as: $\begin{matrix} (4.7) & F (x, M) : = \{\begin{matrix} 0 & G (Y, s * x, M) = G (Y, s * x, M + 1) \\ M & otherwise, \end{matrix} \end{matrix}$ where $Y^{2} \in C$ and $s^{0}$ are standard again. Repeating the steps from the previous paragraph of the proof, we note that $F (\cdot, M)$ satisfies (3.33) and (3.34) for any $M \in Ω$ . Hence, EBI yields that $F (⟨ \cdot ⟩, M)$ is standard for any nonstandard M; As a consequence, we have $G (Y, s, M) = G (Y, s, M + 1)$ by definition, for any nonstandard M. Hence, (4.2) is proved, and we are done. □

Remark 4.2 (The essential use of

EBI

On a side-note, it seems that $EBI$ is essential for the first part of the above proof, but not for the second part: (4.2) follows from applying ${BI}_{0}^{st}$ for $Q (x) \equiv [G (Y, s * x, M) = G (Y, s * x, M + 1)]$ , assuming that $G (Y, s, M)$ is standard for standard $Y^{2} \in C, s^{0}$ and nonstandard M, as was proved in the first part of the above proof using EBI however.

The Gandy–Hyland is unique as noted in [10], Section 6 and [15], Section 8.3.3. We prove a similar result, for which we require: $\begin{matrix} ({GH}_{st} (Γ)) & (\forall^{st} Y^{2} \in C, s^{0}) [Γ (Y^{2}, s^{0}) = Y (s * 0 * (λ n^{0}) Γ (Y, s * (n + 1)))] . \end{matrix}$ The corollary expresses that the standard and unique Gandy–Hyland functional equals its canonical approximation.

Corollary 4.3.
In $P + Σ_{2}^{0} -TRANS + STP$ , the Gandy–Hyland functional exists and equals its canonical approximation, i.e. there is standard $Γ^{3}$ such that ${GH}_{st} (Γ)$ and $\begin{matrix} (CA (Γ)) & (\forall^{st} Y^{2} \in C, s^{0}) (\forall N \in Ω) (G (Y, s, N) = Γ (Y, s)) . \end{matrix}$ Furthermore, the Gandy–Hyland functional is unique, i.e. $(\forall Γ_{1}^{3}) ({GH}_{st} (Γ_{1}) \to CA (Γ_{1}))$ .
Proof.
By (4.2), $G (Y, s, M)$ is Ω-invariant, and $Ω -CA$ and Remark 3.11 yield the standard part of $G (Y, s, M)$ , say $Γ_{0} (Y, s)$ . For standard $Y^{2} \in C, s^{0}$ and $M \in Ω$ , we have that: $\begin{array}{l} Γ_{0} (Y, s) = G (Y, s, M) & = Y (s * 0 * G (Y, s * 1, M) * G (Y, s * 2, M) * \dots) \\ (4.8) & = Y (s * 0 * Γ_{0} (Y, s * 1) * Γ_{0} (Y, s * 2) * \dots), \end{array}$ where we used NPC in the final step. Hence, the standard part $Γ_{0} (\cdot)$ of $G (\cdot, M)$ as provided by $Ω -CA$ is indeed the Gandy–Hyland functional as ${GH}_{st} (Γ_{0})$ follows from (4.8). To prove the uniqueness as in the corollary, suppose there is another $Γ_{1}$ such that ${GH}_{st} (Γ_{1})$ and define $F (x, M)$ as in (4.7), but with $G (Y, s * x, M + 1)$ replaced by $Γ_{1} (Y, s * x)$ . Now proceed as in the proof of the theorem to establish that this modified version of (4.7) satisfies (3.33) and (3.34). From EBI, we obtain that $st (F (⟨ \cdot ⟩, M))$ , implying that $G (Y, s, M) = Γ_{1} (Y, s)$ . The latter thus holds for standard $Y^{2} \in C, s^{0}$ and $M \in Ω$ , and $CA (Γ_{1})$ follows. □

As noted above, the Gandy–Hyland functional is not computable (in the sense of Kleene’s S1-S9) in terms of the fan functional over the total continuous functionals. The following corollaries express that the Gandy–Hyland functional may be computed via a term in Gödel’s $T$ from a modulus-of-continuity functional. We require the following: $\begin{matrix} (GH (Γ)) & (\forall Y^{2} \in C, s^{0}) [Γ (Y^{2}, s^{0}) = Y (s * 0 * (λ n^{0}) Γ (Y, s * (n + 1)))] . \end{matrix}$ Variations of the following relative computability result are discussed below.
Corollary 4.4 (Term Extraction I).

From the proof in $P$ of $\begin{matrix} (4.9) & Σ_{2}^{0} -TRANS + STP \to (\forall Γ^{3}) [{GH}_{st} (Γ) \to CA (Γ)], \end{matrix}$ a term $t^{4}$ can be extracted such that ${E-PA}^{ω *} + {QF-AC}^{1, 0}$ proves that $\begin{array}{l} (4.10) & (\forall μ^{2}, Θ^{3}, Γ^{3}) [(GH (Γ) \land MU (μ) \land SCF (Θ)) \to (\forall Y^{2} \in C, s^{0}) (G (Y, s, t (Y, s, μ, Θ)) = Γ (Y, s))], \end{array}$ i.e. $G (Y, s, t (Y, s, μ, Θ))$ is the Gandy–Hyland functional expressed in terms of Feferman’s search operator and Θ.

Proof.
The following formula is provable in $P$ by Corollary 4.3: $\begin{matrix} (4.11) & (\forall Γ^{3}) [[{GH}_{st} (Γ) \land STP \land Σ_{2}^{0} -TRANS] \to CA (Γ)] . \end{matrix}$ We apply Remark 3.5: Bring all the components of (4.11) in normal form. Note that a normal form of $Σ_{2}^{0} -TRANS$ is given as (3.15); Let $A (f, n)$ be the internal formula in square brackets in the latter.

Secondly, let $(\forall^{st} g^{2}) (\exists^{st} w^{1^{}}) B (g, w)$ be the normal form (3.9) of $STP$ formulated in the proof of Corollary 3.4. Thirdly, Corollary 4.3 combined with underspill implies that for all Γ such that ${GH}_{st} (Γ)$ we have $\begin{matrix} (4.12) & (\forall^{st} Y^{2} \in C, s^{0}) (\exists^{st} K) [(\forall N ⩾ K) (G (Y, s, N) =_{0} Γ (Y, s))], \end{matrix}$ and let $C (Y, s, K, Γ)$ be the formula in square brackets in (4.12). Then (4.11) implies that for all Γ, we have $\begin{array}{l} [(\forall^{st} f^{1}) (\exists^{st} N^{0}) A (f, N) \land (\forall^{st} W^{2}) (\exists^{st} w^{1^{}}) B (W, w) \land {GH}_{st} (Γ)] \\ (4.13) & \to (\forall^{st} Z^{2} \in C, s) (\exists^{st} N) C (Z, s, N, Γ) . \end{array}$ Hence, for all Γ and all standard $Θ, Ψ$ , we have $\begin{array}{l} (4.14) & [(\forall^{st} f^{1}) A (f, Ψ (f)) \land (\forall^{st} W^{2}) B (W, Θ (W)) \land {GH}_{st} (Γ)] \to (\forall^{st} Z^{2} \in C, s) (\exists^{st} N) C (Z, s, N, Γ), \end{array}$ as standard functionals have standard outputs for standard inputs. Strengthening the antecedent of (4.14) to internal formulas, we have for Γ and standard $Θ, Ψ$ that $\begin{array}{l} (4.15) & [(\forall f^{1}) A (f, Ψ (f)) \land (\forall W^{2}) B (W, Θ (W)) \land GH (Γ)] \to (\forall^{st} Z^{2} \in C, s) (\exists^{st} N) C (Z, s, N, Γ) . \end{array}$ Bringing outside all standard quantifiers, (4.15) implies: $\begin{array}{l} (\forall^{st} Θ, Ψ, Z \in C, s) (\forall Γ) (\exists^{st} N^{0}) \\ (4.16) & [((\forall f) A (f, Ψ (f)) \land (\forall W^{2}) B (W, Θ (W)) \land GH (Γ)) \to C (Z, s, N, Γ)], \end{array}$ where $D (\dots)$ is the internal formula in square brackets. Recall Remark 3.12 and apply idealisation I to (4.16): $\begin{array}{l} (4.17) & (\forall^{st} Θ, Ψ, Z \in C, s) (\exists^{st} N^{0}) (\forall Γ) D (Θ, Ψ, Z, s, N, Γ) . \end{array}$ Apply Corollary 2.9 to ‘ $P ⊢ (4.17)$ ’ to obtain a term u such that ${E-PA}^{ω } + {QF-AC}^{1, 0}$ proves $\begin{matrix} (\forall Θ, Ψ, Z \in C, s) (\exists N^{0} \in u (Θ, Ψ, Z, s)) (\forall Γ) D (Θ, Ψ, Z, s, N, Γ), \end{matrix}$ and define $t (Θ, Ψ, Z, s) : = {max}_{i < | u (Θ, Ψ, Z, s) |} u (Θ, Ψ, Z, s) (i)$ . Now note that $\begin{matrix} (4.18) & (\forall Θ, Ψ, Z \in C, s, Γ) D (Θ, Ψ, Z, s, t (Θ, Ψ, Z, s), Γ), \end{matrix}$ due to the monotone behaviour of $C (Z, s, \cdot, Γ)$ . Bringing the Z and s quantifiers into the consequent of D in (4.18), we obtain that for all $Θ, Ψ, Γ$ : $\begin{matrix} [(\forall f) A (f, Ψ (f)) \land SCF (Θ) \land GH (Γ)] \to (\forall Z^{2} \in C, s^{0}) C (Z, s, t (Θ, Ψ, Z, s), Γ) . \end{matrix}$ Finally, we note that Ψ as in $(\forall f) A (f, Ψ (f))$ is Feferman’s second search operator as in ${MU}_{2} (ν)$ . In the proof of Theorem 3.7, the latter functional is explicitly defined in terms of Feferman’s search operator as in $MU (μ)$ . □

Recall Remark 3.12 and note that we performed a similar procedure as in the former remark (involving a term of type $0^{}$ and its maximum) to obtain (4.18) from (4.17) after applying Corollary 2.9 to the latter. Hereon-after, we will sometimes skip the (obvious) step involving the maximum when applying Corollary 2.9 too.
Corollary 4.5.
We can obtain a version of ( 4.10 ) with Feferman’s search operator $MU (μ)$ replaced by $MPC (Ψ)$ , i.e. the Gandy–Hyland functional can be expressed in terms of a modulus-of-continuity functional and Θ.
Proof.
From Ψ as in $MPC (Ψ)$ , one can define a discontinuous type two functional (see [9] and [2], Theorem 19.1). By [13], Prop. 3.7 and [14], Section 3, a discontinuous type two functional can be used to define $μ^{2}$ as in $MU (μ)$ , using choice functionals originating from the application of ${QF-AC}^{1, 0}$ . □

We now discuss a possible strengthening of the above results.
Remark 4.6 (Similar results).

It is an interesting question if the condition ‘ $Y^{2} \in C$ ’ in $NPC$ can be weakened. First of all, we cannot drop this condition: As shown in the proof of Corollary 3.7, NPC gives rise to a modulus-of-continuity functional Ψ as in MPC ( Ψ ) . From the latter functional, one constructs a discontinuous type two functional (see [9] and [2], Theorem 19.1), which contradicts $MPC (Ψ)$ without the restriction ‘ $Y^{2} \in C$ ’. Secondly, going through the proofs in this section, it seems that ‘ $Y^{2} \in C$ ’ can be replaced by any internal formula $D (Y^{2})$ , as long as the latter formula blocks the aforementioned contradiction in the same way as ‘ $Y^{2} \in C$ ’ does.

In Section 4.4, we obtain relative computability results similar to (4.10) with weaker antecedents. We now discuss how the consequent of the above results can be strengthened.

Remark 4.7 (Similar results II).

It is a natural question if the consequent of (4.10) is the best possible. A careful study of the proofs of Theorem 4.1 and Corollary 4.3 reveals the existence of standard $Γ^{3}$ such that ${GH}_{st} (Γ)$ and $\begin{array}{l} (4.19) & (\forall^{st} Y^{2} \in C, α^{1}) (\forall N^{0}, M^{0} \in Ω) (\forall s^{0}) (\overline{α} M =_{0} \overline{s * 00 \dots} M \to Γ (Y, s) =_{0} G (Y, s, N)) . \end{array}$ Indeed, if $s^{0}$ is standard, then the associated instance of (4.19) follows from Corollary 4.3. If $s^{0}$ is nonstandard, it has α as a standard part and (4.19) follows by nonstandard continuity as in $NPC$ . Applying term extraction to a variation of (4.9) involving (4.19), one obtains a term u which computes the Gandy–Hyland functional ‘more uniformly’ than the term t in (4.10), in that u provides one stopping condition for every initial segment $s^{0}$ of the sequence $α^{1}$ . We shall derive $NPC$ from (4.19) in Section 4.5.

Remark 4.8 (Similar results III).

We now discuss whether the previous results go through inside a fragment of $P$ . The ‘good’ news is that our term extraction results, namely Theorem 2.8 and Corollary 2.9, do not really depend on the presence of full Peano arithmetic. In particular, it is an easy verification that the proof of [27], Theorem 7.7 goes through for any fragment of ${E-PA}^{ω *}$ which includes EFA, sometimes also called $I Δ_{0} + EXP$ . The ‘bad’ news is that in light of [8], Section 5, it seems that in order to define the canonical approximations G, one cannot avoid invoking a principle (slightly) stronger than primitive recursive arithmetic ([5], Section 1.2.10).

Remark 4.9 (Similar results IV).

We now discuss whether the use of $NPC$ in Theorem 4.1 is necessary. On one hand, it seems one can replace the use of $NPC$ in the proof of the latter by: nonstandard uniform continuity as in $\begin{matrix} (4.20) & (\forall^{st} Y^{2} \in C, h^{1}) (\forall f^{1}, g^{1} ⩽_{1} h) (f \approx_{1} g \to Y (f) =_{0} Y (g)) \end{matrix}$ and nonstandard ‘weak’ continuity as follows: $\begin{matrix} (4.21) & (\forall^{st} f^{1}, Y^{2} \in C) (\forall g^{1}) (f \approx_{1} g \to st (Y (g))) . \end{matrix}$ Applying the template from Remark 3.5, (4.20) and (4.21) give rise to the fan functional and the weak continuity functional (see [4] for the latter). On the other hand, the proof of Theorem 3.18 suggests that external bar induction EBI requires Transfer, and the latter gives rise to Feferman’s search operator. Hence, it seems adopting (4.20) and (4.21) does not yield a version of (4.10) not involving Feferman’s search operator.

In conclusion, we have proved in Theorem 4.1 that the functional $G (\cdot, M)$ and $Γ (\cdot)$ are equal for standard inputs and nonstandard $M^{0}$ . From this proof, we have extracted a term from Gödel’s T which computes the Γ-functional as a function of a modulus-of-continuity functional. While these relative computability results are not necessarily deep or surprising, our methodology constitutes the true surprise: That from the proof of Theorem 4.1, in which no attention to effective content is given, and involving Nonstandard Analysis, the term t as in Corollary 4.4 may be extracted. We prove variations of these results in Sections 4.4 to 4.6, establishing the robustness of our approach.

4.3. From relative computability to Nonstandard Analysis

In the previous section, we showed how to extract relative computability results like (4.10) from corresponding nonstandard statements like (4.9). Now, it is a natural ‘Reverse Mathematics style’ question whether it is possible to re-obtain the nonstandard implication from (a variation of) the associated relative computability result.

Another natural question is whether we can obtain a version of (4.10) with weaker assumptions; Indeed, to compute $Γ (Y, s)$ it should – intuitively speaking – suffice to have a functional which (only) behaves like the special fan and modulus-of-continuity functional for Y (and functionals explicitly defined from the latter).

To answer these two questions, we define the Hebrandisation of (4.10) as follows. Let $SCF (Θ, g)$ be $SCF (Θ)$ with the leading quantifier involving g dropped. Let ${MU}_{2} (ν, f)$ be ${MU}_{2} (ν)$ from Section 3.1.2 with the leading quantifier involving f dropped. Let GH $(Γ, Y, s)$ be $GH (Γ)$ with the quantifier involving Y and s dropped.

Definition 4.10 (Herbandisation).

Let $i^{3 \to 2^{*}}$ and $o^{4}$ be terms from the language of ${E-PA}^{ω *}$ . The Herbrandisation HER $(i, o)$ of (4.11) is the statement that for all $Ξ = (Θ, ν)$ and all $Γ^{3}, Y^{2} \in C, s^{0}$ $\begin{array}{l} [(\forall (Z^{2} \in C, t^{0}) \in i (Y, s, Ξ) (1)) \\ GH (Γ, Z, t) \land (\forall W^{2} \in i (Y, s, Ξ) (2)) SCF (Θ, W) \land (\forall f^{1} \in i (Y, s, Ξ) (3)) {MU}_{2} (ν, f)] \\ \to (\forall M ⩾ o (Y, s, Ξ)) (G (Y, s, M) = Γ (Y, s)) . \end{array}$

Intuitively speaking, HER $(i, o)$ expresses that to approximate $Γ (Y, s)$ via its canonical approximation G involving the term o, it suffices that Θ and Feferman’s second search operator satisfy their usual definition on the restriction of their domains provided by i. By the following theorem, the nonstandard version (4.11) is ‘meta-equivalent’ to its Herbrandisation in that a proof of the former can be converted into a proof of the latter, and vice versa

Theorem 4.11.
From the proof of ( 4.11 ) in $P$ , two terms $i, o$ can be extracted such that ${E-PA}^{ω } + {QF-AC}^{1, 0}$ proves* $HER (i, o)$ . Moreover, if there are terms $i, o$ such that ${E-PA}^{ω } + {QF-AC}^{1, 0}$ proves* $HER (i, o)$ , then $P$ proves ( 4.11 ).
Proof.
For the first part of the theorem, consider the proof of Corollary 4.4 and note that (4.14) implies (with the same notations as in the aforementioned proof): $\begin{array}{l} (\forall^{st} Θ, Ψ, Z \in C, s) (\forall Γ^{3}) (\exists^{st} N^{0}, f^{1}, g^{2}, V^{2} \in C, t^{0}) \\ (4.22) & [[A (f, Ψ (f)) \land SCF (Θ, g) \land GH (Γ, V, t)] \to C (Z, s, N, Γ)], \end{array}$ by pushing outside, as far as possible, the standard quantifiers in (4.14). Now apply idealisation I to (4.22) to obtain: $\begin{array}{l} (\forall^{st} Θ, Ψ, Z \in C, s) (\exists^{st} W) (\forall Γ^{3}) (\exists (N, f, g, V \in C, t) \in W) \\ [[A (f, Ψ (f)) \land SCF (Θ, g) \land GH (Γ, V, t)] \to C (Z, s, N, Γ)], \end{array}$ and apply Corollary 2.9 to obtain a term w such that ${E-PA}^{ω } + {QF-AC}^{1, 0}$ proves for all $Θ, Ψ, Z \in C, s$ that $\begin{array}{l} (\exists W \in w (Θ, Ψ, Z, s)) (\forall Γ) (\exists (N, f, g, V \in C, t) \in W) \\ [[A (f, Ψ (f)) \land SCF (Θ, g) \land GH (Γ, V, t)] \to C (Z, s, N, Γ)] . \end{array}$ Now define the term o as follows: $o (Θ, Ψ, Z, s)$ is the maximum of the components of $w (Θ, Ψ, Z, s)$ pertaining to N; Similarly, define the terms $i (Θ, Ψ, Z, s) (j)$ for $j = 1$ (resp. $j = 2$ and $j = 3$ ) to be the finite sequence of all components of w pertaining to the variable f (resp. the variable g and the variables $V, t$ ). With these notations, the previous implies for functionals $Ξ = (Θ, Ψ)$ and $Z^{2} \in C, s^{0}$ that: $\begin{array}{l} [(\forall (V \in C, t^{0}) \in i (Z, s, Ξ) (3)) \\ GH (Γ, V, t) \land (\forall g^{2} \in i (Z, s, Ξ) (2)) SCF (Θ, g) \land (\forall f^{1} \in i (Z, s, Ξ) (1)) A (f, Ψ (f))] \\ (4.23) & \to (\forall M ⩾ o (Z, s, Ξ)) (G (Z, s, M) = Γ (Z, s)) . \end{array}$ Note that (4.23) is $HER (i, o)$ with slightly different notations.

For the second part, if there are terms $i, o$ such that ${E-PA}^{ω } ⊢ HER (i, o)$ , then $P ⊢ [HER (i, o) \land st (i) \land st (o)]$ by the second standardness axiom from Definition 2.5. Thus, for standard $Ξ = (Θ, ν)$ and standard $Y^{2} \in C, s^{0}$ , the terms $i (Y, s, Ξ)$ and $o (Y, s, Ξ)$ are standard by the third standardness axiom from Definition 2.5, and HER $(i, o)$ implies the following weakening (for any $Γ^{3}$ and standard $Θ, ν, Y^{2} \in C, s$ ): $\begin{array}{l} [(\forall^{st} Z^{2} \in C, t^{0}) GH (Γ, Z, t) \land (\forall^{st} W^{2}) SCF (Θ, W) \land (\forall^{st} f^{1}) {MU}_{2} (ν, f)] \\ (4.24) & \to (\forall M \in Ω) (G (Y, s, M) = Γ (Y, s)) . \end{array}$ Applying ${HAC}_{int}$ to (3.15), $Σ_{2}^{0} -TRANS$ yields $(\exists^{st} ν) (\forall^{st} f^{1}) {MU}_{2} (ν, f)$ . Similarly, $STP$ implies $(\exists^{st} Θ^{3}) (\forall^{st} Y^{2}) SCF (Θ, Y)$ by the proof of Corollary 3.4. Hence, $NPC + Σ_{2}^{0} -TRANS + STP$ implies the second and third conjunct of the antecedent of (4.24), which yields (4.11), and we are done. □

Thus, we proved that from a proof of (4.11), terms $i, o$ from Gödel’s T can be extracted satisfying the Herbrandisation of (4.11), i.e. o computes $Γ (Y, s)$ as a function of approximations enforced by i of the special fan functional and Feferman’s second search functional. Furthermore, the nonstandard version (4.11) in turn follows from its Herbrandisation, i.e. the latter are ‘equivalent in the meta-theory’ in the sense of the previous theorem.

Obviously, the Herbrandisation $HER (i, o)$ of (4.11) is much more complicated than (4.10). This seems to be due to the fact that Feferman’s second search operator and the special fan functional can be defined explicitly in terms of Feferman’s search operator, while the same seems impossible for the restrictions of the latter imposed by the term i in $HER (i, o)$ . Intuitively speaking, one needs to apply Feferman’s search operator ‘infinitely many times’ to obtain Feferman’s second search operator.

In conclusion, the correspondence exhibited in Theorem 4.11 establishes a direct two-way connection between the field Computability (in particular theoretical computer science) and the field Nonstandard Analysis. Indeed, while the relative computability result $HER (i, o)$ could arguably still be passed off as (theoretical) computer science, experience bears out that the nonstandard version (4.9) does not count as such among computer scientists. We could obtain the (meta-equivalent) Herbrandisation for every nonstandard theorem proved in this paper, but we will not do so in the next sections due to space constraints.
4.4. From Nonstandard Analysis to relative computability II

In this section, we obtain a relative computability result for the Gandy–Hyland functional, not involving Feferman’s search operator. To this end, we shall establish that the proofs of Theorem 4.1 and Corollary 4.3 also go through ‘in a pointwise fashion’, to be understood in the sense of Theorem 4.12.

Recall $GH (Γ, Y, s)$ defined in Section 4.3, and define $GH (Γ, Y)$ as $(\forall s^{0}) GH (Γ, Y, s)$ . Let $NPC (Y)$ be: $\begin{matrix} (NPC (Y)) & (\forall^{st} f^{1}) (\forall g^{1}) (f \approx_{1} g \to Y (f) =_{0} Y (g)), \end{matrix}$ i.e. NPC with the ‘ $(\forall^{st} Y^{2} \in C)$ ’ dropped, and let $ST (Γ, Y)$ be $(\forall^{st} s^{0}) (st (Γ (Y, s)))$ .

Theorem 4.12.
The system $P + STP$ proves that for all $Γ^{3}$ and $Y^{2}$ $\begin{matrix} (4.25) & [NPC (Y) \land GH (Γ, Y) \land ST (Γ, Y)] \to (\forall^{st} s^{0}) (\forall N \in Ω) (Γ (Y, s) = G (Y, s, N)) . \end{matrix}$
Proof.
Fix $Γ^{3}$ and $Y^{2}$ , as in the antecedent of (4.25). As EBI is not available, we shall use ${BI}_{0}^{st}$ , which is available by Theorem 3.14. Thus, fix standard $s^{0}$ and $N \in Ω$ and consider $Q (x) \equiv [G (Y, s * x, N) =_{0} Γ (Y, s * x)]$ .

To prove the first conjunct of ${(3.30)}^{st}$ , note that for $M \in Ω$ and standard $α^{1}$ , we have $G (Y, \overline{α} M, N) = Y (α) = Γ (Y, \overline{α} M)$ , by the nonstandard continuity of $Y^{2}$ and the fact that $(\overline{α} M * γ) \approx_{1} α$ for any $γ^{1}$ . As in the proof of Theorem 4.1, one obtains the first conjunct ${(3.30)}^{st}$ using underspill.

To prove the second conjunct of ${(3.30)}^{st}$ , fix standard $t^{0}$ and assume $Q (t * ⟨ x ⟩)$ for all standard $x^{0}$ . By definition, we have $G (Y, s * t * ⟨ x ⟩, N) = Γ (Y, s * t * ⟨ x ⟩)$ for any standard $x^{0}$ , and these numbers are standard by $ST (Γ, Y)$ . By $STP$ , the sequence $(s * t * 0 * (λ n) G (Y, s * t * (n + 1)), N)$ has a standard part, say $γ^{1}$ . Thus: $\begin{matrix} (s * t * 0 * (λ n) G (Y, s * t * (n + 1)), N) \approx_{1} γ \approx_{1} s * t * 0 * (λ m) Γ (Y, s * t * (m + 1)), \end{matrix}$ and the nonstandard continuity of Y yields: $\begin{array}{l} G (Y, s * t, N) & = Y (s * t * 0 * (λ n) G (Y, s * t * (n + 1)), N) \\ (4.26) & = Y (γ) = Y (s * t * 0 * (λ m) Γ (Y, s * t * (m + 1))) = Γ (Y, s * t), \end{array}$ which implies that $Q (t)$ , and the second conjunct of ${(3.30)}^{st}$ follows. Hence, we have proved ${(3.30)}^{st}$ , yielding $Q (⟨ \cdot ⟩)$ and $G (Y, s, N) =_{0} Γ (Y, s)$ as required, and (4.25) follows. □

We need the following for Corollary 4.13, by $PCM (Y^{2}, Z^{2})$ expresses that Z is a modulus of continuity for Y. $\begin{array}{l} (PCM (Y, Z)) & (\forall f^{1}, g^{1}) (\overline{f} Z (f) =_{0} \overline{g} Z (f) \to Y (f) =_{0} Y (g)) \\ (GHU (Γ, Y, H)) & (\forall s^{0}) [Γ (Y, s) = Y (s * 0 * (λ n) Γ (Y, s * (n + 1))) ⩽ H (Y, s)], \end{array}$
Corollary 4.13 (Term Extraction II).

From the proof in Theorem 4.12 , a term t can be extracted s.t. ${E-PA}^{ω *} + {QF-AC}^{1, 0}$ proves for $Ξ = (H^{1}, Z^{2}, Θ^{3})$ and $Γ^{3}, Y^{2}$ $\begin{matrix} [PCM (Y, Z) \land SCF (Θ) \land GHU (Γ, Y, H)] \to (\forall s) (\forall N ⩾ t (s, Ξ)) (Γ (Y, s) = G (Y, s, N)), \end{matrix}$ i.e. the Gandy–Hyland functional Γ at Y can be approximated via a modulus of continuity of Y, the special fan functional, and an upper bound for $Γ (Y, \cdot)$ .

Proof.
The template from Remark 3.5 applies. We now sketch how one obtains a normal form for all principles in $STP \to (4.25)$ ; The normal form (3.9) of $STP$ has been studied in the proof of Corollary 3.4. The normal form of $NPC (Y)$ , obtained in the same way as the normal form (3.5) of NUC in the proof of Theorem 3.3, is $\begin{matrix} (\forall^{st} f^{1}) (\exists^{st} N^{0}) [(\forall g^{1}) (\overline{f} N =_{0} \overline{g} N \to Y (f) =_{0} Y (g))], \end{matrix}$ and applying ${HAC}_{int}$ , one sees how the modulus of continuity of Y comes about. Finally, $ST (Γ, Y)$ has the following normal form: $(\forall^{st} s^{0}) (\exists^{st} n^{0}) (Γ (Y, s) ⩽_{0} n)$ , and applying ${HAC}_{int}$ one observes where the upper bound H comes from. The normal form for the consequent of (4.25) is as follows: $\begin{matrix} (4.27) & (\forall^{st} s^{0}) (\exists^{st} n^{0}) (\forall N ⩾ n) (Γ (Y, s) = G (Y, s, N)), \end{matrix}$ and follows by underspill. In step (iii) from the template in Remark 3.5, idealisation I needs to be applied to pull the ‘ $(\exists^{st} n)$ ’ quantifier from (4.27) through the quantifier $(\forall Γ^{3}, Y^{2})$ from (4.25), taking into account Remark 3.12. □

Following Definition 4.10, it is easy to define the Herbrandisation of (4.25) and obtain a result similar to Theorem 4.11. In particular, this Hebrandisation tells us on which part of Baire space the functional Y should be continuous (with modulus Z) to guarantee that Γ and G coincide at Y.

In conclusion, we have obtained a ‘pointwise’ relative computability result for the Gandy–Hyland functional not involving Feferman’s search operator. In particular, the term t from Corollary 4.13 allows us to compute approximations of the Gandy–Hyland functional in terms of the special fan functional for any functional Y with a modulus of (pointwise) continuity, and a given upper bound on $Γ (Y, \cdot)$ . Finally, the statement every continuous functional on Baire space has a modulus of pointwise continuity, is rather weak by [12], Prop. 4.4 and 4.8.
4.5. From Nonstandard Analysis to relative computability III

In this section, we show that the approximation of the Gandy–Hyland functional as in (4.19) implies $NPC$ ; We derive the associated relative computability result in which a term from Gödel’s $T$ expresses a modulus-of-continuity functional in terms of an ‘approximation’ functional as in (4.19) for the Gandy–Hyland functional. We also sketch a ‘pointwise’ result similar to what was established in Section 4.4.

First of all, consider the following principle and theorem.

Principle 4.14 ( ${GHS}_{ns}$ ).

There is $Γ^{3}$ such that ${GH}_{st} (Γ)$ and $\begin{matrix} (\forall^{st} Y^{2} \in C, α^{1}) (\forall N^{0}, M^{0} \in Ω) (\forall s^{0}) (\overline{α} M =_{0} \overline{s * 00 \dots} M \to Γ (Y, s) =_{0} G (Y, s, N)) . \end{matrix}$

Theorem 4.15.
In $P$ , we have ${GHS}_{ns} \to NPC$ .
Proof.
In a nutshell, to obtain NPC from ${GHS}_{ns}$ , one computes for standard $Y^{2} \in C$ the numbers $Y (α)$ and $Y (β)$ using ${GHS}_{ns}$ and notes that they are identical if $α \approx_{1} β$ for standard $α^{1}$ and any $β^{1}$ . In more detail, we first apply underspill to the second conjunct of ${GHS}_{ns}$ , to obtain that $\begin{matrix} (\forall^{st} Y^{2} \in C, α^{1}) (\exists^{st} K^{0}) (\forall N^{0}, M^{0} ⩾ K) (\forall s^{0}) (\overline{α} M =_{0} \overline{s * 00 \dots} M \to Γ (Y, s) =_{0} G (Y, s, N)) . \end{matrix}$ Applying ${HAC}_{int}$ to the previous formula yields a standard functional $Ξ^{3}$ such that $\begin{array}{l} (4.28) & (\forall^{st} Y^{2} \in C, α^{1}) (\forall N^{0}, M^{0} ⩾ Ξ (Y, α)) (\forall s^{0}) (\overline{α} M =_{0} \overline{s * 00 \dots} M \to Γ (Y, s) =_{0} G (Y, s, N)), \end{array}$ keeping in mind Remark 3.12. Now fix standard $Y^{2} \in C$ and standard $α^{1}$ , and any $β^{1}$ such that $α \approx_{1} β$ . Since $Y^{2} \in C$ , there are numbers $N_{0}^{0}, M_{0}^{0}$ such that $\begin{array}{l} (4.29) & (\forall γ^{1}) (\overline{γ} M_{0} =_{0} \overline{β} M_{0} \to Y (γ) =_{0} Y (β)), \\ (4.30) & (\forall γ^{1}) (\overline{γ} N_{0} =_{0} \overline{α} N_{0} \to Y (γ) =_{0} Y (α)) . \end{array}$ If $M_{0}$ or $N_{0}$ is standard, we have $Y (α) = Y (β)$ , and we are done. In case $M_{0}$ and $N_{0}$ are nonstandard, we have $Y (\overline{α} N_{0} * 00 \dots) = Y (α)$ and $Y (\overline{β} M_{0} * 00 \dots) = Y (β)$ by (4.29) and (4.30). Also, $Ξ (Y, α)$ is standard, yielding that $Y (\overline{α} Ξ (Y, α) * 00 \dots) = Y (\overline{β} Ξ (Y, α) * 00 \dots)$ by extensionality. The following equalities now follow easily: $\begin{array}{l} (4.31) & Y (α) & = Y (\overline{α} N_{0} * 00 \dots) = G (Y, \overline{α} N_{0}, N_{0}) = Γ (Y, \overline{α} N_{0}) \\ (4.32) & = G (Y, \overline{α} N_{0}, Ξ (Y, α)) \\ = Y (\overline{α} Ξ (Y, α) * 00 \dots) = Y (\overline{β} Ξ (Y, α) * 00 \dots) \\ = G (Y, \overline{β} M_{0}, Ξ (Y, α)) = Γ (Y, \overline{β} M_{0}) = G (Y, \overline{β} M_{0}, M_{0}) = Y (\overline{β} M_{0} * 00 \dots) = Y (β) . \end{array}$ For instance, to obtain the equality between (4.31) and (4.32), one applies (4.28) for $s = \overline{α} N_{0}$ and $N = Ξ (Y, α)$ and $M = N_{0}$ . The remaining equalities are proved similarly, and we are done. □

Now define GHS $(Ψ, Γ)$ as the following formula: $\begin{matrix} (\forall Y^{2} \in C, α^{1}, N, M ⩾ Ψ (Y, α), s^{0}) (\overline{α} M = \overline{s * 00 \dots} M \to G (Y, s, N) =_{0} Γ (Y, s)), \end{matrix}$ which expresses that Ψ witnesses the canonical approximation of Γ via G in a ‘more uniform way’ than in $CA (Γ)$ .
Corollary 4.16 (Term Extraction III).

From the proof ‘ $P ⊢ {GHS}_{ns} \to NPC$ ’, a term t can be extracted such that ${E-PA}^{ω *} + {QF-AC}^{1, 0}$ proves for all $Γ^{3}, Ψ^{3}$ that $\begin{array}{l} (4.33) & [GH (Γ) \land GHS (Ψ, Γ)] \to MPC (t (Ψ)) . \end{array}$

Proof.
Analogous to the proof of Corollary 4.4, i.e. follow the template from Remark 3.5. The normal form of $NPC$ , obtained in the same way as the normal form (3.5) of NUC in the proof of Theorem 3.3, is $\begin{matrix} (4.34) & (\forall^{st} Y^{2} \in C, f^{1}) (\exists^{st} N_{0}^{0}) [(\forall g^{1}) (\overline{f} N =_{0} \overline{g} N \to Y (f) =_{0} Y (g))], \end{matrix}$ and applying ${HAC}_{int}$ , one sees how the modulus-of-continuity functional comes about. In step (iii) from the template in Remark 3.5, idealisation I needs to be applied to pull the ‘ $(\exists^{st} N_{0})$ ’ quantifier from (4.34) through the quantifier $(\forall Γ^{3})$ in ${GHS}_{ns} \to NPC$ , taking into account Remark 3.12. □

Next, we sketch a ‘pointwise’ version of Theorem 4.15 and Corollary 4.16, similar to the results in Section 4.4. Define the ‘pointwise’ version of ${GHS}_{ns}$ as follows:
Principle 4.17 ( ${GHS}_{ns 2} (Y, Γ)$ ).

We have $GH (Γ, Y)$ and $\begin{matrix} (\forall^{st} α^{1}) (\forall N^{0}, M^{0} \in Ω) (\forall s^{0}) (\overline{α} M =_{0} \overline{s * 00 \dots} M \to Γ (Y, s) =_{0} G (Y, s, N)) . \end{matrix}$

Recall the definition of $NPC (Y)$ from Section 4.4.

Theorem 4.18.
In $P$ , we have $(\forall^{st} Y^{2} \in C) (\forall Γ^{3}) [{GHS}_{ns 2} (Y, Γ) \to NPC (Y)]$ .
Proof.
In a nutshell, the proof of Theorem 4.15 goes through with minor modifications. In more detail, fix standard $Y^{2} \in C$ and any $Γ^{3}$ such that ${GHS}_{ns 2} (Y, Γ)$ . Applying underspill to the second conjunct of the latter, we obtain a variation of (4.28), namely the following formula: $\begin{matrix} (\forall^{st} α^{1}) (\exists^{st} K^{0}) (\forall N^{0}, M^{0} ⩾ K) (\forall s^{0}) (\overline{α} M =_{0} \overline{s * 00 \dots} M \to Γ (Y, s) =_{0} G (Y, s, N)) . \end{matrix}$ Applying ${HAC}_{int}$ , there is $ξ^{2}$ witnessing the existential quantifier, bearing in mind Remark 3.12. Now note that in the series of equalities involving (4.32), all equalities resulting from (4.28) only involve $Γ (Y, \cdot)$ and $G (Y, \cdot)$ . Hence, the proof of Theorem 4.15 goes through in this case, but with $ξ (α)$ instead of $Ξ (Y, α)$ . □

Now define GHS $(Y, Ψ, Γ)$ as $GHS (Ψ, Γ)$ without the quantifier ‘ $(\forall Y^{2} \in C)$ ’.
Corollary 4.19 (Term Extraction IV).

From the proof in Theorem 4.18 , a term t can be extracted such that ${E-PA}^{ω *} + {QF-AC}^{1, 0}$ proves for all $Γ^{3}, Ψ^{2}, Y^{2} \in C$ that $\begin{array}{l} (4.35) & [GH (Γ, Y) \land GHS (Y, Ψ, Γ)] \to PCM (Y, t (Y, Ψ)) . \end{array}$

Proof.
Analogous to the proof of Corollary 4.4. □

Note that (4.35) expresses that if for $Y^{2} \in C$ we can approximate the Gandy–Hyland functional at Y ‘uniformly’ via G and Ψ, then $t (Y, Ψ)$ is a modulus of pointwise continuity for Y. A kind of converse was obtained in Corollary 4.13.

In light of (4.10) and6
⁶
Following the proof of Corollary 4.5, Feferman’s search operator may be defined in terms of a modulus-of-continuity functional, i.e. there is a version of (4.33) with consequent $MU (u (Γ, Ψ))$ , where the term u would however contain choice functionals from ${QF-AC}^{1, 0}$ .

(4.33), there are terms from Gödel’s $T$ expressing the (approximations of the) Gandy–Hyland functional in terms of Feferman’s search operator, and vice versa. As it turns out, there is also a recent model-theoretic characterisation of the Gandy–Hyland functional and arithmetical comprehension, namely [15], Theorem 9.5.4, p. 460, which expresses that: $\begin{matrix} (LN) & \begin{matrix} The totality of the Gandy–Hyland functional in a (computationally closed) model is \\ equivalent to that model satisfying arithmetical comprehension. \end{matrix} \end{matrix}$ Consequently, it is a natural question (due to Dag Normann) whether our results are related to the aforementioned model-theoretic result. While our above results regarding the Γ-functional and arithmetical comprehension (as in Feferman’s search operator) bear some resemblance to (LN), they are not really satisfactory. On the other hand, the latter deals with partial functionals, and how would one express partiality in a system like $P$ where all functionals are total anyway? We discuss these matters in the next section where we also improve upon the previous results.
4.6. From Nonstandard Analysis to relative computability IV

4.6.1. Introduction

In this section, we study the equivalences between a version of $NPC$ , principles involving the Γ-functional, and $Π_{1}^{0} - TRANS$ . From these equivalences, we obtain relative computability results for arithmetical comprehension, the Γ-funtional, and a modulus-of-continuity functional, some quite similar to (LN). To this end, we shall work with the associates of continuous functionals, rather than the functionals themselves.

We introduce the notion of associate in Section 4.6.2, and prove an equivalence between $NPC$ for associates and $Π_{1}^{0} - TRANS$ . From this equivalence, we obtain an effective equivalence between arithmetical comprehension as in $(μ^{2})$ , and a modulus-of-continuity functional for associates. In Section 4.6.3, we prove an equivalence between $Π_{1}^{0} - TRANS$ and various statements regarding the Gandy–Hyland functional defined on associates. From these nonstandard equivalences, we obtain various relative computability results regarding the Gandy–Hyland functional and arithmetical comprehension as in $(μ^{2})$ . As we will see, our final result is rather close in spirit to (LN).

4.6.2. Continuity and associates

In this section, we introduce the notion of associate and prove a first equivalence involving $Π_{1}^{0} - TRANS$ and $NPC$ for associates. From this equivalence, we obtain an effective equivalence between arithmetical comprehension as in $(μ^{2})$ , and a modulus-of-continuity functional for associates.

We introduce the definition of associate from [12], Def. 4.3; See also [15], Section 8.2.1.

Definition 4.20 (Associate).

The function $γ^{1}$ is an associate of $Y^{2} \in C$ if:

$(\forall β^{1}) (\exists k^{0}) γ (\overline{β} k) > 0$ ,

$(\forall β^{1}, k^{0}) (γ (\overline{β} k) > 0 \to Y (β) + 1 =_{0} γ (\overline{β} k))$ .

We assume an associate

γ^{1}

to be a neighbourhood function (see [12], Section 4), i.e.

\begin{matrix} (4.36) & (\forall σ^{0}, τ^{0}, n^{0}) ((σ ⪯ τ \land γ (\overline{σ} n) > 0) \to γ (σ) =_{0} γ (τ)), \end{matrix}

where ‘

σ ⪯ τ

’ is ‘

| σ | ⩽ | τ | \land (\forall i < | σ |) (σ (i) = τ (i))

’, i.e. σ is an initial segment of τ.

We now argue why working with associates, rather than continuous functionals, is natural in our context. Recall the following fragment of the axiom of choice.

Definition 4.21 ( ${QF-AC}^{1, 0}$ ).

For internal and quantifier-free $φ_{0}$ , we have $\begin{matrix} (4.37) & (\forall x^{1}) (\exists y^{0}) φ_{0} (x, y) \to (\exists F^{2}) (\forall x^{1}) φ_{0} (x, F (x)) . \end{matrix}$

Applying ${QF-AC}^{1, 0}$ to item (i) in Definition 4.20, the latter gives rise to a continuous functional $Y^{2}$ by putting $Y (α) : = γ (\overline{α} F (α)) - 1$ . Hence, associates give rise to continuous type two functionals, modulo ${QF-AC}^{1, 0}$ . Furthermore, the latter is a very weak principle, as established in [13], Section 2.

Secondly, as noted above, the proof of [12], Prop. 4.4 contains an explicit definition for obtaining an associate from a functional and its modulus of pointwise continuity. Hence, in the presence of a modulus-of-continuity functional (as in Section 4.2) or if a modulus is assumed to be given (as in Section 4.4), working with associates rather than the continuous functionals themselves, amounts to the same.

Thirdly, the logical framework for Reverse Mathematics [24] is second-order arithmetic, and one is thence forced to work with associates (called codes by Simpson in [24]) to study e.g. continuous functionals on Baire or Cantor space, or $R$ (see also [12], Prop. 4.4). The development of Reverse Mathematics does not seem to be hampered by the use of associates

Finally, we note that associates play an important role in higher-order computability theory (see e.g. [15], Section 8.2.1), i.e. they are of independent interest besides the above pragmatic motivations.

In light of the previous observations, it seems acceptable to work with associates directly, in the context of this paper. Thus, we may introduce the following.

Notation 4.22.
We denote ‘ $γ^{1} \in C$ ’ the first item of Definition 4.20 plus the requirement on neighbourhood functions (4.36). Then $(\forall^{st} γ^{1} \in C) φ (γ)$ is short for $\begin{matrix} (4.38) & (\forall γ^{1}) ({st}_{1} (γ) \to [γ^{1} \in C \to φ (γ)]) . \end{matrix}$ Note that no mention of ${(γ^{1} \in C)}^{st}$ is made, and that the formula in square brackets in (4.38) is internal if $φ (γ^{1})$ is. Furthermore, we denote the ‘value of the associate $γ^{1} \in C$ at $α^{1}$ ’ by ‘ $γ (α)$ ’, which is understood to be $γ (\overline{α} N) - 1$ , assuming the latter is at least zero, i.e. for large enough N. An equality ‘ $γ (α) =_{0} m_{0}^{0}$ ’ is then interpreted as $(\forall n^{0}) ((γ (\overline{α} n) > 0 \to γ (\overline{α} n) =_{0} m_{0} + 1))$ , which is not quantifier-free.

The previous notations are in line with those used in Reverse Mathematics, as can be gleaned from [24], II.6.1. With these conventions in place, we can introduce a nonstandard continuity principle on associates, as follows. $\begin{matrix} ({NPC}^{a}) & (\forall^{st} γ^{1} \in C, α^{1}) (\forall β^{1}) (α \approx_{1} β \to γ (α) =_{0} γ (β)), \end{matrix}$ where the final equality is not quantifier-free by Notation 4.22.
Theorem 4.23.
The system $P$ proves ${NPC}^{a} \leftrightarrow Π_{1}^{0} - TRANS$ .
Proof.
For the implication $Π_{1}^{0} - TRANS \to {NPC}^{a}$ , fix standard $γ^{1} \in C$ , standard $α^{1}$ , and any $β^{1} \approx_{1} α^{1}$ . Now consider $(\exists k^{0}) γ (\overline{α} k) > 0$ , implying $(\exists^{st} k_{0}^{0}) γ (\overline{α} k_{0}) > 0$ by $Π_{1}^{0} - TRANS$ . Since $α \approx_{1} β$ , we have $\overline{β} k_{0} =_{0^{}} \overline{α} k_{0}$ for the latter $k_{0}$ . By extensionality, we have $γ (\overline{α} k_{0}) =_{0} γ (\overline{β} k_{0}) > 0$ ; This implies $γ (α) = γ (β)$ , and ${NPC}^{a}$ follows.

Working in $P + {NPC}^{a}$ , suppose $Π_{1}^{0} - TRANS$ is false, i.e. there is standard $h^{1}$ such that $(\forall^{st} n) h (n) = 0$ and $(\exists m_{0}) h (m_{0}) \neq 0$ . Define standard $γ^{1}$ as follows: $\begin{matrix} (4.39) & γ (σ) : = \{\begin{matrix} 1 + σ ((μ n ⩽ | σ |) [h (n) \neq 0]) & (\exists n ⩽ | σ |) [h (n) \neq 0] \\ 0 & otherwise . \end{matrix} \end{matrix}$ Clearly, $γ^{1} \in C$ and ${NPC}^{a}$ implies that the latter is nonstandard continuous. However, for $β_{M} : = (\overline{00 \dots} M) (M M \dots)$ , we note that $β_{0}$ is standard, and that $β_{0} \approx_{1} β_{m_{0}}$ and $γ (β_{0}) = 0 \neq m_{0} = γ (β_{m_{0}})$ if $h (m_{0}) \neq 0$ . This contradiction yields ${NPC}^{a} \to Π_{1}^{0} - TRANS$ , and we are done. □

Recall $MU (μ)$ introduced in Section 3.1.2 and let ${MPC}^{a} (Ψ^{2})$ be $\begin{matrix} (\forall γ^{1} \in C) (\forall f^{1}, g^{1} ⩽_{1} 1) [\overline{g} Ψ (γ, f) =_{0} \overline{f} Ψ (γ, f) \to γ (f) =_{0} γ (g)] . \end{matrix}$ The formula in square brackets in ${MPC}^{a} (Ψ)$ is not quantifier-free due to ‘ $γ (f) =_{0} γ (g)$ ’. We have the following relative computability result.
Corollary 4.24 (Term Extraction V).

From the proof of ${NPC}^{a} \leftrightarrow Π_{1}^{0} - TRANS$ in $P$ , terms $s, t$ can be extracted such that ${E-PA}^{ω *} + {QF-AC}^{1, 0}$ proves $\begin{matrix} (4.40) & (\forall μ^{2}) [MU (μ) \to {MPC}^{a} (s (μ))] \land (\forall Ψ^{2}) [{MPC}^{a} (Ψ) \to MU (u (Ψ))] . \end{matrix}$

Proof.
To obtain a normal form for ${NPC}^{a}$ , proceed in the same way as for $NUC$ and (3.5). In particular the normal form of ${NPC}^{a}$ is $\begin{matrix} (4.41) & (\forall^{st} γ^{1} \in C, f^{1}) (\exists^{st} N^{0}) (\forall g^{1}) [\overline{f} N =_{0} \overline{g} N \to γ (f) =_{0} γ (g)], \end{matrix}$ where the formula in square brackets is internal and not quantifier-free by Notation 4.22. The normal form for $Π_{1}^{0} - TRANS$ is obvious, namely: $\begin{matrix} (4.42) & (\forall^{st} f^{1}) (\exists^{st} n^{0}) [(\exists m^{0}) f (m) \neq 0 \to (\exists i^{0} ⩽_{0} n) f (i) \neq 0] . \end{matrix}$ Now apply the template in Remark 3.5 to ${NPC}^{a} \leftrightarrow Π_{1}^{0} - TRANS$ . □

Finally, we discuss the conceptual meaning of ${NPC}^{a}$ . By Notation 4.22, a type one associate $γ^{1} \in C$ is meant to ‘simulate’ or ‘represent’ a continuous type two functional. By Definition 2.5, standard functionals have standard output for standard input in $P$ ; Thus, a natural question is whether a standard associate $γ^{1} \in C$ has standard output $γ (α)$ for standard input $α^{1}$ , i.e. whether a standard associate also simulates a standard type two functional. By the proof of Theorem 4.23, one requires $Π_{1}^{0} - TRANS$ or ${NPC}^{a}$ to guarantee the ‘expected’ behaviour that standard associates have standard output for standard input. Indeed, $γ^{1} \in C$ as in (4.39) yields nonstandard output for certain standard inputs, assuming $\neg Π_{1}^{0} - TRANS$ .
4.6.3. The Gandy–Hyland functional and associates

In this section, we shall study the connection between arithmetical comprehension and the Gandy–Hyland functional defined on associates. Now, in the previous section, we observed that type one associates may be viewed as type two functionals; In particular, for $γ^{1} \in C$ and $α^{1}$ , it makes sense to apply the former to the latter as in ‘ $γ (α)$ ’, despite the type mismatch. Similarly, we now define how one applies type three functionals (like the Gandy–Hyland functional) to type one associates, again despite the apparent type mismatch.

Notation 4.25.
In the presence of ${QF-AC}^{1, 0}$ , $γ (α)$ equals $γ (\overline{α} F (α)) - 1$ for $γ^{1} \in C$ , where F originates from the former choice axiom applied to $(\forall α^{1}) (\exists N^{0}) γ (\overline{α} N) > 0$ . In this way, we define for $Λ^{3}$ and $γ^{1} \in C$ , the application of the former functional to the latter sequence as $Λ (γ) : = Λ ((λ α^{1}) [γ (\overline{α} F (α)) - 1])$ , where F is the aforementioned choice functional from ${QF-AC}^{1, 0}$ . Similarly, for a formula $A (Y^{2})$ , we shall use the formula $(\forall γ^{1} \in C) A (γ)$ as shorthand for the following formula: $\begin{matrix} (4.43) & (\forall γ^{1}) (\forall F^{2}) [(\forall α^{1}) γ (\overline{α} F (α)) > 0 \to A ((λ α^{1}) [γ (\overline{α} F (α)) - 1])], \end{matrix}$ where no type mismatch occurs. Similar to the convention involving (4.38), the formula ‘ $(\forall^{st} γ^{1} \in C) A (γ)$ ’ is the formula (4.43) with ‘ $(\forall^{st} γ^{1})$ ’ instead of ‘ $(\forall γ^{1})$ ’.

As will become clear, mathematics practice does not change much when working with associates; This has been previously observed in the development of Reverse Mathematics (see e.g. [24], I.4, p. 15).

First of all, we study the following principle regarding the Gandy–Hyland functional and associates: $\begin{array}{l} ({GH}_{ns}^{a}) & (\exists^{st} Γ^{3}) [(\forall^{st} γ^{1} \in C) (\forall s^{0}) GH (Γ, γ, s) \land (\forall^{st} γ^{1} \in C, s^{0}) (\forall N \in Ω) (\hat{G} (γ, s, N) = Γ (γ, s))], \end{array}$ where $\hat{G}$ is G with $Y (s * 11 \dots)$ rather than $Y (s * 00 \dots)$ in the first case of (1.2).

In light of Theorem 4.1 and Theorem 4.23, it is easy to obtain a proof of $Π_{1}^{0} - TRANS \to {GH}_{ns}^{a}$ in $P + STP$ . The more interesting reversal is now as follows.
Theorem 4.26.
The system $P$ proves ${GH}_{ns}^{a} \to Π_{1}^{0} - TRANS$ .
Proof.
Working in $P + {GH}_{ns}^{a}$ , we show that every standard $γ^{1} \in C$ is nonstandard continuous, implying ${NPC}^{a}$ and thus $Π_{1}^{0} - TRANS$ by Theorem 4.23. If we have $(\forall^{st} α^{1}) (\exists^{st} N) γ (\overline{α} N) > 0$ for $γ^{1} \in C$ , then the latter is nonstandard continuous. We now derive a contradiction from $(\exists^{st} α_{0}^{1}) (\forall^{st} N) γ_{0} (\overline{α} N) = 0$ for some standard $γ_{0}^{1} \in C$ . Fix such $α_{0}, γ_{0}$ and define the standard function $γ^{1} \in C$ as follows: $\begin{matrix} (4.44) & γ (σ) : = \{\begin{matrix} 1 + σ ((μ n ⩽ | σ |) γ_{0} (\overline{α_{0}} n) \neq 0) & (\exists n ⩽ | σ |) γ_{0} (\overline{α_{0}}) \neq 0 \\ 0 & otherwise . \end{matrix} \end{matrix}$ Note that $γ (α) = α (m_{0})$ where $m_{0}$ is the least m such that $γ_{0} (\overline{α} m) \neq 0$ . Bearing in mind Notation 4.25, we compute $Γ (γ, ⟨ \cdot ⟩)$ and $\hat{G} (γ, ⟨ \cdot ⟩, m_{0})$ and observe that they are different. This contradiction yields ${NPC}^{a}$ , and $Π_{1}^{0} - TRANS$ by Theorem 4.23. To prove that $Γ (γ, ⟨ \cdot ⟩) \neq \hat{G} (γ, ⟨ \cdot ⟩, m_{0})$ , define $β_{0}^{1}$ as $(0 * (λ n) Γ (γ, n + 1))$ ; By the definition of γ: $\begin{matrix} Γ (γ, ⟨ \cdot ⟩) = γ (0 * (λ n) Γ (γ, n + 1)) = γ (β_{0}) = β_{0} (m_{0}) = Γ (γ, m_{0}) . \end{matrix}$ Similarly, define $β_{1}^{1}$ as $(m_{0} * 0 * (λ n) Γ (γ, m_{0} * (n + 1)))$ and note that: $\begin{array}{l} Γ (γ, m_{0}) = γ (m_{0} * 0 * (λ n) Γ (γ, m_{0} * (n + 1))) = γ (β_{1}) = β_{1} (m_{0}) = Γ (γ, m_{0} * (m_{0} - 1)) . \end{array}$ Hence, $Γ (γ, ⟨ \cdot ⟩) = Γ (γ, m_{0} * (m_{0} - 1))$ , and in the same way one obtains that $\begin{matrix} Γ (γ, ⟨ \cdot ⟩) = Γ (γ, m_{0} * (m_{0} - 1) * \dots * 1) = γ (m_{0} * (m_{0} - 1) * \dots * 1 * 0 * (λ n) (\dots)) = 0 . \end{matrix}$ Secondly, in exactly the same way, we have for $σ_{0}^{0} : = m_{0} * (m_{0} - 1) * \dots * 1$ that $\begin{array}{l} \hat{G} (γ, ⟨ \cdot ⟩, m_{0}) & = \hat{G} (γ, ⟨ m_{0} ⟩, m_{0}) = \hat{G} (γ, ⟨ m_{0}, m_{0} - 1 ⟩, m_{0}) \\ = \hat{G} (γ, ⟨ m_{0}, m_{0} - 1, m_{0} - 2 ⟩, m_{0}) \\ = \dots \\ = \hat{G} (γ, ⟨ m_{0}, m_{0} - 1, m_{0} - 2, \dots, 1 ⟩, m_{0}) \\ = \hat{G} (γ, σ_{0}, m_{0}) \\ = γ (σ_{0} * 11 \dots) = (σ_{0} * 11 \dots) (m_{0}) = 1, \end{array}$ where $m_{0}$ is again the least m such that $h (m) \neq 0$ . □

The previous nonstandard theorem gives rise to the following term extraction corollary, for which we need: $\begin{array}{l} ({GH}^{a} (Γ)) & (\forall γ^{1} \in C, s^{0}) [Γ (γ, s^{0}) = γ (s * 0 * (λ n^{0}) Γ (γ, s * (n + 1)))], \\ ({GHS}^{a} (Ψ, Γ)) & (\forall γ^{1} \in C, s) (\forall N ⩾ Ψ (γ, s)) (\hat{G} (γ, s, N) =_{0} Γ (γ, s)) . \end{array}$
Corollary 4.27 (Term extraction VI).

From the proof of ${GH}_{ns}^{a} \to Π_{1}^{0} - TRANS$ in $P$ , a term t can be extracted such that ${E-PA}^{ω *} + {QF-AC}^{1, 0}$ proves $\begin{matrix} (4.45) & (\forall Ψ^{2}, Γ^{3}) [[{GH}^{a} (Γ) \land {GHS}^{a} (Ψ, Γ)] \to MU (t (Ψ, Γ))] . \end{matrix}$

Proof.
Analgous to the proof of Corollary 4.24; We provide a more detailed sketch to show that Notation 4.25 does not interfere with term extraction as in Remark 3.5. To this end, note that the second conjunct of ${GH}_{ns}^{a}$ is $\begin{matrix} (\forall^{st} γ^{1}) (\forall F^{2}) [(\forall α^{1}) (γ (\overline{α} F (α)) > 0) \to (\forall^{st} s^{0}) (\forall N \in Ω) (\hat{G} (γ_{F}, s, N) = Γ (γ_{F}, s))], \end{matrix}$ where $γ_{F}^{2}$ is $(λ α^{1}) [γ (\overline{α} F (α)) - 1]$ . Clearly, the quantifiers ‘ $(\forall^{st} s^{0}) (\forall N \in Ω)$ ’ can be pushed outside to obtain a formula of the form $(\forall^{st} γ^{1}, s^{0}) (\forall N \in Ω) A (γ, s, N, Γ)$ , where A is internal. Applying underspill, we obtain $\begin{matrix} (4.46) & (\forall^{st} γ^{1}, s^{0}) (\exists^{st} n^{0}) (\forall N ⩾ n) A (γ, s, N, Γ), \end{matrix}$ which is the normal form of the second conjunct of ${GH}_{ns}^{a}$ . The normal form of the first conjunct of the latter is now obtained similarly. The normal form of $Π_{1}^{0} - TRANS$ is (4.42), and applying the template in Remark 3.5 yields (4.45). In particular, in the course of applying step (ii) of the template, (4.46) is transformed into $\begin{matrix} (\exists^{st} Ψ^{2}) (\forall γ^{1}, s^{0}) (\forall N ⩾ Ψ (γ, s)) A (γ, s, N, Γ), \end{matrix}$ and writing out A in full again, we obtain: $\begin{matrix} (\exists^{st} Ψ^{2}) (\forall γ^{1}, s^{0}) (\forall N ⩾ Ψ (γ, s)) (\forall F^{2}) [(\forall α^{1}) (γ (\overline{α} F (α)) > 0) \to \hat{G} (γ_{F}, s, N) = Γ (γ_{F}, s)] . \end{matrix}$ Rearranging the universal quantifiers, the previous formula is $(\exists^{st} Ψ^{2}) {GHS}^{a} (Ψ, Γ)$ by Notation 4.25, which is exactly as required for obtaining (4.45). □

By studying the proof of Theorem 4.26 in more detail, one observes that ‘Γ is standard’ in ${GH}_{ns}^{a}$ is superfluous. Repeating the proof of Corollary 4.27 with this modification, one obtains (4.45) where the term only depends on Ψ.

Next, we study a variation of ${GH}_{ns}^{a}$ based on [22]. In the latter, a number of effective equivalences between arithmetical comprehension and uniform theorems from the Reverse Mathematics zoo [6] are extracted from nonstandard equivalences involving $Π_{1}^{0} - TRANS$ and standard extensionality. Thus, we are led to the following: $\begin{array}{l} ({GH}_{ns 2}^{a}) & (\exists^{st} Γ^{3}) [(\forall^{st} γ^{1} \in C) (\forall s^{0}) GH (Γ, γ, s) \land (\forall^{st} γ^{1}, ε^{1} \in C, s^{0}) (γ \approx_{1} ε \to Γ (γ, s) =_{0} Γ (ε, s)], \end{array}$ which expresses that the Gandy–Hyland functional is standard extensional similar to ${(E)}^{st}$ defined in Remark 2.11. Note that $Π_{1}^{0} - TRANS$ immediately yields standard extensionality ${(E)}^{st}$ from ‘usual’ extensionality ( E ) for standard functionals of type two. The reverse implication is again more interesting.
Theorem 4.28.
The system $P$ proves ${GH}_{ns 2}^{a} \to Π_{1}^{0} - TRANS$ .
Proof.
As in the proof of Theorem 4.26, suppose $(\exists^{st} α_{0}^{1}) (\forall^{st} N) γ_{0} (\overline{α} N) = 0$ for some fixed standard $γ_{0}^{1} \in C$ . Let $γ^{1} \in C$ be as in (4.44) and recall that $Γ (γ, ⟨ \cdot ⟩) = 0$ by the proof of Theorem 4.26. Now define standard $ε^{1} \in C$ as: $\begin{matrix} (4.47) & ε (σ) : = \{\begin{matrix} 2 + σ ((μ n ⩽ | σ |) γ_{0} (\overline{α_{0}} n) \neq 0) & (\exists n ⩽ | σ |) γ_{0} (\overline{α_{0}}) \neq 0 \\ 0 & otherwise . \end{matrix} \end{matrix}$ Note that $ε (α) = 1 + α (m_{0})$ where $m_{0}$ is the least m such that $γ_{0} (\overline{α} m) \neq 0$ . Clearly, we have that $γ \approx_{1} (00 \dots) \approx_{1} ε$ , while at the same time we can compute: $\begin{matrix} (4.48) & Γ (ε, ⟨ \cdot ⟩) = ε (0 * (λ n) Γ (ε, n + 1)) = 1 + Γ (ε, m_{0}) \neq 0 = Γ (γ, ⟨ \cdot ⟩), \end{matrix}$ where $m_{0}$ is again the least m such that $γ_{0} (\overline{α} m) \neq 0$ . This contradiction yields ${NPC}^{a}$ and hence $Π_{1}^{0} - TRANS$ by Theorem 4.23. □

Recall the notion of ‘extensionality functional’ from Section 2.4 and define: $\begin{matrix} ({EXT}^{a} (Ξ^{2}, Λ^{3})) & (\forall γ^{1} \in C, ε^{1} \in C) (\overline{γ} Ξ (γ, ε) =_{0} \overline{ε} Ξ (γ, ε) \to Λ (γ) =_{0} Λ (ε)) . \end{matrix}$
Corollary 4.29 (Term extraction VII).

From the proof of ${GH}_{ns 2}^{a} \to Π_{1}^{0} - TRANS$ in $P$ , a term t can be extracted such that ${E-PA}^{ω *} + {QF-AC}^{1, 0}$ proves that $\begin{matrix} (4.49) & (\forall Ξ^{2}, Γ^{3}) [[{GH}^{a} (Γ) \land (\forall s^{0}) {EXT}^{a} (Ξ (\cdot, s), Γ (\cdot, s))] \to MU (t (Ξ, Γ))] . \end{matrix}$

Proof.
Analogous to the proof of Corollary 4.27. We again show that Notation 4.25 does not cause problems for term extraction as in Remark 3.5. First of all, the second conjunct of ${GH}_{ns}^{a} 2$ is, by Notation 4.22 and Remark 2.11: $\begin{array}{l} (\forall^{st} γ^{1}, ε^{1}) (\forall F^{2}, H^{2}) [(\forall α^{1}) (γ (\overline{α} F (α)) > 0) \land (\forall α^{1}) (ε (\overline{α} H (α)) > 0) \\ (4.50) & \to (\forall^{st} s^{0}) (\exists^{st} N) (\overline{γ} N =_{0} \overline{ε} N \to Γ (γ_{F}, s) =_{0} Γ (ε_{F}, s)], \end{array}$ where $γ_{F}^{2}$ is $(λ α^{1}) [γ (\overline{α} F (α)) - 1]$ , and similar for $ε_{F}^{2}$ . Now, (4.50) can be brought into the form $(\forall^{st} γ^{1}, ε^{1}, s^{0}) (\forall F^{2}, H^{2}) (\exists^{st} N) A (γ, ε, F, H, N, s)$ , where A is internal. Applying idealisation I as in Remark 3.12 yields: $\begin{matrix} (4.51) & (\forall^{st} γ^{1}, ε^{1}, s^{0}) (\exists^{st} N) (\forall F^{2}, H^{2}) A (γ, ε, F, H, N, s) . \end{matrix}$ After applying step (ii) from the template in Remark 3.5, (4.51) becomes $\begin{matrix} (\exists^{st} Φ^{2}) (\forall s^{0}) (\forall γ^{1}, ε^{1}) (\forall F^{2}, H^{2}) A (γ, ε, F, H, Φ (s, γ, ε), s), \end{matrix}$ which can be brought into $(\exists^{st} Ξ^{2}) (\forall s^{0}) {EXT}^{a} (Ξ (\cdot, s), Γ (\cdot, s))$ , by Notation 4.25. A normal form for the first conjunct of ${GH}_{ns 2}^{a}$ is now straightforward, while a normal form for $Π_{1}^{0} - TRANS$ is given by (4.42). The template from Remark 3.5 is now easily seen to yield the relative computability result (4.49). □

Following the proof of Theorem 4.28 in detail, it becomes clear that the condition ‘Γ is standard’ is superfluous, implying that the term in (4.49) only depends on Ξ.

The previous results are not satisfactory since extensionality for associates as in ${EXT}^{a}$ does not ‘fully’ treat $γ^{1}, ε^{1} \in C$ as type two functionals. However, the proof of Theorem 4.28 does provide us with an interesting way forward; In particular, it is easy to compute that $Γ (ε, ⟨ \cdot ⟩)$ from (4.48) is nonstandard. However, this means that Γ is nonstandard for standard inputs, while standard functionals (should) have standard output for standard input. Thus, we are led to the final variation of ${GH}_{ns}^{a}$ : $\begin{array}{l} ({GH}_{ns 3}^{a}) & (\exists Γ^{3}) & [(\forall^{st} γ^{1} \in C) (\forall s^{0}) GH (Γ, γ, s) \land (\forall^{st} ε^{1} \in C) (\forall^{st} t^{0}) ({st}_{0} (Γ (ε, t)))] . \end{array}$ which merely expresses that the Gandy–Hyland functional exists and is standard for standard input. As expected, $Π_{1}^{0} - TRANS$ implies ${GH}_{ns 3}^{a}$ but the reverse implication is again more interesting.
Theorem 4.30.
The system $P$ proves ${GH}_{ns 3}^{a} \to Π_{1}^{0} - TRANS$ .
Proof.
Assume ${GH}_{ns 3}^{a}$ ; As in the proof of Theorem 4.28, suppose $(\exists^{st} α_{0}^{1}) (\forall^{st} N) γ_{0} (\overline{α} N) = 0$ for some fixed standard $γ_{0}^{1} \in C$ , and define standard $ε^{1} \in C$ as in (4.47). Again note that $ε (α) = 1 + α (m_{0})$ where $m_{0}$ is the least m such that $γ_{0} (\overline{α} m) \neq 0$ . Now compute $Γ (ε, ⟨ \cdot ⟩)$ as follows: $Γ (ε, ⟨ \cdot ⟩) = ε (0 * (λ n) Γ (ε, n + 1)) = 1 + Γ (ε, m_{0})$ and $\begin{array}{l} Γ (ε, m_{0}) = ε (m_{0} * 0 * (λ n) Γ (ε, m_{0} * (n + 1))) = 1 + Γ (γ, m_{0} * (m_{0} - 1)) \end{array}$ Similarly, we have $Γ (ε, m_{0} * (m_{0} - 1)) = 1 + Γ (ε, m_{0} * (m_{0} - 1) * (m_{0} - 2))$ , and hence $Γ (ε, ⟨ \cdot ⟩) = 2 + Γ (ε, m_{0} * (m_{0} - 1) * (m_{0} - 2))$ . Ultimately, we obtain $\begin{matrix} (4.52) & Γ (ε, ⟨ \cdot ⟩) = \dots = (m_{0} - 1) + Γ (ε, m_{0} * (m_{0} - 1) * \dots * 1), \end{matrix}$ by applying the same procedure $m_{0} - 1$ times. However, $Γ (ε, ⟨ \cdot ⟩)$ is thus nonstandard, and this contradiction yields ${NPC}^{a}$ , and $Π_{1}^{0} - TRANS$ follows by Theorem 4.23. □
Corollary 4.31 (Term extraction VIII).

From the proof of ${GH}_{ns 3}^{a} \to Π_{1}^{0} - TRANS$ in $P$ , a term t can be extracted such that ${E-PA}^{ω *} + {QF-AC}^{1, 0}$ proves that $\begin{matrix} (4.53) & (\forall Γ^{3}, Ξ^{2}) [[{GH}^{a} (Γ) \land (\forall γ^{1} \in C, s^{0}) (Ξ (γ, s) =_{0} Γ (γ, s))] \to MU (t (Ξ))] . \end{matrix}$

Proof.
Analogous to Corollary 4.27 and 4.29. We show that Notation 4.25 does not cause problems for term extraction as in Remark 3.5. First of all, the second conjunct of ${GH}_{ns 3}^{a}$ is: $\begin{matrix} (\forall^{st} ε^{1}) (\forall F^{2}) [(\forall α^{1}) (ε (\overline{α} F (α)) > 0) \to (\forall^{st} t^{0}) (\exists^{st} n^{0}) (n = Γ (ε_{F}, t))], \end{matrix}$ where $ε_{F}^{2}$ is $(λ α^{1}) [ε (\overline{α} F (α)) - 1]$ . Push all standard quantifiers outside: $\begin{matrix} (\forall^{st} ε^{1}, t^{0}) (\forall F^{2}) (\exists^{st} n^{0}) [(\forall α^{1}) (ε (\overline{α} F (α)) > 0) \to (n = Γ (ε_{F}, t))], \end{matrix}$ and apply idealisation I to obtain: $\begin{matrix} (\forall^{st} ε^{1}, t^{0}) (\exists^{st} m) (\forall F^{2}) (\exists n^{0} ⩽ m) [(\forall α^{1}) (ε (\overline{α} F (α)) > 0) \to (n = Γ (ε_{F}, t))], \end{matrix}$ which is a normal form, which we abbreviate $(\forall^{st} ε^{1}, t^{0}) (\exists^{st} m) A (ε, t, m, Γ)$ , where A is internal. A normal form for $Π_{1}^{0} - TRANS$ is (4.42), which we abbreviate by $(\forall^{st} f^{1}) (\exists^{st} n^{0}) B (f, n)$ , where B is internal. Hence, ${GH}_{ns 3}^{a} \to Π_{1}^{0} - TRANS$ implies: $\begin{matrix} [(\exists Γ^{3}) [{GH}^{a} (Γ) \land (\forall^{st} ε^{1}, t^{0}) (\exists^{st} m) A (ε, t, m, Γ)]] \to (\forall^{st} f^{1}) (\exists^{st} n^{0}) B (f, n), \end{matrix}$ by strengthening the antecedent (by dropping ‘st’ in the first conjunct of ${GH}_{ns 3}^{a}$ ). Now introduce a standard functional $Ξ^{2}$ as follows: $\begin{matrix} (\forall^{st} Ξ^{2}) (\forall Γ^{3}) [[{GH}^{a} (Γ) \land (\forall^{st} ε^{1}, t^{0}) A (ε, t, Ξ (ε, t), Γ)] \to (\forall^{st} f^{1}) (\exists^{st} n^{0}) B (f, n)], \end{matrix}$ and drop the remaining ‘st’ in the antecedent to yield: $\begin{matrix} (\forall^{st} Ξ^{2}) (\forall Γ^{3}) [[{GH}^{a} (Γ) \land (\forall ε^{1}, t^{0}) A (ε, t, Ξ (ε, t), Γ)] \to (\forall^{st} f^{1}) (\exists^{st} n^{0}) B (f, n)] . \end{matrix}$ Push outside the standard quantifiers (as far as possible) to obtain $\begin{matrix} (\forall^{st} Ξ^{2}, f^{1}) (\forall Γ^{3}) (\exists^{st} n^{0}) [[{GH}^{a} (Γ) \land (\forall ε^{1}, t^{0}) A (ε, t, Ξ (ε, t), Γ)] \to B (f, n)], \end{matrix}$ to which we apply idealisation I (as in Remark 3.12) to obtain $\begin{matrix} (\forall^{st} Ξ^{2}, f^{1}) (\exists^{st} n^{0}) (\forall Γ^{3}) [[{GH}^{a} (Γ) \land (\forall ε^{2}, t^{0}) A (ε, t, Ξ (ε, t), Γ)] \to B (f, n)] . \end{matrix}$ Applying Corollary 2.9 now yields a term u such that ${E-PA}^{ω } + {QF-AC}^{1, 0}$ proves $\begin{matrix} (\forall Ξ^{2}, f^{1}) (\exists n^{0} \in u (Ξ, f)) (\forall Γ^{3}) [[{GH}^{a} (Γ) \land (\forall ε^{1}, t^{0}) A (ε, t, Ξ (ε, t), Γ)] \to B (f, n)] . \end{matrix}$ Now define $t (Ξ, f) : = {max}_{i < | u (Ξ, f) |} u (Ξ, f) (i)$ and note that we have $\begin{matrix} (\forall Ξ^{2}, f^{1}, Γ^{3}) [[{GH}^{a} (Γ) \land (\forall ε^{1}, t^{0}) A (ε, t, Ξ (ε, t), Γ)] \to B (f, t (Ξ, f))], \end{matrix}$ due to the monotone behaviour of $B (f, \cdot)$ . Furthermore, ‘ $(\forall f^{1})$ ’ can be pushed inside to obtain that $\begin{matrix} (4.54) & (\forall Ξ^{2}, Γ^{3}) [[{GH}^{a} (Γ) \land (\forall ε^{1}, t^{0}) A (ε, t, Ξ (ε, t), Γ)] \to MU (t (Ξ))] . \end{matrix}$ Finally, we note that $(\forall ε^{1}, t^{0}) A (ε, t, Ξ (ε, t))$ is implied by $(\forall ε^{1} \in C, t^{0}) (Ξ (ε, t) = Γ (ε, t))$ by Notation 4.25. Thus, (4.54) implies (4.53), and we are done. □

In conclusion, (4.53) expresses that a term from Gödel’s $T$ yields arithmetical comprehension as in $(μ^{2})$ from any functional $Ξ^{2}$ which computes the values of the Gandy–Hyland functional Γ defined on associates. Thus, it can be said that (4.53) is the syntactic version of (the forward implication of) the theorem (LN) as in [15], Theorem 9.5.4, p. 460. Of course, the latter theorem is formulated with partial functionals, while all functionals in $P$ are total. We show in the next section that $P$ can ‘simulate’ partiality relative to the standard world*; We also argue that this ‘standard partiality’ explains the results in this section.
5. Concluding remarks

In this paper, we have shown that certain theorems from Nonstandard Analysis give rise to (effective) relative computability results. This resonates nicely with the longstanding (but speculative) claim that Nonstandard Analysis is somehow ‘constructive’ or ‘effective’, captured well by the quote:

It has often been held that Nonstandard Analysis is highly non-constructive, thus somewhat suspect, depending as it does upon the ultrapower construction to produce a model [ $\dots$ ] On the other hand, nonstandard praxis is remarkably constructive; having the extended number set we can proceed with explicit calculations. (Emphasis original: [1], p. 31)

Similar observations regarding the ‘constructive or effective content of Nonstandard Analysis’ are made in numerous places; An incomplete list may be found in [23], Section 1. The results in this paper can be said to make the aforementioned speculative claim regarding the effective content of Nonstandard Analysis more concrete.

By contrast, the following final remark is somewhat vague and speculative, but partially explains the connection between the totality of the Gandy–Hyland functional mentioned in [15], Theorem 9.5.4, p. 460 and Corollary 4.31.

Remark 5.1 (Partiality in $P$ ).

The class of partial computable functions is a central object of study in computability theory ([25], I.2.2). As discussed in the latter, there are good reasons to study partial functions. We now discuss how $P$ can accommodate partial functionals, despite all functionals being total. Intuitively speaking, we show that a total computable function with standard index can output nonstandard numbers for standard input (after running for nonstandard many steps). Such a total function may rightly be called ‘not total from the point of view of the standard world’ in view of the basic axioms of $P$ . More formally:

First of all, consider the well-known predicate ‘ $φ_{e, s}^{A} (n) = m$ ’ which intuitively states that: ‘the eth Turing machine with oracle set A and input n halts after s steps with output m’ ([25], Def. 3.8). Now let $e_{0}, x_{0}$ be standard numbers and A a standard set such that $(\exists s^{0}, m^{0}) [φ_{e_{0}, s}^{A} (x_{0}) = m]$ , i.e. we say that ‘ $φ_{e_{0}}^{A} (x_{0})$ ’ is defined in the usual computability-theoretic terminology.

Secondly, the basic axioms of $P$ in Definition 2.5 guarantee that every standard functional evaluated at a standard input returns a standard output. By contrast, without the presence of $Π_{1}^{0} - TRANS$ , $φ_{e_{0}}^{A} (x_{0})$ as defined above7

⁷

Assume $\neg Π_{1}^{0} - TRANS$ and let $h^{1}$ be as in the proof of Theorem 4.23; Define $e_{0}$ as the (standard) code of the program which tests if the input $x_{0}$ satisfies $x_{0} \in A : = {n : h (n) \neq 0}$ and outputs $x_{0}$ if so, and repeats the previous step for $x_{0} + 1$ otherwise. Then $φ_{e_{0}, m_{0}}^{A} (x_{0}) = m_{0}$ , if $m_{0}$ is the least number such that $h (m_{0}) \neq 0$ , while the inputs $A, e_{0}, x_{0}$ are standard.

may well be nonstandard. In other words, while

φ_{e_{0}}^{A} (x_{0})

is defined and all inputs are standard, the

e_{0} th

Turing machine may well take a nonstandard number s of steps to halt, with a nonstandard output m, as discussed in Footnote 7.

Thirdly, in light of the previous, we are led to the following definition: For standard $e_{0}, x_{0}, A$ , we say that ‘ $φ_{e_{0}}^{A} (x_{0})$ is standard-defined’ if $(\exists^{st} s^{0}, m^{0}) [φ_{e_{0}, s}^{A} (x_{0}) = m]$ , and ‘standard-undefined’ otherwise. Similarly, for standard $e_{0}, A$ , we say that ‘ $φ_{e_{0}}^{A}$ is standard-total’ if we have $(\forall^{st} x_{0}) (\exists^{st} s^{0}, m^{0}) [φ_{e_{0}, s}^{A} (x_{0}) = m]$ , and ‘standard-partial’ otherwise. Hence, define $ψ_{e}^{A}$ as follows for fixed $M \in Ω$ : $\begin{matrix} ψ_{e}^{A} (x) : = \{\begin{matrix} φ_{e}^{A} (x) & (\exists s^{0}, m^{0} ⩽ M) [φ_{e, s}^{A} (x) = m] \\ M + 1 & otherwise . \end{matrix} \end{matrix}$ By definition, $ψ_{e}^{A}$ is total but not standard-total in the presence of $\neg Π_{1}^{0} - TRANS$ by Footnote 7. Hence, we can in fact simulate the concept of partiality inside $P$ by exploiting the dichotomy between ‘standard’ and ‘nonstandard’. Similar definitions are possible for higher-type functionals.

Finally, we arrive at the motivation for the definitions in the previous remark: Consider the standard associates $γ^{1} \in C$ and $ε^{1} \in C$ as in (4.39) and (4.47); To compute $γ (α)$ at standard $α^{1}$ , one simply evaluates $γ (\overline{α} 0)$ , $γ (\overline{α} 1)$ , et cetera, until $N^{0}$ is found such that $γ (\overline{α} N) > 0$ , and the same for $ε^{1} \in C$ . This computation always terminates by the definition of $ε^{1} \in C$ and $γ^{1} \in C$ . However, in the presence of $\neg Π_{1}^{0} - TRANS$ , this computation only terminates after a nonstandard number of steps, i.e. $γ^{1} \in C$ and $ε^{1} \in C$ are ‘standard-partial’ in the above sense. However, ${NPC}^{a}$ implies that every standard $γ^{1} \in C$ is standard-total (as it is nonstandard continuous), and therefore $Π_{1}^{0} - TRANS$ follows from ${NPC}^{a}$ ; In fact, we have an equivalence by Theorem 4.23. In short, ${NPC}^{a}$ guarantees that every standard associate is standard-total, which apparently requires $Π_{1}^{0} - TRANS$ , and the latter becomes $(μ^{2})$ after term extraction by Corollary 4.24.

Furthermore, assuming that the Γ-functional has its usual defining property ${GH}^{a} (Γ)$ on associates, we observe that given $\neg Π_{1}^{0} - TRANS$ , the number $Γ (ε, ⟨ \cdot ⟩)$ is nonstandard, although $ε^{1} \in C$ and $⟨ \cdot ⟩$ are standard inputs, i.e. Γ is also ‘standard partial’ (see the proof of Theorem 4.30 for these results). However, ${GH}_{ns 3}^{a}$ guarantees that there is a standard-total Gandy–Hyland functional defined on associates, and therefore $Π_{1}^{0} - TRANS$ follows, as in Theorem 4.30. In short, ${GH}_{ns 3}^{a}$ guarantees that the Gandy–Hyland functional is standard-total for standard associates and standard sequences, which apparently requires $Π_{1}^{0} - TRANS$ .

In conclusion, we have introduced the notion of ‘standard partiality’ which allows $P$ to accommodate the fundamental notion of ‘partial function(al)’. We have observed that ${NPC}^{a}$ as in Theorem 4.23 and ${GH}_{ns 3}^{a}$ as in Theorem 4.30 can be viewed as principles guaranteeing the standard-totality of (functionals defined on) standard associates. It is an interesting question whether we can fruitfully translate other theorems from computability theory regarding partial function(al)s.

Footnotes

Acknowledgements

This research was sponsored by the John Templeton Foundation, the FWO Flanders, the University of Oslo, and the Alexander von Humboldt Foundation. The author is grateful to these institutions for their support. This work was done partially while the author was visiting the Institute for Mathematical Sciences, National University of Singapore in 2016. The visit was supported by the Institute. The author thanks Dag Normann and Paulo Oliva for their valuable advice. Finally, the referees of this paper deserve thanks for their many helpful suggestions.

References

Albeverio,

Høegh-Krohn,

J.E.

Fenstad and

Lindstrøm, Nonstandard Methods in Stochastic Analysis and Mathematical Physics, Pure and Applied Mathematics, Vol. 122, Academic Press, 1986, xii + 514.

M.J.

Beeson, Foundations of Constructive Mathematics, Ergebnisse der Mathematik und Ihrer Grenzgebiete, Vol. 6, Springer, 1985, Metamathematical studies, xxiii + 466.

Berger and

Oliva, Modified bar recursion and classical dependent choice, in: LC01, Lect. Notes Log., Vol. 20, 2005, pp. 89–107.

Berger and

Oliva, Modified bar recursion, Math. Structures Comput. Sci. 16(2) (2006), 163–183. doi:10.1017/S0960129506005093.

S.R.

Buss, An introduction to proof theory, in: Handbook of Proof Theory, Stud. Logic Found. Math., Vol. 137, North-Holland, Amsterdam, 1998, pp. 1–78.

D.D.

Dzhafarov, Reverse Mathematics Zoo. Available at http://rmzoo.uconn.edu/.

Y.L.

Ershov, Model C of partial continuous functionals, in: Logic Colloquium 76, Studies in Logic and Foundations in Math., Vol. 87, North-Holland, 1977, pp. 455–467.

Escardó,

Oliva and

Powell, System T and the product of selection functions, in: Computer Science Logic 2011, LIPIcs. Leibniz Int. Proc. Inform., Vol. 12, Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2011, pp. 233–247.

Escardó and

Xu, The inconsistency of a Brouwerian continuity principle with the Curry–Howard interpretation, in: 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), Leibniz International Proceedings in Informatics (LIPIcs), Vol. 38, 2015, pp. 153–164.

10.

Gandy and

Hyland, Computable and recursively countable functions of higher type, in: Logic Colloquium, Studies in Logic and Found. Math., Vol. 87, North-Holland, 1977, pp. 407–438.

11.

Gödel, Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes, Dialectica 12 (1958), 280–287. doi:10.1111/j.1746-8361.1958.tb01464.x.

12.

Kohlenbach, Foundational and mathematical uses of higher types, in: Reflections on the Foundations of Mathematics (Stanford, CA, 1998), Lect. Notes Log., Vol. 15, ASL, 2002, pp. 92–116.

13.

Kohlenbach, Higher order reverse mathematics, in: Reverse Mathematics 2001, Lect. Notes Log., Vol. 21, ASL, 2005, pp. 281–295.

14.

Kohlenbach, Applied Proof Theory: Proof Interpretations and Their Use in Mathematics, Springer Monographs in Mathematics, Springer, Berlin, 2008, xx + 532.

15.

Longley and

Normann, Higher-Order Computability, Theory and Applications of Computability, Springer, 2015.

16.

Nelson, Internal set theory: A new approach to Nonstandard Analysis, Bull. Amer. Math. Soc. 83(6) (1977), 1165–1198. doi:10.1090/S0002-9904-1977-14398-X.

17.

Normann, Recursion on the Countable Functionals, LNM, Vol. 811, Springer, 1980, viii + 191.

18.

Normann, Characterizing the continuous functionals, J. Symbolic Logic 48(4) (1983), 965–969.

19.

Normann,

Palmgren and

Stoltenberg-Hansen, Hyperfinite type structures, J. Symbolic Logic 64(3) (1999), 1216–1242. doi:10.2307/2586626.

20.

Normann and

Sanders, Nonstandard Analysis, Computability Theory, and their connections, 2017. Submitted. Available at https://arxiv.org/abs/1702.06556.

21.

Robinson, Non-Standard Analysis, North-Holland, Amsterdam, 1966, xi + 293.

22.

Sanders, Taming the Reverse Mathematics zoo, 2014. Submitted. Available at http://arxiv.org/abs/1412.2022.

23.

Sanders, The unreasonable effectiveness of Nonstandard Analysis, 2015. Submitted. Available at http://arxiv.org/abs/1508.07434.

24.

S.G.

Simpson, Subsystems of Second Order Arithmetic, 2nd edn, Perspectives in Logic, CUP, 2009, xvi + 444.

25.

R.I.

Soare, Recursively Enumerable Sets and Degrees, Perspectives in Mathematical Logic, Springer, 1987, xviii + 437.

26.

A.S.

Troelstra, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics, Vol. 344, Springer, Berlin, 1973, xv + 485.

27.

van den Berg,

Briseid and

Safarik, A functional interpretation for nonstandard arithmetic, Ann. Pure Appl. Logic 163(12) (2012), 1962–1994. doi:10.1016/j.apal.2012.07.003.

28.

van den Berg and

Sanders, Transfer equals Comprehension, 2014. Available at http://arxiv.org/abs/1409.6881.