Families of Sets in Constructive Measure Theory

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 $L^1$-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.