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. 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$ for $i \le n$ form a covering of $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 yields exotic objects in computability theory, while leads to surprising results in Reverse Mathematics. We stress that and 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. (shrink)

In this paper, we discuss uniform versions of some axioms of second order arithmetic in the context of higher order arithmetic. We prove that uniform versions of weak weak König's lemma WWKL and Σ01 separation are equivalent to over a suitable base theory of higher order arithmetic, where is the assertion that there exists Φ2 such that Φf1 = 0 if and only if ∃x0 for all f. We also prove that uniform versions of some well-known theorems are equivalent to (...) or the axiom of the existence of the Suslin operator. (shrink)

We study the formalization within sybsystems of second-order arithmetic of theorems concerning periodic points in dynamical systems on the real line. We show that Sharkovsky's theorem is provable in WKL0. We show that, with an additional assumption, Sharkovsky's theorem is provable in RCA0. We show that the existence for all n of n-fold iterates of continuous mappings of the closed unit interval into itself is equivalent to the disjunction of Σ02 induction and weak König's lemma.

A survey is made of work since 1879 on foundational problems viewed as an analysis, by reduction and formalization, of the concepts proof, feasible, number, set, and constructivity. It is suggested that there are five domains of concepts and methods, viz., anthropologism, finitism, intuitionism, predicativism, and platonism. It is also suggested that the central problem is to characterize these domains by formalization and to determine their interrelations by different forms of reduction. Finally, the range of logic in the narrower sense (...) is discussed, and applications of mathematical logic are briefly outlined.ZusammenfassungDie Entwicklung der Grundlagenforschung seit dem Jahre 1879 wird hier im Überblick dargestellt und zwar vom Standpunkt einer Analyse durch Reduktion and Formalisierung der Begriffe Beweis, Zahl, Menge und Konstruktivität aus gesehen. Fünf Bereiche von Begriffsbildungen und Methoden werden zu Grunde gelegt, nämlich: Anthropologismus, Finitismus, Intuitionismus, Prädikativismus und Platonismus. Als zentrale Aufgabenstellung wird hier die Charakterisierung dieser Bereiche durch Formalisierung betrachtet und weiterhin die Bestimmung ihrer gegenseitigen Zusammenhänge durch verschiedene Arten von Reduktionen. Schliesslich wird das Gebiet der Logik im engeren Sinne diskutiert und Anwendungen der mathematischen Logik skizziert.RésuméL'article réexamine les travaux faits depuis 1879 sur les problèmes du fondement des mathématiques, que P'on considère comme des analyses par réduction et formalisation des concepts de démonstration, de nombre, d'ensemble, et de constructivité. On suggère qu'il existe cinq domaines de concepts et de méthodes, à savoir: anthropologisme, finitisme, intuitionisme, « predicativism » et platonisme. On suggère aussi que le problème essentiel consiste à caractériser ces domaines par formalisation et à déterminer leurs relations réciproques par différentes formes de réduction. Finalement, on étudie la portée de la logique prise dans son sens le plus étroit et on esquisse rapidement les applications de la logique mathématique. (shrink)

We study the logical and computational properties of basic theorems of uncountable mathematics, including the Cousin and Lindelöf lemma published in 1895 and 1903. Historically, these lemmas were among the first formulations of open-cover compactness and the Lindelöf property, respectively. These notions are of great conceptual importance: the former is commonly viewed as a way of treating uncountable sets like e.g. [Formula: see text] as “almost finite”, while the latter allows one to treat uncountable sets like e.g. [Formula: see text] (...) as “almost countable”. This reduction of the uncountable to the finite/countable turns out to have a considerable logical and computational cost: we show that the aforementioned lemmas, and many related theorems, are extremely hard to prove, while the associated sub-covers are extremely hard to compute. Indeed, in terms of the standard scale (based on comprehension axioms), a proof of these lemmas requires at least the full extent of second-order arithmetic, a system originating from Hilbert–Bernays’ Grundlagen der Mathematik. This observation has far-reaching implications for the Grundlagen’s spiritual successor, the program of Reverse Mathematics, and the associated Gödel hierarchy. We also show that the Cousin lemma is essential for the development of the gauge integral, a generalization of the Lebesgue and improper Riemann integrals that also uniquely provides a direct formalization of Feynman’s path integral. (shrink)

In this paper, we discuss uniform versions of some axioms of second order arithmetic in the context of higher order arithmetic. We prove that uniform versions of weak weak König's lemma WWKL and Σ01 separation are equivalent to over a suitable base theory of higher order arithmetic, where is the assertion that there exists Φ2 such that Φf1 = 0 if and only if ∃x0 for all f. We also prove that uniform versions of some well-known theorems are equivalent to (...) or the axiom of the existence of the Suslin operator. (shrink)

We analyze the pointwise convergence of a sequence of computable elements of L1 in terms of algorithmic randomness. We consider two ways of expressing the dominated convergence theorem and show that, over the base theory RCA0, each is equivalent to the assertion that every Gδ subset of Cantor space with positive measure has an element. This last statement is, in turn, equivalent to weak weak Königʼs lemma relativized to the Turing jump of any set. It is also equivalent to the (...) conjunction of the statement asserting the existence of a 2-random relative to any given set and the principle of Σ2 collection. (shrink)