Premium
Decidable fan theorem and uniform continuity theorem with continuous moduli
Author(s) -
Fujiwara Makoto,
Kawai Tatsuji
Publication year - 2021
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.202000028
Subject(s) - mathematics , modulus of continuity , uniform continuity , pointwise , uniform limit theorem , continuous function (set theory) , moduli , pure mathematics , arzelà–ascoli theorem , type (biology) , discrete mathematics , metric space , function (biology) , mathematical analysis , danskin's theorem , brouwer fixed point theorem , fixed point theorem , ecology , physics , quantum mechanics , evolutionary biology , biology
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 strictly stronger than the decidable fan theorem ( DFT ) , but Loeb [17] has shown that the two principles become equivalent by encoding continuous real‐valued functions as type‐one functions. However, the precise relation between such type‐one functions and continuous real‐valued functions (usually described as type‐two objects) has been unknown. In this paper, we introduce an appropriate notion of continuity for a modulus of a continuous real‐valued function on [0, 1], and show that real‐valued functions with continuous moduli are exactly those functions induced by Loeb's codes. Our characterisation relies on two assumptions: (1) real numbers are represented by regular sequences (equivalently Cauchy sequences with explicitly given moduli); (2) the continuity of a modulus is defined with respect to the product metric on the regular sequences inherited from the Baire space. Our result implies that DFT is equivalent to the statement that every pointwise continuous real‐valued function on [0, 1] with a continuous modulus is uniformly continuous. We also show that DFT is equivalent to a similar principle for real‐valued functions on the Cantor space{ 0 , 1 } N . These results extend Berger's [2] characterisation of DFT for integer‐valued functions on{ 0 , 1 } N and unify some characterisations of DFT in terms of functions having continuous moduli.