一句话：在 Bishop 集合论中引入直谓的预测度空间与预积分空间，为 Bishop-Cheng 测度论提供可预测性重构。
Bishop 测度论（BMT）通过集合索引的补子集族等非形式概念保持直谓性，而更一般的 Bishop-Cheng 测度论（BCMT）是 Daniell 测度与积分进路的构造性版本，却因使用真类量化而高度非直谓，例如 L^p 积分空间的定义。本文在 Bishop 集合论（BST）内工作，利用集合索引的补子集族与实值部分函数族，提出预测度空间与预积分空间，作为 BCMT 中测度空间与积分空间的直谓变体。作者给出一个例子：集合 X 的补可判定子集与集中于一点的 Dirac 测度构成的预测度空间；并将 Bishop-Cheng 由测度空间构造积分空间的非平凡论证翻译到该框架，证明预测度空间可诱导简单函数的预积分空间；最后给出可积函数 L^1 作为积分空间完备化的直谓构造。
Bishop's measure theory (BMT) is an abstraction of the measure theory of a locally compact metric space $X$, and the use of an informal notion of a set-indexed family of complemented subsets is crucial to its predicative character. The more general Bishop-Cheng measure theory (BCMT) is a constructive version of the classical Daniell approach to measure and integration, and highly impredicative, as many of its fundamental notions, such as the integration space of $p$-integrable functions $L^p$, rely on quantification over proper classes (from the constructive point of view). In this paper we introduce the notions of a pre-measure and pre-integration space, a predicative variation of the Bishop-Cheng notion of a measure space and of an integration space, respectively. Working within Bishop Set Theory (BST), and using the theory of set-indexed families of complemented subsets and set-indexed families of real-valued partial functions within BST, we apply the implicit, predicative spirit of BMT to BCMT. As a first example, we present the pre-measure space of complemented detachable subsets of a set $X$ with the Dirac-measure, concentrated at a single point. Furthermore, we translate in our predicative framework the non-trivial, Bishop-Cheng construction of an integration space from a given measure space, showing that a pre-measure space induces the pre-integration space of simple functions associated to it. Finally, a predicative construction of the canonically integrable functions $L^1$, as the completion of an integration space, is included.
@article{paperbot2720,
title = {Pre-measure spaces and pre-integration spaces in predicative Bishop-Cheng measure theory},
author = {Iosif Petrakis and Max Zeuner},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 4},
year = {2024},
doi = {10.46298/lmcs-20(4:2)2024}
}