On the logical and computational properties of the Vitali covering theorem

TL;DR

This paper investigates the logical and computational complexity of a weakened version of the Vitali covering theorem, revealing its deep connections to measure theory, reverse mathematics, and higher-order computability.

Contribution

It introduces the $ extsf{WHBU}$ principle, analyzes its proof-theoretic strength, and explores the computational properties of associated functionals, highlighting their relative simplicity compared to related principles.

Findings

$ extsf{WHBU}$ is provable only with Kleene's $orall^{3}$ comprehension.

Realisers for $ extsf{WHBU}$ are computable from $orall^{3}$ but not from weaker functionals.

A specific $ extsf{Lambda}_ ext{S}$-functional adds no power to the Suslin functional.

Abstract

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}$.