Paper detail

Decidable fan theorem and uniform continuity theorem with continuous moduli

The uniform continuity theorem (UCT) states that every pointwise continuous real-valued function on the unit interval is uniformly continuous. In constructive mathematics, UCT is stronger than the decidable fan theorem (DFT); however, Loeb [Ann. Pure Appl. Logic, 132(1):51-66, 2005] has shown that the two principles become equivalent with a suitable coding of "continuous functions" as type-one objects. The question remains whether DFT can be characterised by a weaker version of UCT using a natural subclass of pointwise continuous functions without such a coding. We show that when "pointwise continuous" is replaced with "having a continuous modulus", UCT becomes equivalent to DFT. We also show that this weakening of UCT is equivalent to a similar principle for real-valued functions on the Cantor space $\{0,1\}^{\mathbb{N}}$. These results extend Berger's characterisation of DFT by the similar principle for functions from $\{0,1\}^{\mathbb{N}}$ to $\mathbb{N}$, and unifies these characterisations of DFT in terms of functions having continuous moduli. Furthermore, we directly show that the continuous real-valued functions on the unit interval having continuous moduli are exactly those functions which admit the coding of "continuous functions" due to Loeb. Our result allows us to interpret her work in the usual context of mathematics.