On the logical and computational properties of the Vitali covering theorem

We study a version of the Vitali covering theorem, which we call $\textsf{WHBU}$ and which is a direct weakening of the Heine-Borel theorem for uncountable coverings, called $\textsf{HBU}$. We show that $\textsf{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 $\textsf{WHBU}$ (in the sense of Kohlenbach's higher-order Reverse Mathematics}), and how hard it is to compute the objects claimed to exist by $\textsf{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, $\textsf{WHBU}$ is only provable using Kleene's $\exists^{3}$, which implies full second-order arithmetic. On the other hand, realisers (aka witnessing functionals) for $\textsf{WHBU}$, so-called $\Lambda$-functionals, are computable from Kleene's $\exists^{3}$, but not from weaker comprehension functionals. Despite this hardness, we show that $\textsf{WHBU}$, and certain $\Lambda$-functionals, behave much better than $\textsf{HBU}$ and the associated class of realisers, called $\Theta$-functionals. In particular, we identify a specific $\Lambda$-functional called $\Lambda_{\textsf{S}}$ which adds no computational power to the Suslin functional $\textsf{S}^2$, in contrast to $\Theta$-functionals. Finally, we introduce a hierarchy involving $\Theta$-functionals and $\textsf{HBU}$.