Families of Sets in Constructive Measure Theory
Max Zeuner

TL;DR
This paper develops a predicative framework for Bishop-Cheng measure theory, focusing on set families and avoiding non-constructive axioms, thus making measure theory more compatible with constructive mathematics.
Contribution
It introduces a predicative reconstruction of measure theory using set-indexed families, avoiding the axiom of countable choice and standard non-constructive methods.
Findings
Constructed pre-integration and pre-measure spaces predicatively.
Developed the $L^1$-completion within a predicative setting.
Provided a foundation for constructive measure theory without classical axioms.
Abstract
We present the first steps of a predicative reconstruction of the constructive Bishop-Cheng measure theory. Working in a semi-formal elaboration of Bishop's set theory and invoking the notion of a set-indexed family of subsets (of a given set), we arrive at notions of a pre-integration space and of a pre-measure space. We then construct the pre-integration space of simple functions associated to a pre-measure space and the -completion of a pre-integration space. Unlike the standard presentation of Bishop-Cheng measure theory, our development is completely predicative and avoids the axiom of countable choice.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Topology and Set Theory · Rough Sets and Fuzzy Logic
