We study a version of the Vitali covering theorem, which we call WHBU and which is a direct weakening of the Heine-Borel theorem for uncountable coverings, called HBU. We show that WHBU is central to measure theory by deriving it from various central approximation results related to Littlewood's three principles. A natural question is then how hard it is to prove WHBU (in the sense of Kohlenbach's higher-order Reverse Mathematics), and how hard it is to compute the objects claimed to exist by WHBU (in the sense of Kleene's computation schemes S1-S9). The answer to both questions is ‘extremely hard’, as follows: on one hand, in terms of the usual scale of (conventional) comprehension axioms, WHBU is only provable using Kleene's ∃3, which implies full second-order arithmetic. On the other hand, realisers (aka witnessing functionals) for WHBU, so-called Λ-functionals, are computable from Kleene's ∃3, but not from weaker comprehension functionals. Despite this hardness, we show that WHBU, and certain Λ-functionals, behave much better than HBU and the associated class of realisers, called Θ-functionals. In particular, we identify a specific Λ-functional called ΛS which adds no computational power to the Suslin functional, in contrast to Θ-functionals. Finally, we introduce a hierarchy involving Θ-functionals and HBU.

Abstract Open sets are central to mathematics, especially analysis and topology, in ways few notions are. In most, if not all, computational approaches to mathematics, open sets are only studied indirectly via their ‘codes’ or ‘representations’. In this paper, we study how hard it is to compute, given an arbitrary open set of reals, the most common representation, i.e. a countable set of open intervals. We work in Kleene’s higher order computability theory, in particular its equivalent lambda calculus formulation due to Platek. We establish many computational equivalences between on one hand the ‘structure’ functional that converts open sets to the aforementioned representation, and on the other hand functionals arising from mainstream mathematics, like basic properties of semi-continuous functions, the Urysohn lemma and the Tietze extension theorem. We also compare these functionals with known operations on regulated and bounded variation functions, and the Lebesgue measure restricted to closed sets. We obtain a number of natural computational equivalences for the latter involving theorems from mainstream mathematics.

Abstract Reverse Mathematics (RM hereafter) is a program in the foundations of mathematics where the aim is to identify the minimal axioms needed to prove a given theorem from ordinary, i.e., non-set theoretic, mathematics. This program has unveiled surprising regularities: the minimal axioms are very often equivalent to the theorem over the base theory, a weak system of ‘computable mathematics’, while most theorems are either provable in this base theory, or equivalent to one of only four logical systems. The latter plus the base theory are called the ‘Big Five’ and the associated equivalences are robust following Montalbán, i.e., stable under small variations of the theorems at hand. Working in Kohlenbach’s higher-order RM, we obtain two new and long series of equivalences based on theorems due to Bolzano, Weierstrass, Jordan, and Cantor; these equivalences are extremely robust and have no counterpart among the Big Five systems. Thus, higher-order RM is much richer than its second-order cousin, boasting at least two extra ‘Big’ systems.

Abstract Cantor’s first set theory paper (1874) establishes the uncountability of ${\mathbb R}$ . We study this most basic mathematical fact formulated in the language of higher-order arithmetic. In particular, we investigate the logical and computational properties of ${\mathsf {NIN}}$ (resp. ${\mathsf {NBI}}$ ), i.e., the third-order statement there is no injection resp. bijection from $[0,1]$ to ${\mathbb N}$ . Working in Kohlenbach’s higher-order Reverse Mathematics, we show that ${\mathsf {NIN}}$ and ${\mathsf {NBI}}$ are hard to prove in terms of (conventional) comprehension axioms, while many basic theorems, like Arzelà’s convergence theorem for the Riemann integral (1885), are shown to imply ${\mathsf {NIN}}$ and/or ${\mathsf {NBI}}$ . Working in Kleene’s higher-order computability theory based on S1–S9, we show that the following fourth-order process based on ${\mathsf {NIN}}$ is similarly hard to compute: for a given $[0,1]\rightarrow {\mathbb N}$ -function, find reals in the unit interval that map to the same natural number.

Abstract We investigate the computational properties of basic mathematical notions pertaining to ${\mathbb R}\rightarrow {\mathbb R}$-functions and subsets of ${\mathbb R}$, like finiteness, countability, (absolute) continuity, bounded variation, suprema and regularity. We work in higher-order computability theory based on Kleene’s S1–S9 schemes. We show that the aforementioned italicised properties give rise to two huge and robust classes of computationally equivalent operations, the latter based on well-known theorems from the mainstream mathematics literature. As part of this endeavour, we develop an equivalent $\lambda $-calculus formulation of S1–S9 that accommodates partial objects. We show that the latter are essential to our enterprise via the study of countably based and partial functionals of type $3$.

Abstract The Axiom of Choice (${\textsf{AC}}$ for short) is the most (in)famous axiom of the usual foundations of mathematics, ${\textsf{ZFC}}$ set theory. The (non-)essential use of ${\textsf{AC}}$ in mathematics has been well-studied and thoroughly classified. Now, fragments of countable ${\textsf{AC}}$ not provable in ${\textsf{ZF}}$ have recently been used in Kohlenbach’s higher-order Reverse Mathematics to obtain equivalences between closely related compactness and local–global principles. We continue this study and show that ${\textsf{NCC}}$, a weak choice principle provable in ${\textsf{ZF}}$ and much weaker systems, suffices for many of these results. In light of the intimate connection between Reverse Mathematics and computability theory, we also study realisers for ${\textsf{NCC}}$, i.e. functionals that produce the choice functions claimed to exist by the latter, from the other data. Our hubris of undertaking the hitherto underdeveloped study of the computational properties of (choice functions from) ${\textsf{AC}}$ leads to interesting results. For instance, using Kleene’s S1-S9 computation schemes, we show that various total realisers for ${\textsf{NCC}}$ compute Kleene’s $\exists ^{3}$, a functional that gives rise to full second-order arithmetic, and vice versa. By contrast, partial realisers for ${\textsf{NCC}}$ should be much weaker, but establishing this conjecture remains elusive. By way of catharsis, we show that the Continuum Hypothesis (${\textsf{CH}}$ for short) is equivalent to the existence of a countably based partial realiser for ${\textsf{NCC}}$. The latter kind of realiser does not compute Kleene’s $\exists ^{3}$ and is therefore strictly weaker than a total one.

Abstract To enable the study of open sets in computational approaches to mathematics, lots of extra data and structure on these sets is assumed. For both foundational and mathematical reasons, it is then a natural question, and the subject of this paper, what the influence of this extra data and structure is on the logical and computational properties of basic theorems pertaining to open sets. To answer this question, we study various basic theorems of analysis, like the Baire category, Heine, Heine–Borel, Urysohn and Tietze theorems, all for open sets given by their (third-order) characteristic functions. Regarding computability theory, the objects claimed to exist by the aforementioned theorems undergo a shift from ‘computable’ to ‘not computable in any type 2 functional’, following Kleene’s S1–S9. Regarding reverse mathematics, the latter’s main question, namely which set existence axioms are necessary for proving a given theorem, does not have a unique or unambiguous answer for the aforementioned theorems, working in Kohlenbach’s higher-order framework. A finer study of representations of open sets leads to the new ‘$\varDelta$-functional’ that has unique (computational) properties.

Abstract We investigate the connections between computability theory and Nonstandard Analysis. In particular, we investigate the two following topics and show that they are intimately related. (T.1) A basic property of Cantor space $2^ $ is Heine–Borel compactness: for any open covering of $2^ $ , there is a finite subcovering. A natural question is: How hard is it to compute such a finite subcovering? We make this precise by analysing the complexity of so-called fan functionals that given any $G:2^ \to $ , output a finite sequence $\langle f_0 , \ldots ,f_n \rangle $ in $2^ $ such that the neighbourhoods defined from $\overline {f_i } G\left( {f_i } \right)$ for $i \le n$ form a covering of $2^ $ . (T.2) A basic property of Cantor space in Nonstandard Analysis is Abraham Robinson’s nonstandard compactness, i.e., that every binary sequence is “infinitely close” to a standard binary sequence. We analyse the strength of this nonstandard compactness property of Cantor space, compared to the other axioms of Nonstandard Analysis and usual mathematics. Our study of (T.1) yields exotic objects in computability theory, while (T.2) leads to surprising results in Reverse Mathematics. We stress that (T.1) and (T.2) are highly intertwined, i.e., our study is holistic in nature in that results in computability theory yield results in Nonstandard Analysis and vice versa.

The 12 papers in this special issue arose from the conference CiE 2006: Logical Approaches to Computational Barriers, held at the University of Wales Swansea in July, 2006. CiE 2006 was the second of a new series of conferences associated with the interdisciplinary network Computability in Europe. Computability in Europe (CiE) is an informal network of European scientists working on computability theory, including its foundations, technical development and applications. Among the aims of the network is to advance our theoretical understanding of what can and cannot be computed, by any means of computation. Its scientific vision is broad: computations may be performed with discrete or continuous data by all kinds of algorithms, programs and machines. Computations may be made by experimenting with any sort of physical system obeying the laws of a physical theory such as Newtonian mechanics, quantum theory or relativity. Computations may be very general, depending upon the foundations of set theory; or very specific, using the combinatorics of finite structures. CiE also works on subjects intimately related to computation, especially theories of data and information, and methods for formal reasoning about computations. The sources of new ideas and methods include practical developments in areas such as neural networks, quantum computation, natural computation, molecular computation, computational learning. Applications are everywhere, especially, in algebra, analysis and geometry, or data types and programming.

The ten papers in this special issue arose from the conference CiE 2005: New Computational Paradigms, held at the University of Amsterdam in June, 2005. CiE 2005 was the first of a new series of conferences associated with the interdisciplinary network Computability in Europe focused on computability in theoretical computer science and mathematical logic, and ranging over a broad spectrum of research areas from the application of novel approaches to computation, through computability-theoretic aspects of physical systems to set-theoretic analyses of infinitary computing models.

We show that the extensional ordering of the sequential functionals of pure type 3, for example, as defined via game semantics (Abramsky et al. 1994; Hyland and Ong 2000), is not cpo-enriched. This shows that this model does not equal Milner's (Milner 1977) fully abstract model for PCF.

In this paper we consider two hierarchies of hereditarily total and continuous functionals over the reals based on one extensional and one intensional representation of real numbers, and we discuss under which asumptions these hierarchies coincide. This coincidense problem is equivalent to a statement about the topology of the Kleene-Kreisel continuous functionals. As a tool of independent interest, we show that the Kleene-Kreisel functionals may be embedded into both these hierarchies.

Abstract We show that to every recursive total continuous functional Φ there is a PCF-definable representative Ψ of Φ in the hierarchy of partial continuous functionals, where PCF is Plotkin's programming language for computable functionals. PCF-definable is equivalent to Kleene's S1–S9-computable over the partial continuous functionals.

The notion of a hyperfinite set comes from nonstandard analysis. Such a set has the internal cardinality of a nonstandard natural number. By a transfer principle such sets share many properties of finite sets. Here we apply this notion to give a hyperfinite model of the Kleene-Kreisel continuous functionals. We also extend the method to provide a hyperfinite characterisation of certain transfinite type structures, thus, through the work of Waagbø [14], constructing a hyperfinite model for Martin-Löf type theory. This kind of application is not new. Normann [6] gave a characterisation of the Kleene-Kreisel continuous functionals using ‘hyperfinitary’ functionals. The novelty 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. Our characterisation of the Kleene-Kreisel continuous functionals is a supplement to a number of previous characterisations of topological and recursion-theoretical nature, see [6] for a brief survey. Altogether these characterisations show that the original concept of Kleene and Kreisel forms the correct mathematical model of the idea of finitely based functions of finite types. There is, however, no a priori reason to believe that there is a canonical way to extend the continuous functionals to cover transfinite objects of transfinite type used in, e.g., type theory. Our characterisation of Waagbø's model indicates that the model is natural, not only seen from domain theory but from a higher perspective. Normann and Waagbø (unpublished) have subsequently obtained a limit-space characterisation that further supports this view.

The notion of a ptyx (plural, ptykes) is obtained by generalising the ordinals On and the dilators Dil introduced by Girard [1] into a typed hierarchy. The notion is due to Girard, and a detailed treatment will appear in Girard [2]. In this Introduction we will give a summary of the theory of ptykes. It will be an advantage to be familiar with the theory of dilators as introduced in Girard [1] or as presented in Girard and Normann [3]. The class On of ordinals is organised into a category ON by using strictly increasing maps f: x → y as morphisms. A dilator will be a functor F: ON → ON commuting with pullbacks and direct limits. Associated with each dilator F there is a denotation system DF, obtained as follows: For each x ∈ On and y ∈ F(x), y can be given a unique denotation (c; x0,…, xn−1;x)F, where c∈F(n) (n = {0,…, n − 1}), y = F(ϕ)(c) (where ϕ is defined by ϕ(i) = xi for i < n), and for no m < n and ψ: m → n do we have c ∈ im(ψ). We let the trace Tr(F) be the set of pairs (c, n) occurring in a denotation.

The question of the limits of recursive enumerability was first formulated by Sacks (1980) and investigated further in Sacks (198?). E-recursion or “set recursion”, as a natural generalization of Kleene recursion in normal objects of finite type, was introduced by Normann (1978) in order to facilitate the study of the degrees of functionals. We shall extend the work of Sacks on the question of how definable is the E-closure of an ordinal α (written E(α)). We write gc(κ) to denote the largest τ < κ such that Lκ ⊨ “τ is a cardinal” and cf (τ) for τ ∈ ON to denote the cofinality of τ. In §1 we give the basic definitions and state the results of Silver and Friedman (1980) used by Sacks to show that if E(α) = Lκ and is not Σ1-admissible and then P(gc(κ)) ∩ Lκ is indexical on Lκ and hence RE. We show in this case first that P(gc(κ)) ∩ Lκ indexical implies that Lκ is indexical (and hence RE). In §2 we introduce the notion of a “nonstandard stage comparison” and use it to extend the definability result of §1 to show that this Lκ is in fact REC. Finally we remark that E(α) is indexical if and only if E(α) is RE.

One of the objectives of mathematics is to construct suitable models for practical or theoretical phenomena and to explore the mathematical richness of such models. This enables other scientists to obtain a better understanding of such phenomena. As an example we will mention the real line and related structures. The line can be used profitably in the study of discrete phenomena like population growth, chemical reactions, etc. Today's version of the real line is a topological completion of the rational numbers. This is so because then mathematicians have been able to work out a powerful analysis of the line. By using the real line to construct models for finitary phenomena we are more able to study those phenomena than we would have been sticking only to true-to-nature but finite structures. So we may say that the line is a mathematical model for certain finite structures. This motivates us to seek natural models for other types of finite structures, and it is natural to look for models that in some sense are complete. In this paper our starting point will be finite systems of finite operators. For the sake of simplicity we assume that they all are operators of one variable and that all the values are natural numbers. There is a natural extension of the systems such that they accept several variables and give finite operators as values, but the notational complexity will then obscure the idea of the construction.

Kleene [7] and Kreisel [8] defined independently the countable (continuous) functionals. Kleene [7] defined the countable functionals of type k to be total functionals of type k acting in a continuous way when restricted to countable arguments of type k − 1. He also defined the associates for countable functionals. They are functions α: N → N containing information about how the functional acts on countable arguments. Kleene [7] showed that the countable functionals are closed under the computations derived from S1–S9 of his paper [6], and that every computable functional has a recursive associate. Kreisel defined the continuous functionals to be equivalence-classes of associates. By his definition it is meaningless to let a continuous functional act upon anything but continuous arguments. One disadvantage of Kleene's approach is that two different functionals may have the same associates We will later see that there may be two functionals φ1 and φ2 with the same associates but such that the relations are not the same. In more recent papers on the countable functionals it is normal to regard the hierarchy 〈Ct(k)〉kϵN of countable functionals as a type-structure such that the functionals in Ct(k + 1) are maps from Ct(k) to N(Ct(0) = N), see e.g. Bergstra [1] and Gandy and Hyland [3]. We will then enjoy the streamlined formalism of a type-structure in which S1–S9 have meaning, but avoid the ambiguities of Kleene's original approach. We will presuppose a brief familiarity with the theory of the countable functionals.

The continuous or countable functionals were independently denned by Kleene [9] and Kreisel [10]. They were intended as a suitable basis for constructive mathematics, and thus it is interesting to investigate various notions of recursion on the countable functionals. There have been two main streams in this investigation, the study of countable recursion and the study of computability or Kleene-recursion. Countable recursion is the theory of recursion on the associates. Gandy and Hyland [3] and Hyland [7] are good sources for the recent development of countable recursion. This paper will mostly be concerned with Kleene-recursion on the countable functionals as denned in Kleene [8] and [9]. We assume some familiarity with the countable functionals and associates, as presented in Kleene [9], Bergstra [1] or any other paper on the subject. Pioneering work with recursion in nonnormal objects was done by Grilliot [4], who proved that a functional F of type 2 is normal if and only if its 1-section (that is the set of functions recursive in F) is closed under ordinary jump, and if and only if F is continuous on 1-section (F). Hinman [6] constructed a countable functional that is not recursively equivalent to a function, and thereby showed that recursion in nonnormal functionals is an extension of ordinary recursion in functions. In [6], Hinman asked if there are functionals with topless 1-sections, i.e. with no maximal elements in the semi-lattice of degrees. This was answered in the affirmative by Bergstra [1], using a spoiling construction. Thus the class of 1-sections of functionals extends the class of 1-sections of functions.

In [5] S. S. Wainer introduces a hierarchy for arbitrary type-2-functionals. Given F, he defines a set of ordinal notations OF, and for each a ∈ OF, a function fa recursive in F and an ordinal ∣a∣F < For any f recursive in F there is an a ∈ OF such that f is primitive recursive in fa. Let ρF be the least ordinal α such that for any f recursive in F there is an α ∈ OF with ∣a∣F ≤ α such that f is primitive recursive in fa. If ρF < the hierarchy breaks down. In Bergstra and Wainer [2] ρF is described as “the real ordinal of the 1-section of F”. Using standard methods (originally due to Kleene) one may prove that if F is normal, then ρF = Feferman has proved that if F is recursive, then ρF = ω2. Let 1-section (F) = l-sc(F) = {f; f is recursive in F} where f is a total object of type 1. Grilliot [4] proved that F ↾ 1-sc(F) is continuous if and only if F is not normal. Let h be an associate for a given functional F, and assume that h is recursive in the jump of an element of 1-sc(F).

Several results in the theory of recursion in higher types indicate that the effect of a higher type functional on the lower types does not reflect the high type, i.e. the same effect could be obtained by functionals of relatively low type. The two main results here are: Plus -1 - Theorem (G. Sacks [6] for k = 1, [7] for k > 1). Let H be a normal functional of type ≥ k + 1. Then there exists a normal functional F of type k + 1 such that k-sc(F) = k-sc(H), i.e. the same subsets of tp(k − 1) are recursive in F and H. Plus - 2 - Theorem (L. Harrington [1]). Let H be a normal functional of type ≥ k + 2. Then there exists a normal functional F of type k +2 such that k-en(H) = k-en(F), i.e. the same subsets of tp(k − 1) are semirecursive in F and H. The results in this paper also indicate that higher types cannot have too much influence on lower types. The key is the Skolem-Löwenheim theorem. Among the results we mention: (1) Let n < m. A ⊆ tp(n) × tp(m) be Kleene-semicomputable. Let x ∈ B ⇔ ∀y∈tp(m), ⟨x, y⟩ ∈ A. Then B is . This result may be relativized to a functional of type n + 1. (2) Let k0 be the type-k-functional that is constant zero. Let F be a functional of type < k. Then, for i ≤ k −2, i-sc(F ,k0) = i-sc(F), i-en(F, k0) = ∀tp(i)(i-en(F)).