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

Abstract

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.

Cite

Hayagriva YAML

cp-integration-lcms:
  type: Article
  title: A Predicative Approach to the Constructive Integration Theory of Locally Compact Metric Spaces
  author:
    - Grubmüller, Fabian Lukas
    - Petrakis, Iosif
  date: 2025
  serial-number:
    doi: "https://doi.org/10.4115/jla.2025.17.FDS4"
  parent:
    type: Periodical
    title: Journal of Logic and Analysis
    volume: 17

BibTeX

@article{cp-integration-lcms,
  title = {A Predicative Approach to the Constructive Integration Theory of Locally Compact Metric Spaces},
  author = {Grubmüller, Fabian Lukas and Petrakis, Iosif},
  journal = {Journal of Logic and Analysis},
  volume = {17},
  year = {2025},
  doi = {10.4115/jla.2025.17.FDS4},
  url = {https://doi.org/10.4115/jla.2025.17.FDS4},
}

PDF

Link to PDF