Decidable fan theorem and uniform continuity theorem with continuous moduli

TL;DR

This paper establishes that the decidable fan theorem (DFT) is equivalent to a weakened uniform continuity theorem (UCT) when restricted to functions with continuous moduli, unifying various characterizations of DFT.

Contribution

It shows that replacing pointwise continuity with continuous moduli makes UCT equivalent to DFT, extending and unifying previous characterizations of DFT.

Findings

DFT is equivalent to a weakened UCT for functions with continuous moduli.

This equivalence extends to functions on the Cantor space.

Functions with continuous moduli are precisely those that can be coded as continuous functions.

Abstract

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.