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 $\mathsf{T}$ , then X is countable, and the Cantor–Bendixson rank of X is bounded by the ordinal ${\mathit{\epsilon }}_0$ . To this end we introduce evaluation trees, well founded decorated trees that induce operators from the full set-theoretical class ${\mathbb{N}}^{\mathbb{N}}\to \mathbb{N}$ to ${\mathbb{N}}^{\mathbb{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 $\mathsf{T}$ , to show that all functionals of type $\mathrm{(}{\mathbb{N}}^{\mathbb{N}}\to \mathbb{N}\mathrm{)}\to {\mathbb{N}}^{\mathbb{N}}$ definable in $\mathsf{T}$ can be computed using an evaluation tree of ordinal rank below ${\mathit{\epsilon }}_0$ .