sectioning

# Families of Sets in Constructive Measure Theory

Max Zeuner
Department of Mathematics  Stockholm University
<EMAIL_ADDRESS>
###### Contents

  1. 0 Introduction
  2. 1 Bishop’s set theory
    1. 1 Basics
    2. 2 Complemented subsets and partial functions
    3. 3 On double series of real numbers
  3. 2 Set indexed families
    1. 1 Families of sets
    2. 2 Families of subsets
    3. 3 Families of complemented subsets
    4. 4 Families of partial functions
  4. 3 Measure theory
    1. 1 On the impredicative character of BCMT
      1. 1 Three problems
      2. 2 Pre-measure and pre-integration spaces
    2. 2 The pre-integration space of simple functions
    3. 3 Complete extension of a pre-integration space
      1. 1 The 1-norm of a pre-integration space
      2. 2 The pre-integration space of canonically integrable functions
  5. 4 Conclusion

##  Chapter 0 Introduction

Within Bishop-style constructive mathematics, or constructive analysis more
precisely, the development of constructive measure and integration theory is
especially interesting and challenging. Since classical measure theory draws
heavily on notions of classical set theory and is highly non-constructive in
its character, many central concept cannot directly be translated into a
constructive setting. Bishop himself was not entirely satisfied with the
generality of the measure-theoretic results in chapters 6 and 7 of his seminal
book [Bis67] and developed a new approach to constructive measure theory
together with Cheng in [BC72]. This Bishop-Cheng measure theory (BCMT) is also
included and expanded in Bishop and Bridges’ book [BB85].

Accordingly, the presentation of set theory is a bit different in the two
books in order to meet the demands of the respective measure theories. The
set-theoretic operations on the complemented subsets of a set $X$ were changed
to behave better with BCMT’s function theoretic approach to integration and
measure theory, while parts of chapter 3 of [Bis67] that became obsolete for
BCMT were entirely left out in chapter 3 of [BB85]. However, the general
treatment of set theory is rather short in both books. This led to confusions
about e.g. the status of the powerset in Bishop-style mathematics. It seems
that in BCMT the powerset of a set $X$ is itself treated as a set, while in
the measure theory of [Bis67] the powerset is avoided by invoking set-indexed
families of subsets instead.

The use of the powerset makes BCMT an impredicative theory and even though
BCMT remains an active area of research111There is for example the recent book
on constructive probability theory by Chan, see [Cha21], or work on
formalizing BCMT in the proof-assistant Coq, see [Sem20]., it is desirable to
have a predicative approach to constructive measure theory. Such an
alternative was realized by the point-free, algebraic approach of Coquand and
Palmgren in [CP02], which was further developed by Spitters in [Spi05] and
[Spi06]. This constructive algebraic measure theory is not only predicative,
but also conceived by many as technically and conceptually simpler than BCMT.

However, as already mentioned certain impredicativities were generally avoided
by Bishop in his ’67 book by using set-indexed families instead of the
powerset. So, one might hope that by being more explicit about the use of such
families, BCMT can be ’predicativized’. Afterall, set-indexed families of sets
and subsets are only briefly introduced in chapter 3 of [BB85] and often
appear only implicitly later in the book. Recently Petrakis has studied these
families more extensively in [Pet19a] and [Pet21] and has applied his results
to the theory of Bishop spaces. A full-scale account of various kinds of set-
indexed families, and their application to different areas of constructive
mathematics, will be given in [Pet20]. In this paper we want follow this
strategy to show that central parts of BCMT can be done predicatively.

Of course, we have to revisit Bishop’s set theory and introduce all the
relevant notions before we can turn to measure theory. The paper will thus be
structured as follows:

  1. (i)

Following Petrakis’ work we will introduce an informal language suitable for
Bishop’s set theory (BST) in the next section. This will allow us to talk in
more detail about the fundamental set-theoretic concepts we will need for
BCMT.

  2. (ii)

After that we introduce families of sets and subsets, indexed by some set $I$
in BST. In order to use set-indexed families in BCMT we will also introduce
families of complemented subsets and partial functions indexed by some set
$I$.

  3. (iii)

Having introduced the necessary technical background, we look at the
impredicativities in BCMT and refine the notions integration and measure space
by the explicit use of set-indexed families in order to introduce what we call
pre-integration and pre-measure spaces that are defined predicatively.

  4. (iv)

We give an example of a pre-measure space and show how the pre-integration
space of simple functions over a pre-measure space can be defined.

  5. (v)

Finally, we introduce the pre-integration space of canonically integrable
functions over a pre-integration as a predicative version of the complete
extension. This shows that the impredicative totality of integrable functions
is not needed in order to construct the complete extension.

This paper revisits only some parts of BCMT, so we will sketch a few
directions, which further research using pre-integration and pre-measure
spaces could take.

##  Chapter 1 Bishop’s set theory

Before we can introduce the various forms set-indexed families we need to
discuss the fundamental notions of Bishop set theory (BST) necessary for
formulating Bishop-Cheng measure theory. Note that even though some things are
presented a bit more detailed here than in [BB85], we still work informally.

###  1 Basics

In this section we will follow [Pet21] to introduce the basic ingredients of
BST.111See [Pet19a] for another formulation. The main difference is that there
is a universe of functions $\mathbb{V}_{1}$ but no dependent assignment
routines. First we have a primitive notion of definitional equality $:=$
between terms and a primitive notion of ordered pair $(s,t)$ for some terms
$s,t$ together with projections $\mathsf{pr}_{1}(s,t):=s$ and
$\mathsf{pr}_{2}(s,t):=t$. There is also the primitive notion of a _totality_
and a primitive totality of natural numbers $\mathbb{N}$. Any other totality
$X$ is defined through a membership condition $x\in X$, i.e. a formula
expressing the condition an object $x$ has to satisfy in order to belong to
$X$. For any totality $X$, an _equality_ is a formula $x=_{X}y$ defined for
$x,y\in X$ such that it satisfies the properties of an equivalence relation.
For the primitive totality $\mathbb{N}$ we also have a primitive equality
$=_{\mathbb{N}}$. A pair $(X,=_{X})$, where $X$ is a totality with an equality
$=_{X}$ is a _set_ if the member-ship condition expresses a construction. In
particular $(\mathbb{N},=_{\mathbb{N}})$ is a set. We will often drop the
equality of a set if it is clear from the context.

In BST the notion of a function is not primitive but can be derived from the
primitive notion of an _asssignment routine_ (or finite routine). For
totalities $X,Y$ an assignment routine $\alpha:X\rightsquigarrow Y$ assigns to
each element $x\in X$ an element $y\in Y$, in which case we write
$\alpha(x):=y$. For any $X$ we have an assignment routine
$\text{id}_{X}:X\rightsquigarrow X$, which assigns each $x\in X$ to itself. If
$(X,=_{X})$ and $(Y,=_{Y})$ are sets, an assignment routine
$f:X\rightsquigarrow Y$ is a _function_ if

$\displaystyle\forall x,x^{\prime}\in
X:\;x=_{X}x^{\prime}\;\Rightarrow\;f(x)=_{Y}f(x^{\prime})$

In this case we write $f:X\rightarrow Y$ and denote the totality of functions
$X\rightarrow Y$ by $\mathbb{F}(X,Y)$. We have an equality
$=_{{\mathbb{F}(X,Y)}}$ on $\mathbb{F}(X,Y)$ which is defined by

$\displaystyle f=_{{\mathbb{F}(X,Y)}}g\quad:\Leftrightarrow\quad\forall x\in
X:\;f(x)=_{Y}g(x)$

It easy to check that this satisfies the properties of an equivalence relation
and for any two sets $X,Y$ we have the set of functions
$(\mathbb{F}(X,Y),=_{{\mathbb{F}(X,Y)}})$ from $X$ to $Y$. We say a function
$e:X\rightarrow Y$ is an embbeding if

$\displaystyle\forall x,x^{\prime}\in
X:\;x=_{X}x^{\prime}\;\Leftrightarrow\;e(x)=_{Y}e(x^{\prime})$

In this case we write $e:X\hookrightarrow Y$. We now want to give an important
example of a totality that is not a set.

######  Example 1.1.

Let $\mathbb{V}_{0}$ be the totality of sets. We have an equality on
$\mathbb{V}_{0}$ defined by

$\displaystyle X=_{\mathbb{V}_{0}}Y\;:\Leftrightarrow\;\exists
f\in\mathbb{F}(X,Y)\;\exists g\in\mathbb{F}(Y,X)\text{ s.t. }f\circ
g=_{{\mathbb{F}(X,X)}}\text{id}_{X}\;\&\;g\circ
f=_{{\mathbb{F}(Y,Y)}}\text{id}_{Y}$

In this case we write $(f,g):X=_{\mathbb{V}_{0}}Y$ However,
$(\mathbb{V}_{0},=_{\mathbb{V}_{0}})$ is not a set, since in this case we
would have $\mathbb{V}_{0}\in\mathbb{V}_{0}$, which is not acceptable from a
predicative point of view. There is no general construction to construct a set
$X\in\mathbb{V}_{0}$. Since we still have an equality on $\mathbb{V}_{0}$, we
say that it is a _class_.

Now let $I$ be a set and consider an assignment routine
$\lambda_{0}:I\rightsquigarrow\mathbb{V}_{0}$. We have a primitive notion of a
_dependent assignment routine_ over $\lambda_{0}$, which we will write as

$\displaystyle\Phi:\bigcurlywedge_{i\in I}\lambda_{0}(i)$

and which assigns to each element $i\in I$ an element
$\Phi_{i}\in\lambda_{0}(i)$. We have a totality $\mathbb{A}(I,\lambda_{0})$ of
dependent assignment routines over $\lambda_{0}$ with equality

$\displaystyle\Phi=_{{\mathbb{A}(I,\lambda_{0})}}\Psi\;:\Leftrightarrow\;\forall
i\in I:\;\Phi_{i}=_{\lambda_{0}(i)}\Psi_{i}$

Let $X$ be a set, a _subset_ of $X$ is a pair $(A,i_{A})$, where $A$ is a set
and $i_{A}:A\hookrightarrow X$ is an embedding. We have a totality
$\mathcal{P}(X)$ of subsets of $X$, which is not a set since this would
require that $\mathbb{V}_{0}$ is a set. However, we still have an equality
$=_{{\mathcal{P}(X)}}$ that is defined by

$\displaystyle(A,i_{A})=_{{\mathcal{P}(X)}}(B,i_{B})\;:\Leftrightarrow\;\exists
f\in\mathbb{F}(A,B)\;\exists g\in\mathbb{F}(B,A):\;$ $\displaystyle\forall
a\in A:\;i_{A}(a)=_{X}\big{(}i_{B}\circ f\big{)}(a)$ $\displaystyle\&\;$
$\displaystyle\forall b\in B:\;i_{B}(b)=_{X}\big{(}i_{A}\circ g\big{)}(b)$

i.e. the following diagrams commute

${A}$${B}$${X}$$\scriptstyle{f}$$\scriptstyle{i_{A}}$$\scriptstyle{g}$$\scriptstyle{i_{B}}$

In this case we say that $f$ and $g$ _witness_ the equality of $A$ and $B$ as
subsets and write $(f,g):A=_{{\mathcal{P}(X)}}B$, as we will often drop the
the embedding of a subset if it is clear from the context. It is easy to prove
that in this case $f$ and $g$ are embeddings and

$\displaystyle(f,g):A=_{{\mathcal{P}(X)}}B\;\Rightarrow\;(f,g):A=_{\mathbb{V}_{0}}B$

The next lemma shows that the witnesses for the equality of subsets are
unique. This fact will be usefull later.

######  Lemma 1.2.

Let $X$ be a set and $(A,i_{A})$ and $(B,i_{B})$ be subsets of $X$. Let
$f,\tilde{f}:A\rightarrow B$ and $g,\tilde{g}:B\rightarrow A$ be functions
such that

  * •

$(f,g):A=_{{\mathcal{P}(X)}}B$ and

  * •

$(\tilde{f},\tilde{g}):A=_{{\mathcal{P}(X)}}B$

then $f=_{{\mathbb{F}(A,B)}}\tilde{f}$ and $g=_{{\mathbb{F}(B,A)}}\tilde{g}$.

###### Proof.

Let $a\in A$, then $i_{A}(a)=_{X}i_{B}\big{(}f(a)\big{)}$ and
$i_{A}(a)=_{X}i_{B}\big{(}\tilde{f}(a)\big{)}$, and hence by transitivity
$i_{B}\big{(}f(a)\big{)}=_{X}i_{B}\big{(}\tilde{f}(a)\big{)}$. Since $i_{B}$
is an embedding we get that $f(a)=_{B}\tilde{f}(a)$, and thus
$f=_{{\mathbb{F}(A,B)}}\tilde{f}$. By a completely analogous arument we also
get that $g=_{{\mathbb{F}(B,A)}}\tilde{g}$. ∎

For two subsets $A$ and $B$ of $X$ we say that $A$ is a subset of $B$ if there
is a function $f:A\rightarrow B$ such that for all $a\in A$ we have
$i_{A}(a)=_{X}\big{(}i_{B}\circ f\big{)}(a)$, i.e. if the following diagram
commutes

${A}$${B}$${X}$$\scriptstyle{f}$$\scriptstyle{i_{A}}$$\scriptstyle{i_{B}}$

In this case we write $f:A\subseteq B$. Again, it is easy to prove that in
this case $f$ is an embedding and we get

$\displaystyle f:A\subseteq B\;\&\;g:B\subseteq
A\;\Rightarrow\;(f,g):A=_{{\mathcal{P}(X)}}B$

When we discuss BCMT later, most of the subsets we will be concerned with are
not obtained by constructing some set and then some embedding, but rather by
seperating elements out of some existing set. We shall make this precise now.
Let $X$ be a set and $P$ a property defined for elements of $X$, which is
_extensional_ in the sense that it respects the equality on $X$, i.e. we have
that

$\displaystyle\forall x,y\in
X:\;x=_{X}y\;\Rightarrow\;\big{(}P(x)\;\Rightarrow\;P(y)\big{)}$

Let $X_{P}$ be the totality with membership-condition defined by

$\displaystyle x\in X_{P}\;:\Leftrightarrow\;x\in X\;\&\;P(x)$

Then we get an equality on $X_{P}$ induced by by the equality $=_{X}$ and the
assignment routine $i_{X_{P}}:X_{P}\rightsquigarrow X$ given by $x\mapsto x$
is an embedding. We will usually denote the subset $(X_{P},i_{X_{P}})$ of $X$
by $\\{x\in X:\;P(x)\\}$ and take the embedding as implicitly given. The next
example will be of importance for our definition of set-indexed families.

######  Example 1.3.

Consider two sets $X$ and $Y$, the cartesian product $X\times Y$ is the
totality defined by the membership-formula

$\displaystyle z\in X\times Y\;:\Leftrightarrow\;\exists x\in X\;\exists y\in
Y\text{ s.t. }\big{(}z:=(x,y)\big{)}$

together with the equality

$\displaystyle z=_{X\times
Y}z^{\prime}\;:\Leftrightarrow\;\mathsf{pr}_{1}(z)=_{X}\mathsf{pr}_{1}(z^{\prime})\;\&\;\mathsf{pr}_{2}(z)=_{Y}\mathsf{pr}_{2}(z^{\prime})$

In particular $X\times Y$ is again a set. consider the following property $P$
on $X\times X$:

$\displaystyle
P(z)\;:\Leftrightarrow\;\big{(}z:=(x,y)\;\Rightarrow\;x=_{X}y\big{)}$

This is an extensional property and we call the set $\big{(}{X\times
X}\big{)}_{P}$ the _diagonal_ of $X$ and denote it by

$\displaystyle D(X):=\;\\{(x,y)\in X\times X:\;x=_{X}y\\}$

######  Definition 1.4.

Let $X$ be a set and $(A,i_{A})$ and $(B,i_{B})$ be subsets of $X$. Let the
union $A\cup B$ be the totality defined by the membership-condition

$\displaystyle c\in A\cup B\;:\Leftrightarrow\;\big{(}\exists a\in A\text{
s.t. }c:=a\big{)}\;\text{or}\;\big{(}\exists b\in B\text{ s.t. }c:=b\big{)}$

with the equality

$\displaystyle c=_{A\cup B}c^{\prime}\;:\Leftrightarrow\;$
$\displaystyle\big{(}\exists a,a^{\prime}\in A\text{ s.t.
}c:=a\;\&\;c^{\prime}:=a^{\prime}\;\&\;a=_{A}a^{\prime}\big{)}\text{ or}$
$\displaystyle\big{(}\exists b,b^{\prime}\in B\text{ s.t.
}c:=b\;\&\;c^{\prime}:=b^{\prime}\;\&\;b=_{B}b^{\prime}\big{)}$

and embedding

$\displaystyle i_{A\cup B}:A\cup B$ $\displaystyle\hookrightarrow X$
$\displaystyle c$ $\displaystyle\mapsto\begin{cases}i_{A}(a),\text{ if
}c:=a\text{ for }a\in A\\\ i_{B}(b),\text{ if }c:=b\text{ for }b\in
B\end{cases}$

Let the intersection $A\cap B$ be the set $\\{(a,b)\in A\times
B:\;i_{A}(a)=_{X}i_{B}(b)\\}$ with the embedding

$\displaystyle i_{A\cap B}:A\cap B$ $\displaystyle\hookrightarrow X$
$\displaystyle(a,b)$ $\displaystyle\mapsto i_{A}(a)$

It is easy to check that $i_{A\cap B}$ and $i_{A\cup B}$ are indeed
embeddings, turning $A\cap B$ and $A\cup B$ into subsets of $X$. Later we will
see a different way to define union and intersection that will turn out
equivalent up to equality of subsets.

###  2 Complemented subsets and partial functions

So far, we have seen how to talk about sets, functions and subsets in BST. In
BCMT we are however primarily concerned with partial functions and
complemented subsets, which we want to introduce in this section. The
operations on complemented subsets as presented in [BB85] are different from
that in [Bis67] and we will present the former account in order to be able to
use them in BCMT. Before we do that we will briefly introduce partial
functions.

Let $X$ and $Y$ be sets. A partial function from $X$ to $Y$ is a triple
$(A,i_{A},f)$ such that $(A,i_{A})$ is subset of $X$ and
$f\in\mathbb{F}(A,Y)$. We call $A$ the domain of $f$ and write
$f:X\rightharpoonup Y$ if the domain is clear from the context. Let
$\mathbb{F}^{\rightharpoonup}(X,Y)$ be the totality of partial functions from
$X$ to $Y$ with the following equality. We say two partial functions
$(A,i_{A},f)$ and $(B,i_{B},g)$ are equal if there are functions
$\varphi\in\mathbb{F}(A,B)$ and $\psi\in\mathbb{F}(B,A)$ such that the
following diagrams commute

${A}$${B}$${X}$${Y}$$\scriptstyle{\varphi}$$\scriptstyle{i_{A}}$$\scriptstyle{f}$$\scriptstyle{\psi}$$\scriptstyle{i_{B}}$$\scriptstyle{g}$

In this case we will write
$(\varphi,\psi):(A,i_{A},f)=_{{\mathbb{F}^{\rightharpoonup}(X,Y)}}(B,i_{B},g)$
or just $(\varphi,\psi):f=_{{\mathbb{F}^{\rightharpoonup}(X,Y)}}g$ if the
domains are clear from the context. It follows immediatelly that in this case
we also have $(\varphi,\psi):(A,i_{A})=_{{\mathcal{P}(X)}}(B,i_{B})$. Using
lemma (1.2) we can conclude that the witnesses for the equality of partial
functions are unique. Since the domain of a partial functions can in principle
be any subset of $X$ the totality of partial functions cannot be a set.

Here we will mostly be concerned with real-valued partial functions, i.e. the
case where $Y:=\mathbb{R}$. For the totality of real-valued partial functions
on a set $X$ we write
$\mathcal{F}(X):=\mathbb{F}^{\rightharpoonup}(X,\mathbb{R})$. We want to
define the usual (pointwise) operations on $\mathcal{F}(X)$. Let $(A,i_{A},f)$
and $(B,i_{B},g)$ be real-valued partial functions and $\ast$ be any of the
operations $+,-,\cdot,\wedge,\vee$ on $\mathbb{R}$ (Here $\wedge,\vee$ denote
the minimum and maximum of two reals), then we have a partial function $(A\cap
B,i_{A\cap B},f\ast g)$ with

$\displaystyle f\ast g:A\cap B$ $\displaystyle\rightarrow\mathbb{R}$
$\displaystyle(a,b)$ $\displaystyle\mapsto f(a)\ast g(b)$

Also for any $a\in\mathbb{R}$ and any
$\phi\in\mathbb{F}(\mathbb{R},\mathbb{R})$ we have partial functions
$(A,i_{A},a\cdot f)$ and $(A,i_{A},\phi\circ f)$ that are obtained similarly
by pointwise multiplying with $a$ or composing with $\phi$.

Since negative definitions are often not very useful in constructive
mathematics, we have to use positive counterparts. Complemented subsets are
the positive counterpart to the complement of a subset.

######  Definition 2.1.

Let $X$ be a set and let $\neq_{X}$ be a binary relation defined on $X$. Then
$\neq_{X}$ is said to be an _inequality_ or apartness relation on $X$ if the
following conditions are satisfied:

  1. (i)

$\forall x,y\in X:\;(x=_{X}y\;\&\;x\neq_{X}y)\;\Rightarrow\;\bot$

  2. (ii)

$\forall x,y\in X:\;x\neq_{X}y\;\Rightarrow\;y\neq_{X}x$

  3. (iii)

$\forall x,y\in X:\;x\neq_{X}y\;\Rightarrow\;\big{(}\forall z\in
X:\;x\neq_{X}z\text{ or }y\neq_{X}z\big{)}$

We say that two subsets $(A,i_{A})$ and $(B,i_{B})$ of $X$ are apart with
respect to $\neq_{X}$ if

$\displaystyle\forall a\in A\;\forall b\in B:\;i_{A}(a)\neq_{X}i_{B}(b)$

In this case we write $A][_{\neq_{X}}B$ or just $A][B$ if the inequality
$\neq_{X}$ is clear from the context. A _complemented subset_ of $X$ with
respect to $\neq_{X}$ is a pair of subsets $\bm{A}:=(A^{1},A^{0})$ such that
$A^{1}][_{\neq_{X}}A^{0}$.

The notion of an apartness relation is the positive counterpart of the mere
negation of the equality $=_{X}$. From now on let $X$ be equipped with a fixed
inequality $\neq_{X}$. We denote the totality of complemented subsets by
$\mathcal{P}^{][}(X)$. Again this totality is obviously not a set. Still, we
have an equality defined on $\mathcal{P}^{][}(X)$ by

$\displaystyle\bm{A}=_{{\mathcal{P}^{{{][}}}(X)}}\bm{B}\;:\Leftrightarrow\;A^{1}=_{{\mathcal{P}(X)}}B^{1}\;\&\;A^{0}=_{{\mathcal{P}(X)}}B^{0}$

For complemented subsets $\bm{A}:=(A^{1},A^{0})$ and $\bm{B}:=(B^{1},B^{0})$
we write $\bm{A}<\bm{B}$ if $A^{1}\subseteq B^{1}$ and $B^{0}\subseteq A^{0}$.
We now want to introduce operations of complented union, intersection and
substraction as well as complementation. Let $\bm{A}:=(A^{1},A^{0})$ and
$\bm{B}:=(B^{1},B^{0})$ be complemented subsets and define

  * •

$\bm{A}\wedge\bm{B}:=\big{(}A^{1}\cap B^{1},\;(A^{1}\cap B^{0})\cup(A^{0}\cap
B^{1})\cup(A^{0}\cap B^{0})\big{)}$

  * •

$\bm{A}\vee\bm{B}:=\big{(}(A^{1}\cap B^{0})\cup(A^{0}\cap B^{1})\cup(A^{1}\cap
B^{1}),\;A^{0}\cap B^{0}\big{)}$

  * •

$-\bm{A}:=(A^{0},A^{1})$

  * •

$\bm{A}-\bm{B}:=\bm{A}\wedge(-\bm{B})$

We can prove commutativity and associativity of $\wedge$ and $\vee$ as well as
the following (with $\bm{C}$ being a complemented subset):

  1. (i)

$--\bm{A}=_{{\mathcal{P}^{{{][}}}(X)}}\bm{A}$

  2. (ii)

$-(\bm{A}\wedge\bm{B})=_{{\mathcal{P}^{{{][}}}(X)}}(-\bm{A})\vee(-\bm{B})$

  3. (iii)

$-(\bm{A}\vee\bm{B})=_{{\mathcal{P}^{{{][}}}(X)}}(-\bm{A})\wedge(-\bm{B})$

  4. (iv)

$\bm{A}\wedge(\bm{B}\vee\bm{C})=_{{\mathcal{P}^{{{][}}}(X)}}(\bm{A}\wedge\bm{B})\vee(\bm{A}\wedge\bm{C})$

  5. (v)

$\bm{A}\vee(\bm{B}\wedge\bm{C})=_{{\mathcal{P}^{{{][}}}(X)}}(\bm{A}\vee\bm{B})\wedge(\bm{A}\vee\bm{C})$

The poofs are straightforward though tedious. The definitions of $\wedge$ and
$\vee$ look a bit complicated and indeed the corresponding definitions in
chapter 3 of [Bis67] appear simpler with the same algebraic laws still being
provable. However, the definitions presented here behave much better with the
characteristic functions of complemented subsets. Let $\bm{2}:=\\{0,1\\}$, for
a complemented subset $\bm{A}:=(A^{1},A^{0})$ we define its characteristic
function by

$\displaystyle\chi_{\bm{A}}:\;$ $\displaystyle A^{1}\cup
A^{0}\rightarrow\bm{2}$ $\displaystyle x\mapsto\begin{cases}1,\;x\in A^{1}\\\
0,\;x\in A^{0}\end{cases}$

So, if we interpret $\bm{2}$ as a subset on $\mathbb{R}$ the characteristic
function of a complemented subset is an element of $\mathcal{F}(X)$ and it is
easy to check that

  * •

$\chi_{\bm{A}\wedge\bm{B}}=_{{\mathcal{F}(X)}}\chi_{\bm{A}}\wedge\chi_{\bm{B}}$

  * •

$\chi_{\bm{A}\vee\bm{B}}=_{{\mathcal{F}(X)}}\chi_{\bm{A}}\vee\chi_{\bm{B}}$

  * •

$\chi_{-\bm{A}}=_{{\mathcal{F}(X)}}1-\chi_{\bm{A}}$

where the operations on the characteristic functions are the pointwise minimum
and maximum that we defined above and composition with the function
$(1-\\_):\mathbb{R}\rightarrow\mathbb{R}$. With this the above properties of
the complemented operations can also be proven more easily. We conclude the
section with a final remark on partial functions and inequalities.

######  Remark 2.2.

We have a canonical inequality on $\mathbb{R}$ that is given by

$\displaystyle x\neq_{\mathbb{R}}y\;:\Leftrightarrow\;\lvert x-y\rvert>0$

If $X$ is equipped with an inequality $\neq_{X}$ as well, we take
$\mathcal{F}(X)$ to be the totality of strongly extensional partial functions,
i.e. for any $(A,i_{A},f)$ we assume that

$\displaystyle\forall a,b\in
A:\;f(a)\neq_{\mathbb{R}}f(b)\;\Rightarrow\;i_{A}(a)\neq_{X}i_{A}(b)$

###  3 On double series of real numbers

At the end of this section we want to consider some aspects of constructive
analysis that will be needed for our discussion of BCMT later. One important
point is that converging or Cauchy sequences of reals are taken to be
modulated in order to avoid the axiom of countable choice. We will also prove
a result that is implicitly used in [BB85] for crucial results of BCMT but
doesnt’t seem to be explicitly stated in the literature on constructive
mathematics.

We will follow the presentation in [Sch06]. A real number is a pair
$x=\big{(}(a_{n})_{n\in\mathbb{N}},M)$ consisting of a sequences of rational
numbers $(a_{n})_{n\in\mathbb{N}}$ and $M:\mathbb{N}\rightarrow\mathbb{N}$ is
strictly increasing such that

$\displaystyle\forall p\in\mathbb{N}\;\forall n,m\geq M(p):\;\lvert
a_{n}-a_{m}\rvert\leq\frac{1}{2^{p}}$

Two reals $x=\big{(}(a_{n})_{n\in\mathbb{N}},M)$ and
$y=\big{(}(b_{n})_{n\in\mathbb{N}},N)$ are equal, which we write as
$x=_{\mathbb{R}}y$, if

$\displaystyle\forall p\in\mathbb{N}:\;\lvert
a_{M(p+1)}-b_{N(p+1)}\rvert\leq\frac{1}{2^{p}}$

Note that this is equivalent to

$\displaystyle\forall p\in\mathbb{N}\;\exists n_{0}\in\mathbb{N}\;\forall
n\geq n_{0}:\;\lvert a_{n}-b_{n}\rvert\leq\frac{1}{2^{p}}$

Using this second characterisation of equality it is not hard to show that
$=_{\mathbb{R}}$ is indeed an equality on the totality $\mathbb{R}$. The usual
operations like addition, multiplication and absolute value and the order
realtions can be defined, and the usual basic properties, like the triangle
inequality, can be derived.

######  Definition 3.1.

Let $(x_{n})_{n\in\mathbb{N}}$ be a sequence of reals, $x\in\mathbb{R}$ and
$M:\mathbb{N}\rightarrow\mathbb{N}$ strictly increasing. We say that
$(x_{n})_{n\in\mathbb{N}}$ is a Cauchy-sequence with modulus $M$ if

$\displaystyle\forall p\in\mathbb{N}\;\forall n,m\geq M(p):\;\lvert
x_{n}-x_{m}\rvert\leq\frac{1}{2^{p}}$

Furthermore, we say that $(x_{n})_{n\in\mathbb{N}}$ converges to $x$ with
modulus $M$ if

$\displaystyle\forall p\in\mathbb{N}\;\forall n\geq M(p):\;\lvert
x_{n}-x\rvert\leq\frac{1}{2^{p}}$

Note, that if we use notation like $\lim_{n\rightarrow\infty}x_{n}=x$ or say
that some sequence or series converges we implicitly assume the existence of a
corresponding modulus of convergence.

Finally, for our discussion we will need some facts about the convergence of
double series. Reorderings of infinite series have been studied constructively
in [BB09] and [BBDS13], but we are concerned with a slightly different
problem. We want to show that for some fixed bijection from $\mathbb{N}$ to
$\mathbb{N}\times\mathbb{N}$ we can rearrange a double series into a single
one if it converges absolutely. Consider the following enumeration of
$\mathbb{N}\times\mathbb{N}$:

$\begin{matrix}(1,1)^{\;\bm{1}}&(1,2)^{\;\bm{3}}&(1,3)^{\;\bm{6}}&\iddots\\\
(2,1)^{\;\bm{2}}&(2,2)^{\;\bm{5}}&(2,3)^{\;\bm{9}}\\\
(3,1)^{\;\bm{4}}&(3,2)^{\;\bm{8}}\\\ (4,1)^{\;\bm{7}}\end{matrix}$

Using this pattern as an enumeration of $\mathbb{N}_{0}\times\mathbb{N}_{0}$
starting with zero, we would get a bijection that is quite conveniently
expressed by the following function222This is why this particular bijection is
often used to code pairs in computability theory.

$\displaystyle c:\;$
$\displaystyle\mathbb{N}_{0}\times\mathbb{N}_{0}\rightarrow\mathbb{N}_{0}$
$\displaystyle(x,y)\mapsto\frac{(x+y)(x+y+1)}{2}+y$

That means that our enumeration of $\mathbb{N}\times\mathbb{N}$ corresponds to
a bijection $\varphi:\mathbb{N}\rightarrow\mathbb{N}\times\mathbb{N}$ with
inverse

$\displaystyle\varphi^{-1}(n,m)=c(n-1,m-1)+1$

Using this particular bijection we can state the following lemma.

######  Lemma 3.2.

Let $\big{(}x_{nk}\big{)}_{n,k\in\mathbb{N}}$ be a sequence of sequences in
$\mathbb{R}$, i.e. an element of
$\mathbb{F}(\mathbb{N},\mathbb{F}(\mathbb{N},\mathbb{R}))$, and let
$\big{(}y_{n}\big{)}_{n\in\mathbb{N}}$ be the sequence defined by

$\displaystyle
y_{m}:=x_{\mathsf{pr}_{1}\big{(}\varphi(m)\big{)}\;\mathsf{pr}_{2}\big{(}\varphi(m)\big{)}}$

i.e. $x_{nk}=y_{\varphi^{-1}(n,k)}$. Then $\sum_{n}\sum_{k}x_{nk}$ converges
absolutely if and only if $\sum_{m}y_{m}$ converges absolutely, in which case
we have that

$\displaystyle\sum_{n=1}^{\infty}\sum_{k=1}^{\infty}x_{nk}=\sum_{m=1}^{\infty}y_{m}$

###### Proof.

First assume that $\sum_{n}\sum_{k}\lvert x_{nk}\rvert$ exists and for the
moment let us also assume that $x_{nk}\geq 0$ for all $n,k\in\mathbb{N}$.
Assume that $\big{(}\sum_{k=1}^{N}x_{nk}\big{)}_{N\in\mathbb{N}}$ converges to
$\ell_{n}:=\sum_{k}x_{nk}$ with modulus $M_{n}$ and that
$\big{(}\sum_{n=1}^{N}\sum_{k}x_{nk}\big{)}_{N\in\mathbb{N}}$ converges to
$\ell:=\sum_{n}\sum_{k}x_{nk}$ with modulus $M$. We have to construct a
modulus $M^{\prime}:\mathbb{N}\rightarrow\mathbb{N}$ s.t. for $p\in\mathbb{N}$
and $N\geq M^{\prime}(p)$ we have

$\displaystyle 0\leq\ell-\sum_{m=1}^{N}y_{m}\leq\frac{1}{2^{p}}$

First, consider $N\geq M(p+1)$, then

$\displaystyle 0\leq\ell-\sum_{n=1}^{N}\ell_{n}\leq\frac{1}{2^{(p+1)}}$

Now, consider $N\geq M_{n}(M(p+1)+p+1)$, then

$\displaystyle
0\leq\ell_{n}-\sum_{k=1}^{N}x_{nk}\leq\frac{1}{2^{M(p+1)}}\frac{1}{2^{(p+1)}}\leq\frac{1}{M(p+1)}\frac{1}{2^{(p+1)}}$

Hence

$\displaystyle 0$
$\displaystyle\leq\ell-\sum_{n=1}^{M(p+1)}\;\;\sum_{k=1}^{M_{n}(M(p+1)+p+1)}x_{nk}$
$\displaystyle=\ell-\sum_{n=1}^{M(p+1)}\ell_{n}+\sum_{n=1}^{M(p+1)}\Big{(}\ell_{n}-\sum_{k=1}^{M_{n}(M(p+1)+p+1)}x_{nk}\Big{)}$
$\displaystyle\leq\frac{1}{2^{p}}$

Observe that by our choice of $\varphi$ for any $N\in\mathbb{N}$ and $m,n\leq
N$ we have that $\varphi^{-1}(m,n)\leq\varphi^{-1}(N,N)$. If we define
$M_{\varphi}:\mathbb{N}\rightarrow\mathbb{N}$ by
$M_{\varphi}(N):=\varphi^{-1}(N,N)$, then $M_{\varphi}$ is strictly
increasing. We can now define $M^{\prime}:\mathbb{N}\rightarrow\mathbb{N}$ by

$\displaystyle
M^{\prime}(p):=M_{\varphi}\Big{(}M(p+1)\vee\big{(}\bigvee_{n=1}^{M(p+1)}M_{n}(M(p+1)+p+1)\big{)}\Big{)}$

and for $p\in\mathbb{N}$ and $N\geq M^{\prime}(p)$ we have that

$\displaystyle\sum_{m=1}^{N}y_{m}=\sum_{n=1}^{M(p+1)}\;\;\sum_{k=1}^{M_{n}(M(p+1)+p+1)}x_{nk}+c(N,p)$

where $c(N,p)\geq 0$ is the finite sum of the $x_{nk}$ s.t. $n>M(p+1)$ or
$k>M_{n}(M(p+1)+p+1)$ but $\varphi^{-1}(n,k)\leq N$. It follows that

$\displaystyle 0\leq\ell-\sum_{m=1}^{N}y_{m}\leq\frac{1}{2^{p}}$

Now for the general case. Assume that
$\big{(}\sum_{k=1}^{N}x_{nk}\big{)}_{N\in\mathbb{N}}$ converges to
$\ell_{n}:=\sum_{k}x_{nk}$ with modulus $M_{n}$ and that
$\big{(}\sum_{n=1}^{N}\sum_{k}x_{nk}\big{)}_{N\in\mathbb{N}}$ converges to
$\ell:=\sum_{n}\sum_{k}x_{nk}$ with modulus $M$. Furthermore, assume that
$\big{(}\sum_{k=1}^{N}\lvert x_{nk}\rvert\big{)}_{N\in\mathbb{N}}$ converges
to $\tilde{\ell}_{n}:=\sum_{k}\lvert x_{nk}\rvert$ with modulus
$\tilde{M}_{n}$ and that $\big{(}\sum_{n=1}^{N}\sum_{k}\lvert
x_{nk}\rvert\big{)}_{N\in\mathbb{N}}$ converges to
$\tilde{\ell}:=\sum_{n}\sum_{k}\lvert x_{nk}\rvert$ with modulus $\tilde{M}$.
We have already shown that $\sum_{m}\lvert y_{m}\rvert=\tilde{\ell}$ and may
assume that this series converges with some modulus $\tilde{M}^{\prime}$.
Without loss of generality we can also assume that $M\geq\tilde{M}^{\prime}$
because otherwise we can replace $M$ by $M\vee\tilde{M}^{\prime}$. Again, we
get for $p\in\mathbb{N}$ that

$\displaystyle\left\lvert\ell-\sum_{n=1}^{M(p+1)}\;\;\sum_{k=1}^{M_{n}(M(p+1)+p+1)}x_{nk}\right\rvert\leq\frac{1}{2^{p}}$

Thus, if we define $M^{\prime}:\mathbb{N}\rightarrow\mathbb{N}$ by

$\displaystyle
M^{\prime}(p):=M_{\varphi}\Big{(}M(p+2)\vee\big{(}\bigvee_{n=1}^{M(p+2)}M_{n}(M(p+2)+p+2)\big{)}\Big{)}$

and take $N\geq M^{\prime}(p)$ we get

$\displaystyle\left\lvert\ell-\sum_{m=1}^{N}y_{m}\right\rvert\leq\frac{1}{2^{(p+1)}}+\lvert
c(N,p)\rvert$

and

$\displaystyle\lvert c(N,p)\rvert\leq\sum_{\begin{subarray}{c}(n,k)\text{ s.t.
}\varphi^{-1}(n,k)\leq N,\\\ n>M(p+2)\text{ or
}k>M_{n}(M(p+2)+p+2)\end{subarray}}\lvert
x_{nk}\rvert\leq\sum_{m=M(p+2)}^{\infty}\lvert
y_{m}\rvert\leq\sum_{m=\tilde{M}^{\prime}(p+2)}^{\infty}\lvert
y_{m}\rvert\leq\frac{1}{2^{(p+1)}}$

which finishes the first part of the proof. For the converse direction assume
that $\tilde{\ell}:=\sum_{m}\lvert y_{m}\rvert$ exists and that this series
converges with modulus $\tilde{M}$ and let $\ell:=\sum_{m}y_{m}$ and assume
that this series converges with modulus $M$.

We first have to show that for any $n\in\mathbb{N}$,
$\tilde{\ell}_{n}:=\sum_{k}\lvert x_{nk}\rvert$ exists, so fix
$n\in\mathbb{N}$ and let $N_{0}\leq N_{1}$, then

$\displaystyle\sum_{k=N_{0}}^{N_{1}}\lvert
x_{nk}\rvert=\sum_{m=N_{0}}^{N_{1}}\lvert
y_{\varphi^{-1}(n,m)}\rvert\leq\sum_{m=N_{0}}^{\infty}\lvert y_{m}\rvert$

since $\varphi^{-1}(n,m)\geq m$ for all $m\in\mathbb{N}$. It follows that
$\big{(}\sum_{k=1}^{N}\lvert x_{nk}\rvert\big{)}_{N\in\mathbb{N}}$ is a
Cauchy-sequence and hence we may assume that $\tilde{\ell}_{n}:=\sum_{k}\lvert
x_{nk}\rvert$ exists and the series converges with modulus $\tilde{M}$ and
that $\ell_{n}:=\sum_{k}{x_{nk}}$ exists and the series converges with modulus
$M$. We next have to show that $\sum_{n}\tilde{\ell}_{n}$ exists, so let
$N_{0}\leq N_{1}$, then again

$\displaystyle\sum_{n=N_{0}}^{N_{1}}\tilde{\ell}_{n}\leq\sum_{m=N_{0}}^{\infty}\lvert
y_{m}\rvert$

which shows that
$\big{(}\sum_{n=1}^{N}\tilde{\ell}_{n}\big{)}_{N\in\mathbb{N}}$ is a Cauchy-
sequence and it remains to check that $\sum_{n}\ell_{n}=\ell$. So fix
$N\in\mathbb{N}$, let $p\in\mathbb{N}$ and define $N_{n,p}:=M_{n}(N+p)$ for
$1\leq n\leq N$. Note that $N_{n,p}\geq N$ for all $1\leq n\leq N$ and

$\displaystyle\left\lvert\ell-\sum_{n=1}^{N}\ell_{n}\right\rvert\leq\underbrace{\sum_{n=1}^{N}\;\;\left\lvert\sum_{k=1}^{N_{n,p}}x_{nk}-\ell_{n}\right\rvert}_{\leq
2^{-p}}+\underbrace{\left\lvert\sum_{n=1}^{N}\sum_{k=1}^{N_{n,p}}x_{nk}-\ell\right\rvert}_{(*)}$

and in particular

$\displaystyle(*)\leq\underbrace{\sum_{n=1}^{N}\sum_{k=1}^{N_{n,p}}\lvert
x_{nk}-y_{\varphi^{-1}(n,k)}\rvert}_{=0}+\;\;\sum_{\begin{subarray}{c}(n,k)\text{
s.t. }n>N\\\ \text{or }k>N_{n,p}\geq N\end{subarray}}\lvert
y_{\varphi^{-1}(n,k)}\rvert\leq\sum_{m=N}^{\infty}\lvert y_{m}\rvert$

Since $p\in\mathbb{N}$ was chosen arbitrarily we get that
$\left\lvert\ell-\sum_{n=1}^{N}\ell_{n}\right\rvert\leq\sum_{m=N}^{\infty}\lvert
y_{m}\rvert$, which finishes the proof. ∎

##  Chapter 2 Set indexed families

We have seen that a lot of important notions of BST and BCMT give rise to
totalities that, although equipped with a canonical equality, are not sets or
can at least not be treated as such from a predicative point of view. However,
we are still able to speak about these totalities by invoking so-called _set-
indexed families_. We introduce the various kinds of set-indexed families in
this section.

###  1 Families of sets

As a first example of a totality that is not a set we considered the universe
$\mathbb{V}_{0}$. It is thus natural to introduce families of sets before
introducing families of subsets, complemented subsets and partial functions.
However, when applying set-indexed families to BCMT we won’t be concerned
families of sets. Therefore, the account given here (following [Pet21]) shall
be rather brief and is just included for the sake of completeness.

######  Definition 1.1.

Let $I$ be a set, an _$I$ -family of sets_ is a pair
$\Lambda:=(\lambda_{0},\lambda_{1})$, where
$\lambda_{0}:I\rightsquigarrow\mathbb{V}_{0}$ and
$\lambda_{1}:\bigcurlywedge_{i,j\in
D(I)}\mathbb{F}(\lambda_{0}(i),\lambda_{0}(j))$ is a dependent assignment
routine such that for every $(i,j)\in D(I)$ and
$\lambda_{1}(i,j):=\lambda_{ij}$ we have that
$\lambda_{ii}:=\text{id}_{\lambda_{0}(i)}$, and for every $i,j,k\in I$,
satisfying $i=_{I}j$ and $j=_{I}k$, the following diagram commutes

${\lambda_{0}(i)}$${\lambda_{0}(j)}$${\lambda_{0}(k)}$$\scriptstyle{\lambda_{ik}}$$\scriptstyle{\lambda_{ij}}$$\scriptstyle{\lambda_{jk}}$

We call $I$ the _index set_ of the family $\Lambda$, the function
$\lambda_{ij}$ the _transport_ function from $\lambda_{0}(i)$ to
$\lambda_{0}(j)$, and the dependent assignment routine $\lambda_{1}$ the
_modulus of function-likeness_ of $\lambda_{0}$. We say that $\Lambda$ is an
$I$-_set_ of sets if111Note that the left to right direction always holds,
since for any family of sets we have
$i=_{I}j\Rightarrow(\lambda_{ij},\lambda_{ji}):\lambda_{0}(i)=_{\mathbb{V}_{0}}\lambda_{0}(j)$.

$\displaystyle\forall i,j\in
I:\;i=_{I}j\;\Leftrightarrow\;\lambda_{0}(i)=_{\mathbb{V}_{0}}\lambda_{0}(j)$

######  Definition 1.2.

Let $I$ be a set and $\Lambda:=(\lambda_{0},\lambda_{1})$ and
$M:=(\mu_{0},\mu_{1})$ be $I$-families of sets. A _family map_ from $\Lambda$
to $M$ is a dependent assignement routine

$\displaystyle\Psi:\bigcurlywedge_{i\in
I}\mathbb{F}\big{(}\lambda_{0}(i),\mu_{0}(i)\big{)}$

such that for every $i=_{I}j$ the following diagram commutes

${\lambda_{0}(i)}$${\lambda_{0}(j)}$${\mu_{0}(i)}$${\mu_{0}(j)}$$\scriptstyle{\Psi_{i}}$$\scriptstyle{\lambda_{ij}}$$\scriptstyle{\Psi_{j}}$$\scriptstyle{\mu_{ij}}$

In this case we write $\Psi:\Lambda\Rightarrow M$. We denote by
$\mathtt{Map}_{I}(\Lambda,M)$ the totality of family maps from $\Lambda$ to
$M$, which is equipped with the equality

$\displaystyle\Psi=_{{\mathtt{Map}_{I}(\Lambda,M)}}\Xi\;:\Leftrightarrow\;\forall
i\in I:\;\Psi_{i}=_{{\mathbb{F}(\lambda_{0}(i),\mu_{0}(i))}}\Xi_{i}$

If $N:=(\nu_{0},\nu_{1})$ is an $I$-family as well, then for
$\Psi:\Lambda\Rightarrow M$ and $\Xi:M\Rightarrow N$ the composition
$\Psi\circ\Xi:\Lambda\Rightarrow N$ is defined as
$(\Psi\circ\Xi)_{i}:=\Psi_{i}\circ\Xi_{i}$. The identity family-map from
$\Lambda$ to $\Lambda$ is the dependent assignment routine
$\text{Id}_{\Lambda}:\bigcurlywedge_{i\in
I}\mathbb{F}(\lambda_{0}(i),\lambda_{0}(i))$ defined by
$\big{(}\text{Id}_{\Lambda}\big{)}_{i}:=\text{id}_{\lambda_{0}(i)}$.

Over a family of sets we can define the exterior union and the dependent
product, but since we won’t use these notions in our discussion of BCMT, we
just state the definitions.

######  Definition 1.3.

Let $\Lambda:=(\lambda_{0},\lambda_{1})$ be an $I$-family of sets. The
_exterior union_ , or _disjoint union_ $\sum_{i\in I}\lambda_{0}(i)$ of
$\Lambda$ is defined by

$\displaystyle w\in\sum_{i\in I}\lambda_{0}(i)\;$
$\displaystyle:\Leftrightarrow\;\exists i\in I\;\exists
x\in\lambda_{0}(i)\text{ s.t. }w:=(i,x)$ $\displaystyle(i,x)=_{\sum_{i\in
I}\lambda_{0}(i)}(j,y)\;$
$\displaystyle:\Leftrightarrow\;i=_{I}j\;\text{and}\;\lambda_{ij}(x)=_{\lambda_{0}(j)}y$

######  Definition 1.4.

Let $\Lambda:=(\lambda_{0},\lambda_{1})$ be an $I$-family of sets. The
_dependent product_ $\prod_{i\in I}\lambda_{0}(i)$ is defined by

$\displaystyle\Phi\in\prod_{i\in I}\lambda_{0}(i)\;$
$\displaystyle:\Leftrightarrow\;\Phi:\bigcurlywedge_{i\in
I}\lambda_{0}(i)\text{ s.t. }\forall(i,j)\in
D(I):\;\lambda_{ij}(\Phi_{i})=_{\lambda_{0}(j)}\Phi_{j}$
$\displaystyle\Phi=_{\prod_{i\in I}\lambda_{0}(i)}\Psi\;$
$\displaystyle:\Leftrightarrow\;\forall i\in
I:\;\Phi_{i}=_{\lambda_{0}(i)}\Psi_{i}$

###  2 Families of subsets

We next introduce families of subsets that we will use a lot in our discussion
of BCMT.

######  Definition 2.1.

Let $X$ and $I$ be sets. A _family of subsets_ indexed by $I$ is a triple
$\lambda:=(\lambda_{0},\mathcal{E},\lambda_{1})$, where
$\lambda_{0}:I\rightsquigarrow\mathbb{V}_{0}$, and
$\mathcal{E}:\bigcurlywedge_{i\in I}\mathbb{F}(\lambda_{0}(i),X)$, such that,
for every $i\in I$, we have that $\mathcal{E}(i):=\varepsilon_{i}$ is an
embedding of $\lambda_{0}(i)$ into $X$ (i.e.
$(\lambda_{0}(i),\varepsilon_{i})$ is a subset of $X$). Moreover,
$\lambda_{1}:\bigcurlywedge_{(i,j)\in
D(I)}\mathbb{F}(\lambda_{0}(i),\lambda_{0}(j))$ is called the _modulus of
function-likeness_ of $\lambda_{0}$, and for every $i\in I$ it satisfies
$\lambda_{ii}:=\text{id}_{\lambda_{0}(i)}$, while for every $(i,j)\in D(I)$ it
satisfies
$(\lambda_{ij},\lambda_{ji}):\lambda_{0}(i)=_{\mathcal{P}(X)}\lambda_{0}(j)$,
i.e. the following inner diagrams commute

${\lambda_{0}(i)}$${\lambda_{0}(j)}$${X}$$\scriptstyle{\lambda_{ij}}$$\scriptstyle{\varepsilon_{i}}$$\scriptstyle{\lambda_{ji}}$$\scriptstyle{\varepsilon_{j}}$

We say that $\Lambda$ is an $I$-_set_ of subsets if

$\displaystyle\forall i,j\in
I:\;i=_{I}j\;\Leftrightarrow\;\lambda_{0}(i)=_{{\mathcal{P}(X)}}\lambda_{0}(j)$

Let $\lambda:=(\lambda_{0},\mathcal{E},\lambda_{1})$ and
$\mu:=(\mu_{0},E,\mu_{1})$ be $I$-families of subsets of $X$. A _family of
subsets-map_ is a dependent assignment routine $\Psi:\bigcurlywedge_{i\in
I}\mathbb{F}\big{(}\lambda_{0}(i),\mu_{0}(i)\big{)}$ such that for every $i\in
I$ the following diagram commutes

${\lambda_{0}(i)}$${\mu_{0}(i)}$${X}$$\scriptstyle{\Psi_{i}}$$\scriptstyle{\varepsilon_{i}}$$\scriptstyle{e_{i}}$

i.e. $\Psi_{i}:\lambda_{0}(i)\subseteq\mu_{0}(i)$ for all $i\in I$. In this
case we write $\Psi:\lambda\Rightarrow_{X}\mu$. We denote by
$\mathtt{Map}_{I}^{X}(\lambda,\mu)$ the totality of family maps from $\lambda$
to $\mu$, which is equipped with the equality

$\displaystyle\Psi=_{{\mathtt{Map}_{I}^{X}(\lambda,\mu)}}\Xi\;:\Leftrightarrow\;\forall
i\in I:\;\Psi_{i}=_{{\mathbb{F}(\lambda_{0}(i),\mu_{0}(i))}}\Xi_{i}$

If $\nu:=(\nu_{0},E^{\prime},\nu_{1})$ is an $I$-family of subsets of $X$ as
well, then for $\Psi:\lambda\Rightarrow_{X}\mu$ and
$\Xi:\mu\Rightarrow_{X}\nu$ the composition
$\Psi\circ\Xi:\lambda\Rightarrow_{X}\nu$ is defined as
$(\Psi\circ\Xi)_{i}:=\Psi_{i}\circ\Theta_{i}$. The identity family of subsets-
map from $\lambda$ to $\lambda$ is the dependent assignment routine
$\text{Id}_{\lambda}:\bigcurlywedge_{i\in
I}\mathbb{F}(\lambda_{0}(i),\lambda_{0}(i))$ defined by
$\big{(}\text{Id}_{\lambda}\big{)}_{i}:=\text{id}_{\lambda_{0}(i)}$.

######  Remark 2.2.

It is easy to check that for any $I$-family of subsets of $X$,
$\lambda:=(\lambda_{0},\mathcal{E},\lambda_{1})$, we get a family of sets
$\Lambda_{\lambda}:=(\lambda_{0},\lambda_{1})$. From the definition we get
that for $i=_{I}j$ and $j=_{I}k$ the following diagrams commute

${\lambda_{0}(j)}$${\lambda_{0}(k)}$${\lambda_{0}(i)}$${X}$$\scriptstyle{\lambda_{jk}}$$\scriptstyle{\varepsilon_{j}}$$\scriptstyle{\varepsilon_{k}}$$\scriptstyle{\lambda_{ij}}$$\scriptstyle{\varepsilon_{i}}$
${\lambda_{0}(j)}$${\lambda_{0}(k)}$${\lambda_{0}(i)}$${X}$$\scriptstyle{\lambda_{ji}}$$\scriptstyle{\varepsilon_{j}}$$\scriptstyle{\varepsilon_{k}}$$\scriptstyle{\lambda_{kj}}$$\scriptstyle{\varepsilon_{i}}$

It follows that
$(\lambda_{ij}\circ\lambda_{jk},\lambda_{kj}\circ\lambda_{ji}):\lambda_{0}(i)=_{{\mathcal{P}(X)}}\lambda_{0}(k)$.
But since we have $i=_{I}k$ we get that
$(\lambda_{ik}\lambda_{ki}):\lambda_{0}(i)=_{{\mathcal{P}(X)}}\lambda_{0}(k)$
holds as well and we get from lemma (1.2) that in particular
$\lambda_{ij}\circ\lambda_{jk}=_{{\mathbb{F}(\lambda_{0}(i),\lambda_{0}(k))}}\lambda_{ik}$,
i.e. the following diagram commutes

${\lambda_{0}(i)}$${\lambda_{0}(j)}$${\lambda_{0}(k)}$$\scriptstyle{\lambda_{ik}}$$\scriptstyle{\lambda_{ij}}$$\scriptstyle{\lambda_{jk}}$

Furthermore, a family of subsets-map $\Psi:\lambda\Rightarrow_{X}\mu$ is also
a family map $\Psi:\Lambda_{\lambda}\Rightarrow M_{\mu}$, since for $i=_{I}j$
the following inner diagrams commute

${\lambda_{0}(i)}$${\lambda_{0}(j)}$${X}$${\mu_{0}(i)}$${\mu_{0}(j)}$$\scriptstyle{\lambda_{ij}}$$\scriptstyle{\Psi_{i}}$$\scriptstyle{\varepsilon_{i}}$$\scriptstyle{\Psi_{j}}$$\scriptstyle{\varepsilon_{j}}$$\scriptstyle{\mu_{ij}}$$\scriptstyle{e_{i}}$$\scriptstyle{e_{j}}$

For $x\in\lambda_{0}(i)$ we thus get

$\displaystyle\big{(}e_{j}\circ\mu_{ij}\circ\Psi_{i}\big{)}(x)$
$\displaystyle=_{X}\big{(}e_{i}\circ\Psi_{i}\big{)}(x)$
$\displaystyle=_{X}\varepsilon_{i}(x)$
$\displaystyle=_{X}\big{(}\varepsilon_{j}\circ\lambda_{ij}\big{)}(x)$
$\displaystyle=_{X}\big{(}e_{j}\circ\Psi_{j}\circ\lambda_{ij}\big{)}(x)$

and since $e_{j}$ is an embedding we get that
$\big{(}\mu_{ij}\circ\Psi_{i}\big{)}(x)=_{\mu_{0}(j)}\big{(}\Psi_{j}\circ\lambda_{ij}\big{)}(x)$.

Next, we want to introduce the notion of a subfamily that will play an
important role in redefining the notions of measure and integration space in
BCMT.

######  Definition 2.3.

Let $\lambda:=(\lambda_{0},\mathcal{E},\lambda_{1})$ be an $I$-family of
subsets of $X$ and $J$ be a set with a function $h:J\rightarrow I$. Then by
$(\lambda\circ h):=(\lambda_{0}\circ h,\mathcal{E}\circ h,\lambda_{1}\circ h)$
we denote the $J$ family of subsets that is given by composing all (dependent)
assignment routines with $h$. Now let $\mu:=(\mu_{0},E,\mu_{1})$ be a
$J$-family of subsets of $X$, we say that $\mu$ is a _subfamily_ of $\lambda$
via $h$ if there are family of subset-maps
$\Psi:\mu\Rightarrow_{X}(\lambda\circ h)$ and $\Psi^{-1}:(\lambda\circ
h)\Rightarrow_{X}\mu$ such that
$\Psi\circ\Psi^{-1}=_{{\mathtt{Map}_{J}^{X}(\mu,\mu)}}\text{Id}_{\mu}$ and
$\Psi^{-1}\circ\Psi=_{{\mathtt{Map}_{J}^{X}((\lambda\circ h),(\lambda\circ
h))}}\text{Id}_{(\lambda\circ h)}$, i.e. for each $j\in J$ the following
diagrams commute

${\mu_{0}(j)}$${\lambda_{0}\big{(}h(j)\big{)}}$${\mu_{0}(j)}$${X}$$\scriptstyle{e_{j}}$$\scriptstyle{\Psi_{j}}$$\scriptstyle{\text{id}_{\mu_{0}(j)}}$$\scriptstyle{\Psi_{j}^{-1}}$$\scriptstyle{\varepsilon_{h(j)}}$$\scriptstyle{e_{j}}$
${\lambda_{0}\big{(}h(j)\big{)}}$${\mu_{0}(j)}$${\lambda_{0}\big{(}h(j)\big{)}}$${X}$$\scriptstyle{\varepsilon_{h(j)}}$$\scriptstyle{\Psi_{j}^{-1}}$$\scriptstyle{\text{id}_{\lambda_{0}(h(j))}}$$\scriptstyle{e_{j}}$$\scriptstyle{\Psi_{j}}$$\scriptstyle{\varepsilon_{h(j)}}$

######  Remark 2.4.

If in the above setting $\mu$ is a $J$-set of subsets, then $h:J\rightarrow I$
is an embedding. To see this, assume that we have $j,j^{\prime}\in J$ s.t.
$h(j)=_{I}h(j^{\prime})$. Then the following inner diagrams commute

${\lambda_{0}\big{(}h(j)\big{)}}$${\lambda_{0}\big{(}h(j^{\prime})\big{)}}$${\mu_{0}(j)}$${X}$${\mu_{0}(j^{\prime})}$${\lambda_{0}\big{(}h(j)\big{)}}$${\lambda_{0}\big{(}h(j^{\prime})\big{)}}$$\scriptstyle{\lambda_{h(j)h(j^{\prime})}}$$\scriptstyle{\varepsilon_{h(j)}}$$\scriptstyle{\Psi_{j^{\prime}}^{-1}}$$\scriptstyle{\varepsilon_{h(j^{\prime})}}$$\scriptstyle{\Psi_{j}}$$\scriptstyle{e_{j}}$$\scriptstyle{e_{j^{\prime}}}$$\scriptstyle{\Psi_{j^{\prime}}}$$\scriptstyle{\varepsilon_{h(j)}}$$\scriptstyle{\Psi_{j}^{-1}}$$\scriptstyle{\varepsilon_{h(j^{\prime})}}$$\scriptstyle{\lambda_{h(j^{\prime})h(j)}}$

It follows that $\mu_{0}(j)=_{{\mathcal{P}(X)}}\mu_{0}(j^{\prime})$ and thus
$j=_{J}j^{\prime}$ since $\mu$ is a $J$-set of subsets.

Finally we can introduce the appropriate notions union and intersection of a
family of subsets, corresponding to the exterior union and dependent product
for families of sets.

######  Definition 2.5.

Let $\lambda:=(\lambda_{0},\mathcal{E},\lambda_{1})$ be an $I$-family of
subsets of $X$. The _interior union_ of $\lambda$ is the totality
$\bigcup_{i\in I}\lambda_{0}(i)$ defined by

$\displaystyle z\in\bigcup_{i\in I}\lambda_{0}(i)\;:\Leftrightarrow\;\exists
i\in I\;\exists x\in\lambda_{0}(i)\text{ s.t. }z:=(i,x)$

Let the assignment routine $\varepsilon:\bigcup_{i\in
I}\lambda_{0}(i)\rightsquigarrow X$ be defined by
$\varepsilon(i,x):=\varepsilon_{i}(x)$. The equality on $\bigcup_{i\in
I}\lambda_{0}(i)$ is defined by

$\displaystyle(i,x)=_{\bigcup_{i\in
I}\lambda_{0}(i)}(j,y)\;:\Leftrightarrow\;\varepsilon(i,x)=_{X}\varepsilon(j,y)$

Then $\varepsilon$ is an embedding, turning $\bigcup_{i\in I}\lambda_{0}(i)$
into a subset of $X$. The _intersection_ of $\lambda$ is the totality
$\bigcap_{i\in I}\lambda_{0}(i)$ defined by

$\displaystyle\Psi\in\bigcap_{i\in I}\lambda_{0}(i)\;$
$\displaystyle:\Leftrightarrow\;\Psi:\bigcurlywedge_{i\in
I}\lambda_{0}(i)\text{ s.t. }\forall i,j\in
I:\;\varepsilon_{i}(\Psi_{i})=_{X}\varepsilon_{j}(\Psi_{j})$
$\displaystyle\Phi=_{\bigcap_{i\in I}\lambda_{0}(i)}\Psi\;$
$\displaystyle:\Leftrightarrow\;\forall i\in
I:\;\Phi_{i}=_{\lambda_{0}(i)}\Psi_{i}$

For $i_{0}\in I$ the assignment routine

$\displaystyle\epsilon:\bigcap_{i\in I}\lambda_{0}(i)$
$\displaystyle\hookrightarrow X$ $\displaystyle\Psi$
$\displaystyle\mapsto\varepsilon_{i_{0}}(\Psi_{i_{0}})$

is an embedding (and as a function in $\mathbb{F}\big{(}\bigcap_{i\in
I}\lambda_{0}(i),X\big{)}$ independent of $i_{0}$, turning $\bigcap_{i\in
I}\lambda_{0}(i)$ into a subset of $X$.

######  Example 2.6.

Let $(A,i_{A})$ and $(B,i_{B})$ be subsets of $X$ let
$\lambda:=(\lambda_{0},\mathcal{E},\lambda_{1})$ be the $\bm{2}$-family of
subsets given by

  * •

$\lambda_{0}(0):=A$ and $\lambda_{0}(1):=B$

  * •

$\varepsilon_{0}:=i_{A}$ and $\varepsilon_{1}:=i_{B}$

  * •

$\lambda_{00}:=\text{id}_{A}$ and $\lambda_{11}:=\text{id}_{B}$

then it is easy to verify

$\displaystyle\bigcap_{i\in\bm{2}}\lambda_{0}(i)=_{{\mathcal{P}(X)}}A\cap
B\quad\text{ and
}\quad\bigcup_{i\in\bm{2}}\lambda_{0}(i)=_{{\mathcal{P}(X)}}A\cup B$

######  Remark 2.7.

Talking about intersections and unions of subsets includes a lot of data which
we will ignore in large parts later in our discussion of BCMT. In particular
we will not write elements of unions as pairs but rather identify them with
their image in $X$. Similarly, we won’t write elements of intersections as
dependent assignment routines but treat them like elements of $X$.

###  3 Families of complemented subsets

We now turn to set-indexed families of complemented subsets. Just as a
complemented subset consists of two subsets that are apart, a family of
complemented subsets consists of two families of subsets that are apart at
every index. We follow [Pet19b] in this section.

######  Definition 3.1.

Let $X$ be a set with a fixed inequality $\neq_{X}$ and $I$ be a set. An
$I$-_family of complemented subsets_ of $X$ is a sextuple
$\bm{\lambda}:=(\lambda_{0}^{1},\mathcal{E}^{1},\lambda_{1}^{1},\lambda_{0}^{0},\mathcal{E}^{0},\lambda_{1}^{0})$
where $\lambda^{1}:=(\lambda_{0}^{1},\mathcal{E}^{1},\lambda_{1}^{1})$ and
$\lambda^{0}:=(\lambda_{0}^{0},\mathcal{E}^{0},\lambda_{1}^{0})$ are both
$I$-families of subsets of $X$ such that

$\displaystyle\forall i\in I:\;\lambda_{0}^{1}(i)\;][\;\lambda_{0}^{0}(i)$

We denote by
$\bm{\lambda}_{0}(i):=\big{(}\lambda_{0}^{1}(i),\lambda_{0}^{0}(i)\big{)}$ the
complemented subset associated to $i\in I$. We say that $\bm{\lambda}$ is an
$I$-_set_ of complemented subsets if

$\displaystyle\forall i,j\in
I:\;i=_{I}j\;\Leftrightarrow\;\bm{\lambda}_{0}(i)=_{{\mathcal{P}^{{{][}}}(X)}}\bm{\lambda}_{0}(j)$

If $\bm{\nu}:=(\nu_{0}^{1},E^{1},\nu_{1}^{1},\nu_{0}^{0},E^{0},\nu_{1}^{0})$
is an $I$-family of complemented subsets as well, then a family of
complemented subsets-map from $\bm{\lambda}$ to $\bm{\nu}$ is a pair
$\bm{\Psi}:=(\Psi^{1},\Psi^{0})$ such that
$\Psi^{1}:\lambda^{1}\Rightarrow_{X}\nu^{1}$ and
$\Psi^{0}:\lambda^{0}\Rightarrow_{X}\nu^{0}$. We denote by
$\mathtt{Map}_{I}^{X,\;][}(\bm{\lambda},\bm{\nu})$ the totality of family of
complemented subsets-maps from $\bm{\lambda}$ to $\bm{\nu}$, equipped with the
equality of componentwise equality of family of subsets-maps. Concatenation of
family of complemented subsets-maps and the identity map are also defined
componentwise in the canonical way.

To talk about measure-spaces in BCMT predicatively we also need the notion of
a subfamily of complemented subsets.

######  Definition 3.2.

Let
$\bm{\lambda}:=(\lambda_{0}^{1},\mathcal{E}^{1},\lambda_{1}^{1},\lambda_{0}^{0},\mathcal{E}^{0},\lambda_{1}^{0})$
be an $I$-family of complemented subsets of $X$ and $J$ be a set with a
function $h:J\rightarrow I$. Then by $(\bm{\lambda}\circ h)$ we denote the
$J$-family of complemented subsets that is given by composing all (dependent)
assignment routines with $h$. Now let
$\bm{\nu}:=(\nu_{0}^{1},E^{1},\nu_{1}^{1},\nu_{0}^{0},E^{0},\nu_{1}^{0})$ be a
$J$-family of complemented subsets of $X$, we say that $\bm{\nu}$ is a
subfamily of $\bm{\lambda}$ via $h$ if there are family of complemented
subset-maps $\bm{\Psi}$ from $\bm{\nu}$ to $(\bm{\lambda}\circ h)$ and
$\bm{\Psi}^{-1}$ from $(\bm{\lambda}\circ h)$ to $\bm{\nu}$ such that
$\bm{\Psi}\circ\bm{\Psi}^{-1}=_{{\mathtt{Map}_{J}^{X,\;][}(\bm{\nu},\bm{\nu})}}\text{Id}_{\bm{\nu}}$
and
$\bm{\Psi}^{-1}\circ\bm{\Psi}=_{{\mathtt{Map}_{J}^{X,\;][}((\bm{\lambda}\circ
h),(\bm{\lambda}\circ h))}}\text{Id}_{(\bm{\lambda}\circ h)}$

By remark (2.4) it follows directly from the previous definitions that if in
the above setting $\bm{\nu}$ is $J$-set of complemented subsets, we have an
embedding $h:J\hookrightarrow I$.

At the end of this section we want to give an example of a canonical family of
complemented subsets that can be constructed for any inhabited set, the family
of detachable subsets of a set. Classically, the detachable subsets are in a
one-to-one correspondence with the subsets of $X$.

######  Definition 3.3.

Let $X$ be an inhabited set and let $\bm{2}:=\\{0,1\\}$. Let $\neq_{X}$ be the
following inequality on $X$:

$\displaystyle x\neq_{X}y\;:\Leftrightarrow\;\exists
f\in\mathbb{F}(X,\bm{2})\text{ s.t. }f(x)\neq f(y)$

Let
$\bm{\delta}=(\delta_{0}^{1},\mathcal{E}^{1},\delta_{1}^{1},\delta_{0}^{0},\mathcal{E}^{0},\delta_{1}^{0})$
be the $\mathbb{F}(X,\bm{2})$-family of complemented subset of $(X,\neq_{X})$
with $\mathbb{F}(X,\bm{2})$-families of subsets
$\delta^{1}=(\delta_{0}^{1},\mathcal{E}^{1},\delta_{1}^{1})$ and
$\delta^{0}=(\delta_{0}^{0},\mathcal{E}^{0},\delta_{1}^{0})$ given by the
following data:

  * •

For $f\in\mathbb{F}(X,\bm{2})$ we have that $\delta_{0}^{1}(f):=\\{x\in
X:\;f(x)=_{\bm{2}}1\\}$
and $\delta_{0}^{0}(f):=\\{x\in X:\;f(x)=_{\bm{2}}0\\}$

  * •

The embeddings $\varepsilon_{f}^{1}:\delta_{0}^{1}(f)\hookrightarrow X$ and
$\varepsilon_{f}^{0}:\delta_{0}^{0}(f)\hookrightarrow X$ are all defined by
$x\mapsto x$ for any $f\in\mathbb{F}(X,\bm{2})$.

  * •

The transport maps
$\delta_{fg}^{1}:\delta_{0}^{1}(f)\rightarrow\delta_{0}^{1}(g)$ and
$\delta_{fg}^{0}:\delta_{0}^{0}(f)\rightarrow\delta_{0}^{0}(g)$ are all
defined by $x\mapsto x$ for any $f=_{{\mathbb{F}(X,\bm{2})}}g$.

For $f\in\mathbb{F}(X,\bm{2})$ we define
$\bm{\delta}_{0}(f):=\big{(}\delta_{0}^{1}(f),\delta_{0}^{0}(f)\big{)}$ to be
the associated _detachable complemented subset_.

######  Remark 3.4.

It is not hard to check that $\neq_{X}$ actually defines an appartness
relation on $X$ and that $\bm{\delta}$ actually defines a
$\mathbb{F}(X,\bm{2})$-family of complemented subsets w.r.t. this inequality.
Moreover, we have that
$\delta_{0}^{1}(f)\cup\delta_{0}^{0}(f)=_{{\mathcal{P}(X)}}X$ and
$\chi_{\bm{\delta}_{0}(f)}=_{{\mathbb{F}(X,\bm{2})}}f$ for any
$f\in\mathbb{F}(X,\bm{2})$. Using this, one can immediately see that

$\displaystyle\forall
f,g\in\mathbb{F}(X,\bm{2}):\;\;f=_{{\mathbb{F}(X,\bm{2})}}g\;\Leftrightarrow\;\bm{\delta}_{0}(f)=_{{\mathcal{P}^{{{][}}}(X)}}\bm{\delta}_{0}(g)$

i.e. that $\bm{\delta}$ is actually a set of complemented subsets.

###  4 Families of partial functions

Finally, we introduce families of partial functions. Since a partial function
consists of a subset (its domain) and a function on that subset, a family of
partial functions consists of a family of subsets (the family of domains) and
a dependent assignment routine, assigning to each index a function on the
respective domain.

######  Definition 4.1.

Let $X,Y$ and $I$ be sets. An $I$-_family of partial functions_ from $X$ to
$Y$ is a quadruple $\bm{\Lambda}:=(\lambda_{0},\mathcal{E},\lambda_{1},F)$,
where

  * •

$\lambda_{0}:I\rightsquigarrow\mathbb{V}_{0}$

  * •

$\mathcal{E}:\bigcurlywedge_{i\in I}\mathbb{F}(\lambda_{0}(i),X)$, such that,
for every $i\in I$, we have that $\mathcal{E}(i):=\varepsilon_{i}$ is an
embedding of $\lambda_{0}(i)$ into $X$

  * •

$\lambda_{1}:\bigcurlywedge_{i,j\in
D(I)}\mathbb{F}(\lambda_{0}(i),\lambda_{0}(j))$ is called the _modulus of
function-likeness_ of $\lambda_{0}$, and for every $i\in I$ it satisfies
$\lambda_{ii}:=\text{id}_{\lambda_{0}(i)}$, while for every $(i,j)\in D(I)$ it
satisfies
$(\lambda_{ij},\lambda_{ji}):\lambda_{0}(i)=_{\mathcal{P}(X)}\lambda_{0}(j)$

  * •

$F:\bigcurlywedge_{i\in I}\mathbb{F}(\lambda_{0}(i),Y)$ such that, for every
$i\in I$, we have that $F(i):=f_{i}$ and for $(i,j)\in D(I)$ and
$x\in\lambda_{0}(i)$ we have that
$f_{i}(x)=_{Y}\big{(}f_{j}\circ\lambda_{ij}\big{)}(x)$.

i.e. for $(i,j)\in D(I)$ the following diagrams commute

${\lambda_{0}(i)}$${\lambda_{0}(j)}$${X}$${Y}$$\scriptstyle{\lambda_{ij}}$$\scriptstyle{\varepsilon_{i}}$$\scriptstyle{f_{i}}$$\scriptstyle{\lambda_{ji}}$$\scriptstyle{\varepsilon_{j}}$$\scriptstyle{f_{j}}$

We say that $\bm{\Lambda}$ is an $I$-_set_ of partial functions if

$\displaystyle\forall i,j\in
I:\;i=_{I}j\;\Leftrightarrow\;f_{i}=_{{\mathbb{F}^{\rightharpoonup}(X,Y)}}f_{j}$

If $\bm{M}:=(\mu_{0},E,\mu_{1},G)$ is an $I$-family of partial functions from
$X$ to $Y$ as well, a family of partial functions-map from $\bm{\Lambda}$ to
$\bm{M}$ is a dependent assignment routine $\Psi:\bigcurlywedge_{i\in
I}\mathbb{F}(\lambda_{0}(i),\mu_{0}(i))$ s.t. for every $i\in I$ the following
diagrams commute

${\lambda_{0}(i)}$${\mu_{0}(i)}$${X}$${Y}$$\scriptstyle{\Psi_{i}}$$\scriptstyle{\varepsilon_{i}}$$\scriptstyle{f_{i}}$$\scriptstyle{e_{i}}$$\scriptstyle{g_{i}}$

We denote by $\mathtt{Map}_{I}^{X\rightharpoonup Y}(\bm{\Lambda},\bm{M})$ the
totality of family of partial functions-maps from $\bm{\Lambda}$ to $\bm{M}$,
which is equipped with the equality

$\displaystyle\Psi=_{{\mathtt{Map}_{I}^{X\rightharpoonup
Y}(\bm{\Lambda},\bm{M})}}\Xi\;:\Leftrightarrow\;\forall i\in
I:\;\Psi_{i}=_{{\mathbb{F}(\lambda_{0}(i),\mu_{0}(i))}}\Xi_{i}$

Composition of family of partial functions-maps and the identity map are
defined just like for family of subsets-maps.

######  Remark 4.2.

Note that any $I$-family of partial functions
$\bm{\Lambda}:=(\lambda_{0},\mathcal{E},\lambda_{1},F)$ we get an induced
$I$-family of subsets $(\lambda_{0},\mathcal{E},\lambda_{1})$, which we may
call the family of domains. It follows directly from the definitions that a
family of partial functions-map is also a family of subsets-map between the
respective families of domains.

######  Definition 4.3.

Let $\bm{\Lambda}:=(\lambda_{0},\mathcal{E},\lambda_{1},F)$ be an $I$-family
of partial functions from $X$ to $I$ and $J$ be a set with a function
$h:J\rightarrow I$. Then by $(\bm{\Lambda}\circ h)$ we denote the $J$ family
of partial functions that is given by composing all (dependent) assignment
routines with $h$. Now let $\bm{M}:=(\mu_{0},E,\mu_{1};G)$ be a $J$-family of
partial functions, we say that $\mu$ is a subfamily of $\lambda$ via $h$ if
there are family of partial functions-maps $\Psi$ from $\bm{M}$ to
$(\bm{\Lambda}\circ h)$ and $\Psi^{-1}$ from $(\bm{\Lambda}\circ h)$ to
$\bm{M}$, such that $\Psi\circ\Psi^{-1}=_{{\mathtt{Map}_{I}^{X\rightharpoonup
Y}(\bm{M},\bm{M})}}\text{Id}_{\bm{M}}$ and
$\Psi^{-1}\circ\Psi=_{{\mathtt{Map}_{I}^{X\rightharpoonup
Y}((\bm{\Lambda}\circ h),(\bm{\Lambda}\circ h))}}\text{Id}_{(\bm{\Lambda}\circ
h)}$, i.e. for each $j\in J$ the following diagrams commute.

${Y}$${\mu_{0}(j)}$${\lambda_{0}\big{(}h(j)\big{)}}$${\mu_{0}(j)}$${X}$$\scriptstyle{e_{j}}$$\scriptstyle{\Psi_{j}}$$\scriptstyle{g_{j}}$$\scriptstyle{\Psi_{j}^{-1}}$$\scriptstyle{\varepsilon_{h(j)}}$$\scriptstyle{f_{h(j)}}$$\scriptstyle{e_{j}}$$\scriptstyle{g_{j}}$
${X}$${\lambda_{0}\big{(}h(j)\big{)}}$${\mu_{0}(j)}$${\lambda_{0}\big{(}h(j)\big{)}}$${X}$$\scriptstyle{\varepsilon_{h(j)}}$$\scriptstyle{\Psi_{j}^{-1}}$$\scriptstyle{f_{h(j)}}$$\scriptstyle{e_{j}}$$\scriptstyle{\Psi_{j}}$$\scriptstyle{g_{j}}$$\scriptstyle{\varepsilon_{h(j)}}$$\scriptstyle{f_{h(j)}}$

Note that this means
$(\Psi_{j},\Psi_{j}^{-1}):\;g_{j}=_{{\mathbb{F}^{\rightharpoonup}(X,Y)}}f_{h(j)}$
for any $j\in J$ .

######  Remark 4.4.

If in the above setting $\bm{M}$ is a $J$-set of partial functions, we get
that $h:J\hookrightarrow I$ is actually an embedding. This follows from the
fact that any family of partial functions-map is a family of subsets-map on
the family of domains, which allows us to use the proof given in remark (2.4).

##  Chapter 3 Measure theory

So far, we have considered some of the fundamental notions of BST and we have
introduced the corresponding notions of set-indexed families. In this section
we want to apply these tools to BCMT. Not only will our reformulation be
predicative but we also can develop central parts of BCMT entirely without the
axiom of countable choice.

###  1 On the impredicative character of BCMT

The basic notions of BCMT are integration and measure spaces. Their
definitions in [BB85] are already somewhat problematic from a predicative
point of view. Moreover, the complete extension of an integration space, which
plays a crucial role in BCMT, takes the class of integrable functions to a be
set. As we will see below, this is not acceptable predicatively, a fact which
has been pointed out repeatedely in the literature. In fact, the development
of algebraic constructive measure theory mentioned in the introduction
specifically addresses this problem and proposes a solution by giving a new
point-free approach.

However, we are interested in a solution that still works within BCMT or BISH
more generally. In the next section we will take an in-depth look at the
impredicativities present in BCMT and single out three particular problems
that a predicative account needs to address. Two of those problems can be
resolved by refining the definition of an integration and a measure space.
This will lead us to the notions of a pre-integration and pre-measure space
that, among other things, make explicit use of set-indexed families. The third
problem concerns the integrable function and our proposal for its solution
will be postponed to the last section of this capter.

####  1 Three problems

Consider the definition of a measure space as given in [BB85, p. 282]:

> A _measure space_ is a triple $(X,M,\mu)$ consisting of a nonvoid set $X$
> with an inequality $\neq$, a set $M$ of complemented sets in $X$, and a
> mapping $\mu$ of $M$ into $\mathbb{R}^{0+}$, such that the following
> properties hold. […]

and likewise that of an integration space [BB85, p. 217]:

> A triple $(X,L,I)$ is an _integration space_ if $X$ is a nonvoid set with an
> inequality $\neq$, $L$ a subset of $\mathcal{F}(X)$, and $I$ is a mapping of
> $L$ into $\mathbb{R}$ such that the following properties hold. […]

The question now arises, how we can speak about or define sets of complemented
subsets and real-valued partial functions if the totalities
$\mathcal{P}^{][}(X)$ and $\mathcal{F}(X)$ are not sets. Defining these sets
by seperating them out of the totalities of complemented subsets or partial
functions by some extensional property is not possible. However, at least the
phrase "_$L$ a subset of $\mathcal{F}(X)$_" seems to suggest such a reading.

This first problem is easily resolved using the tools introduced in the
previous section. We defined sets of complemented subsets or partial functions
to be certain kinds of set-indexed families. It is safe to assume that Bishop
had these notions of sets of complemented subsets or partial functions in
mind, but did not explicitly mention the respective index sets in order to
make BCMT more accessible to classically trained mathematicians.

We want to make sure that we work absolutely predicatively and thus introduce
the required indexing explicitely. A measure space is thus actually a
quadruple $(X,I,\bm{\lambda},\mu)$ where $X$ is an inhabited set with a fixed
inequality $\neq_{X}$, $I$ is some index-set, $\bm{\lambda}$ is an $I$-set of
complemented subsets of $X$ and $\mu$ is the measure, such that certain
conditions hold. Similarly, an integration space is thus actually a quadruple
$(X,I,\bm{\Lambda},\int)$ where $X$ is an inhabited set with a fixed
inequality $\neq_{X}$, $I$ is some index-set, $\bm{\Lambda}$ is an $I$-set of
real valued partial functions of $X$ and $\int$ is the integral, such that
certain conditions hold.

The second problem is a bit more serious. Consider the second defining
property of a measure space in [BB85, p. 282]:

> (10.1.2) If $A$ and $A\wedge B$ belong to $M$, then so does $A-B$, and
> $\mu(A)=\mu(A\wedge B)+\mu(A-B)$.

Formally, with the indexing being made explicit, this condition looks as
follows:

$\displaystyle\forall i\in
I\;\forall\bm{B}\in\mathcal{P}^{][}(X):\;\bigg{(}\exists j\in I\text{ s.t.
}\bm{\lambda}_{0}(j)=\bm{\lambda}_{0}(i)\wedge\bm{B}\bigg{)}\;$
$\displaystyle\Rightarrow\;\bigg{(}\exists k\in I\text{ s.t.
}\bm{\lambda}_{0}(k)=\bm{\lambda}_{0}(i)-\bm{B}\quad\&\quad\mu(\bm{\lambda}_{0}(i))=\mu(\bm{\lambda}_{0}(j))+\mu(\bm{\lambda}_{0}(k))\bigg{)}$

This means that the definition of measure space contains universal
quantification over $\mathcal{P}^{][}(X)$, a totality which is not a set. From
a predicative point of view this is not an acceptable definition. In his ’67
book Bishop was much more cautious regarding this problem, giving the follong
definition of measure space (see [Bis67, p.183]):

> […] Let $\mathfrak{F}$ be any family of complemented subsets of $X$ […] Let
> $\mathfrak{M}$ be a subfamily of $\mathfrak{F}$ closed under finite unions,
> intersections, and differences. Let the function
> $\mu:\mathfrak{M}\rightarrow\mathbb{R}^{0+}$ satisfy the following
> conditions […]

Here a measure space takes the form $(X,I,\bm{\lambda},J,\bm{\nu},\mu)$, where
$\bm{\lambda}$ is an $I$-family and $\bm{\nu}$ is a $J$-family of complemented
subsets s.t. $\bm{\lambda}$ is a subfamily of $\bm{\nu}$. The measure $\mu$ is
defined on the ‘smaller’ family $\bm{\lambda}$ and the ‘larger’ family
$\bm{\nu}$ works as a substitute for the totality $\mathcal{P}^{][}(X)$. The
troubling defining condition then takes the form:

> If $A\in\mathfrak{M}$, if $B\in\mathfrak{F}$, and if $A\cap
> B\in\mathfrak{M}$, then $A-B\in\mathfrak{M}$ and $\mu(A)=\mu(A\cap
> B)+\mu(A-B)$

This means that we can replace quantification over $\mathcal{P}^{][}(X)$ by
quantification over the larger index set $J$.

Before we put everything we discussed above together to give a precise and
predicative definition of integration and measure space we want to mention the
third problem that is also the most serious one. Consider the definition of an
integrable function over some integration space $(X,L,I)$ in [BB85, p. 222]:

> An element $f$ of $\mathcal{F}(X)$ is an _integrable function_ if there
> exists a sequence $(f_{n})$ of functions in $L$ such that $\sum_{n}I(\lvert
> f_{n}\rvert)$ converges and, and $f(x)=\sum_{n}{f_{n}(x)}$ whenever
> $\sum_{n}\lvert f_{n}(x)\rvert$ converges. The sequence $(f_{n})$ is called
> a _representation_ of $f$ […] in $L$. We write $L_{1}$ for the class of
> integrable functions.

It has been pointed out that this class $L_{1}$ is in general not a set, since
its membership condition explicitly involves the totality of partial
functions. However, the complete extension of an integration space contains
$L_{1}$ as its set of partial functions, on which the extended integral is
defined. Our strategy to resolve this problem is to replace $L_{1}$ by
something smaller that actually constitutes a set of partial functions and
show that working with that smaller family is actually sufficient to construct
the complete extension.

####  2 Pre-measure and pre-integration spaces

Before tackling the third problem mentioned in the previous section, we have
to give precise definitions of the notions of integration and measure space
that we want to work with. We argued that sets of complemented subsets and
partial functions should explicitly be treated as set-indexed families. This
forces us to make a few choices on how to express the defining conditions of
integration and measure spaces. In BCMT a measure is a function on a set of
complemented subsets and an integral is function on a set of partial
functions. Since we are concerned with set-indexed families rather than simple
sets we have to make precise what kind of functions measures and integrals
actually are. Also, the definitions of measure and integration spaces involve
certain closedness conditions that we want to rewrite in a way that allows us
to avoid the use of choice principles.

In his paper "Mathematics as a numerical language" Bishop makes a suggestion
on how to formalize the measure theory of his ’67 book:

> A _measure space_ is a family $\mathcal{M}\equiv\\{A_{t}\\}_{t\in T}$ of
> complemented subsets of a set $X$ […], a map
> $\mu:T\rightarrow\mathbb{R}^{0+}$ and an additional structure as follows:
> […] If $t$ and $s$ are in $T$, there exists an element $s\vee t$ of $T$ such
> that $A_{s\vee t}<A_{t}\cup A_{s}$. Similarly, there exist operations
> $\wedge$ and $\sim$ on $T$, corresponding to the set-theoretic operations
> $\cap$ and $-$.
>
> \- [Bis70, p. 67]

Translating this to BCMT, there are two main ideas here to consider:

  1. (i)

The measure of a measure space is a function defined on the index-set of the
set of complemented susets and likewise is the integral a function on the
index-set of the set of partial functions.

  2. (ii)

Set theoretic operations under which the complemented subsets of a measure
space are closed are introduced via operations on the index-set corresponding
to those set-theoretic operation. The same applies to the function-theoretic
operations under which the partial functions of an integration space are
closed.

Putting everything together we arrive at what will be called pre-integration
and pre-measure spaces. For the remainder of this paper we want to show that
important parts of BCMT can be recovered using these predicative notions
rather the original measure and integration spaces as defined in [BB85]. We
start by introducing pre-integration spaces.

######  Definition 1.1.

Let $X$ be an inhabited set with inequality $\neq_{X}$, $I$ a set,
$\bm{\Lambda}=(\lambda_{0},\lambda_{1},\mathcal{E},F)$ an $I$-set of real-
valued partial functions and $\int:I\rightarrow\mathbb{R}$ a function.
Furthermore, assume that we have assignment routines

$\displaystyle\\_\cdot\\_:\mathbb{R}\times I\rightsquigarrow I$
$\displaystyle\\_+\\_:I\times I\rightsquigarrow I$
$\displaystyle\lvert\\_\rvert:I\rightsquigarrow I$
$\displaystyle\wedge_{1}:I\rightsquigarrow I$

Then $(X,I,\bm{\Lambda},\int)$ is called a _pre-integration_ space if the
following conditions hold (PIS4)

$\forall i,j\in I\;\forall a,b\in\mathbb{R}$ we have

  * •

$f_{a\cdot i}=_{{\mathcal{F}(X)}}af_{i}$

  * •

$f_{i+j}=_{{\mathcal{F}(X)}}f_{i}+f_{j}$

  * •

$f_{\lvert i\rvert}=_{{\mathcal{F}(X)}}\lvert f_{i}\rvert$

  * •

$f_{\wedge_{1}(i)}=_{{\mathcal{F}(X)}}f_{i}\wedge 1$

and we have that $\int(a\cdot i+b\cdot j)=_{\mathbb{R}}a\int i+b\int j$

$\forall i\in I\;\forall\alpha\in\mathbb{F}(\mathbb{N},I)$, if

  * •

$\forall m\in\mathbb{N}:\;f_{\alpha(m)}\geq 0$ and

  * •

$\ell:=\lim_{n\rightarrow\infty}\int\sum_{k=1}^{n}\alpha(k)=\sum_{k=1}^{\infty}\int\alpha(k)$
exists and $\ell<\int i$

then there is
$x\in\lambda_{0}(i)\cap\big{(}\bigcap_{n\in\mathbb{N}}\lambda_{0}(\alpha(n))\big{)}$
s.t. ${\ell^{\prime}:=\sum_{k=1}^{\infty}f_{\alpha(k)}(x)}$ exists and
$\ell^{\prime}<f_{i}(x)$.

$\exists i\in I$ s.t. $\int i=_{\mathbb{R}}1$

$\forall i\in I$, for $\alpha,\beta\in\mathbb{F}(\mathbb{N},I)$ defined by
$\alpha(m)=m\cdot(\wedge_{1}(m^{-1}\cdot i))\text{ and
}\beta(m)=m^{-1}\cdot(\wedge_{1}(m\cdot\lvert i\rvert))$ we have that
$\ell:=\lim_{n\rightarrow\infty}\int\alpha(n),\;\ell^{\prime}:=\lim_{n\rightarrow\infty}\int\beta(n)$
exist and $\ell=_{\mathbb{R}}\int i$ and $\ell^{\prime}=_{\mathbb{R}}0$.

######  Remark 1.2.

From (PIS1) and the fact that $\bm{\Lambda}$ is an $I$-set of partial
functions it follows that the assignment routines
$\cdot,+,\lvert\\_\rvert,\wedge_{1}$ are functions. Also note that we can
define operations $\vee,\wedge:I\rightarrow I$ by $i\vee
j:=j+\frac{1}{2}\cdot(i-j+\lvert i-j\rvert)$ and $i\wedge
j:=-\big{(}(-i)\vee(-j)\big{)}$ for $i,j\in I$ such that $f_{i\vee
j}=_{{\mathcal{F}(X)}}f_{i}\vee f_{j}$ and $f_{i\wedge
j}=_{{\mathcal{F}(X)}}f_{i}\wedge f_{j}$.

######  Definition 1.3.

Let $X$ be an inhabited set with an apartness-relation $\neq_{X}$, $I,J$ sets,
$\bm{\lambda}=(\lambda_{0}^{1},\lambda_{1}^{1},\mathcal{E}^{1},\lambda_{0}^{0},\lambda_{1}^{0},\mathcal{E}^{0})$
an $I$-set and
$\bm{\nu}=(\nu_{0}^{1},\nu_{1}^{1},E^{1},\nu_{0}^{0},\nu_{1}^{0},E^{0})$ a
$J$-set of complemented subsets of $X$ s.t. $\bm{\lambda}$ is a subfamily of
$\bm{\nu}$ (i.e. we have an embedding ${h:I\hookrightarrow J}$ and family maps
$\bm{\Psi},\bm{\Psi}^{-1}$ that we take as implicitly given) and
$\mu:I\rightarrow\mathbb{R}_{\geq 0}$ a function. Furthermore, assume that we
have assignment routines $\wedge:J\times J\rightsquigarrow J$, $\vee:J\times
J\rightsquigarrow J$ and $\sim:J\rightsquigarrow J$, as well as
$\wedge:I\times I\rightsquigarrow I$, $\vee:I\times I\rightsquigarrow I$ and
$\sim:I\times I\rightsquigarrow I$ s.t. for all $i,j\in I$ we have

  * •

$h(i\wedge j)=_{J}h(i)\wedge h(j)$

  * •

$h(i\vee j)=_{J}h(i)\vee h(j)$

  * •

$h(i\sim j)=_{J}h(i)\wedge\sim h(j)$

Then $(X,I,\bm{\lambda},J,\bm{\nu},\mu)$ is a _pre-measure space_ if the
following conditions hold: (PMS4)

$\forall i,j\in J$ we have

  * •

$\bm{\nu}_{0}(i\wedge
j)=_{{\mathcal{P}^{{{][}}}(X)}}\bm{\nu}_{0}(i)\wedge\bm{\nu}_{0}(j)$

  * •

$\bm{\nu}_{0}(i\vee
j)=_{{\mathcal{P}^{{{][}}}(X)}}\bm{\nu}_{0}(i)\vee\bm{\nu}_{0}(j)$

  * •

$\bm{\nu}_{0}(\sim i)=_{{\mathcal{P}^{{{][}}}(X)}}-\bm{\nu}_{0}(i)$

and for $i,j\in I$ we have that $\mu(i)+(j)=_{\mathbb{R}}\mu(i\vee
j)+\mu(i\wedge j)$.

$\forall i\in I\;\forall j\in J:$ If there is a $k\in I$ s.t.
$h(k)=_{J}h(i)\wedge j$, then there exist $l\in I$ s.t.
$h(l)=_{J}h(i)\wedge\sim j$ and $\mu(i)=_{\mathbb{R}}\mu(k)+\mu(l)$.

$\exists i\in I\text{ s.t. }\mu(i)>0$.

$\forall\alpha\in\mathbb{F}(\mathbb{N},I):$ If
$\ell:=\lim_{m\rightarrow\infty}\mu(\bigwedge_{n=1}^{m}\alpha(n))$ exists and
$\ell>0$, then there is a
$x\in\bigcap_{n\in\mathbb{N}}\lambda_{0}^{1}(\alpha(n))$ (i.e.
$\bigcap_{n\in\mathbb{N}}\lambda_{0}^{1}(\alpha(n))$ is inhabited).

######  Remark 1.4.

Let $i,j\in I$, then it follows that

  * •

$\bm{\lambda}_{0}(i\wedge
j)=_{{\mathcal{P}^{{{][}}}(X)}}\bm{\lambda}_{0}(i)\wedge\bm{\lambda}_{0}(j)$

  * •

$\bm{\lambda}_{0}(i\vee
j)=_{{\mathcal{P}^{{{][}}}(X)}}\bm{\lambda}_{0}(i)\vee\bm{\lambda}_{0}(j)$

  * •

$\bm{\lambda}_{0}(i\sim
j)=_{{\mathcal{P}^{{{][}}}(X)}}\bm{\lambda}_{0}(i)-\bm{\lambda}_{0}(j)$

from (PMS1) and the fact $\bm{\lambda}$ is a subfamily of $\bm{\nu}$. Also it
follows from (PMS2) that $\mu(i)=\mu(i\wedge j)+\mu(i\sim j)$ for all $i,j\in
I$.

At the end of this section we want to give a concrete example of a pre-measure
space. We have alredy seen that if we equip any set $X$ with the inequality

$\displaystyle x\neq_{X}y\;:\Leftrightarrow\;\exists
f\in\mathbb{F}(X,\bm{2})\text{ s.t. }f(x)\neq f(y)$

We can define the $\mathbb{F}(X,\bm{2})$-set of detachable subsets, which
classically corresponds to the powerset of $X$. The perhaps simplest example
of a measure space in classical measure theory is the $\sigma$-algebra of all
subsets together with the Dirac-measure, i.e. the measure concentrated at a
single point. We want to give an analogous example for pre-measure
spaces.111This example was first described [Pet19b], but appears here in a
slightly different form since we use a different notion of pre-measure space.

Let $X$ be inhabited with $x_{0}\in X$ and equiped with the inequality
$\neq_{X}$ defined above. From now on we regard $\bm{2}$ as asubset of
$\mathbb{R}$. Define

$\displaystyle\mu_{x_{0}}:\mathbb{F}(X,\bm{2})$
$\displaystyle\rightarrow\mathbb{R}_{\geq 0}$ $\displaystyle f$
$\displaystyle\mapsto f(x_{0})$

We have to introduce operations on $\mathbb{F}(X,\bm{2})$, so let
$f,g\in\mathbb{F}(X,\bm{2})$ and define

  * •

$f\wedge g:=fg$

  * •

$f\vee g:=f+g-fg$

  * •

$\sim f:=1-f$

Then
$(X,\mathbb{F}(X,\bm{2}),\bm{\delta},\mathbb{F}(X,\bm{2}),\bm{\delta},\mu_{x_{0}})$
is a pre-measure space, where the embedding
$\text{id}_{\mathbb{F}(X,\bm{2})}:\mathbb{F}(X,\bm{2})\rightarrow\mathbb{F}(X,\bm{2})$
and the identity family maps make $\bm{\delta}$ into a subfamily of itself and
the operations are the ones defined above for both index-sets.

It remains to verify (PMS1)-(PMS4). Recall that for any
$f\in\mathbb{F}(X,\bm{2})$ we have that
$\chi_{\bm{\delta}_{0}(f)}=_{{\mathcal{F}(X)}}f$ and that complemented subsets
are equal if and only if their characteristic functions are equal as partial
functions, which gives us

  * •

$\bm{\delta}_{0}(f\wedge
g)=_{{\mathcal{P}^{{{][}}}(X)}}\bm{\delta}_{0}(f)\wedge\bm{\delta}_{0}(g)$

  * •

$\bm{\delta}_{0}(f\vee
g)=_{{\mathcal{P}^{{{][}}}(X)}}\bm{\delta}_{0}(f)\vee\bm{\delta}_{0}(g)$

  * •

$\bm{\delta}_{0}(\sim f)=_{{\mathcal{P}^{{{][}}}(X)}}-\bm{\delta}_{0}(f)$

Moreover, we have that

$\displaystyle\mu_{x_{0}}(f)+\mu_{x_{0}}(g)=f(x_{0})+g(x_{0})-f(x_{0})g(x_{0})+f(x_{0})g(x_{0})=\mu_{x_{0}}(f\vee
g)+\mu_{x_{0}}(f\wedge g)$

which finishes the verification of (PMS1) and we have that

$\displaystyle\mu_{x_{0}}(f)=f(x_{0})\big{(}1-g(x_{0})\big{)}+f(x_{0})g(x_{0})=\mu_{x_{0}}(f\sim
g)+\mu_{x_{0}}(f\wedge g)$

which finishes the verification of (PMS2), since the first part of (PMS2)
holds trivially. To check (PMS3), observe that for
$\bar{1}\in\mathbb{F}(X,\bm{2})$, the constant function $1$, we have that
$\mu_{x_{0}}(\bar{1})=1$. Finally let
$\alpha\in\mathbb{F}(\mathbb{N},\mathbb{F}(X,\bm{2}))$ be such that

$\displaystyle\ell:=\lim_{m\rightarrow\infty}\mu_{x_{0}}\bigg{(}\bigwedge_{n=1}^{m}\alpha_{n}\bigg{)}=\lim_{m\rightarrow\infty}\prod_{n=1}^{m}\alpha_{n}(x_{0})$

exists and $\ell>0$. Then $\ell=1$ and in particular $\alpha_{n}(x_{0})=1$ for
all $n\in\mathbb{N}$, which means
$x_{0}\in\bigcap_{n\in\mathbb{N}}\delta_{0}^{1}(\alpha_{n})$. This proves
(PMS4).

###  2 The pre-integration space of simple functions

In this section we start with a pre-measure space
$(X,I,\bm{\lambda},J,\bm{\nu},\mu)$ and want to construct the corresponding
pre-integration space of simple functions. Together with the previous example
of the pre-measure space of detachable subsets with the Dirac-measure this
gives us a first example of a pre-integration space. We start by proving a few
basic facts about pre-measure spaces (see [BB85, p. 283-284]).

######  Lemma 2.1.

Let $i\in I$ s.t. $\lambda_{0}^{1}(i)=\emptyset$, then $\mu(i)=0$

###### Proof.

Assume that $\mu(i)>0$ and let $\alpha\in\mathbb{F}(\mathbb{N},I)$ be given by
$\alpha(n):=i$ for all $n\in\mathbb{N}$. Then
$\mu(i)=\lim_{m\rightarrow\infty}\mu\big{(}\bigwedge_{n=1}^{m}\alpha(n)\big{)}>0$
(in particular this limit exists). By (PMS4) we get that
$\bigcap_{n\in\mathbb{N}}\lambda_{0}^{1}(\alpha(n))=_{{\mathcal{P}(X)}}\lambda_{0}^{1}(i)$
is inhabited, which is a contradiction. Hence $\mu(i)=0$ by Lemma (2.18) of
[BB85] and the fact that $\mu(i)\geq 0$. ∎

######  Lemma 2.2.

Let $i_{1},...,i_{n}\in I$ and define
$F:=\bigcap_{k=1}^{n}\big{(}\lambda_{0}^{1}(i_{k})\cup\lambda_{0}^{0}(i_{k})\big{)}$,
then there is a $j\in I$ s.t. $\bm{\lambda}_{0}(j)=(\emptyset,F)$.

###### Proof.

For each $k=1,...,n$ we have that $\bm{\lambda}_{0}(i_{k}\sim
i_{k})=(\emptyset,\lambda_{0}^{1}(i_{k})\cup\lambda_{0}^{0}(i_{k}))$. It
follows that $\bm{\lambda}_{0}(\bigvee_{k=1}^{n}i_{k}\sim
i_{k})=\bigvee_{k=1}^{n}\bm{\lambda}_{0}(i_{k}\sim i_{k})=(\emptyset,F)$. ∎

######  Lemma 2.3.

Forall $j,i_{1},...,i_{n}\in I$ and define
$F:=\bigcap_{k=1}^{n}(\lambda_{0}^{1}(i_{k})\cup\lambda_{0}^{0}(i_{k}))$ there
is a $k\in I$ s.t. $\bm{\lambda}_{0}(k)=(\lambda_{0}^{1}(j)\cap
F,\lambda_{0}^{0}(j)\cap F)$ and $\mu(k)=\mu(j)$.

###### Proof.

Let $l:=\bigvee_{k=1}^{n}i_{k}\sim i_{k}\in I$ and define $k:=j\sim l\in I$.
Note that $\bm{\lambda}_{0}(k)=(\lambda_{0}^{1}(j)\cap
F,\lambda_{0}^{0}(j)\cap F)$ by lemma (2.2). Since $\bm{\lambda}_{0}(j\wedge
l)=(\emptyset,(\lambda_{0}^{1}(j)\cup\lambda_{0}^{0}(j))\cap F)$, we get that
$\mu(j\wedge l)=0$ by lemma (2.1). Thus by (PMS2) we get that

$\displaystyle\mu(j)=\mu(j\wedge l)+\mu(k)=\mu(k)$

∎

######  Lemma 2.4.

Let $i,j,i_{1},...,i_{n}\in I$ and define
$F:=\bigcap_{k=1}^{n}(\lambda_{0}^{1}(i_{k})\cup\lambda_{0}^{0}(i_{k}))$,
$F_{i}:=\lambda_{0}^{1}(i)\cup\lambda_{0}^{0}(i)$,
$F_{j}:=\lambda_{0}^{1}(j)\cup\lambda_{0}^{0}(j)$ and $F^{\prime}:=F_{i}\cap
F_{j}\cap F$. If
$\chi_{\bm{\lambda}_{0}(i)}(x)\leq\chi_{\bm{\lambda}_{0}(j)}(x)$ for every
$x\in F^{\prime}$, then $\mu(i)\leq\mu(j)$.

###### Proof.

Let $i^{\prime},j^{\prime}\in I$ be s.t.

  * •

$\bm{\lambda}_{0}(i^{\prime})=(\lambda_{0}^{1}(i)\cap
F^{\prime},\lambda_{0}^{0}(i)\cap F^{\prime})$

  * •

$\bm{\lambda}_{0}(j^{\prime})=(\lambda_{0}^{1}(j)\cap
F^{\prime},\lambda_{0}^{0}(j)\cap F^{\prime})$

They exist by lemma (2.3) and we have $\mu(i)=\mu(i^{\prime})$ and
$\mu(j)=\mu(j^{\prime})$. Since we have
$\chi_{\bm{\lambda}_{0}(i)}\wedge\chi_{\bm{\lambda}_{0}(j)}=\chi_{\bm{\lambda}_{0}(i)}$
on $F^{\prime}$, it follows that $j^{\prime}\wedge i^{\prime}=_{I}i^{\prime}$.
Let $k:=j^{\prime}\sim i^{\prime}$, then by (PMS2) we get that

$\displaystyle\mu(i)=\mu(i^{\prime})=\mu(j^{\prime})-\mu(k)\leq\mu(j^{\prime})=\mu(j)$

∎

We now want to introduce the set of simple functions over our pre-measure
space. To do this we first have to define an appropriate index set, construct
the family of simple functions over this index set and show that this family
is indeed a set of partial functions.

######  Definition 2.5.

Let $X$ be a set with an apartness-relation $\neq_{X}$, $I$ be a set and
$\bm{\lambda}=(\lambda_{0}^{1},\lambda_{1}^{1},\mathcal{E}^{1},\lambda_{0}^{0},\lambda_{1}^{0},\mathcal{E}^{0})$
an $I$-family of complemented subsets of $X$. The set $S(I)$ is the totality
$\sum_{n\in\mathbb{N}}(\mathbb{R}\times I)^{n}$ with the equality:

$\displaystyle(a_{k},i_{k})_{k=1}^{n}=_{S(I)}(b_{\ell},j_{\ell})_{\ell=1}^{m}\;:\Leftrightarrow\;\sum_{k=1}^{n}a_{k}\cdot\chi_{\bm{\lambda}_{0}(i_{k})}=_{{\mathcal{F}(X)}}\sum_{\ell=1}^{m}b_{\ell}\cdot\chi_{\bm{\lambda}_{0}(j_{\ell})}$

We define the $S(I)$-family of (real-valued) partial functions
$\bm{\Lambda}=(\lambda_{0},\lambda_{1},\mathcal{E},F)$ as follows:

  1. (i)

$\lambda_{0}:S(I)\rightsquigarrow\mathbb{V}_{0}$ is the the assignment-routine
given by

$\displaystyle(a_{k},i_{k})_{k=1}^{n}\;\mapsto\;\bigcap_{k=1}^{n}\big{(}\lambda_{0}^{1}(i_{k})\cup\lambda_{0}^{0}(i_{k})\big{)}$

  2. (ii)

$\mathcal{E}:\bigcurlywedge_{v\in S(I)}\mathbb{F}(\lambda_{0}(v),X)$ is the
dependent assignment routine that associates each $v:=(a_{k},i_{k})_{k=1}^{n}$
with the embedding
$\varepsilon_{v}:\bigcap_{k=1}^{n}\big{(}\lambda_{0}^{1}(i_{k})\cup\lambda_{0}^{0}(i_{k})\big{)}\hookrightarrow
X$ induced by the embeddings $\varepsilon_{i_{k}}^{1}$ and
$\varepsilon_{i_{k}}^{0}$

  3. (iii)

$\lambda_{1}:\bigcurlywedge_{(v,w)\in
S(I)}\mathbb{F}(\lambda_{0}(v),\lambda_{0}(w))$ is the dependent assignment
routine that associates each $(v,w)\in S(I)$ with the function
$\lambda_{vw}:\lambda_{0}(v)\rightarrow\lambda_{0}(w)$ s.t.

     * •

$\lambda_{vv}:=\text{id}_{\lambda_{0}(v)}$ and

     * •

$(\lambda_{vw},\lambda_{wv})$ witnesses the equality $v=_{S(I)}w$.222Here we
use lemma (1.2), i.e. the fact that two functions witnessing an equality of
subsets are equal.

  4. (iv)

$F:\bigcurlywedge_{v\in S(I)}\mathbb{F}(\lambda_{0}(v),\mathbb{R})$ is the
dependent assignment routine that assigns each $v:=(a_{k},i_{k})_{k=1}^{n}$
the function $f_{v}:=\sum_{k=1}^{n}a_{k}\cdot\chi_{\bm{\lambda}_{0}(i_{k})}$.

Note that from the definition of the equality $=_{S(I)}$ it immediatelly
follows that $\bm{\Lambda}$ is an $S(I)$-set of partial functions. Also note
that this construction can be done for any $I$-family $\bm{\lambda}$ of
complemented subsets. We now return to the case where we have a pre-measure
space $(X,I,\bm{\lambda},J,\bm{\nu},\mu)$ and want to show that we can define
an integral on $S(I)$ that allows us to construct the pre-integration of
simple functions. We first have to prove a few lemmas that use the additional
structure on the index set $I$ provided by the pre-measure space.

######  Lemma 2.6.

The assignment routine

$\displaystyle\mathsf{disjrep}:S(I)$ $\displaystyle\rightsquigarrow S(I)$
$\displaystyle(a_{k},i_{k})_{k=1}^{n}$
$\displaystyle\mapsto\Big{(}\sum_{f(k)=1}a_{k},\big{(}\bigwedge_{f(k)=1}i_{k}\big{)}\sim\big{(}\bigvee_{f(k)=0}i_{k}\big{)}\Big{)}_{f:\\{1,...,n\\}\rightarrow\bm{2}}$

is a function and as such identical to $\text{id}_{S(I)}$, i.e. for all $v\in
S(I)$ we have $v=_{S(I)}\mathsf{disjrep}(v)$. If for $v\in S(I)$ we have that
$\mathsf{disjrep}(v):=(b_{\ell},j_{\ell})_{\ell=1}^{m}$ then the
$\bm{\lambda}_{0}(j_{\ell})$ are _disjoint_ , i.e. for distinct $\ell$ and $k$
we have
$\chi_{\bm{\lambda}_{0}(j_{k})}\cdot\chi_{\bm{\lambda}_{0}(j_{\ell})}=0$ on
$\big{(}\lambda_{0}^{1}(j_{k})\cup\lambda_{0}^{0}(j_{k})\big{)}\cap\big{(}\lambda_{0}^{1}(j_{\ell})\cup\lambda_{0}^{0}(j_{\ell})\big{)}$.
For $v\in S(I)$ we call $\mathsf{disjrep}(v)$ the _disjoint representation_ of
$v$.

###### Proof.

Let $v:=(a_{k},i_{k})_{k=1}^{n}$. For a function
$f:\\{1,...,n\\}\rightarrow\bm{2}$ define $j_{f}\in I$ by

$\displaystyle
j_{f}:=\Big{(}\bigwedge_{f(k)=1}i_{k}\Big{)}\sim\Big{(}\bigvee_{f(k)=0}i_{k}\Big{)}$

Then

$\displaystyle\bm{\lambda}_{0}(j_{f})=\Big{(}\bigwedge_{f(k)=1}\bm{\lambda}_{0}(i_{k})\Big{)}\wedge\Big{(}\bigwedge_{f(k)=0}-\bm{\lambda}_{0}(i_{k})\Big{)}$

Using this it is easy to verify that we have

$\displaystyle\sum_{k=1}^{n}a_{k}\cdot\chi_{\bm{\lambda}_{0}(i_{k})}=_{{\mathcal{F}(X)}}\sum_{f:\\{1,...,n\\}\rightarrow\bm{2}}\bigg{(}\sum_{f(k)=1}a_{k}\bigg{)}\cdot\chi_{\bm{\lambda}_{0}(j_{f})}$

Now let $f,g:\\{1,...,n\\}\rightarrow\bm{2}$ be distinct functions, i.e. there
is a $k\in\\{1,...,n\\}$ s.t. $f(k)=1$ but $g(k)=0$ or vice versa. For such a
$k$ we get that $\lambda_{0}^{1}(j_{f})\subseteq\lambda_{0}^{1}(i_{k})$ and
$\lambda_{0}^{1}(j_{g})\subseteq\lambda_{0}^{0}(i_{k})$ or vice versa. This
implies that $\bm{\lambda}_{0}(j_{f})$ and $\bm{\lambda}_{0}(j_{g})$ are
disjoint. ∎

######  Lemma 2.7.

For each $v:=(a_{k},i_{k})_{k=1}^{n}\in S(I)$ we have

$\displaystyle\sum_{k=1}^{n}a_{k}\cdot\mu(i_{k})=\sum_{f:\\{1,...,n\\}\rightarrow\bm{2}}\bigg{(}\sum_{f(k)=1}a_{k}\bigg{)}\cdot\mu(j_{f})$

where $j_{f}\in I$ is defined for $f:\\{1,...,n\\}\rightarrow\bm{2}$ as in the
proof of the previous lemma.

###### Proof.

Let $F:=\bigcap_{k=1}^{n}(\lambda_{0}^{1}(i_{k})\cup\lambda_{0}^{0}(i_{k}))$,
without loss of generality we can assume that for every $k\in\\{1,...,n\\}$ we
have $\lambda_{0}^{1}(i_{k})\cup\lambda_{0}^{0}(i_{k})\subseteq F$ since
otherwise we can consider $i_{k}^{\prime}\in I$ s.t.
$\bm{\lambda}_{0}(i_{k}^{\prime})=(\lambda_{0}^{1}(i_{k})\cap
F,\lambda_{0}^{0}(i_{k})\cap F)$. By lemma (2.3) we have that
$\mu(i_{k})=\mu(i_{k}^{\prime})$ for each $k\in\\{1,...,n\\}$ and since for
each $f:\\{1,...,n\\}\rightarrow\bm{2}$ the domain of
$\chi_{\bm{\lambda}_{0}(j_{f})}$ is $F$ (with $j_{f}\in I$ as in the proof of
lemma (2.6)), we have that

$\displaystyle\bm{\lambda}_{0}(j_{S})=\Big{(}\bigwedge_{f(k)=1}\bm{\lambda}_{0}(i_{k})\Big{)}\wedge\Big{(}\bigwedge_{f(k)=0}-\bm{\lambda}_{0}(i_{k})\Big{)}=\Big{(}\bigwedge_{f(k)=1}\bm{\lambda}_{0}(i_{k}^{\prime})\Big{)}\wedge\Big{(}\bigwedge_{f(k)=0}-\bm{\lambda}_{0}(i_{k}^{\prime})\Big{)}$

For $k\in\\{1,...,n\\}$, let $P(k)$ be the set of functions
$f:\\{1,...,n\\}\rightarrow\bm{2}$ s.t. $f(k)=1$. Note that for each $x\in F$
we have

$\displaystyle x\in\lambda_{0}^{1}(i_{k})\;$
$\displaystyle\Leftrightarrow\;x\in\bigcup_{f\in
P(k)}\lambda_{0}^{1}(j_{f})\text{ and}$ $\displaystyle
x\in\lambda_{0}^{0}(i_{k})\;$ $\displaystyle\Leftrightarrow\;x\in\bigcap_{f\in
P(k)}\lambda_{0}^{0}(j_{f})$

It follows that $\chi_{\bm{\lambda}_{0}(i_{k})}=\bigvee_{f\in
P(k)}\chi_{\bm{\lambda}_{0}(j_{f})}$ on $F$ and since
$\lambda_{0}^{1}(i_{k})\cup\lambda_{0}^{0}(i_{k})\subseteq F$ we get that
$\bm{\lambda}_{0}(i_{k})=\bigvee_{f\in P(k)}\bm{\lambda}_{0}(j_{f})$.

Furthermore, note that for any $i,j\in I$ s.t. $\bm{\lambda}_{0}(i)$ and
$\bm{\lambda}_{0}(j)$ are disjoint we have that
$\lambda_{0}^{1}(i)\cap\lambda_{0}^{1}(j)=\emptyset$ and thus by lemma (2.1)
it follows that $\mu(i\wedge j)=0$. Hence by (PMS1) $\mu(i_{k})=\sum_{f\in
P(k)}\mu(j_{f})$. Using this it is easy to see that

$\displaystyle\sum_{k=1}^{n}a_{k}\cdot\mu(i_{k})$
$\displaystyle=\sum_{k=1}^{n}a_{k}\cdot\Big{(}\sum_{f\in
P(k)}\mu(j_{f})\Big{)}$
$\displaystyle=\sum_{f:\\{1,...,n\\}\rightarrow\bm{2}}\Big{(}\sum_{k\text{
s.t. }f\in P(k)}a_{k}\Big{)}\cdot\mu(j_{f})$
$\displaystyle=\sum_{f:\\{1,...,n\\}\rightarrow\bm{2}}\Big{(}\sum_{f(k)=1}a_{k}\Big{)}\cdot\mu(j_{f})$

∎

######  Lemma 2.8.

Let $v:=(a_{k},i_{k})_{k=1}^{n},w:=(b_{\ell},j_{\ell})_{\ell=1}^{m}\in S(I)$
be s.t.

$\displaystyle\sum_{k=1}^{n}a_{k}\cdot\chi_{\bm{\lambda}_{0}(i_{k})}(x)\leq\sum_{\ell=1}^{m}b_{\ell}\cdot\chi_{\bm{\lambda}_{0}(j_{\ell})}(x)$

for all $x\in
F:=\Big{(}\bigcap_{k=1}^{n}(\lambda_{0}^{1}(i_{k})\cup\lambda_{0}^{0}(i_{k}))\Big{)}\cap\Big{(}\bigcap_{\ell=1}^{m}(\lambda_{0}^{1}(j_{\ell})\cup\lambda_{0}^{0}(j_{\ell}))\Big{)}$,
then

$\displaystyle a:=\sum_{k=1}^{n}a_{k}\cdot\mu(i_{k})\leq
b:=\sum_{\ell=1}^{m}b_{\ell}\cdot\mu(j_{\ell})$

###### Proof.

Without loss of generality we can assume that $n=m$ and for each
$k\in\\{1,...,n\\}$ we have $i_{k}=_{I}j_{k}$, because otherwise we can add
appropriate indices with coefficient $0$ to both functions respectively. Now,
assume that $a>b$, i.e. that
$\sum_{k=1}^{n}(a_{k}-b_{k})\cdot\mu(\bm{\lambda}_{0}(i_{k}))>0$. By lemma
(2.7) we get that

$\displaystyle\sum_{f:\\{1,...,n\\}\rightarrow\bm{2}}\Big{(}\sum_{f(k)=1}a_{k}-\sum_{f(k)=1}b_{k}\Big{)}\cdot\mu(j_{f})>0$

By (2.16) of [BB85] there is a function $f:\\{1,...,n\\}\rightarrow\bm{2}$
s.t. $\Big{(}\sum_{f(k)=1}a_{k}-\sum_{f(k)=1}b_{k}\Big{)}>0$ and
$\mu(j_{f})>0$. From the proof of lemma (2.1) it follows that there is an
$x\in\lambda_{0}^{1}(j_{f})\subseteq F$. For each $k\in\\{1,...,n\\}$ we get
that

$\displaystyle\chi_{\bm{\lambda}_{0}(i_{k})}(x)=1\;\Leftrightarrow\;f(k)=1$

and thus

$\displaystyle\sum_{f(k)=1}a_{k}=\sum_{k=1}^{n}a_{k}\cdot\chi_{\bm{\lambda}_{0}(i_{k})}(x)\leq\sum_{k=1}^{n}b_{k}\cdot\chi_{\bm{\lambda}_{0}(i_{k})}(x)=\sum_{f(k)=1}b_{k}$

which is a contradiction. Hence $a\leq b$. ∎

We can now define the integral on the simple functions and show that it is
indeed a function.

######  Lemma 2.9.

The assignment-routine

$\displaystyle\int\\_d\mu:S(I)$ $\displaystyle\rightsquigarrow\mathbb{R}$
$\displaystyle(a_{k},i_{k})_{k=1}^{n}$
$\displaystyle\mapsto\sum_{k=1}^{n}a_{k}\cdot\mu(i_{k})$

is a function.

###### Proof.

Let $v:=(a_{k},i_{k})_{k=1}^{n},w:=(b_{\ell},j_{\ell})_{\ell=1}^{m}\in S(I)$
be s.t. $v=_{S(I)}w$ (i.e. $f_{v}=_{{\mathcal{F}(X)}}f_{w}$) and let
$F:=\lambda_{0}(v)\cap\lambda_{0}(w)$. We thus have $f_{v}\leq f_{w}$ on $F$
and $f_{v}\geq f_{w}$ on $F$, and thus by lemma (2.8)

$\displaystyle\Big{(}\int v\;d\mu\leq\int w\;d\mu\;\;\&\;\int v\;d\mu\geq\int
w\;d\mu\Big{)}\;\Rightarrow\;\int v\;d\mu=\int w\;d\mu$

∎

It remains to show that $(X,S(I),\bm{\Lambda},\int\\_d\mu)$ is a pre-
integration space. For this we need two more lemmas. Since we don’t want to
use countable choice, the next lemma and its proof is a bit more involved than
lemma 10.8 in [BB85, p. 284].

######  Lemma 2.10.

Let $S^{+}(I):=\\{v\in S(I):f_{v}\geq 0\\}$, then there is a function
${\phi:\mathbb{N}\rightarrow S^{+}(I)\rightarrow I}$ with
$N\mapsto(\phi_{N}:S^{+}(I)\rightarrow I)$, s.t. for all $N\in\mathbb{N}$ and
$v\in S(I)$ we have

  * •

$\lambda_{0}^{1}(\phi_{N}(v))\cup\lambda_{0}^{0}(\phi_{N}(v))\subseteq\lambda_{0}(v)$

  * •

$\forall x\in\lambda_{0}^{0}(\phi_{N}(v)):\;f_{v}(x)<N^{-1}$

  * •

$\mu(\phi_{N}(v))\leq 2N\int v\;d\mu$

###### Proof.

Fix $N\in\mathbb{N}$ and let $v\in S^{+}(I)$ and
$\mathsf{disjrep}(v):=(a_{k},i_{k})_{k=1}^{n}$. Then $a_{k}\geq 0$ for all
$k=1,...,n$. Let $f,g:\\{1,...,n\\}\rightarrow\bm{2}$ be functions s.t.

  1. (i)

$\forall k\in\\{1,...,n\\}:\;f(k)\vee g(k)=1$

  2. (ii)

$f(k)=1\;\Rightarrow\;a_{k}<N^{-1}$

  3. (iii)

$g(k)=1\;\Rightarrow\;a_{k}>(2N)^{-1}$

Such $f$ and $g$ exist by corollary (2.17) of [BB85]. We have that

$\displaystyle\Big{(}\forall
k\in\\{1,...,n\\}:\;f(k)=1\Big{)}\quad\text{or}\quad\Big{(}\exists
k\in\\{1,...,n\\}\text{ s.t. }g(k)=1\Big{)}$

Now assume we have another pair of functions
$f^{\prime},g^{\prime}:\\{1,...,n\\}\rightarrow\bm{2}$ s.t. the conditions
(i)-(iii) hold. Let $f^{\prime\prime}:=f\vee f^{\prime}$ and
$g^{\prime\prime}:=g\vee g^{\prime}$. It is easy to verify that
$f^{\prime\prime},g^{\prime\prime}$ also fulfill (i)-(iii).

Since there are only finitely many pairs of functions
$\\{1,...,n\\}\rightarrow\bm{2}$ s.t. (i)-(iii) hold and they are closed under
taking (pointwise) maxima we can consider the _maximal_ functions
$\varphi_{v},\psi_{v}:\\{1,...,n\\}\rightarrow\bm{2}$ s.t. (i)-(iii) hold. In
particular they will be given by

$\displaystyle\Bigg{(}\varphi_{v}=\bigvee_{\begin{subarray}{c}\exists
g:\\{1,...,n\\}\rightarrow\bm{2}\\\ (f,g)\text{ fulfill
(i)-(iii)}\end{subarray}}f\Bigg{)}\quad\quad\&\quad\quad\Bigg{(}\psi_{v}=\bigvee_{\begin{subarray}{c}\exists
f:\\{1,...,n\\}\rightarrow\bm{2}\\\ (f,g)\text{ fulfill
(i)-(iii)}\end{subarray}}g\Bigg{)}$

Now, let

$\displaystyle\phi_{N}(v):=\begin{cases}\bigvee_{k=1}^{n}(i_{k}\sim
i_{k}),\text{ if }\forall k\in\\{1,...,n\\}:\;\varphi_{v}(k)=1\\\
\Big{(}\bigvee_{\psi_{v}(k)=1}i_{k}\Big{)}\sim\Big{(}\bigvee_{k=1}^{n}(i_{k}\sim
i_{k})\Big{)},\text{ else}\end{cases}$

Notice that this is a valid case distinction. In order to verify that
$\phi_{N}(v)$ does indeed satisfy the three conditions of the lemma, observe
that $\bm{\lambda}_{0}(\bigvee_{k=1}^{n}(i_{k}\sim
i_{k}))=(\emptyset,\lambda_{0}(v))$ and for
$i_{v}:=\bigvee_{\psi_{v}(k)=1}i_{k}$ we have

$\displaystyle\bm{\lambda}_{0}\big{(}i_{v}\sim\bigvee_{k=1}^{n}(i_{k}\sim
i_{k})\big{)}=\big{(}\lambda_{0}^{1}(i_{v})\cap\lambda_{0}(v),\lambda_{0}^{0}(i_{v})\cap\lambda_{0}(v)\big{)}$

First assume that $\Big{(}\forall
k\in\\{1,...,n\\}:\;\varphi_{v}(k)=1\Big{)}$. Then for
$j:=\bigvee_{k=1}^{n}(i_{k}\sim i_{k})$ we have $\phi_{N}(v)=_{I}j$ and
clearly $\lambda_{0}^{1}(j)\cup\lambda_{0}^{0}(j)\subseteq\lambda_{0}(v)$ and
$\big{(}\forall x\in\lambda_{0}^{0}(j):\;f_{v}(x)<N^{-1}\big{)}$. Note that
$(2N)^{-1}\cdot\chi_{\bm{\lambda}_{0}(j)}\leq f_{v}$ on $\lambda_{0}(v)$. From
this, the third property follows by lemma (2.8).

If $\Big{(}\exists k\in\\{1,...,n\\}:\;\varphi_{v}(k)=0\Big{)}$, i.e.
$\psi_{v}(k)=1$, let $j:=i_{v}\sim\bigvee_{k=1}^{n}(i_{k}\sim i_{k})$. Then we
have $\phi_{N}(v)=_{I}j$ and clearly
$\lambda_{0}^{1}(j)\cup\lambda_{0}^{0}(j)\subseteq\lambda_{0}(v)$. Let
$x\in\lambda_{0}^{0}(j)$. Then
$x\in\bigcap_{\psi_{v}(k)=1}\lambda_{0}^{0}(i_{k})$ and thus $f_{v}(x)=0$ or
there is a $k\in\\{1,...,n\\}$ with $\varphi_{v}(k)=1$ s.t.
$x\in\lambda_{0}^{1}(i_{k})$, in which case $f_{v}(x)=a_{k}<N^{-1}$ since the
$\bm{\lambda}_{0}(i_{k})$ are disjoint. In either case the second condition is
fulfilled.

Using lemma (2.3) and the fact that the $\bm{\lambda}_{0}(i_{k})$ are disjoint
we get that

$\displaystyle\mu(j)=\mu(i_{v})=\sum_{\psi_{v}(k)=1}\mu(i_{k})\leq\sum_{\psi_{v}(k)=1}(2N)^{-1}\cdot
a_{k}\cdot\mu(i_{k})\leq(2N)^{-1}\int v\;d\mu$

Here the last inequality follows from lemma (2.8) using the fact that on
$\lambda_{0}(v)$ we have
$\sum_{\psi_{v}(k)=1}a_{k}\cdot\chi_{\bm{\lambda}_{0}(i_{k})}\leq f_{v}$.

It remains to check that $\phi_{N}$ is a function. So let $w\in S^{+}(I)$ s.t.
$v=_{S(I)}w$ (i.e. $f_{v}=_{{\mathcal{F}(X)}}f_{w}$) and
$\mathsf{disjrep}(w):=(b_{\ell},j_{\ell})_{\ell=1}^{m}$. Since $\bm{\lambda}$
is an $I$-set of complemented subsets it suffices to check that
$\bm{\lambda}_{0}(\phi_{N}(v))=_{{\mathcal{P}^{{{][}}}(X)}}\bm{\lambda}_{0}(\phi_{N}(w))$.

Note that by the above remarks $\chi_{\bm{\lambda}_{0}(\phi_{N}(v))}$ and
$\chi_{\bm{\lambda}_{0}(\phi_{N}(w))}$ have the same domain
$\lambda_{0}(v)=_{{\mathcal{P}(X)}}\lambda_{0}(w)$. Now, assume that for
$x\in\lambda_{0}(v)$ we have $\chi_{\bm{\lambda}_{0}(\phi_{N}(v))}(x)=1$, i.e.
$\lambda_{0}^{1}(\phi_{N}(v))$ is inhabited and we have
$x\in\lambda_{0}^{1}(i_{k})$ for some $k\in\\{1,...,n\\}$ with
$\psi_{v}(k)=1$. Thus $f_{v}(x)=a_{k}>(2N)^{-1}>0$ and since $f_{v}=f_{w}$ we
must also have $x\in\lambda_{0}^{1}(j_{\ell})$ for some $\ell=1,...,m$.
Moreover, $b_{\ell}=a_{k}>(2N)^{-1}$ and hence $\psi_{w}(\ell)=1$ by the
maximality of $\psi_{w}$. It follows that $x\in\lambda_{0}^{1}(i_{w})$ where
$i_{w}:=\bigvee_{\psi_{w}(\ell)=1}j_{\ell}$.

Also note that since $\lambda_{0}^{1}(\phi_{N}(v))$ is inhabited there is a
$k=1,...,n$ s.t. $\varphi_{v}(k)=0$ and hence we get that $a_{k}\geq N^{-1}$
and $\lambda_{0}^{1}(i_{k})$ is inhabited by the maximality of $\varphi_{v}$.
Thus, since $f_{v}=f_{w}$, there is an $\ell=1,...,m$ s.t. $b_{\ell}\geq
N^{-1}$ and $\lambda_{0}^{1}(j_{\ell})$ is inhabited, i.e. there is a
$\ell=1,...,m$ s.t. $\varphi_{w}(\ell)=0$ and
$\phi_{N}(w)=i_{w}\sim\bigvee_{\ell=1}^{m}(j_{\ell}\sim j_{\ell})$. It follows
that $\chi_{\bm{\lambda}_{0}(\phi_{N}(w))}(x)=1$. Repeating the argument for
$x\in\lambda_{0}(w)$ with $\chi_{\bm{\lambda}_{0}(\phi_{N}(w))}(x)=1$ we can
conclude that

$\displaystyle\Big{(}\lambda_{0}^{1}(\phi_{N}(v))\cup\lambda_{0}^{0}(\phi_{N}(v)\Big{)}=\lambda_{0}(v)$
$\displaystyle=\lambda_{0}(w)=\Big{(}\lambda_{0}^{1}(\phi_{N}(w))\cup\lambda_{0}^{0}(\phi_{N}(w)\Big{)}$
$\displaystyle\&\quad\quad\forall
x\in\lambda_{0}(v):\;\chi_{\bm{\lambda}_{0}(\phi_{N}(v))}(x)=1\;$
$\displaystyle\Leftrightarrow\;\chi_{\bm{\lambda}_{0}(\phi_{N}(w))}(x)=1$

which finishes the proof. ∎

######  Lemma 2.11.

Let $v:=(a_{k},i_{k})_{k=1}^{n}\in S(I)$ and $c>0$ be s.t. $f_{v}\leq c$ on
$\lambda_{0}(v)$. Let $i\in I$ be s.t. $f_{v}\leq 0$ on
$\lambda_{0}^{0}(i)\cap\lambda_{0}(v)$, then for every $\varepsilon>0$ there
exists a $j\in I$ s.t.

  1. (i)

$\lambda_{0}^{1}(j)\cup\lambda_{0}^{0}(j)\subseteq\lambda_{0}(v)$

  2. (ii)

$\forall x\in\lambda_{1}^{0}(j):\;f_{v}(x)>\varepsilon$

  3. (iii)

$\mu(j)\geq c^{-1}\big{(}\int v\;d\mu-2\varepsilon\mu(i)\big{)}$

###### Proof.

Again w.l.o.g. we can assume that the $\bm{\lambda}_{0}(i_{k})$ are disjoint
(otherwise replace $v$ by $\mathsf{disjrep}(v)$). Let
$f,g:\\{1,...,n\\}\rightarrow\bm{2}$ be functions s.t.

  1. (i)

$\forall k\in\\{1,...,n\\}:\;\text{either }f(k)=1\text{ or }g(k)=1$

  2. (ii)

$f(k)=1\;\Rightarrow\;a_{k}<N^{-1}$

  3. (iii)

$g(k)=1\;\Rightarrow\;a_{k}>(2N)^{-1}$

Such $f$ and $g$ exist by corollary (2.17) of [BB85]. We have that

$\displaystyle\Big{(}\forall
k\in\\{1,...,n\\}:\;f(k)=1\Big{)}\quad\text{or}\quad\Big{(}\exists
k\in\\{1,...,n\\}:\;g(k)=1\Big{)}$

In the first case, let $j\in I$ be such that
$\bm{\lambda}_{0}(j)=(\emptyset,\lambda_{0}(v))$ (such a $j$ exists by lemma
(2.2)). Then clearly
$\lambda_{0}^{1}(j)\cup\lambda_{0}^{0}(j)\subseteq\lambda_{0}(v)$ and $\forall
x\in\lambda_{1}^{0}(j):\;f_{v}(x)>\varepsilon$ is vacuously true. By lemma
(2.1) $\mu(j)=0$, so in order to check (iii) we need to prove

$\displaystyle 2\varepsilon\mu(i)\geq\int v\;d\mu$

which follows from lemma (2.8) and the fact that $f_{v}\leq
2\varepsilon\chi_{\bm{\lambda}_{0}(i)}$ on
$\lambda_{0}(v)\cap\big{(}\lambda_{0}^{1}(i)\cup\lambda_{0}^{0}(i)\big{)}$.
This inequality holds since $a_{k}<2\varepsilon$ for all $k$ and $f_{v}\leq 0$
on $\lambda_{0}^{0}(i)\cap\lambda_{0}(v)$.

Now assume that $\Big{(}\exists k\in\\{1,...,n\\}:\;g(k)=1\Big{)}$ is
inhabited. Let $j^{\prime}:=\bigvee_{g(k)=1}i_{k}$ and $j\in I$ s.t.
$\bm{\lambda}_{0}(j)=\big{(}\lambda_{0}^{1}(j^{\prime})\cap\lambda_{0}(v),\lambda_{0}^{0}(j^{\prime})\cap\lambda_{0}(v)\big{)}$.
Then clearly
$\lambda_{0}^{1}(j)\cup\lambda_{0}^{0}(j)\subseteq\lambda_{0}(v)$. If
$x\in\lambda_{0}^{1}(j)$ then in particular $x\in\lambda_{0}^{1}(i_{k})$ for
some $k\in\\{1,...,n\\}$ with $g(k)=1$ and hence $f_{v}(x)=a_{k}>\varepsilon$.

For each $k\in\\{1,...,n\\}$ let $j_{k}:=i_{k}\wedge i$ and define
$w:=(a_{k},i_{k}\wedge i)_{k=1}^{n}\in S(I)$. Using lemma (2.8) we get that

$\displaystyle\int v\;d\mu$ $\displaystyle\leq\int w\;d\mu$
$\displaystyle=\sum_{f(k)=1}a_{k}\mu(j_{k})\;+\;\sum_{g(k)=1}a_{k}\mu(j_{k})$
$\displaystyle\leq
2\varepsilon\Big{(}\sum_{f(k)=1}\mu(j_{k})\Big{)}\;+\;c\Big{(}\sum_{g(k)=1}\mu(j_{k})\Big{)}$
$\displaystyle\leq 2\varepsilon\mu(i)+c\mu(j)$

Note that the $\bm{\lambda}_{0}(j_{k})$ are disjoint, which allows us to make
the following estimates for the last inequality:

$\displaystyle\sum_{f(k)=1}\mu(j_{k})=\mu(\bigvee_{f(k)=1}j_{k})=\mu(i\wedge\bigvee_{f(k)=1}i_{k})\leq\mu(i)$

and

$\displaystyle\sum_{g(k)=1}\mu(j_{k})\leq\sum_{g(k)=1}\mu(i_{k})=\mu(j^{\prime})=\mu(j)$

∎

######  Theorem 2.12.

$(X,S(I),\bm{\Lambda},\int\\_d\mu)$ is a pre-integration space

###### Proof.

We first have to define the required assignment routines, so let $v,w\in S(I)$
s.t. $\mathsf{disjrep}(v):=(a_{k},i_{k})_{k=1}^{n}$ and
$\mathsf{disjrep}(w):=(b_{\ell},j_{\ell})_{\ell=1}^{m}$, $a\in\mathbb{R}$ and
define:

$\displaystyle a\cdot v$ $\displaystyle:=(a\cdot a_{k},i_{k})_{k=1}^{n}$
$\displaystyle v+w$
$\displaystyle:=\big{(}(a_{1},i_{1}),...,(a_{n},i_{n}),(b_{1},j_{1}),...,(b_{m},j_{m})\big{)}$
$\displaystyle\lvert v\rvert$ $\displaystyle:=(\lvert
a_{k}\rvert,i_{k})_{k=1}^{n}$ $\displaystyle\wedge_{1}(v)$
$\displaystyle:=(a_{k}\wedge 1,i_{k})_{k=1}^{n}$

It is easy to check that these assignment routines fulfill (PIS1).

By (PMS3) there is an $i\in I$ s.t. $\mu(i)>0$. Let $v:=(\mu(i)^{-1},i)\in
S(I)$, then $\int v\;d\mu=1$, which verifies (PIS3). Let $v\in S(I)$ with
$\mathsf{disjrep}(v):=(a_{k},i_{k})_{k=1}^{n}$ and
$\alpha,\beta\in\mathbb{F}(\mathbb{N},S(I))$ be given by
$\alpha(m)=m\cdot(\wedge_{1}(m^{-1}\cdot v))$ and
$\beta(m)=m^{-1}\cdot(\wedge_{1}(m\cdot\lvert v\rvert))$ for $m\in\mathbb{N}$.
Let $M_{0}\in\mathbb{N}$ be s.t. $M_{0}>a_{1}\vee...\vee a_{n}$ and $m\geq
M_{0}$. Then $f_{\alpha(m)}=f_{v}$, i.e. $\alpha(m)=_{S(I)}v$ and thus
$\lim_{n\rightarrow\infty}\int\alpha(n)\;d\mu=\int v\;d\mu$. Now, let
$M_{1}\in\mathbb{N}$ s.t. $M_{1}^{-1}<|a_{1}|\wedge...\wedge|a_{n}|$ and
$m\geq M_{1}$. Then

$\displaystyle\int\beta(m)\;d\mu=\frac{n}{m}\sum_{k=1}^{n}\mu(i_{k})\xrightarrow{m\rightarrow\infty}0$

It remains to check (PIS2). So let $v\in S(I)$ with
$v:=(a_{k},i_{k})_{k=1}^{n}$ and $\alpha\in\mathbb{F}(\mathbb{N},S(I))$ s.t.
for all $n\in\mathbb{N}$ we have $f_{\alpha(n)}\geq 0$ and
$\ell:=\sum_{k=1}^{\infty}\int\alpha(k)\;d\mu$ exists and $\ell<\int i\;d\mu$.
Let $M:\mathbb{N}\rightarrow\mathbb{N}$ be the (strictly increasing) modulus
of convergence with which
$\big{(}\sum_{k=1}^{n}\int\alpha(k)\;d\mu\big{)}_{n=1}^{\infty}$ converges to
$\ell\in\mathbb{R}$, i.e. for each $p\in\mathbb{N}$ we have that

$\displaystyle\left\lvert\ell-\sum_{k=1}^{M(p)}\int\alpha(k)\;d\mu\right\rvert=\sum_{k=M(p)+1}^{\infty}\int\alpha(k)\;d\mu\leq\frac{1}{2^{p}}$

Let $i:=\bigvee_{k=1}^{n}i_{k}$ and note that $f_{v}=0$ on
$\lambda_{0}^{0}(i)$. Furthermore take $c>0$ s.t. $f_{v}\leq c$ on
$\lambda_{0}(v)$ and define

  * •

$r:=\int v\;d\mu-\ell$

  * •

$\varepsilon:=\nicefrac{{1}}{{2}}\big{(}1+\mu(i)\big{)}^{-1}r$

  * •

$\alpha:=\nicefrac{{1}}{{c}}\big{(}r-2\varepsilon\mu(i)\big{)}$

Define the strictly increasing sequence $\eta:\mathbb{N}\rightarrow\mathbb{N}$
by $\eta(1):=1$ and for $n\geq 2$ by $\eta(n):=M(2n+1+p)-1$, where
$p\in\mathbb{N}$ is s.t. $2^{-p}<\alpha\varepsilon$. Then for $n\geq 2$ we
have that

$\displaystyle\sum_{k=\eta(n)}^{\eta(n+1)-1}\int\alpha(k)\;d\mu\leq\frac{1}{2^{(2n+1)}}\alpha\varepsilon$

Let $\gamma\in\mathbb{F}(\mathbb{N},S(I))$ be given by
$\gamma(n):=\sum_{k=\eta(n)}^{\eta(n+1)-1}\alpha(k)$ for all $n\in\mathbb{N}$.
Let $q\in\mathbb{N}$ be s.t. $q^{-1}<\varepsilon$ and for $k\geq 2$ let
$j_{k}:=\phi_{2^{k}q}(\gamma(k))$ with $\phi$ as defined in lemma (2.10). It
follows that
$\lambda_{0}^{1}(j_{k})\cup\lambda_{0}^{0}(j_{k})\subseteq\lambda_{0}(\gamma(k))$
and for all $x\in\lambda_{0}^{0}(j_{k})$ we have
$f_{\gamma(k)}(x)<2^{-k}\varepsilon$ and

$\displaystyle\mu(j_{k})\leq\frac{2^{(k+1)}}{\varepsilon}\int\gamma(k)\;d\mu\leq
2^{-k}\alpha$

Furthermore, let $j\in I$ be s.t. for $w:=v-{\gamma(1)}$ we have that
$\lambda_{0}^{1}(j)\cup\lambda_{0}^{0}(j)\subseteq\lambda_{0}(w)$ and for all
$x\in\lambda_{0}^{1}(j)$ we have $f_{w}(x)>\varepsilon$ and

$\displaystyle\mu(j)\geq c^{-1}\bigg{(}\int
w\;d\mu-2\varepsilon\mu(i)\bigg{)}\geq
c^{-1}\big{(}r-2\varepsilon\mu(i)\big{)}=\alpha$

Such a $j$ exists by lemma (2.11), since we have $0\leq f_{\gamma(1)}\leq\ell$
and thus $f_{w}\leq f_{v}<c$ on $\lambda_{0}(w)$ and $f_{w}\leq f_{v}=0$ on
$\lambda_{0}^{0}(i)$. Finally, let $\delta\in\mathbb{F}(\mathbb{N},I)$ be
given by $\delta(n):=\bigwedge_{k=2}^{n}(j-j_{k})$ for $n\geq 2$. We now claim
that $\ell^{\prime}:=\lim_{n\rightarrow\infty}\mu\big{(}\delta(n)\big{)}$
exists and that

$\displaystyle\ell^{\prime}\geq\mu(j)-\sum_{k=2}^{\infty}2^{-k}\alpha\geq\frac{\alpha}{2}>0$

From this claim it follows by (PMS4) that there is an inhabitant

$\displaystyle
x\in\bigcap_{n\in\mathbb{N}}\lambda_{0}^{1}(\delta(n))=\lambda_{0}^{1}(j)\cap\big{(}\bigcap_{n\in\mathbb{N}}\lambda_{0}^{0}(j_{n})\big{)}$

For $k\geq 2$ we get that $f_{\gamma(k)}(x)<2^{-k}\varepsilon$ and thus
$\ell^{\prime\prime}:=\lim_{n\rightarrow\infty}f_{\beta(n)}(x)=\sum_{k=1}^{\infty}f_{\gamma(k)}(x)$
exists and

$\displaystyle
f_{v}(x)-\ell^{\prime\prime}=\underbrace{f_{v}(x)-f_{\gamma(1)}(x)}_{=f_{w}(x)}-\sum_{k=2}^{\infty}f_{\gamma(k)}(x)\geq\varepsilon-\sum_{k=2}^{\infty}2^{-k}\varepsilon=\frac{\varepsilon}{2}>0$

This completes the verification of (PIS2) so it remains to proof the claim.

For $m>n\geq 2$ we have:

$\displaystyle 0$ $\displaystyle\leq\mu(\delta(n))-\mu(\delta(m))\quad\text{by
lemma (\ref{pre-10.5})}$
$\displaystyle\overset{(*)}{\leq}\mu\big{(}\delta(n)-\delta(m)\big{)}$
$\displaystyle=\mu\big{(}(j-\bigvee_{k=2}^{n}j_{k})-(j-\bigvee_{k=2}^{m}j_{k})\big{)}$
$\displaystyle\overset{(**)}{\leq}\mu\big{(}\bigvee_{k=2}^{m}j_{k}-\bigvee_{k=2}^{n}j_{k}\big{)}$
$\displaystyle\overset{(***)}{\leq}\mu\big{(}\bigvee_{k=n+1}^{m}j_{k}\big{)}\leq\sum_{k=n+1}^{m}\mu(j_{k})\leq\sum_{k=n+1}^{m}2^{-k}\alpha$

It follows that the sequence $\big{(}\mu(\delta(n))\big{)}_{n\in\mathbb{N}}$
is a Cauchy-sequence and hence its limit exist. Furthermore, we get

$\displaystyle\lim_{n\rightarrow\infty}\mu(\delta(n))$
$\displaystyle=\lim_{n\rightarrow\infty}\mu\big{(}j-\bigvee_{k=2}^{n}j_{k}\big{)}$
$\displaystyle\overset{(*)}{\geq}\mu(j)-\lim_{n\rightarrow\infty}\mu(\bigvee_{k=2}^{n}j_{k})$
$\displaystyle\geq\mu(j)-\sum_{k=2}^{\infty}2^{-k}\alpha\geq\frac{\alpha}{2}>0$

Note that we used the following inequalities: Let $A,B,C\in I$, we have

$\displaystyle(*)\quad\mu(A-B)\overset{{\text{(PMS2)}}}{=}\mu(A)-\mu(A\wedge
B)\overset{{\text{lemma (\ref{pre-10.5})}}}{\geq}\mu(A)-\mu(B)$
$\displaystyle(**)\quad\mu((A-B)-(A-C))$ $\displaystyle=\mu((A-B)\wedge(-A\vee
C))$ $\displaystyle=\mu\big{(}((A-B)-A)\vee(A\wedge(C-B))\big{)}$
$\displaystyle\leq\underbrace{\mu((A-A)-B)}_{{\leq\mu(A-A)=0\text{ by lemma
(\ref{pre-10.2})}}}+\quad\mu(A\wedge(C-B)\leq\mu(C-B)$
$\displaystyle(***)\quad\mu(A\vee
B-B)=\mu((A-B)\vee(B-B))\leq\mu(A-B)+\mu(B-B)\leq\mu(A)$

∎

This finishes the section on the simple functions. Note that most arguments
have been directly translated from section 10 of chapter 6 of [BB85] to our
setting of pre-measure and pre-integration spaces. However, we were able to
make certain things more precise, like the formulation and proof of lemma
(2.10) and the proof of theorem (2.12) and thus avoided using the axiom of
countable choice.

###  3 Complete extension of a pre-integration space

Recall that we haven’t addressed the most serious problems of BCMT from a
predicative perspective. The construction of the complete extension of an
integration space relies on the assumption that the totality of integrable
functions forms a set, which is not acceptable from a predicative viewpoint.
For the remainder of this paper we want to propose a solution to this problem.
As we will see it suffices to consider the totality of canonically integrable
functions, which does form a set, in order to construct the complete
extension.

####  1 The 1-norm of a pre-integration space

Before we can give a predicative account of the complete extension of a pre-
integration space, we have to make precise in what way this extended pre-
integration space is the completion of the first one. In this section we will
show how we can define a norm on the index set of the set of partial functions
of a pre-integration space. We start by proving some basic results about pre-
integration spaces (see [BB85, pp. 217-218]) that will be useful later.

######  Lemma 3.1.

Let $i\in I$ and $\alpha\in\mathbb{F}(\mathbb{N},I)$ be such that for all
$n\in\mathbb{N}$ we have $f_{\alpha(n)}\geq 0$ and $\sum_{n}\int\alpha(n)$
extists and $\int i+\sum_{n}\int\alpha(n)>0$. Then there exists
$x\in\lambda_{0}(i)\cap\bigcap_{n}\lambda(\alpha(n))$ such that
$\sum_{n}f_{\alpha(n)}(x)$ exists and $f_{i}(x)+\sum_{n}f_{\alpha(n)}(x)>0$.

###### Proof.

Let $N\in\mathbb{N}$ be s.t.
$\sum_{n=N+1}^{\infty}\int\alpha(n)<\frac{1}{2}\big{(}\int
i+\sum_{n}\int\alpha(n)\big{)}$, then using induction, we get that

$\displaystyle\sum_{n=N+1}^{\infty}\int\alpha(n)<\int
i+\sum_{n=1}^{N}\int\alpha(n)=\int\bigg{(}i+\sum_{n=1}^{N}\alpha(n)\bigg{)}$

From (PIS2) it follows that there is a
$x\in\lambda_{0}(i)\cap\bigcap_{n}\lambda(\alpha(n))$ such that
$\sum_{n=N+1}^{\infty}f_{\alpha(n)}(x)$ exists and
$f_{i}(x)+\sum_{n=1}^{N}f_{\alpha(n)}(x)>\sum_{n=N+1}^{\infty}f_{\alpha(n)}(x)$.
Now the result follows since for all $n\in\mathbb{N}$ we have that
$f_{\alpha(n)}\geq 0$. ∎

######  Lemma 3.2.

$\forall i\in I:\;f_{i}\geq 0\;\Rightarrow\;\int i\geq 0$

###### Proof.

Let $i\in I$ and assume that $f_{i}\geq 0$ but $\int i<0$. Consider the
sequence $(0\cdot i,0\cdot i,...)$ then $f_{0\cdot
i}=_{{\mathcal{F}(X)}}0f_{i}=0$ and $\sum_{n}\int 0\cdot i=0$ and
$\int(-i)+\sum_{n}\int 0\cdot i>0$. Hence, by lemma (3.1) there is an
$x\in\lambda_{0}(i)$ s.t. $-f_{i}(x)+\sum_{n}0f_{i}(x)=-f_{i}(x)>0$ which is a
contradiction. ∎

######  Lemma 3.3.

$\forall i\in I:\;\left\lvert\int i\right\rvert\leq\int\lvert i\rvert$

###### Proof.

The result is immediatelly obtained by applying lemma (3.2) to $\lvert
i\rvert-i$ and $\lvert i\rvert+i$ respectively. ∎

######  Lemma 3.4.

Let $i,j\in I$ be s.t. for all $x\in\lambda_{0}(i)\cap\lambda_{0}(j)$ we have
$f_{i}(x)\leq f_{j}(x)$, then $\int i\leq\int j$

###### Proof.

Consider $j-i\in I$, then
$\lambda_{0}(j-i)=_{{\mathcal{P}(X)}}\lambda_{0}(i)\cap\lambda_{0}(j)$ and
thus $f_{j-i}\geq 0$. Hence, by lemma (3.2)

$\displaystyle\int j-\int i=\int(j-i)\geq 0$

∎

In classical measure theory one often identifies integrable functions that
agree almost everywhere and the normed space $L^{1}$ is then defined modulo
this equivalence relation. The positive, constructive counterpart is to
identify functions in the complete extension of an integration space that
agree on a full set. Proposition 2.12 in [BB85, p. 227] then tells us that we
can define the 1-norm modulo this equality. Since, we don’t have recourse to
the notion of a full set in a predicative setting, we have to introduce the
1-norm a bit differently.

######  Theorem 3.5.

The relation $=_{\int}$, defined for $i,j\in I$ by

$\displaystyle i=_{\int}j\;:\Leftrightarrow\;\int\lvert i-j\rvert=0$

is an equivalence relation on $I$ and the assignment routine
$\int:(I,=_{\int})\rightsquigarrow\mathbb{R}$ given by $i\mapsto\int i$ is a
function. Moreover, the functions $\cdot$ and $+$ make $(I,=_{\int})$ into a
$\mathbb{R}$-vector space with neutral element $0\cdot p$, where $p\in I$ is
s.t. $\int p=1$, which exists by (PMS3). The function

$\displaystyle\lVert\\_\rVert_{1}:\;I$
$\displaystyle\rightarrow\mathbb{R}_{\geq 0}$ $\displaystyle\lVert
i\rVert_{1}$ $\displaystyle:=\int\lvert i\rvert$

Defines a norm on $(I,=_{\int};\;\cdot,+,0\cdot p)$.

###### Proof.

First, we have to check that $=_{\int}$ defines an equivalence relation on
$I$. Reflexivity follows by (3.2) and from the fact that $f_{\lvert
i-i\rvert}=\lvert f_{i}-f_{i}\rvert=0$ for all $i\in I$. For $i,j\in I$ we
have $\lvert f_{i}-f_{j}\rvert=_{{\mathcal{F}(X)}}\lvert f_{j}-f_{i}\rvert$
and thus $\lvert i-j\rvert=_{I}\lvert j-i\rvert$, since $\bm{\Lambda}$ is an
$I$-set of partial functions. This establishes the symmetry of $=_{\int}$. For
transitivity let $i,j,k\in I$ s.t $i=_{\int}j$ and $j=_{\int}k$. For any
$x\in\lambda_{0}(i)\cap\lambda_{0}(j)\cap\lambda_{0}(k)$ we have that

$\displaystyle f_{\lvert i-j\rvert}(x)=\lvert
f_{i}(x)-f_{k}(x)+f_{k}(x)-f_{j}(x)\rvert\leq f_{\lvert
i-k\rvert}(x)+f_{\lvert j-k\rvert}(x)$

and thus by lemma (3.4)

$\displaystyle 0\leq\int\lvert i-j\rvert=\int\lvert
i-k+k-j\rvert\leq\int\lvert i-k\rvert+\int\lvert k-j\rvert=0$

which means that $i=_{\int}j$. For $i=_{\int}j$, we have $0\leq\left\lvert\int
i-\int j\right\rvert\leq\int\lvert i-j\rvert=0$ by lemma (3.3), and hence
$\int i=\int j$ which proves that
$\int:(I,=_{\int})\rightsquigarrow\mathbb{R}$ is a function.

It follows directly from (PIS1) that $+,\cdot$ satisfy the associativity,
commutativity and distributivity laws of a vector-space on the set
$(I,=_{I})$. Since for all $i,j\in I$ if $i=_{I}j$ then $\int i={\int}j$ by
lemma (3.2), it follows that these laws also hold for $(I,=_{\int})$. It
remains to check that $0\cdot p$ is indeed a neutral element that and additive
inverses exist. But this follows from $i+0\cdot p=_{\int}i$ and
$i-i=_{\int}0\cdot p$ for all $i\in I$, which we get using lemma (3.2).

It remains to check that $\lVert\\_\rVert_{1}$ defines a norm $(I,=_{\int})$.
Let $i\in I$, we have to show that

$\displaystyle\lVert i\rVert_{1}=0\;\Leftrightarrow\;i=_{\int}0\cdot p$

Using the fact that $\bm{\Lambda}$ is an $I$-set of functions, we get that
$\lvert i-0\cdot p\rvert=_{I}\lvert i\rvert-0\cdot p$, which by lemma (3.4)
and (PIS1) gives us the desired result. The other norm axioms can be obtained
similarly. ∎

####  2 The pre-integration space of canonically integrable functions

In our predicative setting we don’t have that the totality of integrable
functions forms a set. However, in Bishop-Cheng measure theory two integrable
functions are identified if they agree on a full set. Each integrable function
$f$ has a representation $(f_{n})_{n}$ and agrees with the _canonically
integrable function_ 333This terminology is due to Bas Spitters, see [Spi02,
p. 24]. $\sum_{n}f_{n}$ on a full set, namely the domain of the canonically
integrable function. To construct the complete extension as the metric
completion w.r.t. the 1-norm it thus suffices to only consider the canonically
integrable functions. In this section we will show that we can actually
construct the set of canonically integrable functions and construct the
corresponding pre-integration space that will be the complete extension.

######  Definition 3.6.

Let $(X,I,L,\int)$ be an pre-integration space. We define the set of
_representations_ to be the totality

$\displaystyle
I_{1}:=\bigg{\\{}\;\alpha\in\mathbb{F}(\mathbb{N},I)\;:\;\sum_{n=1}^{\infty}\int\lvert\alpha(n)\rvert\text{
exists}\;\bigg{\\}}$

together with the equality

$\displaystyle\alpha=_{I_{1}}\beta\;:\Leftrightarrow\;\Big{(}F_{\alpha},e_{F_{\alpha}},\sum_{n}f_{\alpha(n)}\Big{)}=_{{\mathcal{F}(X)}}\Big{(}F_{\beta},e_{F_{\beta}},\sum_{n}f_{\beta(n)}\Big{)}$

where for $\alpha,\beta\in I_{1}$

$\displaystyle
F_{\alpha}:=\bigg{\\{}\;x\in\bigcap_{n}\lambda_{0}\big{(}\alpha(n)\big{)}\;:\;\sum_{n}\lvert
f_{\alpha(n)}(x)\rvert\text{ exists}\;\bigg{\\}}$

with embedding $e_{F_{\alpha}}:F_{\alpha}\hookrightarrow X$ induced by the
embeddings $\varepsilon_{\alpha(n)}$ and $(F_{\beta},e_{F_{\beta}})$ is
defined accordingly. We define the set of _canonically integrable functions_
to be the $I_{1}$-family of partial functions
$\bm{\Lambda}_{1}=(\nu_{0},\nu_{1},E,G)$ given by

  * •

$\nu_{0}:I_{1}\rightsquigarrow\mathbb{V}_{0}$ is the assignment routine given
by $\nu_{0}(\alpha):=F_{\alpha}$.

  * •

$E:\bigcurlywedge_{\alpha\in I_{1}}\mathbb{F}(\nu_{0}(\alpha),X)$ is the
dependent assignment routine that maps each $\alpha\in I_{1}$ to the embedding
$e_{\alpha}:=e_{F_{\alpha}}$.

  * •

$\nu_{1}:\bigcurlywedge_{(\alpha,\beta)\in
D(I_{1})}\mathbb{F}(\nu_{0}(\alpha),\nu_{0}(\beta))$ is the dependent
assignment routine that maps each $(\alpha,\beta)\in D(I_{1})$ to the function
$\nu_{\alpha\beta}:\nu_{0}(\alpha)\rightarrow\nu_{0}(\beta)$ s.t.
$\nu_{\alpha\alpha}:=\text{id}_{\nu_{0}(\alpha)}$ and
$(\nu_{\alpha\beta},\nu_{\beta\alpha})$ witnesses the equality
$\alpha=_{I_{1}}\beta$.444Here we use the fact that two functions witnessing
an equality of subsets are equal.

  * •

$G:\bigcurlywedge_{\alpha\in I_{1}}\mathbb{F}(\nu_{0}(\alpha),\mathbb{R})$ is
the dependent assignment routine that maps each $\alpha\in I_{1}$ to the
function $g_{\alpha}:\nu_{0}(\alpha)\rightarrow\mathbb{R}$ that is given by
$g_{\alpha}(x):=\sum_{n=1}^{\infty}g_{\alpha(n)}(x)$ for each
$x\in\nu_{0}(\alpha)$.

######  Remark 3.7.

It follows directly from the definition of $=_{I_{1}}$ that $\bm{\Lambda}_{1}$
is an $I_{1}$-set of partial functions. Furthermore the assignment routine

$\displaystyle h:I$ $\displaystyle\rightsquigarrow I_{1}$ $\displaystyle i$
$\displaystyle\mapsto\big{(}i,0\cdot i,0\cdot i,...\big{)}$

defines an embedding since for $i,j\in I$ we have

$\displaystyle i=_{I}j\;$
$\displaystyle\Leftrightarrow\;f_{i}=_{{\mathcal{F}(X)}}f_{j}$
$\displaystyle\Leftrightarrow\bigg{(}\lambda_{0}(i),\varepsilon_{i},f_{i}+\sum_{n=2}^{\infty}0\cdot
f_{i}\bigg{)}=_{{\mathcal{F}(X)}}\bigg{(}\lambda_{0}(j),\varepsilon_{j},f_{j}+\sum_{n=2}^{\infty}0\cdot
f_{j}\bigg{)}$ $\displaystyle\Leftrightarrow h(i)=_{I_{1}}h(j)$

since one can easily verify that
$\lambda_{0}(i)=_{{\mathcal{P}(X)}}\nu_{0}(h(i))$ and
$\lambda_{0}(j)=_{{\mathcal{P}(X)}}\nu_{0}(h(j))$.

Let $\alpha,\beta\in I_{1}$ and $a\in\mathbb{R}$. We can define the following
functions

$\displaystyle\\_+_{1}\\_:I_{1}\times I_{1}\rightarrow I_{1}$
$\displaystyle\;\;\alpha+_{1}\beta:={{\big{(}\;\alpha(1),\;\beta(1),\;\alpha(2),\;\beta(2),...\big{)}}},$
$\displaystyle\\_\cdot_{1}\\_:\mathbb{R}\times I_{1}\rightarrow I_{1}$
$\displaystyle\;\;a\cdot_{1}\alpha:={{\big{(}\;a\cdot\alpha(1),\;a\cdot\alpha(2),...\big{)}}},$
$\displaystyle\lvert\\_\rvert_{1}:I_{1}\rightarrow I_{1}$
$\displaystyle\;\;\lvert\alpha\rvert_{1}:={{\big{(}\;\lvert\alpha(1)\rvert,\;\alpha(1),\;(-1)\cdot\alpha(1),\;\lvert\alpha(1)+\alpha(2)\rvert-\lvert\alpha(1)\rvert,\;\alpha(2),\;(-1)\cdot\alpha(2),\;\lvert\alpha(1)+\alpha(2)+\alpha(3)\rvert-\lvert\alpha(1)+\alpha(2)\rvert,...\big{)}}},$
$\displaystyle\wedge_{1}^{1}:I_{1}\rightarrow I_{1}$
$\displaystyle\;\;\wedge_{1}^{1}(\alpha):={{\big{(}\;1\wedge\alpha(1),\;\alpha(1),\;(-1)\cdot\alpha(1),\;1\wedge(\alpha(1)+\alpha(2))-1\wedge(\alpha(1)),\;\alpha(2),\;(-1)\cdot\alpha(2),\;1\wedge(\alpha(1)+\alpha(2)+\alpha(3))-1\wedge(\alpha(1)+\alpha(2)),...\big{)}}}$

See [BB85, p. 224] to check that

  * •

$g_{\alpha+_{1}\beta}=_{{\mathcal{F}(X)}}g_{\alpha}+g_{\beta}$

  * •

$g_{a\cdot_{1}\alpha}=_{{\mathcal{F}(X)}}ag_{\alpha}$

  * •

$g_{\lvert\alpha\rvert_{1}}=_{{\mathcal{F}(X)}}\lvert g_{\alpha}\rvert$

  * •

$g_{\wedge_{1}^{1}(\alpha)}=_{{\mathcal{F}(X)}}g_{\alpha}\wedge 1$

Note that for construction of these sequences no choice principles were
needed. Furthermore we get that these maps are compatible with
$h:I\hookrightarrow I_{1}$, i.e. for $i,j\in I$ and $a\in\mathbb{R}$ we have
that

  * •

$h(i+j)=_{I_{1}}h(i)+_{1}h(j)$

  * •

$h(a\cdot i)=_{I_{1}}a\cdot_{1}h(i)$

  * •

$h(\lvert i\rvert)=_{I_{1}}\lvert h(i)\rvert_{1}$

  * •

$h(\wedge_{1}(i))=_{I_{1}}\wedge_{1}^{1}(h(i))$

In the following we will thus drop the subscript $1$ for all of these
functions.

Finally the assignment routine $\int_{1}:I_{1}\rightsquigarrow\mathbb{R}$
given by $\int_{1}\alpha:=\sum_{n}\int\alpha(n)$ is a function. To see this
let $\alpha=_{I_{1}}\beta$ and assume that
$\int_{1}\alpha\neq_{\mathbb{R}}\int_{1}\beta$. Take $a\in\mathbb{R}$ and
$N\in\mathbb{N}$ s.t.

  * •

$0<3a<\left\lvert\sum_{n}\int\alpha(n)-\sum_{n}\int\beta(n)\right\rvert$

  * •

$\sum_{n=N+1}^{\infty}\int\lvert\alpha(n)\rvert<a$

  * •

$\sum_{n=N+1}^{\infty}\int\lvert\alpha(n)-\beta(n)\rvert<a$

Then

$\displaystyle\sum_{n=N+1}^{\infty}\int\lvert\alpha(n)\rvert$
$\displaystyle\;+\sum_{n=N+1}^{\infty}\int\lvert\alpha(n)-\beta(n)\rvert<2a$
$\displaystyle<\left\lvert\sum_{n=1}^{\infty}\int\alpha(n)-\sum_{n=1}^{\infty}\int\beta(n)\right\rvert-a$
$\displaystyle<\left\lvert\sum_{n=1}^{N}\int\big{(}\alpha(n)-\beta(n)\big{)}\right\rvert\;+\sum_{n=N+1}^{\infty}\int\lvert\alpha(n)-\beta(n)\rvert-a$
$\displaystyle<\left\lvert\sum_{n=1}^{N}\int\big{(}\alpha(n)-\beta(n)\big{)}\right\rvert\leq\int\left\lvert\sum_{n=1}^{N}\big{(}\alpha(n)-\beta(n)\big{)}\right\rvert$

Thus by (PIS2) for the pre-integration space $(X,I,\bm{\Lambda},\int)$ there
is a
$x\in\big{(}\bigcap_{n}\lambda_{0}(\alpha(n))\big{)}\cap\big{(}\bigcap_{n}\lambda_{0}(\beta(n))\big{)}$
s.t. $\sum_{n}\lvert f_{\alpha(n)}(x)\rvert$ and $\sum_{n}\lvert
f_{\alpha(n)}(x)-f_{\beta(n)}(x)\rvert$ both exist and we have

$\displaystyle\sum_{n=N+1}^{\infty}\lvert
f_{\alpha(n)}(x)\rvert\;+\sum_{n=N+1}^{\infty}\lvert
f_{\alpha(n)}(x)-f_{\beta(n)}(x)\rvert<\left\lvert\sum_{n=1}^{N}\big{(}f_{\alpha(n)}(x)-f_{\beta(n)}(x)\big{)}\right\rvert$

Hence, $\sum_{n}\lvert f_{\beta(n)}(x)\rvert$ exists and thus

$\displaystyle 0\leq\sum_{n=N+1}^{\infty}\lvert f_{\alpha(n)}(x)\rvert$
$\displaystyle<\left\lvert\sum_{n=1}^{N}\big{(}f_{\alpha(n)}(x)-f_{\beta(n)}(x)\big{)}\right\rvert\;-\sum_{n=N+1}^{\infty}\lvert
f_{\alpha(n)}(x)-f_{\beta(n)}(x)\rvert$
$\displaystyle\leq\left\lvert\sum_{n=1}^{\infty}\big{(}f_{\alpha(n)}(x)-f_{\beta(n)}(x)\big{)}\right\rvert$

But this is a contradiction since $\alpha=_{I_{1}}\beta$ implies that
$\sum_{n}f_{\alpha(n)}(x)=_{\mathbb{R}}\sum_{n}f_{\beta(n)}(x)$. It is also
clear that $\int_{1}h(i)=\int i$ for all $i\in I$. We will thus drop the
subscript $1$ here as well.

We now prove some basic properties of $I_{1}$ and $\bm{\Lambda}_{1}$. Again,
all of the arguments are taken from section 2 of chapter 6 of [BB85].

######  Lemma 3.8.

$\forall\alpha\in
I_{1}:\;\left\lvert\int\alpha\right\rvert\leq\int\lvert\alpha\rvert$

###### Proof.

From the definition we get that

$\displaystyle\int\lvert\alpha\rvert=\lim_{n\rightarrow\infty}\int\left\lvert\sum_{k=1}^{n}\alpha(k)\right\rvert$

Now assume that $\left\lvert\int\alpha\right\rvert>\int\lvert\alpha\rvert$,
then there is $n$ large enough s.t.

$\displaystyle\int\left\lvert\sum_{k=1}^{n}\alpha(k)\right\rvert<\left\lvert\sum_{k=1}^{n}\int\alpha(k)\right\rvert=\left\lvert\int\sum_{k=1}^{n}\alpha(k)\right\rvert$

This is a contradiction to lemma (3.3). ∎

######  Lemma 3.9.

Let $\alpha\in I_{1}$ be s.t. for all $x\in\nu_{0}(\alpha)$ we have
$g_{\alpha}(x)\geq 0$, then $\int\alpha\geq 0$.

###### Proof.

For $i\in I$ define

$\displaystyle i^{+}$ $\displaystyle:=\frac{1}{2}\cdot\lvert
i\rvert+\frac{1}{2}\cdot i$ $\displaystyle i^{-}$
$\displaystyle:=\frac{1}{2}\cdot\lvert i\rvert-\frac{1}{2}\cdot i$

Then $f_{i^{+}}=_{{\mathcal{F}(X)}}f_{i}^{+}$ and
$f_{i^{-}}=_{{\mathcal{F}(X)}}f_{i}^{-}$. Let $\alpha\in I_{1}$, then by
assumption we have that $\sum_{n}\int\alpha(n)^{+}$ and
$\sum_{n}\int\alpha(n)^{-}$ exist and that

$\displaystyle\int\alpha:=\sum_{n=1}^{\infty}\int{\alpha(n)}=\sum_{n=1}^{\infty}\int{\alpha(n)}^{+}-\sum_{n=1}^{\infty}\int{\alpha(n)}^{-}$

Furthermore, we have for $x\in\nu_{0}(\alpha)$ that
$\sum_{n}|f_{\alpha(n)}(x)|$ exists if and only if
$\sum_{n}f_{\alpha(n)}^{+}(x)$ and $\sum_{n}f_{\alpha(n)}^{-}(x)$ exist, in
which case

$\displaystyle\sum_{n=1}^{\infty}f_{\alpha(n)}^{+}(x)-\sum_{n=1}^{\infty}f_{\alpha(n)}^{-}(x)=g_{\alpha}(x)\geq
0$

Now, suppose that $\int\alpha<0$ and take $\varepsilon>0$ s.t.
$\sum_{n}\int{\alpha(n)}^{+}<\sum_{n}\int{\alpha(n)}^{-}-2\varepsilon$. Also
take $N\in\mathbb{N}$ large enough s.t.
$\sum_{n=N+1}^{\infty}\int{\alpha(n)}^{-}<\varepsilon$. We have that

$\displaystyle\sum_{n=1}^{\infty}\int{\alpha(n)}^{+}+\sum_{n=N+1}^{\infty}\int\alpha(n)^{-}<\sum_{n=1}^{N}\int{\alpha(n)}^{-}+2\sum_{n=N+1}^{\infty}\int{\alpha(n)}^{-}-2\varepsilon<\sum_{n=1}^{N}\int{\alpha(n)}^{-}$

Hence, by (PIS2) there is a $x\in\bigcap_{n}(\lambda_{0}(\alpha(n))$ s.t.
$\sum_{n}f_{\alpha(n)}^{+}(x)$ and $\sum_{n}f_{\alpha(n)}^{-}(x)$ exist , and
thus also $\sum_{n}|f_{\alpha(n)}(x)|$ converges, i.e. $x\in\nu_{0}(\alpha)$,
and we have

$\displaystyle\sum_{n=1}^{\infty}f_{\alpha(n)}^{+}(x)<\sum_{n=1}^{N}f_{\alpha(n)}^{-}(x)\leq\sum_{n=1}^{\infty}f_{\alpha(n)}^{-}(x)$

it follows that $g_{\alpha}(x)=\sum_{n}f_{\alpha(n)}(x)<0$, which is a
contradiction and thus $\int\alpha\geqslant 0$. ∎

######  Lemma 3.10.

Let $\alpha,\beta\in I_{1}$ be s.t. for all
$x\in\nu_{0}(\alpha)\cap\nu_{0}(\beta)$ we have that $g_{\alpha}(x)\leq
g_{\beta}(x)$, then $\int\alpha\leq\int\beta$.

###### Proof.

Consider $\beta-\alpha\in I_{1}$, then
$\nu_{0}(\beta-\alpha)=_{{\mathcal{P}(X)}}\nu_{0}(\alpha)\cap\nu_{0}(\beta)$
and thus $g_{\beta-\alpha}\geq 0$. Hence, by lemma (3.9)

$\displaystyle\int\beta-\int\alpha=\int(\beta-\alpha)\geq 0$

∎

######  Lemma 3.11.

There is a function $\phi:I_{1}\rightarrow\mathbb{N}\rightarrow I_{1}$ s.t.
for every $\alpha\in I_{1}$ and $n\in\mathbb{N}$ we have that
$\phi(\alpha,n):=\beta=_{I_{1}}\alpha$ and
$\sum_{k}\int\lvert\beta(k)\rvert\leq\int\lvert\alpha\rvert+2^{-n}$.

###### Proof.

Let $\alpha\in I_{1}$ and $n\in\mathbb{N}$. Let
$M:\mathbb{N}\rightarrow\mathbb{N}$ be the modulus of converengence of the
sequence
$\big{(}\sum_{k=1}^{m}\int\lvert\alpha(k)\rvert\big{)}_{m=1}^{\infty}$ and
$N:=M(n+1)$, i.e. we have $\sum_{k=N+1}^{\infty}\int\lvert\alpha(k)\rvert\leq
2^{-(n+1)}$. Let $\beta\in\mathbb{F}(\mathbb{N},I)$ be given by

$\displaystyle\Big{(}\sum_{k=1}^{N}{\alpha(k)},\alpha(N+1),\alpha(N+2),...\Big{)}$

Then $\sum_{k}\int\lvert\beta(k)\rvert\leq\sum_{k}\int\lvert\alpha(k)\rvert$
and thus $\beta\in I_{1}$, i.e. $\phi(\alpha,n):=\beta$ is well-defined.
Furthermore, we clearly have
$\nu_{0}(\beta)=_{{\mathcal{P}(X)}}\nu_{0}(\alpha)$ and
$g_{\beta}=_{{\mathcal{F}(X)}}g_{\alpha}$.

For $m>N$ we obtain, by using lemma (3.10), that

$\displaystyle\sum_{k=1}^{\infty}\int\lvert\beta(k)\rvert$
$\displaystyle\leq\int\lvert\beta(1)\rvert+\frac{1}{2^{n+1}}$
$\displaystyle\leq\int\Bigg{(}\left\lvert\sum_{k=1}^{m}\alpha(k)\right\rvert\Bigg{)}+\int\Bigg{(}\left\lvert\sum_{k=1}^{N}\alpha(k)\right\rvert-\left\lvert\sum_{k=1}^{m}{\alpha(k)}\right\rvert\Bigg{)}+\frac{1}{2^{n+1}}$
$\displaystyle\leq\int\Bigg{(}\left\lvert\sum_{k=1}^{m}{\alpha(k)}\right\rvert\Bigg{)}+\int\Bigg{(}\left\lvert\sum_{k=N+1}^{m}{\alpha(k)}\right\rvert\Bigg{)}+\frac{1}{2^{n+1}}$
$\displaystyle\leq\int\Bigg{(}\left\lvert\sum_{k=1}^{m}{\alpha(k)}\right\rvert\Bigg{)}+\sum_{k=N+1}^{m}\int\lvert{\alpha(k)}\rvert+\frac{1}{2^{n+1}}$
$\displaystyle<\int\Bigg{(}\left\lvert\sum_{k=1}^{m}{\alpha(k)}\right\rvert\Bigg{)}+2^{-n}$

By the proof of lemma (3.8) we have that

$\displaystyle\lim_{m\rightarrow\infty}\int\Bigg{(}\left\lvert\sum_{k=1}^{m}{\alpha(k)}\right\rvert\Bigg{)}=\int\lvert\alpha\rvert$

which finishes the proof. ∎

We are now able to prove the predicative, constructive version of Lebesgue’s
series theorem. The proof generally follows the proof theorem 2.15 in [BB85],
but we have to be a bit more cautious, since we don’t have a notion of a full
set at hand and thus have to work around arguments that rely on properties of
full sets. Again, using lemma (3.11) instead of a more straightforward
translation of 2.14 in [BB85] allows us to avoid countable choice.

######  Theorem 3.12.

Let $\Gamma\in\mathbb{F}(\mathbb{N},I_{1})$ be s.t.
$\sum_{n}\int\lvert\Gamma(n)\rvert$ exists. Then there is an $\alpha\in I_{1}$
s.t.

$\displaystyle\nu_{0}(\alpha)\subseteq\bigg{\\{}\;x\in\bigcap_{n=1}^{\infty}\nu_{0}\big{(}\Gamma(n)\big{)}\;:\;\sum_{n=1}^{\infty}\lvert
g_{\;\Gamma(n)}(x)\rvert\text{ exists}\;\bigg{\\}}$
$\displaystyle\text{and}\quad\forall
x\in\nu_{0}(\alpha):\;g_{\alpha}(x)=\sum_{n=1}^{\infty}g_{\;\Gamma(n)}(x)$

Furthermore, for any $\alpha\in I_{1}$ fulfilling the above condition we have

$\displaystyle\lim_{N\rightarrow\infty}\int\lvert\alpha-\sum_{n=1}^{N}\Gamma(n)\rvert=0$

###### Proof.

Let
$A:=\\{x\in\bigcap_{n=1}^{\infty}\nu_{0}\big{(}\Gamma(n)\big{)}:\sum_{n=1}^{\infty}\lvert
g_{\;\Gamma(n)}(x)\rvert\text{ exists}\\}$ and $i_{A}:A\hookrightarrow X$ be
the embedding induced by the $e_{\Gamma(n)}$. Let

$\displaystyle g_{A}:A$ $\displaystyle\rightarrow\mathbb{R}$ $\displaystyle x$