2018/08/13 by Tatsuji Kawai, Kawai, Tatsuji
Computer Science · Mathematics · Physics and Astronomy · #03F03 #03F55 #03F60 #Baire category theorem #Baire space #Bar (unit) #Computability, Logic, AI Algorithms #Discrete mathematics #FOS: Mathematics #Geometry #Logic (math.LO) #Mathematical and Theoretical Analysis #Mathematics #Monotone polygon #Physics #Pure mathematics #Quantum Mechanics and Applications #math.LO #msc:03F03 #msc:03F55 #msc:03F60
paper · pdf · doi:10.48550/arxiv.1808.04082
arxiv created 2018/08/13 · openalex publication_date 2018/08/13 · arxiv updated 2018/08/14 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/06
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.