Principles of bar induction and continuity on Baire space

Abstract

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 bar induction. We also show that the
monotone bar induction and the decidable bar induction can be characterised by
similar principles of continuity.
Moreover, we show that the Π01 bar induction in general implies LLPO (the
lesser limited principle of omniscience). This, together with a fact that the Σ01
bar induction implies LPO (the limited principle of omniscience), shows that an
intuitionistically acceptable form of bar induction requires the bar to be monotone.