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 The smooth development of large parts of mathematics hinges on the idea that some sets are ‘small’ or ‘negligible’ and can therefore be ignored for a given purpose. The perhaps most famous smallness notion, namely ‘measure zero’, originated with Lebesgue, while a second smallness notion, namely ‘meagre’ or ‘first category’, originated with Baire around the same time. The associated Baire category theorem is a central result governing the properties of meagre (and related) sets, while the same holds for Tao’s pigeonhole principle for measure spaces and measure zero sets. In this paper, we study these theorems in Kohlenbach’s higher - order Reverse Mathematics , identifying a considerable number of equivalent and robust theorems. The latter involve most basic properties of semi-continuous and pointwise discontinuous functions, Blumberg’s theorem, Riemann integration, and Volterra’s early work circa 1881. All the aforementioned theorems fall (far) outside of the Big Five of Reverse Mathematics, and we investigate natural restrictions like Baire 1 and quasi-continuity that make these theorems provable again in the Big Five (or similar). Finally, despite the fundamental differences between measure and category, the proofs of our equivalences turn out to be similar.

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 As suggested by the title, the aim of this paper is to uncover the vast computational content of classical Nonstandard Analysis. To this end, we formulate a template ${\mathfrak{C}\mathfrak{I}}$ which converts a theorem of ‘pure’ Nonstandard Analysis, i.e. formulated solely with the nonstandard definitions (of continuity, integration, differentiability, convergence, compactness, etc.), into the associated effective theorem. The latter constitutes a theorem of computable mathematics no longer involving Nonstandard Analysis. To establish the huge scope of ${\mathfrak{C}\mathfrak{I}}$, we apply this template to representative theorems from the Big Five categories from Reverse Mathematics. The latter foundational program provides a classification of the majority of theorems from ‘ordinary’, i.e. non-set theoretical, mathematics into the aforementioned five categories. The Reverse Mathematics zoo gathers exceptions to this classification, and is studied in [ 74, 77] using ${\mathfrak{C}\mathfrak{I}}$. Hence, the template ${\mathfrak{C}\mathfrak{I}}$ is seen to apply to essentially all of ordinary mathematics, thanks to the Big Five classification (and associated zoo) from Reverse Mathematics. Finally, we establish that certain ‘highly constructive’ theorems, called Herbrandizations, also imply the original theorem of Nonstandard Analysis from which they were obtained via ${\mathfrak{C}\mathfrak{I}}$.

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.

Prediction models were developed to generate forecasts of solar radiation, and, by proxy, expected solar plant power output, for one hour and 24 hours in the future. Data was sourced from the Georgia Automated Environmental Monitoring Network (GAEMN) and the National Oceanic and Atmospheric Administration (NOAA) for five cities in Georgia. Early predictive models only made use of historical recorded solar radiation and other weather phenomena as inputs, while later models incorporated weather forecasts for the target area and surrounding areas. Including weather forecast data in the prediction models resulted in a 7.6% reduction in mean absolute error (MAE) for one-hour predictions when compared to using historical observations alone, and a 40.2% reduction in MAE for 24-hour predictions. Results from several machine learning techniques were compared, with Random Forests achieving the lowest error rate. The results indicate that weather forecasts are an important component of accurate solar radiation prediction even over short- and medium-term prediction timeframes, and the inclusion of the surrounding geographical area in addition to the target city is an important component of these predictions.

Abstract Elementary Recursive Nonstandard Analysis, in short ERNA, is a constructive system of nonstandard analysis with a PRA consistency proof, proposed around 1995 by Patrick Suppes and Richard Sommer. Recently, the author showed the consistency of ERNA with several transfer principles and proved results of nonstandard analysis in the resulting theories (see [12] and [13]). Here, we show that Weak König's lemma (WKL) and many of its equivalent formulations over RCA0 from Reverse Mathematics (see [21] and [22]) can be ‘pushed down’ into the weak theory ERNA, while preserving the equivalences, but at the price of replacing equality with equality ‘up to infinitesimals’. It turns out that ERNA plays the role of RCA0 and that transfer for universal formulas corresponds to WKL.

Abstract Elementary Recursive Nonstandard Analysis, in short ERNA, is a constructive system of nonstandard analysis proposed around 1995 by Patrick Suppes and Richard Sommer, who also proved its consistency inside PRA. It is based on an earlier system developed by Rolando Chuaqui and Patrick Suppes, of which Michal Rössler and Emil Jeřábek have recently proposed a weakened version. We add a Πı-transfer principle to ERNA and prove the consistency of the extended theory inside PRA. In this extension of ERNA a Σı-supremum principle ‘up-to-infinitesimals’, and some well-known calculus results for sequences are deduced. Finally, we prove that transfer is ‘too strong’ for finitism by reconsidering Rössler and Jeřábek's conclusions.