Dini's theorem in the light of reverse mathematics

Josef Berger

Peter Schuster

pp. 153-166

in: Erik Palmgren, Krister Segerberg (eds), Logicism, intuitionism, and formalism, Berlin, Springer, 2009

Abstract

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.