Families of Sets in Constructive Measure Theory

2022/07/08 by Max Zeuner, Zeuner, Max
Computer Science · Mathematics · #Advanced Topology and Set Theory #FOS: Mathematics #Logic (math.LO) #Rough Sets and Fuzzy Logic

paper · pdf · doi:10.48550/arxiv.2207.04000

openalex publication_date 2022/07/08 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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¹-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.

Related

• Families of Sets in Bishop Set Theory
• Constructivist and Structuralist Foundations: Bishop's and Lawvere's Theories of Sets
• How constructive is constructing measures?
• Measures and all that --- A Tutorial
• A Carathéodory's Extension Theorem for Families Simpler Than an Algebras of Sets