Representations in measure theory: between a non-computable rock and a hard to prove place

Dag Normann, Sam Sanders

Published 2019-02-07Version 1

The development of measure theory in 'computational' frame-works like e.g. Reverse Mathematics, constructive mathematics, and computable analysis, proceeds by studying the computational properties of countable approximations of measurable objects. At the most basic level, these representations are provided by Littlewood's three principles, and the associated approximation theorems due to e.g. Lusin and Egorov. In light of this fundamental role, it is then a natural question how hard it is to prove the aforementioned theorems (in the sense of the Reverse Mathematics program), and how hard it is to compute the countable approximations therein (in the sense of Kleene's schemes S1-S9). The answer to both questions is 'extremely hard', as follows: one one hand, proofs of these approximation theorems require weak compactness, the measure-theoretical principle underlying e.g. Vitali's covering theorem. In terms of the usual scale of comprehension axioms, weak compactness is only provable using full second-order arithmetic. On the other hand, computing the associated approximations requires the weak fan functional $\Lambda$, which is a realiser for weak compactness, and is only computable from (a certain comprehension functional for) full second-order arithmetic. Despite this observed hardness, we show that weak compactness, and certain instances of $\Lambda$, behave much better than (Heine-Borel) compactness and the associated realiser, called the special fan functional $\Theta$. In particular, we show that the combination of $\Lambda$ and the Suslin functional has no more computational power than the latter functional alone, in contrast to $\Theta$. Finally, our results have significant foundational implications for any approach to measure theory that makes use of representations.