A continuity principle equivalent to the monotone $Π^{0}_{1}$ fan theorem

Principles of bar induction and continuity on Baire space

Brouwer-operations, also known as inductively defined neighbourhood functions, provide a good notion of continuity on Baire space which naturally extends that of uniform continuity on Cantor space. In this paper, we introduce a continuity principle for Baire space which says that every pointwise continuous function from Baire space to the set of natural numbers is induced by a Brouwer-operation. Working in Bishop constructive mathematics, we show that the above principle is equivalent to a version of bar induction whose strength is between that of the monotone bar induction and the decidable b…

Decidable fan theorem and uniform continuity theorem with continuous moduli

The uniform continuity theorem (UCT) states that every pointwise continuous real-valued function on the unit interval is uniformly continuous. In constructive mathematics, UCT is stronger than the decidable fan theorem (DFT); however, Loeb [Ann. Pure Appl. Logic, 132(1):51-66, 2005] has shown that the two principles become equivalent with a suitable coding of "continuous functions" as type-one objects. The question remains whether DFT can be characterised by a weaker version of UCT using a natural subclass of pointwise continuous functions without such a coding. We show that when "pointwise co…

Brouwer's fan theorem

Brouwer's fan theorem states that every bar is a uniform bar. We give an overview of the status of this axiom in Bishop's constructive mathematics. In particular, we describe the relationship between the fan theorem, the weak König lemma, and the uniform continuity theorem.

Separating the Fan Theorem and Its Weakenings

Varieties of the Fan Theorem have recently been developed in reverse constructive mathematics, corresponding to different continuity principles. They form a natural implicational hierarchy. Some of the implications have been shown to be strict, others strict in a weak context, and yet others not at all, using disparate techniques. Here we present a family of related Kripke models which separates all of the as yet identified fan theorems.

关于单调函数一致连续性的一点注记

A note on uniform continuity of monotone functions

本文证明在ZFC一致地，每个非递减函数在某个大小为连续统基数的子集上一致连续，并给出基数特征$\mathfrak d^*$的刻画及其与$\mathfrak u,\mathfrak r,\mathfrak d$的关系。

On a continuity theorem for constructive functions

One proves that any everywhere defined constructive mapping from a complete metric space into a complete metric space which preserves the property of precompacity of subsets is locally uniformly continuous. This fact can be viewed as interpretation of L. E. J. Brower's fan theorem in terms of A. A. Markov's constructive analysis.