“Constructive equivalence between Brouwer’s fixed-point theorem and weak König’s lemma”
Giovedì 24 Settembre 2026, ore 15:00 - Sala Riunioni 7B2 - Tatsuji Kawai (University of Kochi)
Abstract
In classical reverse mathematics, the weak, Konig’s lemma (WKL) is equivalent to Brouwer’s fixed-point theorem over $RCA_0$. On the other hand, in Bishop’s constructive mathematics (BISH), Brouwer’s fixed-point theorem is equivalent to the lesser limited principle of omniscience (LLPO) , which is in turn equivalent to WKL. Hence, the equivalence between Brouwer’s fixed-point theorem and WKL over BISH cannot be directly compared to the equivalence between these two statements over $RCA_0$. In this talk, we show that Brouwer’s fixed-point theorem and WKL are equivalent in the context of constructive reverse mathematics. 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.
