In this paper, we introduce a system of nonstandard second-order arithmetic $\mathsf{ns}$-$\mathsf{WWKL_0}$ which consists of $\mathsf{ns}$-$\mathsf{BASIC}$ plus Loeb measure property. Then we show that $\mathsf{ns}$-$\mathsf{WWKL_0}$ is a conservative extension of $\mathsf{WWKL_0}$ and we do Reverse Mathematics for this system.

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)

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 initiate the reverse mathematics of general topology. We show that a certain metrization theorem is equivalent to Π2 1 comprehension. An MF space is defined to be a topological space of the form MF(P) with the topology generated by $\lbrace N_p \mid p \in P \rbrace$ . Here P is a poset, MF(P) is the set of maximal filters on P, and $N_p = \lbrace F \in MF(P) \mid p \in F \rbrace$ . If the poset P is countable, (...) the space MF(P) is said to be countably based. The class of countably based MF spaces can be defined and discussed within the subsystem ACA0 of second order arithmetic. One can prove within ACA0 that every complete separable metric space is homeomorphic to a countably based MF space which is regular. We show that the converse statement, "every countably based MF space which is regular is homeomorphic to a complete separable metric space," is equivalent to Π2 1-CA0. The equivalence is proved in the weaker system Π1 1-CA0. This is the first example of a theorem of core mathematics which is provable in second order arithmetic and implies Π2 1 comprehension. (shrink)

We initiate the reverse mathematics of general topology. We show that a certain metrization theorem is equivalent to Π12 comprehension. An MF space is defined to be a topological space of the form MF with the topology generated by {Np ∣ p ϵ P}. Here P is a poset, MF is the set of maximal filters on P, and Np = {F ϵ MF ∣ p ϵ F }. If the poset P is countable, the space MF is said to (...) be countably based. The class of countably based MF spaces can be defined and discussed within the subsystem ACA0 of second order arithmetic. One can prove within ACA0 that every complete separable metric space is homeomorphic to a countably based MF space which is regular. We show that the converse statement, “every countably based MF space which is regular is homeomorphic to a complete separable metric space,” is equivalent to. The equivalence is proved in the weaker system. This is the first example of a theorem of core mathematics which is provable in second order arithmetic and implies Π12 comprehension. (shrink)

We show that each of $\Delta _{3}^{1}-{\rm CA}_{0}+\Sigma _{3}^{1}-{\rm IND}$ and $\Pi _{2}^{1}-{\rm CA}_{0}+\Pi _{3}^{1}-{\rm TI}$ proves $\Delta _{3}^{0}-{\rm Det}$ and that neither $\Sigma _{3}^{1}-{\rm IND}$ nor $\Pi _{3}^{1}-{\rm TI}$ can be dropped. We also show that neither $\Delta _{3}^{1}-{\rm CA}_{0}+\Sigma _{\infty}^{1}-{\rm IND}$ nor $\Pi _{2}^{1}-{\rm CA}_{0}+\Pi _{\infty}^{1}-{\rm TI}$ proves $\Sigma _{3}^{0}-{\rm Det}$. Moreover, we prove that none of $\Delta _{2}^{1}-{\rm CA}_{0}$, $\Sigma _{3}^{1}-{\rm IND}$ and $\Pi _{2}^{1}-{\rm TI}$ is provable in $\Delta _{1}^{1}-{\rm Det}_{0}={\rm ACA}_{0}+\Delta _{1}^{1}-{\rm Det}$.

We show that each of Δ13-CA0 + Σ13-IND and Π12-CA0 + Π13-TI proves Δ03-Det and that neither Σ31-IND nor Π13-TI can be dropped. We also show that neither Δ13-CA0 + Σ1∞-IND nor Π12-CA0 + Π1∞-TI proves Σ03-Det. Moreover, we prove that none of Δ21-CA0, Σ31-IND and Π21-TI is provable in Δ11-Det0 = ACA0 + Δ11-Det.

The so-called weak König's lemma WKL asserts the existence of an infinite path b in any infinite binary tree . Based on this principle one can formulate subsystems of higher-order arithmetic which allow to carry out very substantial parts of classical mathematics but are Π 2 0 -conservative over primitive recursive arithmetic PRA . In Kohlenbach 1239–1273) we established such conservation results relative to finite type extensions PRA ω of PRA . In this setting one can consider also a uniform (...) version UWKL of WKL which asserts the existence of a functional Φ which selects uniformly in a given infinite binary tree f an infinite path Φf of that tree. This uniform version of WKL is of interest in the context of explicit mathematics as developed by S. Feferman. The elimination process in Kohlenbach [10] actually can be used to eliminate even this uniform weak König's lemma provided that PRA ω only has a quantifier-free rule of extensionality QF-ER instead of the full axioms of extensionality for all finite types. In this paper we show that in the presence of , UWKL is much stronger than WKL: whereas WKL remains to be Π 2 0 -conservative over PRA, PRA ω ++ UWKL contains full Peano arithmetic PA. We also investigate the proof–theoretic as well as the computational strength of UWKL relative to the intuitionistic variant of PRA ω both with and without the Markov principle. (shrink)

We show that each of the five basic theories of second order arithmetic that play a central role in reverse mathematics has a natural counterpart in the language of nonstandard arithmetic. In the earlier paper [3] we introduced saturation principles in nonstandard arithmetic which are equivalent in strength to strong choice axioms in second order arithmetic. This paper studies principles which are equivalent in strength to weaker theories in second order arithmetic.

In this paper we study a new approach to classify mathematical theorems according to their computational content. Basically, we are asking the question which theorems can be continuously or computably transferred into each other? For this purpose theorems are considered via their realizers which are operations with certain input and output data. The technical tool to express continuous or computable relations between such operations is Weihrauch reducibility and the partially ordered degree structure induced by it. We have identified certain choice (...) principles such as co-finite choice, discrete choice, interval choice, compact choice and closed choice, which are cornerstones among Weihrauch degrees and it turns out that certain core theorems in analysis can be classified naturally in this structure. In particular, we study theorems such as the Intermediate Value Theorem, the Baire Category Theorem, the Banach Inverse Mapping Theorem, the Closed Graph Theorem and the Uniform Boundedness Theorem. We also explore how existing classifications of the Hahn—Banach Theorem and Weak Kőnig's Lemma fit into this picture. Well-known omniscience principles from constructive mathematics such as LPO and LLPO can also naturally be considered as Weihrauch degrees and they play an important role in our classification. Based on this we compare the results of our classification with existing classifications in constructive and reverse mathematics and we claim that in a certain sense our classification is finer and sheds some new light on the computational content of the respective theorems. Our classification scheme does not require any particular logical framework or axiomatic setting, but it can be carried out in the framework of classical mathematics using tools of topology, computability theory and computable analysis. We develop a number of separation techniques based on a new parallelization principle, on certain invariance properties of Weihrauch reducibility, on the Low Basis Theorem of Jockusch and Soare and based on the Baire Category Theorem. Finally, we present a number of metatheorems that allow to derive upper bounds for the classification of the Weihrauch degree of many theorems and we discuss the Brouwer Fixed Point Theorem as an example. (shrink)

We present an extension of Heyting arithmetic in finite types called Uniform Heyting Arithmetic that allows for the extraction of optimized programs from constructive and classical proofs. The system has two sorts of first-order quantifiers: ordinary quantifiers governed by the usual rules, and uniform quantifiers subject to stronger variable conditions expressing roughly that the quantified object is not computationally used in the proof. We combine a Kripke-style Friedman/Dragalin translation which is inspired by work of Coquand and Hofmann and a variant (...) of the refined A-translation due to Buchholz, Schwichtenberg and the author to extract programs from a rather large class of classical first-order proofs while keeping explicit control over the levels of recursion and the decision procedures for predicates used in the extracted program. (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)