This paper is a contribution to constructive (reverse) mathematics. The formal system in which the author works is an extension of the intuitionistic theory of analysis IDB one, an extension of intuitionistic arithmetic in all finite types, together with the axiom of unique choice. The principle of Brouwer continuity (BC), a continuity principle for Baire space, is introduced and it is shown equivalent to continuous bar induction c-BI, an introduced version of bar induction.
In the Introduction, the author describes how the relation between the uniform continuity principle (UC) on Cantor space and the fan theorem motivated his study of the relation between statements similar to UC for the Baire space and various forms of bar induction. A brief description of the formal system used is added.
In Section 2, the principle of continuous bar induction c-BI is introduced and it is shown that it implies the version c-FT of the fan theorem introduced by J. Berger [Lect. Notes Comput. Sci. 3988, 35–39 (2006; Zbl 1145.03339)].
In Section 3, the principle of Brouwer continuity (BC) is introduced, according to which every pointwise continuous function from the Baire space to the natural numbers is appropriately induced by the inductively defined notion of a Brouwer operation. It is also shown that BC, restricted to the Cantor space, is equivalent to uniform continuity.
In Section 4, the equivalence between BC and c-BI is shown.
In Section 5, the decidable version and the monotone version of bar induction are characterised by variations of BC.
In Section 6, continuity axioms on Baire space are related to the decidable, monotone and the continuous version of bar induction, respectively.
In Section 7, the pi-one-zero version of bar induction is shown to imply the lesser limited principle of omniscience.