Formally continuous functions on Baire space

2017/10/24 by Tatsuji Kawai, Kawai, Tatsuji
Computer Science · Mathematics · #03F55 #03F60 #06D22 #Computability, Logic, AI Algorithms #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #Mathematical and Theoretical Analysis #Rough Sets and Fuzzy Logic

paper · pdf · doi:10.48550/arxiv.1710.08755

openalex publication_date 2017/10/24 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

A function from Baire space to the natural numbers is called formally continuous if it is induced by a morphism between the corresponding formal spaces. We compare formal continuity to two other notions of continuity on Baire space working in Bishop constructive mathematics: one is a function induced by a Brouwer-operation (i.e. inductively defined neighbourhood function); the other is a function uniformly continuous near every compact image. We show that formal continuity is equivalent to the former while it is strictly stronger than the latter.

Related

• Principles of bar induction and continuity on Baire space
• A generalization of a Baire theorem concerning barely continuous functions
• Representing definable functions of HA^ω by neighbourhood functions
• No function is continuous only at points in a countable dense subset
• Continuity is an adjoint functor