Splittings and robustness for the Heine-Borel theorem

TL;DR

This paper explores the Heine-Borel theorem for uncountable coverings within higher-order Reverse Mathematics, establishing its equivalence to a version restricted to almost everywhere continuous functions and revealing its splitting into related principles.

Contribution

It proves the robustness of HBU by showing equivalence to its restriction to almost everywhere continuous functions and derives a splitting into multiple foundational principles.

Findings

HBU is equivalent to its restriction to functions continuous almost everywhere.

HBU can be split into WHBU$^{+}$, HBC$_{0}$, and WKL$_0$.

The results connect uncountable coverings with classical theorems in Reverse Mathematics.

Abstract

The Heine-Borel theorem for uncountable coverings has recently emerged as an interesting and central principle in higher-order Reverse Mathematics and computability theory, formulated as follows: HBU is the Heine-Borel theorem for uncountable coverings given as $\cup_{x\in [0,1]}(x-\Psi(x), x+\Psi(x))$ for arbitrary $\Psi:[0,1]\rightarrow \mathbb{R}^{+}$, i.e. the original formulation going back to Cousin (1895) and Lindel\"of (1903). In this paper, we show that HBU is equivalent to its restriction to functions continuous almost everywhere, an elegant robustness result. We also obtain a nice splitting HBU $\leftrightarrow$ [WHBU$^{+}$+HBC$_{0}$ + WKL$_0]$ where WHBU$^{+}$ is a strengthening of Vitali's covering theorem and where HBC$_{0}$ is the Heine-Borel theorem for countable collections (and \textbf{not sequences}) of basic open intervals, as formulated by Borel himself in 1898.