On the logical and computational properties of the Vitali covering theorem

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