Constructive equivalence between Brouwer's fixed-point theorem and weak König's lemma

Abstract

In the context of constructive reverse mathematics, we show that Brouwer's fixed-point theorem and weak König's lemma (WKL) are equivalent. To derive WKL from Brouwer's fixed-point theorem, the construction of a continuous function on the unit square without fixed points due to Orevkov [Soviet Math. Doklady (1963), 1253--1256] is generalised to yield a uniformly continuous function on the unit square whose fixed points encode information about infinite paths of a given infinite tree.

arXiv commentCorrected the proof of the last theorem in Section 3. It now uses the minimum principle instead of WKL. The previous proof using WKL was wrong since it was applied to a Sigma^0_1 tree