### 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.

#### Full Text:

FT3. [PDF]DOI: https://doi.org/10.4115/jla.2019.11.FT3

This work is licensed under a Creative Commons Attribution 3.0 License.

Journal of Logic and Analysis ISSN: 1759-9008