PreprintarXiv licencearXiv
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.
Related
- A local-to-global fixed point theorem for CAT(0) spaces with a uniform elliptic gap
- Applications of the fixed point theorem for mappings contracting perimeters of triangles: ODEs, PDEs, integer and difference equations
- Positive Solutions of a Fractional BVP and the Reach of the Omitted Ray Fixed Point Theorem
- Space curves in Hahn calculus: rotation structure, a fundamental theorem, and q-deformed invariants at the fixed point
- Differentiable Horn Programs: A Constructive Expressivity Theorem for Latent Rule Operators
BibTeX
@misc{kawai2026constructive,
title = {{Constructive equivalence between Brouwer's fixed-point theorem and weak König's lemma}},
author = {Tatsuji Kawai},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2609.04644},
eprint = {2609.04644},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.04644},
}
RIS
TY - UNPB
TI - Constructive equivalence between Brouwer's fixed-point theorem and weak König's lemma
AU - Tatsuji Kawai
PY - 2026
DA - 2026/10/14
PB - arXiv
DO - 10.48550/arxiv.2609.04644
UR - https://arxiv.org/abs/2609.04644
AB - 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.
ER -