On the Cantor–Bendixson rank of a set that is searchable in Gödel’s T

Abstract

We prove that if a closed subset X of the Baire space is searchable in the sense of Escardó [Logical Methods in Computer Science 4(3) (2008), 3], and by a functional definable in Gödel’s $T$ , then X is countable, and the Cantor–Bendixson rank of X is bounded by the ordinal $ε_{0}$ . To this end we introduce evaluation trees, well founded decorated trees that induce operators from the full set-theoretical class $N^{N} \to N$ to $N^{N}$ . We prove that when a search operator for a set X is induced from an evaluation tree T, then the Cantor–Bendixson rank of X is bounded by the Kleene–Brouwer order type of T. Further we use a theorem due to Howard [Journal of Symbolic Logic 45(3) (1980), 493–504], estimating the ordinal complexity of the reduction tree of a term in system $T$ , to show that all functionals of type $(N^{N} \to N) \to N^{N}$ definable in $T$ can be computed using an evaluation tree of ordinal rank below $ε_{0}$ .

Keywords

Searchable Cantor–Bendixson rank

1. Introduction

In this paper, we will give partial answers to the following question:

Let X be a set. Assuming that there is a procedure Φ that to a predicate P on X decides if P is empty on X or not, what can we say about X?

The question is not very precise, and in order to turn it into a mathematical problem we have to specify:

What kind of sets X will we consider?

What do we mean with a “procedure”?

Will we consider all predicates or just a natural collection of them?

If X is a finite set ${x_{1}, \dots, x_{n}}$ , the answer will be that as long as we allow for using oracle calls $P (x_{i})$ in our model for procedures, whatever this model of procedures might be, we can decide if P is empty on X or not.

If X is infinite, a procedure will essentially have to take a function $\begin{matrix} P : X \to {0, 1} \end{matrix}$ as an input, and then give one of the two values 0 or 1 as the output, so the procedure will itself be an object of type level 2 over X. This suggests that various models for computing with functionals will be of interest when we make our problem precise. When nothing else is said, we will let X be a compact subset of Baire space $N^{N}$ . X is then a topological space, and we will either let P range over all functions from X to ${0, 1}$ or, as in Section 4, the continuous ones.

Escardó [5] defined the concepts of searchable and exhaustible sets originally for continuous models of $LCF$ [15] (or equivalently $PCF$ [14]). We will discuss this in more detail below. Later he also considered these concepts as induced by the computational model of Gödel’s $T$ [7]. Our main concern will be with searchable sets modulo $T$ , but we will also consider an intermediate model, Kleene’s S1–S9 [9]. We will let $T$ and S1–S9 have their standard interpretations over the full set-theoretical type structure.

For a detailed introduction to higher order computability, one may consult the forthcoming [12]. Here we will give brief introductions to $PCF$ , to Kleene’s S1–S9 and to the calculus we are mainly interested in, Gödel’s $T$ .

1.1. Background

The Kleene schemes S1–S9 and the corresponding concept of computability was originally defined for the full type-structure of pure types, and it is a calculus that gives meaning to expressions like $\begin{matrix} {e} (Φ_{1}, \dots, Φ_{n}) = a . \end{matrix}$

Here e may be viewed as a Gödel number of an algorithm, $Φ_{1}, \dots, Φ_{n}$ will range over the functionals of some pure, finite types (coded into e) in the full set-theoretical type structure and a is a non-negative integer. S1–S9 are nine clauses in a grand strictly positive inductive definition of the set of sequences $(e, Φ_{1}, \dots, Φ_{n}, a)$ such that ${e} (Φ_{1}, \dots, Φ_{n}) = a$ . However, Kleene’s definition will also make sense in other reasonably closed type structures of total or partial functionals, and the strength of this model of computability will strongly depend on the typed structure it is interpreted in.

The Kleene–Kreisel continuous functionals were essentially and independently defined in Kleene [10] and Kreisel [11]. There are numerous characterizations of this typed structure. The one being most useful for our purpose is via the partial continuous functionals. We define the typed structure of partial continuous functionals over the integers within the category of Scott–Ershov domains, as initiated in Scott [15]. We then isolate the hereditarily total objects in this structure with the canonical equivalence relation of extensional equivalence. The equivalence classes will correspond to the Kleene–Kreisel continuous functionals.

In his seminal, but for a long time, unpublished note [15], Scott introduced the formal calculus $LCF$ , which was later transformed into a programming language $PCF$ by Plotkin [14]. $PCF$ is a formal calculus without reference to any particular model, and may be viewed as a typed λ-calculus with least fixed point operators of all types. The partial continuous functionals will serve as a model for $PCF$ , and in this model $PCF$ and S1–S9 have the same computational power. An element of the corresponding equivalence class will be a representative of a functional. We say that a Kleene–Kreisel functional is $PCF$ -definable if there is a representative of it among the partial continuous functionals that is the interpretation of a $PCF$ -term. Normann [13] proved that if a Kleene–Kreisel functional has a representative that can be approximated by a computably enumerable set of finitary elements of the Scott–Ershov domain, then it is $PCF$ -definable. This also means that there is a representative that is S1–S9-computable in the model of partially computable functionals. This is seemingly in contrast to the theorem in Tait [17], where it is proved that the fan functional (see discussion later) is not Kleene computable, but fortunately, only seemingly.

Martín Escardó [5] introduced searchable and exhaustible sets in the framework of $PCF$ , the partial continuous functionals and the Kleene–Kreisel continuous functionals. A set X of Kleene–Kreisel functionals is searchable in the original sense of Escardó if there is a $PCF$ -definable operator ε such that whenever P is a continuous function mapping X into ${0, 1}$ then $ε (P) \in X$ and $\begin{matrix} \exists x \in X (P (x) = 1) ⟺ P (ε (P)) = 1 . \end{matrix}$

Escardó proved that all searchable sets are compact and that there are close analogies between being non-empty and compact and being searchable. In particular he proved an effective analogue of the Tychonoff’s theorem for countable products of searchable sets. He also considered searchable sets of hereditarily total functionals in the Scott-domains, but this will not be of relevance to us.

An important source of inspiration for Escardó’s work was a theorem due to Berger [1]:

There is a $PCF$ -definable representative for the fan functional.

The fan functional is a Kleene–Kreisel functional of pure type 3. We will let

C = {0, 1}^{N}

be our version of the Cantor set. C is compact, so every continuous functional F of type 2 will be uniformly continuous on F. This again means that there is a uniform modulus n of continuity, i.e., if

f, g \in C

agrees on

0, \dots, n - 1

, then

F (f) = F (g)

. The fan functional Φ “computes” the least such modulus of continuity. Φ has a computable representative, but Tait [17] proved that Φ is not computable in Kleene’s original calculus based on S1–S9. The key to the argument is that a Kleene algorithm with an input F of type 2 can only utilize F restricted to a countable set, while

Φ (F)

will need to know F on the full Cantor set C.

Berger [1] proved that the fan functional is $PCF$ -definable. According to private information from Martin Hyland, this was known to Robin Gandy, but not published. Simpson [16] used the methods of Berger to prove that there are $PCF$ -programs for Riemann integration and for computing the maximal value of a continuous function on a closed, bounded interval, in the sense of the model for exact computing with reals suggested by Di Gianantonio [2–4].

1.2. Searchability in weaker systems

1.2.1. System $T$

Our version of $T$ will be like this:

We consider all finite types over the base type 0. We write $\begin{matrix} σ = τ_{1}, \dots, τ_{n} \to 0 \end{matrix}$ for $σ = τ_{1} \to (\dots \to (τ_{n} \to 0) \dots)$ .

Our term language will be that of typed λ-calculus with extra constants $\hat{0}$ of type 0, successor suc of type $0 \to 0$ and recursors ${rec}_{σ}$ of types $0, σ, (0, σ \to σ) \to σ$ for each type σ. We write N, M, etc. for terms.

We will, by recursion, write $\hat{n + 1}$ for $suc \hat{n}$ . The terms $\hat{n}$ are called numerals.

The conversion rules will be the conversion rules of typed λ-calculus with α- and β-conversion $\begin{matrix} \begin{matrix} α : & λ x^{σ} . M ⇝ λ y . M [x / y], \\ β : & (λ x^{σ} . M) N ⇝ M [x / N], \end{matrix} \end{matrix}$ where we also accept conversion of subterms. We of course assume that all substitutions are legal.

We have standard conversion rules for the constants:

${rec}_{σ} \hat{0} M N ⇝ M$ ,

${rec}_{σ} \hat{n + 1} M N ⇝ N \hat{n} ({rec}_{σ} \hat{n} M N)$ .

We will let ⇝ be reflexive and transitive. We extend

T

T_{P}

by adding a new constant

\hat{P}

of type

(0 \to 0) \to 0

We will not add conversion rules for $\hat{P}$ directly, but for each instance P we may consider an infinitary P-rule: If M is a term of type $0 \to 0$ and $M \hat{m} ⇝ \hat{f (n)}$ for each $n \in N$ , then $\hat{P} M ⇝ \hat{P (f)}$ .

We finally say that a term M defines Φ of type $((0 \to 0) \to 0) \to 0$ if for every P and n, $Φ (P) = n$ if and only if $M ⇝ \hat{n}$ when we use the P-rule. We then say that Φ is $T$ -definable. These concepts extend trivially to functionals into $N^{N}$ .

1.2.2. The conjecture

Escardó [6] found examples of infinite, countable sets that are searchable by operators definable in System $T$ . The least ordinal > ω closed under addition, multiplication and exponentiation is known as $ε_{0}$ . For each ordinal $α < ε_{0}$ Escardó found a compact, well-ordered subset $X_{α}$ of the Cantor-space C of order type $β ⩾ α$ , such that X is searchable by a functional definable in $T$ . $T$ of course offers a weaker model of computability than $PCF$ , so it is remarkable that for these examples, the search algorithms will even work for all predicates, not just the continuous ones.

Escardó presented these results, later published in [6], at the workshop Types 2011 in September 2011. There he suggested that if a set X is searchable via an operator definable in $T$ , then X must be countable. He also mentioned the possibility of the Cantor–Bendixson rank of X to be bounded by the ordinal $ε_{0}$ and left this as an open problem. At a Dagstuhl workshop in October 2011 he presented his results again, this time actually conjecturing that $ε_{0}$ is an upper bound for the topological complexity of $T$ -searchable sets. The main result of this paper is that this conjecture is true.1

¹
The author had intense discussions with Escardó on this conjecture during the Dagstuhl meeting. In May–June of 2012 we met again, this time at the Newton Institute in Cambridge, UK in connection with the program SAS, and we continued our discussions with some further progress.

The technical breakthrough came during the autumn of 2012 and was due to the author. We decided, after some discussion, not to write a joint paper, but the influence of Escardó is important, both as a supplier of motivation and as a discussion partner.

1.2.3. This paper

In Sections 2 and 3 we prove that if X is searchable in $T$ with respect to all predicates on X, then the Cantor–Bendixson rank of X is bounded by $ε_{0}$ . In Section 2 we introduce the concept of an evaluation tree and, in the case where there is a search operator for all total predicates P on X computable using an evaluation tree, we show that the ordinal rank of the evaluation tree induces an ordinal bound on the Cantor–Bendixson rank of X.

In Section 3 we use a result by Howard [8] and show that when an operator of type 3 is $T$ -definable, then it is computable via an evaluation tree of rank < ε₀.

In Section 4 we strengthen the result from Section 2 by only assuming that the search algorithm of the evaluation tree works for predicates that are continuous on X. This section actually makes Section 2 obsolete, but we believe that the basic intuition is easier to see from the exposition in Section 2 than it would have been if the sharpest result had been proved directly.

It is also reasonable to ask when a set X may be searchable by a functional ε definable in Kleene’s S1–S9 interpreted in the classical way. If we assume that $X \subseteq N^{N}$ is closed and searchable with respect to all predicates that are continuous on X in this way, results of Escardó [5] give us that X is compact.

Employing the method of Tait [17] we can show that while deciding that the empty predicate O is empty on X, the computation tree of $ε (O)$ must make an oracle call $O (f) ?$ for each $f \in X$ . Thus X has to be countable, and there will actually be an effective enumeration $\begin{matrix} X = {f_{n} ∣ n \in N} \end{matrix}$ of the elements in X, an enumeration extractable from the computable, infinite and well-founded computation tree of $ε (O)$ . We say that $X \subseteq N^{N}$ is computably enumerable when there is a computable enumeration like this. It is an open problem whether it suffices that a set X is compact and computably enumerable for X to be searchable in the original sense of Kleene computability over the hereditarily total functionals.

For the sake of completeness, we will define the Cantor–Bendixson rank in the next section. Let us consider here the set A of pairs $(h, g)$ from $N^{N}$ where g codes a total ordering on a set $dom (g)$ , h maps $N$ onto $dom (g)$ , and for each $n \in N$ we have that $h (n) \in dom (g)$ has a rank in $dom (g)$ that equals the Cantor–Bendixson rank of $f_{n}$ in X. A will be an arithmetical set, and when $(h, g) \in A$ , g will code an ordinal exceeding the Cantor–Bendixson rank of X. Thus there is a $Σ_{1}^{1}$ -set of codes for well orderings where each well ordering bounds the Cantor–Bendixson rank of X. By standard descriptive set theory, this shows that the Cantor–Bendixson rank of X is a computable ordinal. Since there are no original technical aspects of this argument, we omit further details.

2. Sets that are searchable using evaluation trees

2.1. Preliminaries

It is well known that a countable, compact Hausdorff-space X is homeomorphic to the ordering topology of a countable successor ordinal. A familiar proof will use the Cantor–Bendixson rank, CB-rank, of the elements of X defined as follows:

If x is isolated in X, then $CB‐rank (x) = 0$ .

If $α > 0$ , we do not have that $CB‐rank (x) < α$ but there is a neighbourhood B of x such that $CB‐rank (y) < α$ for all $y \in B$ that are different from x, we let $CB‐rank (x) = α$ .

If X is a compact, countable Hausdorff space, each $x \in X$ will have a CB-rank. By sequential compactness, there will be an element with maximal CB-rank, and there can only be finitely many of those.

We will make use of the following observation. The proof will use sequential compactness, and the observation may serve as a student exercise in general topology.

Lemma 2.1.
Let X and Y be countable, compact Hausdorff-spaces, $ϕ : X \to Y$ be continuous and surjective.

For each $y \in Y$ there is an $x \in X$ such that $\begin{matrix} ϕ (x) = y and CB‐rank (x) ⩾ CB‐rank (y) . \end{matrix}$

In this paper, a tree will be a set of finite sequences from $N$ , closed under sub-sequences. The empty sequence e will be the root of the tree. The elements of the tree are called nodes.

A subtree of a tree T will be a subset that is also a tree. If $s \in T$ , the child tree of s is the set of sequences t such that the concatenation $s t \in T$ . In the notation for concatenation, we will identify a number with the corresponding sequence of length 1.

A branch in a tree will be the set of subsequences of some node in the tree. We will not assume that a branch necessarily ends in a leaf node, but of course it may do so.

Let $<_{l}$ be the following partial variant of the lexicographical ordering on the set of finite sequences: $\begin{matrix} a_{0} \dots a_{n - 1} <_{l} b_{0} \dots b_{m - 1} if there is an i < min {n, m} such that a_{i} < b_{i} and a_{j} = b_{j} for all j < i . \end{matrix}$

Let $s ≺ t$ if s is a proper subsequence of t and let $s ⪯ t$ if s is just a subsequence of t. We sometimes write “left of” for $<_{l}$ .

We will use the Kleene–Brouwer ordering $<_{KB}$ of the set of finite sequences from $N$ defined as follows: $s <_{KB} t$ if $t ≺ s$ or if $s <_{l} t$ . We let $⩽_{KB}$ be the reflexive counterpart. The Kleene–Brouwer ordering is a total ordering. The key property is that a tree T is well founded if and only if the Kleene–Brouwer ordering well-orders T. A well-founded tree will have ordinal rank < ε₀ if and only if the Kleene–Brouwer ordering of the tree has length < ε₀.

Our trees will for the most be decorated, meaning that we attach some mathematical object to each node in the tree.
2.2. Evaluation trees

Our tool for investigating the Cantor–Bendixson rank of sets searchable in weak systems will be evaluation trees.

Definition 2.2.
An evaluation tree will be a well founded, decorated tree T of finite sequences s from $N$ satisfying:
A node s in T is either a leaf node in T, or a full branching node, i.e. the nth successor $s n \in T$ for all $n \in N$ .

If s is a leaf node, then it is decorated with a function $f_{s} \in N^{N}$ .

If s is a branching node, it will be decorated with a continuous functional $F_{s} : N^{N} \to N^{N}$ .

Definition 2.3.
If T is an evaluation tree as above, $P : N^{N} \to N$ and $s \in T$ , we let ${[[s]]}_{T} (P) \in N^{N}$ be defined by transfinite recursion as follows:
If s is a leaf node then ${[[s]]}_{T} (P) = f_{s}$ .

If s is a branching node, we let ${[[s]]}_{T} (P) = F_{s} (λ n . P (f_{s n}))$ .
We will normally drop the lower index T when it is clear from the context.

2.3. The main theorem

This section is devoted to the proof our main technical result.

Theorem 2.4.
Let $X \subseteq N^{N}$ be closed. Let T be an evaluation tree such that $\begin{matrix} P \mapsto {[[e]]}_{T} (P) \end{matrix}$ is a search operator for X (where e still denotes the empty sequence).

Then X is countable, and the Cantor–Bendixson rank of the elements of X are bounded by the rank of the Kleene–Brouwer ordering of T.
Proof.
We will split the proof into several lemmas, where we assume that X and T are as in the theorem. Our intuition is that in order to define a search operator, T must implicitly search through X for an f satisfying P, and, when at a node in T finds an f satisfying P, this information is brought to the top. In this section we turn this intuition, restricted to one-point predicates, into the definition of being a relevant node. Our construction will be non-constructive, because we cannot tell in an effective way which are the nodes in T actually contributing to ${[[e]]}_{T}$ being a search operator and which nodes are just dummy ones.

We will let O denote the everywhere zero function on $N^{N}$ and for $f \in X$ we will let $\begin{matrix} P_{f} (g) = \{\begin{matrix} 1 & if f = g, \\ 0 & if f \neq g . \end{matrix} \end{matrix}$ Note that we will have that $[[e]] (P_{f}) = f$ for all $f \in X$ . Definition 2.5.
A node $s \in T$ is relevant for $f \in X$ if $[[t]] (P_{f}) = f$ for all $t ⪯ s$ . A node s in T is critical for $f \in X$ if it is ⪯-maximal among the set of nodes relevant for f.

The set of nodes s in T that are relevant for $f \in X$ will form a subtree $T_{f}$ , and the leaf nodes of $T_{f}$ will be the nodes that are critical for f.

Since e is relevant for all $f \in X$ , there will be at least one critical node for each $f \in X$ . Lemma 2.6.
Let $f \in X$ and let s be critical for f.

Then $f = [[s]] (O)$ .
Proof.
If s is a leaf node, we have that $[[s]] (O) = f_{s} = [[s]] (P_{f}) = f$ , where the last equation follows from the assumption of the lemma.

If s is a branching node, we have that $[[s n]] (P_{f}) \neq f$ for each $n \in N$ , and thus $\begin{matrix} [[s]] (O) = F_{s} (λ n . O ([[s n]] (O))) = F_{s} (λ n . P_{f} ([[s n]] (P_{f}))) = [[s]] (P_{f}) = f . \end{matrix}$ This ends the proof. □

This shows in particular that X must be countable.

For each $s \in T$ , we now let $R (s)$ be the set of $f \in X$ such that s is on the leftmost branch in $T_{f}$ .2
²
In Section 4 we will just assume that X is searchable by T with respect to continuous predicates. We will then modify our proof and also define an alternative to $R (s)$ .

We let $T^{}$ be the set of nodes s for which $R (s) \neq \emptyset$ . $T^{}$ will be a subtree of T, and the Kleene–Brouwer ordering on $T^{}$ will be a sub-ordering of the Kleene–Brouwer ordering of T. Our aim will be to construct a surjective map ϕ from $T^{}$ onto X that is continuous with respect to the order topology of the Kleene–Brouwer ordering of $T^{}$ . Since the order topology of $T^{}$ will be compact, X is compact. We then use Lemma 2.1 to obtain the theorem.

Observe that if $s ⪯ t \in T^{}$ , then $R (t) \subseteq R (s)$ . Lemma 2.7.
If $t \in T^{}$ , $t n_{i} \in T^{}$ for each* $i \in N$ , ${lim}_{i \to \infty} n_{i} = \infty$ and $f_{i}$ is in the closure of $R (t n_{i})$ for each $i \in N$ , then
$[[t]] (O) = {lim}_{i \to \infty} f_{i}$ ,

$[[t]] (O)$ is in the closure of $R (t)$ .

Proof.
(ii) is a consequence of (i) and the fact that the closure of $R (t n_{i})$ is a subset of the closure of $R (t)$ for each $i \in N$ . In order to prove (i) it is sufficient to assume that $f_{i} \in R (t n_{i})$ for each $i \in N$ .

The point of selecting the leftmost path is that if $n < n_{i}$ , then $[[t n]] (P_{f_{i}}) \neq f_{i}$ , so $P_{f_{i}} ([[t n]] (P_{f_{i}})) = 0$ when $n < n_{i}$ .

It follows that $\begin{matrix} [[t]] (O) = F_{t} (λ n .0) = lim_{i \to \infty} F_{t} (λ n . [[t n]] (P_{f_{i}})) = lim_{i \to \infty} [[t]] (P_{f_{i}}) = lim_{i \to \infty} f_{i} . \end{matrix}$ This ends the proof of the lemma. □

We now define $ϕ (t)$ for $t \in T^{}$ as follows:
$ϕ (t) = [[t]] (O)$ if $[[t]] (O)$ is in the closure of $R (t)$ .

$ϕ (t) \in R (t)$ is arbitrary otherwise.
Lemma 2.8.
ϕ is continuous and onto X, when* $T^{}$ has the order topology of the Kleene–Brouwer ordering on* $T^{}$ .
Proof.
ϕ will be surjective because when t is the leftmost node critical for f we have that $f = ϕ (t)$ .

Let $t \in T^{}$ . We will prove that ϕ is continuous in the point t. If t is an isolated point in the order topology, there is nothing to prove, so assume that t is a cluster point. It suffices to prove continuity with respect to sequences ${t_{i}}_{i \in N}$ where each $t_{i}$ is a proper extension of t, since any sequence of points different from t, but converging to t, will consist almost everywhere of extensions of t.

Then, for each $i \in N$ there is an $n_{i}$ such that $t_{i}$ extends $t n_{i}$ , and we will have that ${lim}_{i \to \infty} n_{i} = \infty$ .

Since $ϕ (t_{i})$ is in the closure of $R (t_{i})$ we have, by monotonicity of R, that $ϕ (t_{i})$ is in the closure of $R (t n_{i})$ , and also in the closure of $R (t)$ .

By Lemma 2.7 we see that $[[t]] (O) = {lim}_{i \to \infty} ϕ (t_{i})$ and thus that $[[t]] (O)$ is in the closure of $R (t)$ . Then $ϕ (t) = [[t]] (O)$ , and ϕ is continuous with respect to this sequence. Since continuity is equivalent to sequential continuity in this case, this proves that ϕ is continuous. □

This ends the proof of Theorem 2.4. □

2.4. Pre-evaluation trees

In Section 3 we will prove that whenever a functional Φ of type $((0 \to 0) \to 0) \to (0 \to 0)$ is definable in Gödel’s $T$ , then there is an evaluation tree of rank less than $ε_{0}$ that computes Φ. We will use a theorem from Howard [8], where he proves that a specific tree related to a term for Φ has rank < ε₀. The tree we naturally obtain from Howard’s analysis will be what we call a pre-evaluation tree. In this section we will define this concept and see that each pre-evaluation tree can be transformed to an evaluation tree with the same effect without increasing the rank.

Definition 2.9.

An even pre-evaluation tree will be a well founded decorated tree T of finite sequences of natural numbers such that:

If $t \in T$ has an even length, then $t n \in T$ for all $n \in N$ , and there is no decoration.

If $t \in T$ has an uneven length, the decoration will be a pair $(I_{t}, F_{t})$ where $I_{t} \subseteq N$ and $F_{t} : (I_{t} \to N) \to N$ is continuous.

If $t \in T$ has an uneven length, then $t n \in T \Leftrightarrow n \in I_{t}$ .

An uneven pre-evaluation tree will be like an even one, except that we switch even for uneven and vice versa in the definition.

If T is an even/uneven pre-evaluation tree, $t \in T$ and F is of pure type 2 we define $[[t]] (F) \in N$ if the length of t is uneven/even and $[[t]] (F) \in N^{N}$ if the length of t is even/uneven as follows:

$[[t]] (F) = F_{t}$ ( $λ n \in I_{t} . [[t n]] (F)$ ) when the length of t is uneven/even.

$[[t]] (F) = λ n . [[t n]] (F)$ if the length of t is even/uneven.

Given two trees T and S that either are evaluation or even pre-evaluation trees, we say that they are equivalent if $λ F . [[e]] (F)$ is the same function for the two trees.

Remark 2.1.
For even trees, the leaf nodes will be nodes s of uneven length where $I_{s} = \emptyset$ . We may then identify $F_{s}$ with an integer.
Lemma 2.10.
For every even pre-evaluation tree T of ordinal rank α there is an equivalent evaluation tree $T^{}$ of rank* $⩽ α$ .
Proof.
The proof is by transfinite induction over T, but otherwise trivial. Note that we do not require the construction of $T^{}$ from T to be effective, and for our applications, it would be irrelevant to do so.

The induction base is when e has no extensions of even length in T.

Then $I_{n} = \emptyset$ for all n, and $F_{n}$ is just a number $a_{n}$ . Then e will be the one and only node in $T^{}$ . We let e be decorated with $λ n . a_{n}$ .

The induction step is when $I_{n} \neq \emptyset$ for at least one n.

Let ${n_{i} m_{i}}_{i \in N}$ be a surjective enumeration of all sequences $n m$ in T of length 2, and for each $i \in N$ we let $T_{i}$ be the child tree of $n_{i} m_{i}$ .

Bringing the decoration along, $T_{i}$ will be an even pre-evaluation tree for $λ F . [[n_{i} m_{i}]] (F)$ . Let $T_{i}^{}$ be the equivalent evaluation tree for each i, and let $T^{}$ consist of e, all sequences i of length one, and all sequences $i s$ where $s \in T_{i}^{}$ .

We bring with us all decorations from each $T_{i}^{}$ and ad a decoration $F_{e}$ that we describe informally:

In order to compute $F_{e} (f) (n)$ let $\begin{matrix} J_{n} = {i ∣ n_{i} = n \land m_{i} \in I_{n} \land \forall j < i (n_{j} \neq n \lor m_{j} \neq m_{i})} . \end{matrix}$

Then f restricted to $J_{n}$ will induce a map $g : I_{n} \to N$ . We let $F_{e} (f) (n) = F_{n} (g)$ . Since each $F_{n}$ is continuous, $F_{e}$ will be continuous.

The verifications of the remaining properties are now trivial. □

3. Applications to Gödel’s $T$

As mentioned in the Introduction, our aim is to show that if a set X is searchable with an algorithm expressible in Gödel’s $T$ , then the Cantor–Bendixson rank of X is strictly bounded by the ordinal $ε_{0}$ . Using Theorem 2.4 it will be sufficient to prove that if X is searchable in this way, this search can be carried out by an evaluation tree of ordinal rank below $ε_{0}$ . We will use results from Howard [8] to establish the ordinal bound, and we will be brief when explaining how we obtain a tree from a term in $T$ .

We will prove that if Φ is $T$ -definable and of type $\begin{matrix} ((0 \to 0) \to 0) \to (0 \to 0) \end{matrix}$ then there is an evaluation tree for Φ of ordinal rank < $ε_{0}$ .

Definition 3.1.
Let M be a term in $T$ , possibly with free variables.

The Howard tree of M will be the tree of finite sequences of terms where M is at the top node and branching is generated by the following definition of successor. In all cases except (8) the term of which we define the successors will be of type 0, we assume that everything is well typed and that necessary uses of α-conversions are implicit:
If M is a numeral, then M is a leaf node.

If $M = (λ x M_{1}) N_{1} \dots N_{k}$ then $M_{1} (x / N_{1}) N_{2} \dots N_{k}$ is the one successor.

If $M = {rec}_{σ} \hat{0} N_{2} N_{3} \dots N_{k}$ then $N_{2} N_{4} \dots N_{k}$ is the one successor.

If $M = {rec}_{σ} \hat{n + 1} N_{2} N_{3} \dots N_{k}$ then $(N_{3} \hat{n} ({rec}_{σ} \hat{n} N_{2} N_{3})) N_{4} \dots N_{k}$ is the one successor.

If $M = {rec}_{σ} N_{1} \dots N_{k}$ where $N_{1}$ is not a numeral, then $N_{1}$ is a successor ( $N_{1}$ will be of type 0) and ${rec}_{σ} \hat{n} N_{2} \dots N_{k}$ are successors for each $n \in N$ .

If $M = suc N$ then N is the one successor.

If M is of the form $Z N_{1} \dots N_{k}$ where Z is a variable, then the successors are $N_{1}, \dots, N_{k}$ .

If M is a term of type $\neq 0$ , then the successors will be all $M N_{1} \dots N_{k}$ where each $N_{i}$ either is a variable or a numeral.

Theorem 3.2 (Howard [8]).

The Howard tree will always be well founded.

Moreover, for each $n \in N$ there is an ordinal $α_{n} < ε_{0}$ such that for each term M with all subterms having types of level $< n$ , the Howard tree will have rank $< α_{n}$ .

We refer to the original paper [8] for the proof.

Our situation will not be as general as this. The terms we consider will have one free variable $\hat{P}$ at the most. Then (7) will reduce to the case $\hat{P} N$ where the successor will be N.

The successors of N will be all terms $N x$ , where x is a variable of type 0, and $N \hat{n}$ for each n. Our reduced Howard tree will be the one where we only consider successors $N \hat{n}$ to terms N of type $0 \to 0$ . These reduced trees will of course also satisfy Theorem 3.2.

Theorem 3.3.
Let Φ of type $((0 \to 0) \to 0) \to (0 \to 0)$ be definable in Gödel’s $T$ .

Then there is an evaluation tree of rank < ε₀ computing Φ .
Proof.
By Lemma 2.10 it is sufficient to produce an even pre-evaluation tree.

Let $\hat{P}$ be a variable of type $(0 \to 0) \to 0$ and let $M_{0}$ with at most the variable $\hat{P}$ free be such that $M_{0}$ defines Φ. We will need uneven pre-evaluation trees for the terms $M_{0} \hat{n}$ for each n in order to produce the even pre-evaluation tree for Φ, and in order to prove their existence we give a general construction.

Let M be an arbitrary term of type 0 with only $\hat{P}$ free and let H be the reduced Howard tree of M. The construction of the uneven pre-evaluation tree will be by the same cases as the definition of H, where some of the cases are treated together:
If M is a numeral $\hat{n}$ , we let $I_{e} = \emptyset$ and $F_{e}$ be the constant n.

If M is of cases (2), (3) or (4) in Definition 3.1, let $M_{1}$ be the immediate successor and we use the uneven pre-evaluation tree for $M_{1}$ .

If $M = suc M_{1}$ and $H_{1}$ is the reduced Howard tree of $M_{1}$ , we let our pre-evaluation tree for M be constructed from $H_{1}$ , except that we increase the values of $F_{e}$ with 1.

If M is of case (5), the pre-evaluation tree will be constructed as a kind of amalgamation of the pre-evaluation trees of $N_{1}$ and each ${rec}_{σ} \hat{n} N_{2} \dots N_{k}$ . Let J be the set of immediate successors of e and let G be the evaluation function for e in the tree for $N_{1}$ . Let $I_{n}$ , $F_{n}$ be the corresponding items for ${rec}_{σ} \hat{n} N_{2}, \dots, N_{k}$ .

We imbed J and the $I_{n}$ ’s into disjoint sets $J^{'}$ and $I_{n}^{'}$ in $N$ , and let I be the union, where p and $q_{n}$ are the injective maps.

We let the child tree of $m \in J$ in our tree for $N_{1}$ now be the child tree of $p (m)$ , and likewise we transport child trees of $m \in I_{n}$ to child trees of $q_{n} (m) \in I$ . If $f : I \to N$ we compute $F (f)$ as follows: Let $n = G (p^{- 1} (f))$ and then let $F (f) = G_{n} (F_{n} (q_{n}^{- 1} (f)))$ . This F will be our new $F_{e}$ .

If $M = \hat{P} N$ , the successors two steps down will be all terms of the form $N \hat{n}$ . This is where the reduction of the Howard tree comes in. Our pre-evaluation tree will now have a branching to all n and the node n is continued with the pre-evaluation tree constructed from the reduced Howard tree of the term $N \hat{n}$ .
It now follows by an easy transfinite induction on the reduced Howard tree that the uneven pre-evaluation tree will compute the number that is the value of M. □

4. Search with respect to continuous predicates only

In this section we will still let T be an evaluation tree for a search operator on a closed set $X \subseteq N^{N}$ , but we will only assume that $[[e]]$ is a search operator on X with respect to predicates P that are continuous on X.

The main result of the section will be that the CB-rank of X is still bounded by the Kleene–Brouwer order type of T. The idea and structure of the proof is like our proof of Theorem 2.4 with an adjusted definition of the predicate R.

We will let s, t range over nodes in T. We let Σ be the set of finite sequences with extensions in X. We let σ, possibly with indices, range over Σ. We will consider σ to be a finite partial function, so an expression like $f = {lim}_{n \to \infty} σ_{n}$ will make sense. Our argument will work for all compact sets $X \subseteq N^{N}$ , but to ease the use of notation, we let $X \subseteq {0, 1}^{N}$ . Violating standard terminology, we let $\bar{f} (n)$ denote the sequence ( $f (0), \dots, f (n - 1)$ ), and not the sequence number of this sequence.

We let $\begin{matrix} B_{σ} = {f \in X ∣ σ ≺ f} \end{matrix}$ and we let $P_{σ}$ be the characteristic function of $B_{σ}$ restricted to X. As before, we let O denote the constant zero function on X, the characteristic function of the empty predicate. We let P, possibly with an index, denote a continuous predicate on X given as a characteristic function.

We will now redefine some concepts from the proof of Theorem 2.4 and prove the analogue lemmas and theorem.

Definition 4.1.
Let P be a non-empty continuous predicate on X, $s \in T$ .

s is relevant for P if $P ([[t]] (P)) = 1$ for all $t ⪯ s$ .

We say that s is leftmost relevant for P if s is on the leftmost branch in T consisting of t’s that are relevant for P.

We say that s is critical for P if s is relevant for P and there is no $k \in N$ such that $s k$ is relevant for P.

We observe that if s is relevant for P and s is a leaf node in T, then s is critical for P. We also observe that e is relevant for all non-empty continuous predicates P. This is a consequence of the assumption that $[[e]]$ is a search operator for X. Thus there will be a leftmost path of relevant nodes for P ending in a node that is critical for P.
Lemma 4.2.
If s is critical for P, then $P ([[s]] (O)) = 1$ .
Proof.
The proof is essentially the same as the proof of Lemma 2.6. □

We now define the alternative $R^{+}$ of R.
Definition 4.3.
Let $t \in T$ . Let $f \in R^{+} (t)$ if t is leftmost relevant for $P_{\bar{f} (n)}$ for infinitely many $n \in N$ .

Let $\begin{matrix} T^{+} = {t \in T ∣ R^{+} (t) \neq \emptyset} . \end{matrix}$
Lemma 4.4.
Let $s \in T$ be a branching node. Let $k_{n} \in N$ and $σ_{n} \in Σ$ for each $n \in N$ . Assume that $s k_{n}$ is leftmost relevant for $P_{σ_{n}}$ for each $n \in N$ .

Assume further that ${lim}_{n \to \infty} k_{n} = \infty$ .

Then $\begin{matrix} [[s]] (O) = lim_{n \to \infty} σ_{n} . \end{matrix}$
Proof.
$[[s]] (O) = F_{s} (λ k .0)$ .

By the assumption $\begin{matrix} P_{σ_{n}} ([[s k]] (P_{σ_{n}})) = 0 \end{matrix}$ for $k < k_{n}$ so since ${lim}_{n \to \infty} k_{n} = \infty$ we have that $\begin{matrix} λ k .0 = lim_{n \to \infty} λ k . P_{σ_{n}} ([[s k]] (P_{σ_{n}})) . \end{matrix}$ Then, since $F_{s}$ is continuous, $\begin{matrix} [[s]] (O) = lim_{n \to \infty} F_{s} (λ k . P_{σ_{n}} ([[s k]] (P_{σ_{n}}))) = lim_{n \to \infty} [[s]] (P_{σ_{n}}) . \end{matrix}$

Since $s ≺ s k_{n}$ for all n we have that s is relevant for each $P_{σ_{n}}$ , so $σ_{n} ≺ [[s]] (P_{σ_{n}})$ .

Finally we observe that since there are only finitely many σ of a fixed length and each $k_{n}$ can be repeated at most a finite number of times, the lengths of the $σ_{n}$ ’s will converge to ∞. □

The claim of the lemma now follows.
Lemma 4.5.
If $f \in X$ , there is a node $s \in T^{+}$ such that $f \in R^{+} (s)$ and $[[s]] (O) = f$ .
Proof.
We know that $f \in R^{+} (e)$ since e is (leftmost) relevant for all continuous predicates.

Since $T^{+}$ is well founded it is sufficient to prove that if $f \in R^{+} (s)$ then either $f = [[s]] (O)$ or $f \in R^{+} (s k)$ for some k.

So assume that $f \in R^{+} (s)$ and that $f \neq [[s]] (O)$ .

Let ${n_{i}}_{i \in N}$ be an increasing sequence such that s is leftmost relevant for $P_{\bar{f} (n_{i})}$ for each $i \in N$ . For each $i \in N$ we have that either is s critical for $P_{\bar{f} (n_{i})}$ (which will be the case when s is a leaf node) or there is some $k_{i}$ such that $s k_{i}$ is leftmost relevant for $P_{\bar{f} (n_{i})}$ .

If s is critical for $P_{\bar{f} (n_{i})}$ , we use Lemma 4.2 and see that $\bar{f} (n_{i}) ≺ [[s]] (O)$ . Since we assumed that $f \neq [[s]] (O)$ this can only be the case for finitely many $i \in N$ , so for all but finitely many $i \in N$ there is a leftmost $k_{i}$ such that $s k_{i}$ is relevant for $P_{\bar{f} (n_{i})}$ .

If ${k_{i} ∣ i \in N}$ is unbounded we may find a strictly increasing subsequence ${k_{i_{j}}}_{j \in N}$ and then, by Lemma 4.2, we have that $\begin{matrix} f = lim_{j \to \infty} \bar{f} (n_{i_{j}}) = [[s]] (O), \end{matrix}$ contradicting our assumption.

Thus ${k_{i} ∣ i \in N}$ is bounded, and there will be one number k and a subsequence ${n_{i_{j}}}_{j \in N}$ of ${n_{i}}_{i \in N}$ such that $k_{i_{j}} = k$ for all $j \in N$ .

Then $f \in R^{+} (s k)$ . This ends the proof of the lemma. □

We now let $ϕ : T^{+} \to X$ be defined as before:
$ϕ (s) = [[s]] (O)$ if $[[s]] (O)$ is in the closure of $R^{+} (s)$ .

$ϕ (s) \in R^{+} (s)$ is chosen arbitrarily otherwise.
As before we have that $\begin{matrix} t ⪯ s ⟹ R^{+} (s) \subseteq R^{+} (t) \end{matrix}$ and then, by construction, we have that $ϕ (t)$ is in the closure of $R^{+} (s)$ whenever $s ⪯ t$ .

By Lemma 4.5 we have that ϕ is surjective. We will prove that ϕ is continuous, and draw our main consequence as before.
Lemma 4.6.
Let $s \in T^{+}$ , let $s k_{i} \in T^{+}$ for each $i \in N$ .

Assume that ${lim}_{i \to \infty} k_{i} = \infty$ and let $f_{i}$ be in the closure of $R^{+} (s k_{i})$ for each $i \in N$ .

Then $\begin{matrix} [[s]] (O) = lim_{i \to \infty} f_{i} . \end{matrix}$
Proof.
It is sufficient to assume that $f_{i} \in R^{+} (s k_{i})$ for each i.

Let ${n_{i}}_{i \in N}$ be a strictly increasing sequence from $N$ such that $s k_{i}$ is leftmost relevant for $P_{{\bar{f}}_{i} (n_{i})}$ for each i. The existence of this sequence follows from the definition of $R^{+}$ .

By Lemma 4.2 we have that $\begin{matrix} [[s]] (O) = lim_{i \to \infty} \bar{f} (n_{i}) = lim_{i \to \infty} f_{i} . \end{matrix}$ This ends the proof of the lemma. □
Lemma 4.7.
The function ϕ is continuous.
Proof.
The proof is as the proof of Lemma 2.8. □

We now have everything we need to prove the following theorem. Theorem 4.8.
Let $X \subseteq {0, 1}^{N}$ be closed and assume that there is an evaluation tree T such that for all continuous predicates P on X we have that $\begin{matrix} \exists f \in X (P (f) = 1) ⟺ P ([[e]] (P)) = 1 . \end{matrix}$ Then X is countable, and the Cantor–Bendixson rank of X is bounded by the Kleene–Brouwer order type of the tree T.

5. Concluding remarks

5.1. Summary

We have been investigating the topological nature of sets in $N^{N}$ that are searchable via an operator definable in Gödel’s $T$ . Howard [8] showed how terms in $T$ give rise to computation trees of rank less than $ε_{0}$ , and we have transformed his trees to what we called evaluation trees. The main technical result is that if a set X is searchable for all predicates on X with the aid of an evaluation tree, then the rank of the Kleene–Brouwer ordering bounds the Cantor–Bendixson rank of X. It is sufficient to assume that this holds for continuous predicates on X.

We also discussed the consequence of X being searchable in the sense of Kleene’s original S1–S9.

5.2. Related problems

Our proof is non-constructive, even from the point of view of classical logic, since there are no algorithms for constructing the trees $T^{*}$ and $T^{+}$ used in the proofs. Thus our proofs do not say much about the internal structure of searchable sets beyond the bounds on the Cantor–Bendixson rank. We are nowhere near a characterization of when a closed set may be searchable in $T$ , neither with respect to continuous predicates nor with respect to all predicates.

Problem 5.1.

If X is $T$ -searchable with respect to continuous predicates, is X then $T$ -searchable with respect to all predicates?

The problem may not be so interesting in itself, but a positive solution will probably give us more information about the structure of search algorithms. We may ask a similar question for searchability by evaluation trees.

We also discussed briefly what can be said about a set X that is searchable in S1–S9, and concluded that X is computably enumerable and compact. We sketched an argument showing that when X is compact and computably enumerable, then the Cantor–Bendixson rank of X is a computable ordinal.

The natural problem here is if we can characterize all sets $X \subseteq N^{N}$ that are S1–S9-searchable in Kleene’s original sense. It is easy by the methods developed in Escardó [6] to prove that we for every computable ordinal α can find a set X searchable in this sense and with a CB-rank exceeding α. We know that if X is a S1–S9-searchable subset of the Cantor space, then X is closed, computably enumerable and the set of neighbourhoods containing elements from X is decidable. It is not likely that these properties are sufficient for proving the converse. The problem will be to find some informative characterization of the compact sets X that are S1–S9-searchable.

The following problem is also open.

Problem 5.2.

Assume that X is S1–S9-searchable. Is X then searchable by a computable evaluation tree?

The search operators constructed by Escardó [5,6] do not just provide an element of each non-empty set, they search through all the elements of X (or a dense subset of X when we only consider continuous predicates) until they find an element satisfying P, and then this element will be the output. This behaviour cannot be described as a denotational property of the search operator, but it is tempting to look for further properties of search operators that might be used to analyse when a set e.g. is sequentially searchable. One possible such property is the following monotonicity property: $\begin{matrix} If e (P) = f \in P and f \in Q \subseteq P then e (Q) = f . \end{matrix}$

We believe that the concept of searchability must be strengthened if we want to deduce further properties of the operational semantics from the denotational interpretation of a search operator and the mere fact that it is definable in some given calculus.

Footnotes

Acknowledgements

During the research for this note, I had, as explained in footnote , important and valuable discussions with Martín Escardó. To a large extent these discussions took place at the Isaac Newton Institute for Mathematical Sciences in Cambridge, England. I am grateful to the Institute for hosting the program Semantics and Syntax: A Legacy of Alan Turing and for inviting me to take part in this program. During this stay, I also benefited from discussions with the proof theorists Arnold Beckmann, Anton Setzer and Monica Seisenberger.

An anonymous referee gave valuable feedback on the exposition.

References

[1]

Berger, Totale Objekte und Mengen in der Bereichtheorie, PhD thesis, München, 1990 (in German).

[2]

Di Gianantonio, A functional approach to computability on real numbers, PhD thesis, Università di Pisa, Genova, Udine, 1993.

[3]

Di Gianantonio, Real number computability and domain theory, Information and Computation 127 (1996), 11–25.

[4]

Di Gianantonio, An abstract data type for real numbers, Theoretical Computer Science 221 (1999), 295–326.

[5]

M.H.

Escardó, Exhaustible sets in higher-type computation, Logical Methods in Computer Science 4(3) (2008).

[6]

M.H.

Escardó, Infinite sets that satisfy the principle of omniscience in all varieties of constructive mathematics, Journal of Symbolic Logic 78(3) (2013), 764–784.

[7]

Gödel, Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes, Dialectica 12 (1958), 280–287.

[8]

W.A.

Howard, Ordinal analysis of terms of finite type, Journal of Symbolic Logic 45(3) (1980), 493–504.

[9]

S.C.

Kleene, Recursive functionals and quantifiers of finite types I, Transactions of the American Mathematical Society 91(1) (1959), 1–52.

10.

[10]

S.C.

Kleene, Countable functionals, in: Constructivity in Mathematics,

Heyting, ed., North-Holland, 1959, pp. 81–100.

11.

[11]

Kreisel, Interpretation of analysis by means of functionals of finite type, in: Constructivity in Mathematics,

Heyting, ed., North-Holland, 1959, pp. 101–128.

12.

[12]

J.R.

Longley and

Normann, Higher-Order Computability, Springer, to appear.

13.

[13]

Normann, Computability over the partial continuous functionals, Journal of Symbolic Logic 65(3) (2000), 1133–1142.

14.

[14]

G.D.

Plotkin, LCF considered as a programming language, Theoretical Computer Science 5(3) (1977), 223–255.

15.

[15]

D.S.

Scott, A type-theoretical alternative to ISWIM, CUCH, OWHY, Unpublished manuscript, Oxford, 1969.

16.

[16]

A.S.

Simpson, Lazy functional algorithms for exact real functionals, in: Mathematical Foundations of Computer Science 1998, Lecture Notes in Computer Science, Vol. 1450, 1998, pp. 456–464.

17.

[17]

W.W.

Tait, Continuity properties of partial recursive functionals of finite type, Unpublished manuscript, 1958.