The strength of the minimum principle in constructive reverse mathematics
Abstract
The minimum principle states that every real-valued uniformly continuous function f : X -> R on a compact metric space X attains its minimum. Working in the base system EL0 of constructive reverse mathematics, we show that the minimum principle is equivalent to weak Konig's lemma and to the Cantor intersection theorem (i.e., the contrapositive of the Heine-Borel theorem). Moreover, the above equivalence naturally extends to the equivalence between the corresponding principles with unique existence assumptions, which are then shown to be equivalent to the Fan theorem for detachable bars and the positivity property for a real-valued uniformly continuous function on a compact space. These results sharpen the equivalence among these principles obtained by Ishihara [Math. Log. Q. (1990), 237-240] and Berger and Ishihara [Math. Log. Q. (2005), 360-364] in Bishop's constructive mathematics.
Related
- Inequalities and equalities of means in Constructive Mathematics
- The Generative Mechanism of Dimension: An Axiomatic Construction of Dimensional Conventions (Constructive Mathematics Series, Paper 6; Lean formalization, model-pair independence, numerical evidence)
- A constructive violation of additivity of minimum output von Neumann entropy
- From foundations to applications: reverse mathematics and philosophy
- Anchor Numbers: Completing Dynamic Number with the Anchor Primitive (Constructive Mathematics Series; E-system completion case No.1; Lean formalization, three heterogeneous anchored families, collapse of Cauchy dynamics)
BibTeX
@misc{kawai2026strength,
title = {{The strength of the minimum principle in constructive reverse mathematics}},
author = {Tatsuji Kawai},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.12964},
eprint = {2610.12964},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.12964},
}
RIS
TY - UNPB
TI - The strength of the minimum principle in constructive reverse mathematics
AU - Tatsuji Kawai
PY - 2026
DA - 2026/10/09
PB - arXiv
DO - 10.48550/arxiv.2610.12964
UR - https://arxiv.org/abs/2610.12964
AB - The minimum principle states that every real-valued uniformly continuous function f : X -> R on a compact metric space X attains its minimum. Working in the base system EL0 of constructive reverse mathematics, we show that the minimum principle is equivalent to weak Konig's lemma and to the Cantor intersection theorem (i.e., the contrapositive of the Heine-Borel theorem). Moreover, the above equivalence naturally extends to the equivalence between the corresponding principles with unique existence assumptions, which are then shown to be equivalent to the Fan theorem for detachable bars and the positivity property for a real-valued uniformly continuous function on a compact space. These results sharpen the equivalence among these principles obtained by Ishihara [Math. Log. Q. (1990), 237-240] and Berger and Ishihara [Math. Log. Q. (2005), 360-364] in Bishop's constructive mathematics.
ER -