Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.12964

The strength of the minimum principle in constructive reverse mathematics

Tatsuji Kawai
View original source ↗Read source document ↗Export metadata ↓

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.

Explore related subjects

math.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Tatsuji Kawai. 2026-10-09. The strength of the minimum principle in constructive reverse mathematics. https://arxiv.org/abs/2610.12964

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Intuitionistic Linear Logic with Subexponentials: Type Theory, Categorical Models and Realisability

In this paper, we present a typed lambda calculus ${\bf SILL}(λ)_Σ$, a type-theoretic version of multiplicative intuitionistic linear logic with subexponentials, that is, we have many comonadic resource modalities with some interconnections between them given by a subexponential signature $Σ$. We introduce the concept of a $Σ$-assemblage to characterise models of ${\bf SILL}(λ)_Σ$ by expanding the concept of a linear category where one has multiple resource comonads and symmetric lax monoidal comonad morphisms. We also generalise several known results from linear logic and show that every $Σ$-assemblage can be viewed as a symmetric monoidal closed category equipped with a family of monoidal adjunctions and morphisms by modernising and generalising Benton's results by involving the formal theory of comonads in the fashion of Street. We give a stronger 2-categorical characterisation of $Σ$-assemblages and show that the 2-category of $Σ$-assemblages 1,2-fully faithfully embeds into the 2-category of particular families of monoidal adjunctions, their left morphisms and transformations, that is, polymodal expansions of linear-non-linear models. In the final section, we describe realisability models for the particular case of a three-element subexponential signature by describing BCI algebras with extra operators viewed as applicative morphisms and assemblies over them.

math.LO↗
arXiv2026

Dichotomy results for classes of countable graphs

We study classes of countable graphs where every member does not contain a given finite graph as an induced subgraph -- denoted by $\mathsf{Free}(\mathcal{G})$ for a given finite graph $\mathcal{G}$. Our main results establish a structural dichotomy for such classes: If $\mathcal{G}$ is not an induced subgraph of $\mathcal{P}_4$, then $\mathsf{Free}(\mathcal{G})$ is on top under effective bi-interpretability, implying that the members of $\mathsf{Free}(\mathcal{G})$ exhibit the full range of structural and computational behaviors. In contrast, if $\mathcal{G}$ is an induced subgraph of $\mathcal{P}_4$, then $\mathsf{Free}(\mathcal{G})$ is structurally simple, as witnessed by the fact that every member satisfies the computable embeddability condition. This dichotomy is mirrored in the finite setting when one considers combinatorial and complexity-theoretic properties. Specifically, it is known that $\mathsf{Free}(\mathcal{G})^{fin}$ is complete for graph isomorphism and not a well-quasi-order under embeddability whenever $\mathcal{G}$ is not an induced subgraph of $\mathcal{P}_4$, while in all other cases $\mathsf{Free}(\mathcal{G})^{fin}$ forms a well-quasi-order and the isomorphism problem for $\mathsf{Free}(\mathcal{G})^{fin}$ is solvable in polynomial time.

math.LO↗
arXiv2026

Forcing and cardinal invariants of universally null sets

We study universally null sets in forcing extensions and the cardinal invariants of their ideal $\mathcal{UN}$. We prove that the Miller model contains a nonmeager universally null set of cardinality $\aleph_2=\mathfrak{c}$, answering a question of Brendle and Larson. The proof uses preservation of universal nullity by countable support iterations of Miller forcing and shows that the set of Miller reals added during the iteration is universally null. We also prove that every universally null set in the $\mathbb{PT}_{f,g}$ model has cardinality at most $\aleph_1$, and show that there is consistently a forcing destructible universally null set. For the cardinal invariants, we show that $|X|<\operatorname{cof}(\mathcal{UN})$ for every $X\in\mathcal{UN}$, and that $\operatorname{add}(\mathcal{N})=\mathfrak{c}$ implies $\operatorname{cof}(\mathcal{UN})=\mathfrak{d}_{\mathfrak{c}}$. Finally, we prove the consistency of $\operatorname{add}(\mathcal{UN})<\operatorname{cov}(\mathcal{UN}) <\operatorname{non}(\mathcal{UN})<\operatorname{cof}(\mathcal{UN})$.

math.LO↗