We give an overview of the role of equicontinuity of sequences of real-valued functions on [0,1] and related notions in classical mathematics, intuitionistic mathematics, Bishop’s constructive mathematics, and Russian recursive mathematics. We then study the logical strength of theorems concerning these notions within the programme of Constructive Reverse Mathematics. It appears that many of these theorems, like a version of Ascoli’s Lemma, are equivalent to fan-theoretic principles.

In his previous work, the author has introduced the axiom schema of inductive dichotomy, a weak variant of the axiom schema of inductive definition, and used this schema for elementary ) positive operators to separate open and clopen determinacies for those games in which two players make choices from infinitely many alternatives in various circumstances. Among the studies on variants of inductive definitions for bounded ) positive operators, the present article investigates inductive dichotomy for these operators, and applies it to (...) constructive investigations of variants of determinacy statements for those games in which the players make choices from only finitely many alternatives. As a result, three formulations of open determinacy, that are all classically equivalent with each other, are equivalent to three different semi-classical principles, namely Markov’s Principle, Lesser Limited Principle of Omniscience and Limited Principle of Omniscience, over a suitable constructive base theory that proves clopen determinacy. Open and clopen determinacies for these games are thus separated. Some basic results on variants of inductive definitions for \ positive operators will also be given. (shrink)

We define classes Φnof formulae of first-order arithmetic with the following properties:(i) Everyφϵ Φnis classically equivalent to a Πn-formula (n≠ 1, Φ1:= Σ1).(ii)(iii)IΠnandiΦn(i.e., Heyting arithmetic with induction schema restricted to Φn-formulae) prove the same Π2-formulae.We further generalize a result by Visser and Wehmeier. namely that prenex induction within intuitionistic arithmetic is rather weak: After closing Φnboth under existential and universal quantification (we call these classes Θn) the corresponding theoriesiΘnstill prove the same Π2-formulae. In a second part we consideriΔ0plus collection-principles. We (...) show that both the provably recursive functions and the provably total functions ofare polynomially bounded. Furthermore we show that the contrapositive of the collection-schema gives rise to instances of the law of excluded middle and hence. (shrink)

A number of classical theories are interpreted in analogous theories that are based on intuitionistic logic. The classical theories considered include subsystems of first- and second-order arithmetic, bounded arithmetic, and admissible set theory.

We show that certain model-theoretic forcing arguments involving subsystems of second-order arithmetic can be formalized in the base theory, thereby converting them to effective proof-theoretic arguments. We use this method to sharpen the conservation theorems of Harrington and Brown-Simpson, giving an effective proof that WKL+0 is conservative over RCA0 with no significant increase in the lengths of proofs.

In this paper we present some metapredicative subsystems of analysis. We deal with reflection principles, $\omega-model$ existence axioms (limit axioms) and axioms asserting the existence of hierarchies. We show several equivalences among the introduced subsystems. In particular we prove the equivalence of $\sum_1^1$ transfinite dependent choice and $\prod_2^1$ reflection on $\omega-models$ of $\sum_1^1-DC$.

We show how to extract effective bounds Φ for $\bigwedge u^1 \bigwedge v \leq_\gamma tu \bigvee w^\eta G_0$ -sentences which depend on u only (i.e. $\bigwedge u \bigwedge v \leq_\gamma tu \bigvee w \leq_\eta \Phi uG_0$ ) from arithmetical proofs which use analytical assumptions of the form \begin{equation*}\tag{*}\bigwedge x^\delta\bigvee y \leq_\rho sx \bigwedge z^\tau F_0\end{equation*} (γ, δ, ρ, and τ are arbitrary finite types, η ≤ 2, G0 and F0 are quantifier-free, and s and t are closed terms). If τ (...) ≤ 2, (*) can be weakened to $\bigwedge x^\delta, z^\tau\bigvee y \leq_\rho sx \bigwedge \tilde{z} \leq_\tau z F_0$ . This is used to establish new conservation results about weak König's lemma. Applications to proofs in classical analysis, especially uniqueness proofs in approximation theory, will be given in subsequent papers. (shrink)

We measure, in the presence of the axiom of infinity, the proof-theoretic strength of the axioms of set theory which make the theory look really like a “theory of sets”, namely, the axiom of extensionality Ext, separation axioms and the axiom of regularity Reg . We first introduce a weak weak set theory as a base over which to clarify the strength of these axioms. We then prove the following results about proof-theoretic ordinals:1. and ,2. and . We also show (...) that neither Reg nor affects the proof-theoretic strength, i.e., where T is Basic plus any combination of Ext and. (shrink)

This paper is divided into two parts. Part I provides a resumé of the evolution of the notion of predicativity. Part II describes our own work on the subject.Part I§1. Conceptions of sets.Statements about sets lie at the heart of most modern attempts to systematize all (or, at least, all known) mathematics. Technical and philosophical discussions concerning such systematizations and the underlying conceptions have thus occupied a considerable portion of the literature on the foundations of mathematics.

In recent years the question of whether adding the limited principle of omniscience, LPO, to constructive Zermelo–Fraenkel set theory, CZF, increases its strength has arisen several times. As the addition of excluded middle for atomic formulae to CZF results in a rather strong theory, i.e. much stronger than classical Zermelo set theory, it is not obvious that its augmentation by LPO would be proof-theoretically benign. The purpose of this paper is to show that CZF+RDC+LPO has indeed the same strength as (...) CZF, where RDC stands for relativized dependent choice. In particular, these theories prove the same Π02 theorems of arithmetic. (shrink)

Classically, weak König's lemma and Brouwer's fan theorem for detachable bars are equivalent. We give a direct constructive proof that the former implies the latter.

V. Lifschitz defined in 1979 a variant of realizability which validates Church's thesis with uniqueness condition, but not the general form of Church's thesis. In this paper we describe an extension of intuitionistic arithmetic in which the soundness of Lifschitz' realizability can be proved, and we give an axiomatic characterization of the Lifschitz-realizable formulas relative to this extension. By a "q-variant" we obtain a new derived rule. We also show how to extend Lifschitz' realizability to second-order arithmetic. Finally we describe (...) an analogous development for elementary analysis, with partial continuous application replacing partial recursive application. (shrink)

We will overview the results in an informal approach to constructive reverse mathematics, that is reverse mathematics in Bishop’s constructive mathematics, especially focusing on compactness properties and continuous properties.

In this article we study the systems KF and VF of truth over set theory as well as related systems and compare them with the corresponding systems over arithmetic.

This article provides an ordinal analysis of Σ11 transfinite dependent choice.

We will overview the results in an informal approach to constructive reverse mathematics, that is reverse mathematics in Bishop’s constructive mathematics, especially focusing on compactness properties and continuous properties.

In this paper we study the logical strength of the determinacy of infinite binary games in terms of second order arithmetic. We define new determinacy schemata inspired by the Wadge classes of Polish spaces and show the following equivalences over the system RCA0*, which consists of the axioms of discrete ordered semi‐rings with exponentiation, Δ10 comprehension and Π00 induction, and which is known as a weaker system than the popularbase theory RCA0: 1. Bisep(Δ10, Σ10)‐Det* ↔ WKL0, 2. Bisep(Δ10, Σ20)‐Det* ↔ (...) ATR0 + Σ11 induction, 3. Bisep(Σ10, Σ20)‐Det* ↔ Sep(Σ10, Σ20)‐Det* ↔ Π11‐CA0, 4. Bisep(Δ20, Σ20)‐Det* ↔ Π11‐TR0, where Det* stands for the determinacy of infinite games in the Cantor space (© 2009 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim). (shrink)

In the first part of this paper we investigate the intuitionistic version $iI\!\Sigma_1$ of $I\!\Sigma_1$ (in the language of $PRA$ ), using Kleene's recursive realizability techniques. Our treatment closely parallels the usual one for $HA$ and establishes a number of nice properties for $iI\!\Sigma_1$ , e.g. existence of primitive recursive choice functions (this is established by different means also in [D94]). We then sharpen an unpublished theorem of Visser's to the effect that quantifier alternation alone is much less powerful intuitionistically (...) than classically: $iI\!\Sigma_1$ together with induction over arbitrary prenex formulas is $\Pi_2$ -conservative over $iI\!\Pi_2$ . In the second part of the article we study the relation of $iI\!\Sigma_1$ to $iI\!\Pi_1$ (in the usual arithmetical language). The situation here is markedly different from the classical case in that $iI\!\Pi_1$ and $iI\!\Sigma_1$ are mutually incomparable, while $iI\!\Sigma_1$ is significantly stronger than $iI\!\Pi_1$ as far as provably recursive functions are concerned: All primitive recursive functions can be proved total in $iI\!\Sigma_1$ whereas the provably recursive functions of $iI\!\Pi_1$ are all majorized by polynomials over ${\Bbb N}$ . 0 $iI\!\Pi_1$ is unusual also in that it lacks closure under Markov's Rule $\mbox{MR}_{PR}$. (shrink)

The paper is a contribution to intuitionistic reverse mathematics. We introduce a formal system called Basic Intuitionistic Mathematics BIM, and then search for statements that are, over BIM, equivalent to Brouwer’s Fan Theorem or to its positive denial, Kleene’s Alternative to the Fan Theorem. The Fan Theorem is true under the intended intuitionistic interpretation and Kleene’s Alternative is true in the model of BIM consisting of the Turing-computable functions. The task of finding equivalents of Kleene’s Alternative is, intuitionistically, a nontrivial (...) extension of the task of finding equivalents of the Fan Theorem, although there is a certain symmetry in the arguments that we shall try to make transparent. We introduce closed-and-separable subsets of Baire space $${\mathcal{N}}$$ and of the set $${\mathcal{R}}$$ of the real numbers. Such sets may be compact and also positively noncompact. The Fan Theorem is the statement that Cantor space $${\mathcal{C}}$$, or, equivalently, the unit interval [0, 1], is compact and Kleene’s Alternative is the statement that $${\mathcal{C}}$$, or, equivalently, [0, 1], is positively noncompact. The class of the compact closed-and-separable sets and also the class of the closed-and-separable sets that are positively noncompact are characterized in many different ways and a host of equivalents of both the Fan Theorem and Kleene’s Alternative is found. (shrink)

In this paper, we consider, for a set \ of natural numbers, the following notions of finitenessFIN1:There are a natural number l and a bijection f between \\);FIN5:It is not the case that \\), and infinitenessINF1:There are not a natural number l and a bijection f between \\);INF5:\\). In this paper, we systematically compare them in the method of constructive reverse mathematics. We show that the equivalence among them can be characterized by various combinations of induction axioms and non-constructive principles, (...) including the axiom of bounded comprehension. (shrink)

The author proved in his Ph.D. Thesis [W. Veldman, Investigations in intuitionistic hierarchy theory, Ph.D. Thesis, Katholieke Universiteit Nijmegen, 1981] that, in intuitionistic analysis, the positively Borel subsets of Baire space form a genuinely growing hierarchy: every level of the hierarchy contains sets that do not occur at any lower level. It follows from this result that there are natural examples of analytic and also of co-analytic sets that are not positively Borel. It turns out, however, that, in intuitionistic analysis, (...) one may give surprisingly different and, in some sense, much more simple examples of analytic and co-analytic sets that fail to be positively Borel. In the paper, two such examples are given. In proving them correct, one obtains new proofs of the Borel Hierarchy Theorem. Brouwer’s Continuity Principle plays a crucial role in arguments. (shrink)

In this note, we prove that certain theories of (many‐sorted) intuitionistic predicate logic are closed under the independence of premiss rule (IPR). As corollaries, we show that and extended by some non‐classical axioms and non‐constructive axioms are closed under IPR.