Decidable fan theorem and uniform continuity theorem with continuous moduli
From MaRDI portal
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 . These results extend Berger's characterisation of DFT by the similar principle for functions from to , 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.
Recommendations
- New Computational Paradigms
- König's lemma, weak König's lemma, and the decidable fan theorem
- scientific article; zbMATH DE number 5676623
- Factoring Out Intuitionistic Theorems: Continuity Principles and the Uniform Continuity Theorem
- The uniform bounded deciding property and the separable quotient problem
- Brouwer's fan theorem and unique existence in constructive analysis
- Hausdorff separations and decidability
- scientific article; zbMATH DE number 4164193
- Decidable theories of non-projectable l-groups of continuous functions
- A Weak Constructive Sequential Compactness Property and the Fan Theorem
Cites work
- A separation result for varieties of Brouwer's fan theorem
- Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
- Constructivism in mathematics. An introduction. Volume I
- Domains for Computation in Mathematics, Physics and Exact Real Arithmetic
- Equivalence of bar induction and bar recursion for continuous functions with continuous moduli
- Equivalents of the (weak) fan theorem
- scientific article; zbMATH DE number 3900744 (Why is no real title available?)
- scientific article; zbMATH DE number 1870414 (Why is no real title available?)
- scientific article; zbMATH DE number 3291139 (Why is no real title available?)
- scientific article; zbMATH DE number 2247263 (Why is no real title available?)
- Logical Approaches to Computational Barriers
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- New Computational Paradigms
- On Brouwer's continuity principle
- Principles of intuitionism. Lectures presented at the summer conference on intuitionism and proof theory (1968) at SUNY at Buffalo, NY
- Real number computability and domain theory
- Sequences of real functions on [0,1] in constructive reverse mathematics
- Subsystems of second order arithmetic
Cited in
(4)
This page was built for publication: Decidable fan theorem and uniform continuity theorem with continuous moduli
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6047675)
