Principles of bar induction and continuity on Baire space

TL;DR

This paper explores the relationship between bar induction principles and continuity on Baire space within Bishop constructive mathematics, establishing equivalences and implications among various forms of bar induction and continuity principles.

Contribution

It introduces a new continuity principle for Baire space, characterizes bar induction variants through continuity, and links bar induction to classical principles like LLPO and LPO.

Findings

The continuity principle is equivalent to a specific form of bar induction.

Monotone and decidable bar inductions are characterized by similar continuity principles.

Pi^0_1 bar induction implies LLPO, connecting bar induction with classical logical principles.

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 $\Pi^{0}_{1}$ bar induction in general implies LLPO (the lesser limited principle of omniscience). This, together with a fact that the $\Sigma^{0}_{1}$ bar induction implies LPO (the limited principle of omniscience), shows that an intuitionistically acceptable form of bar induction requires the bar to be monotone.