The Vitali covering theorem in constructive mathematics
(English)Article in journal (Refereed) Submitted
This paper investigates the Vitali Covering Theorem from various constructive angles. A Vitali Cover of a metric space is a cover such that for every point there exists an arbitrarily small set of the cover containing this point. The VCT now states, that for any Vitali Cover one can find a finite, disjoint family of sets in the Vitali Cover that cover the entire space up to a set of a given non-zero measure. We will show, by means of a recursive counterexample, that there cannot be a fully constructive proof, but that adding a very weak semi-constructive principle suffices to give such a proof. Lastly, we will show that with an appropriate formalization in formal topology the non-constructive problems can be avoided completely.
Constructive mathematics, Reverse mathematics, Measure theory, Vitali's covering theorem, Formal topology
Research subject Mathematical Logic
IdentifiersURN: urn:nbn:se:uu:diva-152066OAI: oai:DiVA.org:uu-152066DiVA: diva2:412413