Proof of Kit for def:measure-measure-space

Throughout, formulas are written with abbreviations as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (vi), a formula being predicative when it is so with its abbreviations eliminated, and the given $x_{0},\dots,x_{n-1}$ are the first of distinct set variables $x_{0},x_{1},\dots$ as in Renaming and Substituting Variables in Predicative Formulas, so that $x_{0},\dots,x_{6}$ are distinct also when $n<7$. The parameters of the statement, the class variables $E$, $L$, $Z$, $P$, $\mathbb{N}$, $R$, $Q$ and the set variables $\infty$, $0$, $1$, are other than $x_{0},x_{1},\dots$ and the bound variables below, and are at their fixed values as in Conditions Expressed by a Predicative Formula, and Guards (i). The letters $m$ and $l$ denote further set variables, distinct from each other, from $x_{0},x_{1},\dots$ and from the parameters. Routine facts about sets and maps are used without comment (Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (i), Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (iii)), and so is the agreement of the earlier version of sequences, on which Sums of Sequences in [0,∞] as Typed Terms and as a Map and Sequences: Enlarging the Codomain, Extensionality and the Range are stated, with the current one (The Earlier and the New Versions of the Definitions of Sequences, Limits, Cauchy Sequences, Series and Iterated Operations Agree (i)).

The formula for sums in $[0,\infty]$. Let $\gamma$ be the formula $x_{0}\in Z^{\mathbb{N}}\wedge x_{1}\in Z$, where $Z^{\mathbb{N}}$ is the class term of functions from $\mathbb{N}$ to $[0,\infty]$; it is predicative with free variables among $x_{0}$, $x_{1}$, $Z$ and $\mathbb{N}$, so it is a guard, with $x_{0},x_{1}$ in place of the variables of Conditions Expressed by a Predicative Formula, and Guards (i). By Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (i), $x_{0}$ is a term of type $[0,\infty]^{\mathbb{N}}$ under $\gamma$ and $x_{1}$ a term of type $[0,\infty]$ under $\gamma$. By Sums of Sequences in [0,∞] as Typed Terms and as a Map (i), applied to the term $x_{0}$, with the class variables $E$, $L$, $Z$, $P$, $\mathbb{N}$, $R$ and $Q$ of the statement as its $E$, $L$, $Z$, $P$, $N$, $R$ and $Q$, the expression $\sum_{s\in\mathbb{N}}(x_{0})_{s}$ is a term of type $[0,\infty]$ under $\gamma$ whose value, under an assignment satisfying $\gamma$, is the sum of the sequence assigned to $x_{0}$. By Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (v), the condition $\gamma\wedge x_{1}=\sum_{s\in\mathbb{N}}(x_{0})_{s}$ is expressed by a predicative formula $\psi$. As the elements of $[0,\infty]^{\mathbb{N}}$ are exactly the sequences in $[0,\infty]$ (The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i)), $\psi$ is a predicative formula in $x_{0},x_{1}$, in the sense of Renaming and Substituting Variables in Predicative Formulas, that holds for sets $c$ and $r$ assigned to $x_{0}$ and $x_{1}$ if and only if $c$ is a sequence in $[0,\infty]$, $r\in[0,\infty]$ and

$$r=\sum_{s\in\mathbb{N}}c_{s}.$$

The formula for pairwise disjoint sequences. Write $\mathcal{F}$ and $a$ for $x_{0}$ and $x_{1}$, and let

$$\delta=a\in\mathcal{F}^{\mathbb{N}}\wedge\forall m\,\forall l\,\bigl(m\in\mathbb{N}\wedge l\in\mathbb{N}\wedge\neg\,m=l\Rightarrow a(m)\cap a(l)=\emptyset\bigr).$$

Here $\mathcal{F}^{\mathbb{N}}$ is the class term of functions from $\mathbb{N}$ to $\mathcal{F}$ and $a(m)\cap a(l)$ that of the intersection, both given by class abstraction with predicative formulas, and the values $a(m)$, $a(l)$ and the empty set $\emptyset$ are defined set symbols. The empty set exists, and $a(m)$ and $a(l)$ occur only under the hypotheses $a\in\mathcal{F}^{\mathbb{N}}$, which makes $a$ a function with domain $\mathbb{N}$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), and $m,l\in\mathbb{N}$; so each defined set symbol is used as Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (viii) permits. Every quantifier of $\delta$ is over a set variable, so $\delta$ is predicative (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v)), with free variables among $x_{0}$, $x_{1}$ and $\mathbb{N}$. For sets $\mathcal{F}$ and $a$ assigned to $x_{0}$ and $x_{1}$, the first conjunct holds exactly when $a$ is a map $\mathbb{N}\to\mathcal{F}$ (The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i)), that is, a sequence in $\mathcal{F}$, and the second exactly when $a(m)\cap a(l)=\emptyset$ for all distinct $m,l\in\mathbb{N}$. So $\delta$ is a predicative formula in $x_{0},x_{1}$ expressing the condition of (i) with $\mathcal{F}=x_{0}$ and $a=x_{1}$. Below, a sequence $a$ in a set $\mathcal{F}$ with $a(m)\cap a(l)=\emptyset$ for all distinct $m,l\in\mathbb{N}$ is called pairwise disjoint; when $\mathcal{F}$ is a $\sigma$-algebra, this is the pairwise disjointness of Measure, Measure Space, and Probability Measure.

Pairwise disjoint sequences. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $2$ and $\pi(0)=i$, $\pi(1)=j$, the formula $\delta(x_{i},x_{j})$ is a predicative formula in $x_{0},\dots,x_{n-1}$ that holds exactly when $x_{j}$ is a pairwise disjoint sequence in $x_{i}$. This proves (i).

The formula for measures. By Kit for def:sigma-algebra-measurable-space (i), with its $n$ equal to $2$, $i=0$ and $j=1$, and its parameter the class variable $\mathbb{N}$, there is a predicative formula $\sigma$ in $x_{0},x_{1}$ expressing "$x_{1}$ is a $\sigma$-algebra on $x_{0}$", with free variables among $x_{0}$, $x_{1}$ and $\mathbb{N}$. By Renaming and Substituting Variables in Predicative Formulas (i), with its $n$ equal to $7$, the formula $\delta(x_{1},x_{3})$, given by $\pi(0)=1$ and $\pi(1)=3$, holds exactly when $x_{3}$ is a pairwise disjoint sequence in $x_{1}$, and the formula $\psi(x_{4},x_{6})$, given by $\pi(0)=4$ and $\pi(1)=6$, holds exactly when $x_{4}$ is a sequence in $[0,\infty]$, $x_{6}\in[0,\infty]$ and $x_{6}$ is the sum of $x_{4}$; their bound variables are renamed so as to be other than $x_{0},\dots,x_{6}$ and $m$. Let

$$\begin{aligned} \varphi={}&\sigma\wedge x_{2}\in Z^{x_{1}}\wedge(\emptyset,0)\in x_{2}\\ &\wedge\forall x_{3}\,\forall x_{4}\,\forall x_{5}\,\forall x_{6}\,\Bigl(\delta(x_{1},x_{3})\wedge x_{4}\in Z^{\mathbb{N}}\wedge\forall m\,\bigl(m\in\mathbb{N}\Rightarrow(x_{3}(m),x_{4}(m))\in x_{2}\bigr)\\ &\qquad\wedge x_{5}=\bigcup_{m\in\mathbb{N}}x_{3}(m)\wedge(x_{5},x_{6})\in x_{2}\Rightarrow\psi(x_{4},x_{6})\Bigr). \end{aligned}$$

Here $Z^{x_{1}}$ is the class term of functions from $x_{1}$ to $[0,\infty]$ and $\bigcup_{m\in\mathbb{N}}x_{3}(m)$ that of the union, both given by class abstraction with predicative formulas; the ordered pair and $\emptyset$ exist for all arguments, and the values $x_{3}(m)$ and $x_{4}(m)$ occur only under the hypotheses $\delta(x_{1},x_{3})$, whose first conjunct is $x_{3}\in x_{1}^{\mathbb{N}}$, $x_{4}\in Z^{\mathbb{N}}$ and $m\in\mathbb{N}$. As for $\delta$, $\varphi$ is predicative, with free variables among $x_{0}$, $x_{1}$, $x_{2}$ and the parameters.

Let sets $X$, $\mathcal{F}$ and $\mu$ be assigned to $x_{0}$, $x_{1}$ and $x_{2}$. By σ-Algebra and Measurable Space (ii), $(X,\mathcal{F})$ is a measurable space if and only if $\mathcal{F}$ is a $\sigma$-algebra on $X$, that is, if and only if $\sigma$ holds; assume it does. The second conjunct of $\varphi$ holds exactly when $\mu$ is a map $\mu:\mathcal{F}\to[0,\infty]$ (The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i)); assume this too. As $\emptyset\in\mathcal{F}$, the third conjunct says that $\mu(\emptyset)=0$. In the last conjunct, $x_{3}$ ranges over all pairwise disjoint sequences $(A_{m})$ in $\mathcal{F}$, each being an element of $\mathcal{F}^{\mathbb{N}}$ and so a set. Fix one. Its union $U=\bigcup_{m\in\mathbb{N}}A_{m}$ is an element of $\mathcal{F}$, so a set, and $x_{5}=\bigcup_{m\in\mathbb{N}}x_{3}(m)$ holds exactly when $U$ is assigned to $x_{5}$; then $(x_{5},x_{6})\in x_{2}$ holds exactly when $\mu(U)$ is assigned to $x_{6}$. The sets $c$ satisfying $x_{4}\in Z^{\mathbb{N}}$ and the condition on all $m\in\mathbb{N}$ are the sequences in $[0,\infty]$ with $c_{m}=\mu(A_{m})$ for every $m\in\mathbb{N}$. The composite $\mu\circ(A_{m})$ is such a sequence, the sequence $m\mapsto\mu(A_{m})$, and it is the only one (Sequences: Enlarging the Codomain, Extensionality and the Range (ii)). So, as $\mu(U)\in[0,\infty]$, the last conjunct of $\varphi$ holds if and only if

$$\mu\Bigl(\bigcup_{m\in\mathbb{N}}A_{m}\Bigr)=\sum_{m\in\mathbb{N}}\mu(A_{m})$$

for every pairwise disjoint sequence $(A_{m})$ in $\mathcal{F}$. By Measure, Measure Space, and Probability Measure (i), $\varphi$ holds if and only if $(X,\mathcal{F})$ is a measurable space and $\mu$ is a measure on $(X,\mathcal{F})$. So $\varphi$ is a predicative formula in $x_{0},x_{1},x_{2}$ expressing this condition.

Measures. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $3$ and $\pi(0)=i$, $\pi(1)=j$, $\pi(2)=k$, the formula $\varphi(x_{i},x_{j},x_{k})$ is a predicative formula in $x_{0},\dots,x_{n-1}$ that holds exactly when $(x_{i},x_{j})$ is a measurable space and $x_{k}$ is a measure on it. This proves (ii).

Measure spaces. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $3$, its $n$ equal to $4$ and $\pi(0)=1$, $\pi(1)=2$, $\pi(2)=3$, the formula $\varphi(x_{1},x_{2},x_{3})$ is a predicative formula in $x_{0},\dots,x_{3}$, its bound variables renamed so as to be other than $x_{0},\dots,x_{3}$. Let

$$\nu=\exists x_{1}\,\exists x_{2}\,\exists x_{3}\,\bigl(x_{0}=((x_{1},x_{2}),x_{3})\wedge\varphi(x_{1},x_{2},x_{3})\bigr).$$

It is predicative, with free variables among $x_{0}$ and the parameters. By The Ordered Pair of Two Sets and Nested Tuples (ii), $((X,\mathcal{F}),\mu)$ is the tuple $\langle X,\mathcal{F},\mu\rangle$. A measure on a measurable space $(X,\mathcal{F})$ is an element of $[0,\infty]^{\mathcal{F}}$ (The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i)) and so a set, as are $X$ and $\mathcal{F}$. Hence, for a set $M$ assigned to $x_{0}$, $\nu$ holds if and only if $M=\langle X,\mathcal{F},\mu\rangle$ for a measurable space $(X,\mathcal{F})$ and a measure $\mu$ on it, that is, by Measure, Measure Space, and Probability Measure (ii), if and only if $M$ is a measure space. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $1$ and $\pi(0)=i$, the formula $\nu(x_{i})$ is a predicative formula in $x_{0},\dots,x_{n-1}$ that holds exactly when $x_{i}$ is a measure space. This proves (iii).

The formulas for finite, $\sigma$-finite and probability measures. Let

$$\begin{aligned} \varphi_{\mathrm{fin}}={}&\varphi\wedge\exists x_{3}\,\bigl((x_{0},x_{3})\in x_{2}\wedge(x_{3},\infty)\in L\wedge\neg\,x_{3}=\infty\bigr),\\ \varphi_{\sigma}={}&\varphi\wedge\exists x_{3}\,\Bigl(x_{3}\in x_{1}^{\mathbb{N}}\wedge x_{0}=\bigcup_{m\in\mathbb{N}}x_{3}(m)\wedge\forall m\,\bigl(m\in\mathbb{N}\Rightarrow\exists x_{4}\,((x_{3}(m),x_{4})\in x_{2}\wedge(x_{4},\infty)\in L\wedge\neg\,x_{4}=\infty)\bigr)\Bigr),\\ \varphi_{1}={}&\varphi\wedge(x_{0},1)\in x_{2}. \end{aligned}$$

As for $\varphi$, these are predicative, the values $x_{3}(m)$ occurring only under the hypotheses $x_{3}\in x_{1}^{\mathbb{N}}$ and $m\in\mathbb{N}$, with free variables among $x_{0}$, $x_{1}$, $x_{2}$ and the parameters. Let sets $X$, $\mathcal{F}$ and $\mu$ assigned to $x_{0}$, $x_{1}$ and $x_{2}$ satisfy $\varphi$, so that $\mu$ is a measure on the measurable space $(X,\mathcal{F})$. Then $X\in\mathcal{F}$, and every value of $\mu$ lies in $[0,\infty]$, hence in $[-\infty,\infty]$; for $r\in[0,\infty]$, $r<\infty$ holds if and only if $(r,\infty)\in L$ and $r\neq\infty$, by The Extended Real Line, Its Order, and [0,∞] (iii). So the second conjunct of $\varphi_{\mathrm{fin}}$ holds exactly when $\mu(X)<\infty$, that is, by Measure, Measure Space, and Probability Measure (iii), when $\mu$ is finite. In $\varphi_{\sigma}$, $x_{3}$ ranges over the sequences $(X_{m})$ in $\mathcal{F}$, which are sets, being elements of $\mathcal{F}^{\mathbb{N}}$ (The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i)); for such a sequence, $x_{0}=\bigcup_{m\in\mathbb{N}}x_{3}(m)$ says that $\bigcup_{m\in\mathbb{N}}X_{m}=X$, and the last conjunct that $\mu(X_{m})<\infty$ for every $m\in\mathbb{N}$. So the second conjunct of $\varphi_{\sigma}$ holds exactly when $\mu$ is $\sigma$-finite, by Measure, Measure Space, and Probability Measure (iv). The second conjunct of $\varphi_{1}$ holds exactly when $\mu(X)=1$, that is, by Measure, Measure Space, and Probability Measure (v), when $\mu$ is a probability measure. Hence $\varphi_{\mathrm{fin}}$, $\varphi_{\sigma}$ and $\varphi_{1}$ are predicative formulas in $x_{0},x_{1},x_{2}$ expressing "$(x_{0},x_{1})$ is a measurable space and $x_{2}$ is a measure on it that is finite", respectively "that is $\sigma$-finite", respectively "that is a probability measure".

Finite, $\sigma$-finite and probability measures. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $3$ and $\pi(0)=i$, $\pi(1)=j$, $\pi(2)=k$, the formulas $\varphi_{\mathrm{fin}}(x_{i},x_{j},x_{k})$, $\varphi_{\sigma}(x_{i},x_{j},x_{k})$ and $\varphi_{1}(x_{i},x_{j},x_{k})$ are predicative formulas in $x_{0},\dots,x_{n-1}$ expressing the conditions of (iv), (v) and (vi). This proves these three clauses.

The set of pairwise disjoint sequences. Let $\mathcal{F}$ be a set, and let $y$ be a parameter, a set variable other than those above, with value $\mathcal{F}$. By Renaming and Substituting Variables in Predicative Formulas (iii), with its number of variables equal to $2$ and its $n$ equal to $1$, $\tau_{0}=y$ and $\tau_{1}=x_{0}$, the formula $\delta(y,x_{0})$ is a predicative formula in $x_{0}$ that holds, for a set $a$ assigned to $x_{0}$, exactly when $a$ is a pairwise disjoint sequence in $\mathcal{F}$. By The Class Comprehension Theorem for Predicative Formulas (i), with one set variable $x_{0}$ and parameters $y$ and $\mathbb{N}$, there is a class $\mathcal{D}$ such that, for every set $a$, $a\in\mathcal{D}$ if and only if $a$ is a pairwise disjoint sequence in $\mathcal{F}$. This extends to every class $a$: an element of $\mathcal{D}$ is a set, and a sequence in $\mathcal{F}$ is an element of $\mathcal{F}^{\mathbb{N}}$ (The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i)), so a set. Hence $\mathcal{D}\subseteq\mathcal{F}^{\mathbb{N}}$, which is a set by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (ii), and $\mathcal{D}$ is a set by Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper (i). This proves (vii).

The sets of measures, of finite, of $\sigma$-finite and of probability measures. Let $X$ and $\mathcal{F}$ be sets such that $(X,\mathcal{F})$ is a measurable space, and let $y$ and $z$ be parameters, distinct set variables other than those above, with values $X$ and $\mathcal{F}$. By Renaming and Substituting Variables in Predicative Formulas (iii), with its number of variables equal to $3$ and its $n$ equal to $1$, $\tau_{0}=y$, $\tau_{1}=z$ and $\tau_{2}=x_{0}$, the formula $\varphi(y,z,x_{0})$ is a predicative formula in $x_{0}$ that holds, for a set $\mu$ assigned to $x_{0}$, exactly when $\mu$ is a measure on $(X,\mathcal{F})$; likewise $\varphi_{\mathrm{fin}}(y,z,x_{0})$, $\varphi_{\sigma}(y,z,x_{0})$ and $\varphi_{1}(y,z,x_{0})$ hold exactly when $\mu$ is a measure on $(X,\mathcal{F})$ that is finite, $\sigma$-finite, or a probability measure. By The Class Comprehension Theorem for Predicative Formulas (i), with one set variable $x_{0}$ and the parameters $y$, $z$ and those of the statement, there are classes $\mathcal{M}$, $\mathcal{M}_{\mathrm{fin}}$, $\mathcal{M}_{\sigma}$ and $\mathcal{M}_{1}$ whose elements among the sets are exactly the measures on $(X,\mathcal{F})$, the finite ones, the $\sigma$-finite ones and the probability measures. This extends to every class $\mu$: an element of a class is a set, and a measure on $(X,\mathcal{F})$ is a map $\mathcal{F}\to[0,\infty]$, hence an element of $[0,\infty]^{\mathcal{F}}$ (The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i)), and so a set. Hence each of the four classes is a subclass of $[0,\infty]^{\mathcal{F}}$, which is a set by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (ii), and so is a set by Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper (i). This proves (viii), (x), (xi) and (xii).

The class of measure spaces. By The Class Comprehension Theorem for Predicative Formulas (i), with one set variable $x_{0}$, the parameters of the statement and the formula $\nu$, there is a class $\mathcal{S}$ such that, for every set $M$, $M\in\mathcal{S}$ if and only if $M$ is a measure space. This extends to every class $M$: an element of $\mathcal{S}$ is a set, and a measure space is a tuple, which is a set (The Ordered Pair of Two Sets and Nested Tuples (ii)). This proves (ix).