A uniform continuity principle for the Baire space and a corresponding bar induction

The uniform continuity principle (UC) is the following statement: UC Every pointwise continuous function F: {0, 1}N → N is uniformly continu-ous. Since the Cantor space {0, 1}N is compact, UC is classically true. It is well known, however, that this need not be the case in the constructive mathematics in the sense of Bishop [2]. Berger [1] showed that, in Bishop constructive mathematics,UC is equivalent to a version of fan theorem, called c–FT, thereby gave a characterisation of UC in terms of a fan theorem. In this talk, we generalise the above equivalence to the setting of the Baire space NN. We formulate the corresponding uniform continuity principle UCB for the Baire space and a version of bar induction, called c–BI, and show that UCB and c–BI are equivalent. The principle UCB is the following statement: UCB Every pointwise continuous function F: NN → N is formally representable. Here, a function F: NN → N is formally representable if F is of the for