A Predicative Approach to the Constructive Integration Theory of Locally Compact Metric Spaces

Based on the inherently impredicative approach of Bishop to constructive integration theory, we present a predicative version of the integration theory of locally compact metric spaces. For that, we first introduce locally compact metric spaces with a modulus of local compactness. This notion of local compactness is incompatible to Mandelkern's but equivalent to both Bishop's and Chan's corresponding notions. Using our definition, we reconstruct the integration theory of continuous functions with compact support using set-indexed families of subsets, avoiding the impredicativity of the original constructive theory of Bishop and Cheng. We work within Bishop Set Theory, which provides an expressive framework for Bishop-style constructive mathematics and constitutes a minimal extension of Bishop's original theory of sets.