Dini’s Theorem in the Light of Reverse Mathematics

  • Josef Berger
  • Peter Schuster
Part of the Synthese Library book series (SYLI, volume 341)


Dini’s theorem says that compactness of the domain, a metric space, ensures the uniform convergence of every simply convergent monotone sequence of uniformly continuous real-valued functions whose limit is uniformly continuous. By showing that it is equivalent to Brouwer’s fan theorem for detachable bars, we provide Dini’s theorem with a classification in the constructive reverse mathematics recently propagated by Ishihara. If the functions occurring in Dini’s theorem are pointwise continuous but integer-valued, then to still obtain such a classification we need to replace the fan theorem by the principle that every pointwise continuous integer-valued function on the Cantor space is uniformly continuous. As a complement, Dini’s theorem both for pointwise and uniformly continuous functions is proved to be equivalent to the analogue of the fan theorem, weak König’s lemma, in the classical setting of reverse mathematics started by Friedman and Simpson.


Binary Sequence Uniform Continuity Constructive Mathematics Cantor Space Reverse Mathematic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Berger, J., Constructive equivalents of the uniform continuity theorem. J. UCS 11, 1878–1883, 2005zbMATHMathSciNetGoogle Scholar
  2. 2.
    Berger, J., and P. Schuster, Classifying Dini’s theorem. Notre Dame J. Formal Logic 47, 253–262, 2006zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Bishop, E., Foundations of Constructive Analysis. McGraw–Hill, New York, 1967zbMATHGoogle Scholar
  4. 4.
    Bishop, E., and D. Bridges, Constructive Analysis. Springer, Berlin etc., 1985zbMATHGoogle Scholar
  5. 5.
    Bridges, D.S., Dini’s theorem: a constructive case study. In: C.S. Calude et al., eds., Combinatorics, Computability and Logic. 3rd International Conference DMTCS01, Constanţa, Romania, 2001. Proceedings. Springer, London, 69–80, 2001Google Scholar
  6. 6.
    Bridges, D., and F. Richman, Varieties of Constructive Mathematics. Cambridge University Press, Cambridge, 1987zbMATHGoogle Scholar
  7. 7.
    Dummett, M., Elements of Intuitionism. 2nd ed., Oxford University Press, Oxford, 2000Google Scholar
  8. 8.
    Ishihara, H., Informal constructive reverse mathematics. Sūrikaisekikenkyūsho Kōkyūroku 1381, 108–117, 2004Google Scholar
  9. 9.
    Ishihara, H., Constructive reverse mathematics: compactness properties. In: L. Crosilla et al., eds., From Sets and Types to Topology and Analysis. Oxford University Press, Oxford, 245–267, 2005CrossRefGoogle Scholar
  10. 10.
    Ishihara, H., Weak König’s lemma implies Brouwer’s fan theorem: a direct proof. Notre Dame J. Formal Logic 47, 249–252, 2006zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Ishihara, H., Reverse mathematics in Bishop’s constructive mathematics. Philosophia Scientiae, cahier special 6 (2006), 43–59Google Scholar
  12. 12.
    Julian, W.H., and F. Richman, A uniformly continuous function on [0,1] which is everywhere different from its infimum. Pacific J. Math 111, 333–340, 1984zbMATHMathSciNetGoogle Scholar
  13. 13.
    Kohlenbach, U., Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals. Arch. Math. Logic. 36, 31–71, 1996zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Kohlenbach, U., The use of a logical principle of uniform boundedness in analysis. In: A. Cantini et al., eds., Logic and Foundations of Mathematics. Kluwer, Dordrecht, 93–106, 1999Google Scholar
  15. 15.
    Loeb, I., Equivalents of the (weak) fan theorem. Ann. Pure Appl. Logic 132, 51–66, 2005zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    Richman, F., Intuitionism as generalization. Philos. Math. 5, 124–128, 1990zbMATHMathSciNetGoogle Scholar
  17. 17.
    Richman, F., The fundamental theorem of algebra: a constructive development without choice. Pacific J. Math. 196, 213–230, 2000zbMATHMathSciNetCrossRefGoogle Scholar
  18. 18.
    Richman, F., Constructive mathematics without choice. In: P. Schuster et al., eds., Reuniting the Antipodes. Constructive and Nonstandard Views of the Continuum. Kluwer, Dordrecht, 199–205, 2001Google Scholar
  19. 19.
    Simpson, S.G., Subsystems of Second Order Arithmetic. Springer, Berlin etc., 1999zbMATHGoogle Scholar
  20. 20.
    Troelstra, A.S., and D. van Dalen, Constructivism in Mathematics. Two volumes. North-Holland, Amsterdam, 1988Google Scholar
  21. 21.
    Veldman, W., Brouwer’s fan theorem as an axiom and as a contrast to Kleene’s alternative. Preprint, Radboud University, Nijmegen, 2005Google Scholar

Copyright information

© Springer Science+Business Media B.V. 2009

Authors and Affiliations

  • Josef Berger
    • 1
  • Peter Schuster
    • 1
  1. 1.Mathematisches InstitutUniversität MünchenTheresienstr. 39Germany

Personalised recommendations