On the logical and computational properties of the Vitali covering theorem

Abstract

We study a version of the Vitali covering theorem, which we call $\text{WHBU}$ and which is a direct weakening of the Heine-Borel theorem for uncountable coverings, called $\text{HBU}$. We show that $\text{WHBU}$ is central to measure theory by deriving it from various central approximation results related to Littlewood's three principles. A natural question is then how hard it is to prove $\text{WHBU}$ (in the sense of Kohlenbach's higher-order Reverse Mathematics}), and how hard it is to compute the objects claimed to exist by $\text{WHBU}$ (in the sense of Kleene's schemes S1-S9). The answer to both questions is `extremely hard', as follows: on one hand, in terms of the usual scale of (conventional) comprehension axioms, $\text{WHBU}$ is only provable using Kleene's ${\exists }^3$, which implies full second-order arithmetic. On the other hand, realisers (aka witnessing functionals) for $\text{WHBU}$, so-called $\Lambda$-functionals, are computable from Kleene's ${\exists }^3$, but not from weaker comprehension functionals. Despite this hardness, we show that $\text{WHBU}$, and certain $\Lambda$-functionals, behave much better than $\text{HBU}$ and the associated class of realisers, called $\Theta$-functionals. In particular, we identify a specific $\Lambda$-functional called ${\Lambda }_{\text{S}}$ which adds no computational power to the Suslin functional ${\text{S}}^2$, in contrast to $\Theta$-functionals. Finally, we introduce a hierarchy involving $\Theta$-functionals and $\text{HBU}$.

arXiv comment34 pages