We investigate the reverse-mathematical status of several theorems to the effect that the natural number system is second-order categorical. One of our results is as follows. Define a system to be a triple A,i,f such that A is a set and i∈A and f:A→A. A subset X⊆A is said to be inductive if i∈X and ∀a ∈X). The system A,i,f is said to be inductive if the only inductive subset of A is A itself. Define a Peano system to be (...) an inductive system such that f is one-to-one and i∉the range of f. The standard example of a Peano system is N,0,S where N={0,1,2,…,n,…}=the set of natural numbers and S:N→N is given by S=n+1 for all n∈N. Consider the statement that all Peano systems are isomorphic to N,0,S. We prove that this statement is logically equivalent to WKL0 over RCA0⁎ source. From this and similar equivalences we draw some foundational/philosophical consequences. (shrink)

In this paper, we show that equation image is a equation image-conservative extension of BΣ1 + exp, thus it does not imply IΣ1.

We show that many principles of first-order arithmetic, previously only known to lie strictly between [Formula: see text]-induction and [Formula: see text]-induction, are equivalent to the well-foundedness of [Formula: see text]. Among these principles are the iteration of partial functions of Hájek and Paris, the bounded monotone enumerations principle by Chong, Slaman, and Yang, the relativized Paris–Harrington principle for pairs, and the totality of the relativized Ackermann–Péter function. With this we show that the well-foundedness of [Formula: see text] is a (...) far more widespread than usually suspected. Further, we investigate the [Formula: see text]-iterated version of the bounded monotone iterations principle, and show that it is equivalent to the well-foundedness of the -height [Formula: see text]-tower [Formula: see text]. (shrink)

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.

Let f be a computable function from finite sequences of 0ʼs and 1ʼs to real numbers. We prove that strong f-randomness implies strong f-randomness relative to a PA-degree. We also prove: if X is strongly f-random and Turing reducible to Y where Y is Martin-Löf random relative to Z, then X is strongly f-random relative to Z. In addition, we prove analogous propagation results for other notions of partial randomness, including non-K-triviality and autocomplexity. We prove that f-randomness relative to a (...) PA-degree implies strong f-randomness, hence f-randomness does not imply f-randomness relative to a PA-degree. (shrink)

We study the first-order consequences of Ramsey’s Theorem fork-colourings ofn-tuples, for fixed$n, k \ge 2$, over the relatively weak second-order arithmetic theory$\mathrm {RCA}^*_0$. Using the Chong–Mourad coding lemma, we show that in a model of$\mathrm {RCA}^*_0$that does not satisfy$\Sigma ^0_1$induction,$\mathrm {RT}^n_k$is equivalent to its relativization to any proper$\Sigma ^0_1$-definable cut, so its truth value remains unchanged in all extensions of the model with the same first-order universe.We give a complete axiomatization of the first-order consequences of$\mathrm {RCA}^*_0 + \mathrm {RT}^n_k$for$n \ge (...) 3$. We show that they form a non-finitely axiomatizable subtheory of$\mathrm {PA}$whose$\Pi _3$fragment coincides with$\mathrm {B} \Sigma _1 + \exp $and whose$\Pi _{\ell +3}$fragment for$\ell \ge 1$lies between$\mathrm {I} \Sigma _\ell \Rightarrow \mathrm {B} \Sigma _{\ell +1}$and$\mathrm {B} \Sigma _{\ell +1}$. We also give a complete axiomatization of the first-order consequences of$\mathrm {RCA}^*_0 + \mathrm {RT}^2_k + \neg \mathrm {I} \Sigma _1$. In general, we show that the first-order consequences of$\mathrm {RCA}^*_0 + \mathrm {RT}^2_k$form a subtheory of$\mathrm {I} \Sigma _2$whose$\Pi _3$fragment coincides with$\mathrm {B} \Sigma _1 + \exp $and whose$\Pi _4$fragment is strictly weaker than$\mathrm {B} \Sigma _2$but not contained in$\mathrm {I} \Sigma _1$.Additionally, we consider a principle$\Delta ^0_2$-$\mathrm {RT}^2_2$which is defined like$\mathrm {RT}^2_2$but with both the$2$-colourings and the solutions allowed to be$\Delta ^0_2$-sets rather than just sets. We show that the behaviour of$\Delta ^0_2$-$\mathrm {RT}^2_2$over$\mathrm {RCA}_0 + \mathrm {B}\Sigma ^0_2$is in many ways analogous to that of$\mathrm {RT}^2_2$over$\mathrm {RCA}^*_0$, and that$\mathrm {RCA}_0 + \mathrm {B} \Sigma ^0_2 + \Delta ^0_2$-$\mathrm {RT}^2_2$is$\Pi _4$- but not$\Pi _5$-conservative over$\mathrm {B} \Sigma _2$. However, the statement we use to witness failure of$\Pi _5$-conservativity is not provable in$\mathrm {RCA}_0 +\mathrm {RT}^2_2$. (shrink)

In this paper, we introduce the systems ns-ACA₀ and ns-WKL₀ of non-standard second-order arithmetic in which we can formalize non-standard arguments in ACA₀ and WKL₀, respectively. Then, we give direct transformations from non-standard proofs in ns-ACA₀ or ns-WKL₀ into proofs in ACA₀ or WKL₀.

The Jordan decomposition theorem states that every function $f \colon \, [0,1] \to \mathbb {R}$ of bounded variation can be written as the difference of two non-decreasing functions. Combining this fact with a result of Lebesgue, every function of bounded variation is differentiable almost everywhere in the sense of Lebesgue measure. We analyze the strength of these theorems in the setting of reverse mathematics. Over $\mathsf {RCA}_{0}$, a stronger version of Jordan’s result where all functions are continuous is equivalent to (...) $\mathsf {ACA}_0$, while the version stated is equivalent to ${\textsf {WKL}}_{0}$. The result that every function on $[0,1]$ of bounded variation is almost everywhere differentiable is equivalent to ${\textsf {WWKL}}_{0}$. To state this equivalence in a meaningful way, we develop a theory of Martin–Löf randomness over $\mathsf {RCA}_0$. (shrink)

In this paper, we show within ${\mathsf{RCA}_0}$ that both the Jordan curve theorem and the Schönflies theorem are equivalent to weak König’s lemma. Within ${\mathsf {WKL}_0}$ , we prove the Jordan curve theorem using an argument of non-standard analysis based on the fact that every countable non-standard model of ${\mathsf {WKL}_0}$ has a proper initial part that is isomorphic to itself (Tanaka in Math Logic Q 43:396–400, 1997).

This research is motivated by the program of reverse mathematics and non-standard arguments in second-order arithmetic. Within a weak subsystem of second-order arithmetic ACA0, we investigate some aspects of non-standard analysis related to sequential compactness. Then, using arguments of non-standard analysis, we show the equivalence of the Riemann mapping theorem and ACA0 over WKL0. (© 2007 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim).

In this paper, we introduce systems of nonstandard second-order arithmetic which are conservative extensions of systems of second-order arithmetic. Within these systems, we do reverse mathematics for nonstandard analysis, and we can import techniques of nonstandard analysis into analysis in weak systems of second-order arithmetic. Then, we apply nonstandard techniques to a version of Riemannʼs mapping theorem, and show several different versions of Riemannʼs mapping theorem.

We aim at developing a systematic method of separating omniscience principles by constructing Kripke models for intuitionistic predicate logic $\mathbf {IQC}$ and first-order arithmetic $\mathbf {HA}$ from a Kripke model for intuitionistic propositional logic $\mathbf {IPC}$. To this end, we introduce the notion of an extended frame, and show that each IPC-Kripke model generates an extended frame. By using the extended frame generated by an IPC-Kripke model, we give a separation theorem of a schema from a set of schemata in (...) $\mathbf {IQC}$ and a separation theorem of a sentence from a set of schemata in $\mathbf {HA}$. We see several examples which give us separations among omniscience principles. (shrink)

This research is motivated by the program of Reverse Mathematics. We investigate basic part of complex analysis within some weak subsystems of second order arithmetic, in order to determine what kind of set existence axioms are needed to prove theorems of basic analysis. We are especially concerned with Cauchy’s integral theorem. We show that a weak version of Cauchy’s integral theorem is proved in RCAo. Using this, we can prove that holomorphic functions are analytic in RCAo. On the other hand, (...) we show that a full version of Cauchy’s integral theorem cannot be proved in RCAo but is equivalent to weak König’s lemma over RCAo. (shrink)

The program of Reverse Mathematics (Simpson 2009) has provided us with the insight that most theorems of ordinary mathematics are either equivalent to one of a select few logical principles, or provable in a weak base theory. In this paper, we study the properties of the Dirac delta function (Dirac 1927; Schwartz 1951) in two settings of Reverse Mathematics. In particular, we consider the Dirac Delta Theorem, which formalizes the well-known property \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} (...) \begin{document}$${\int_\mathbb{R}f(x)\delta(x)\,dx=f(0)}$$\end{document} of the Dirac delta function. We show that the Dirac Delta Theorem is equivalent to weak König’s Lemma (see Yu and Simpson in Arch Math Log 30(3):171–180, 1990) in classical Reverse Mathematics. This further validates the status of WWKL0 as one of the ‘Big’ systems of Reverse Mathematics. In the context of ERNA’s Reverse Mathematics (Sanders in J Symb Log 76(2):637–664, 2011), we show that the Dirac Delta Theorem is equivalent to the Universal Transfer Principle. Since the Universal Transfer Principle corresponds to WKL, it seems that, in ERNA’s Reverse Mathematics, the principles corresponding to WKL and WWKL coincide. Hence, ERNA’s Reverse Mathematics is actually coarser than classical Reverse Mathematics, although the base theory has lower first-order strength. (shrink)

We prove that any proof of a [Formula: see text] sentence in the theory [Formula: see text] can be translated into a proof in [Formula: see text] at the cost of a polynomial increase in size. In fact, the proof in [Formula: see text] can be obtained by a polynomial-time algorithm. On the other hand, [Formula: see text] has nonelementary speedup over the weaker base theory [Formula: see text] for proofs of [Formula: see text] sentences. We also show that for (...) [Formula: see text], proofs of [Formula: see text] sentences in [Formula: see text] can be translated into proofs in [Formula: see text] at a polynomial cost in size. Moreover, the [Formula: see text]-conservativity of [Formula: see text] over [Formula: see text] can be proved in [Formula: see text], a fragment of bounded arithmetic corresponding to polynomial-time computation. For [Formula: see text], this answers a question of Clote, Hájek and Paris. (shrink)