Weak König's lemma implies the uniform continuity theorem (Q2851185)

From MaRDI portal

!

This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:

scientific article; zbMATH DE number 6214531
Language Label Description Also known as
default for all languages
No label defined
    English
    Weak König's lemma implies the uniform continuity theorem
    scientific article; zbMATH DE number 6214531

      Statements

      0 references
      10 October 2013
      0 references
      constructive mathematics
      0 references
      constructive reverse mathematics
      0 references
      weak König's lemma
      0 references
      WKL
      0 references
      uniform continuity theorem
      0 references
      fan theorem
      0 references
      Weak König's lemma implies the uniform continuity theorem (English)
      0 references
      The paper makes a contribution to the ``constructive reverse mathematics'' programme of classifying the strength of mathematical statements within Bishop-style constructive mathematics. The main result is that weak König's lemma (WKL) implies the uniform continuity theorem for functions from the Cantor space into the reals (which is actually equivalent to the uniform continuity theorem for functions from any compact metric space into an arbitrary metric space). It was known earlier that WKL implies the uniform continuity theorem for functions from the Cantor space into the Baire space [\textit{J. Berger}, J. Symb. Log. 73, No. 3, 933--939 (2008; Zbl 1171.03032)].NEWLINENEWLINEThe first part of the proof shows that, assuming WKL, the image of a sequentially continuous real-valued function on the Cantor space is order-located. Then, using the fact that WKL implies Brouwer's fan theorem for c-bars, it is possible to deduce that for a pointwise continuous function this image is actually bounded. By [\textit{D. Bridges} and \textit{H. Diener}, J. Symb. Log. 72, No. 4, 1379--1384 (2007; Zbl 1132.03032)], the statement ``every pointwise continuous function from the Cantor space into the reals is bounded'' is equivalent to the uniform continuity theorem.
      0 references

      Identifiers

      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references