Vitali's theorem and WWKL (Q1407535)

The authors analyze theorems of classical Lebesgue measure theory using the framework of reverse mathematics. Principal results include the provability of pairwise disjoint countable additivity for open sets in RCA\(_0\), and the equivalence of the system WWKL\(_0\) and the Vitali Covering Theorem. An interesting alternative intensional formulation of Lebesgue measure is introduced, accompanied by a proof in WWKL\(_0\) of the equivalence of this formulation with the previously used definition. The article concludes with a substantial bibliography which lists half a dozen related papers by \textit{X. Yu}, for example [Ann. Pure Appl. Logic 79, 211-219 (1996; Zbl 0855.03036)].