Weak König's lemma implies the uniform continuity theorem
type: Item
instance of: scholarly article
zbMATH Open document ID: 1278.03088
DOI: 10.3233/COM-13009
author: Hannes Diener
published in: Computability
publication date: 2013-10-10T00:00:00Z
Mathematics Subject Classification ID: 03F60
Mathematics Subject Classification ID: 03B30
Mathematics Subject Classification ID: 03F35
zbMATH DE Number: 6214531
zbMATH Keywords: constructive mathematics
zbMATH Keywords: constructive reverse mathematics
zbMATH Keywords: weak König's lemma
zbMATH Keywords: WKL
zbMATH Keywords: uniform continuity theorem
zbMATH Keywords: fan theorem
MaRDI profile type: Publication
Wikidata QID: Q124798689
full work available at URL: com-13009
OpenAlex ID: W1911952075
title: Weak König's lemma implies the uniform continuity theorem
review text: 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.
description: scientific article; zbMATH DE number 6214531