Proof of The Measures, the Finite Measures and the Probability Measures on a Measurable Space Form Sets

Throughout, $\Phi=[0,\infty]^{\mathcal{F}}$ and $\mathcal{S}=[0,\infty]^{\mathbb{N}}$ are sets whose elements are exactly the functions $\mathcal{F}\to[0,\infty]$ and the sequences in $[0,\infty]$, respectively, and every sequence in $\mathcal{F}$ is an element of the set $\mathcal{F}^{\mathbb{N}}$ (The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (ii)); in particular sequences in $\mathcal{F}$ and in $[0,\infty]$ are sets, so quantifiers over sets reach all of them. Further, $\emptyset,X\in\mathcal{F}$ and $0,1\in[0,\infty]$ are as in Measure, Measure Space, and Probability Measure, and $\infty$ is as in The Extended Real Line, Its Order, and [0,∞] (i).

Consider the following formula trees in the set variable $\mu=x_0$. Every further letter, bound by a quantifier or naming a value, is the next unused variable at its place; conjunctions and implications are grouped to the right, and $\varphi\Leftrightarrow\psi$ abbreviates $(\varphi\Rightarrow\psi)\wedge(\psi\Rightarrow\varphi)$. The parts

$$\begin{aligned} \delta(A)&:\ \forall m\,\forall k\,\bigl(m\in\mathbb{N}\Rightarrow k\in\mathbb{N}\Rightarrow\neg\,m=k\Rightarrow(a=A_{m}\text{ before }b=A_{k}\text{ before }\neg\exists w\,(w\in a\wedge w\in b))\bigr),\\ \varepsilon(\mu,A,s)&:\ \forall m\,\bigl(m\in\mathbb{N}\Rightarrow(t=s_{m}\text{ before }a=A_{m}\text{ before }u=\mu(a)\text{ before }t=u)\bigr) \end{aligned}$$

say that for $m\neq k$ no $w$ lies in both $A_{m}$ and $A_{k}$, and that $s_{m}=\mu(A_{m})$ for every $m\in\mathbb{N}$, with $A_{m}=A(m)$, $A_{k}$, $s_{m}=s(m)$ and $\mu(A_{m})$ as named values. With the value-free tree

$$\theta_{\cup}(A,U):\ \forall w\,\bigl(w\in U\Leftrightarrow\exists m\,(m\in\mathbb{N}\wedge\exists b\,((m,b)\in A\wedge w\in b))\bigr)$$

and the condition $\theta_{\Sigma}(s,\sigma)$, "$s\in\mathcal{S}$ and $\sigma=\sum_{m\in\mathbb{N}}s_{m}$", where $\sum_{m\in\mathbb{N}}s_{m}$ is the sum of $s$, let

$$\begin{aligned} \Theta(\mu):\ \ &\mu:\mathcal{F}\to[0,\infty]\ \wedge\ \bigl(c=\mu(\emptyset)\text{ before }c=0\bigr)\ \wedge\ \forall A\,\Bigl(A:\mathbb{N}\to\mathcal{F}\Rightarrow\delta(A)\Rightarrow\forall s\,\Bigl(s:\mathbb{N}\to[0,\infty]\Rightarrow\varepsilon(\mu,A,s)\Rightarrow\\ &\quad\bigl(U=\textstyle\bigcup_{m\in\mathbb{N}}A_{m}\text{ with }\theta_{\cup}\text{ before }v=\mu(U)\text{ before }\sigma=\textstyle\sum_{m\in\mathbb{N}}s_{m}\text{ with }\theta_{\Sigma}\text{ before }v=\sigma\bigr)\Bigr)\Bigr),\\ \Theta_{\mathrm{f}}(\mu):\ \ &\Theta(\mu)\wedge\bigl(v=\mu(X)\text{ before }((v,\infty)\in{\le}\wedge\neg\,v=\infty)\bigr),\\ \Theta_{1}(\mu):\ \ &\Theta(\mu)\wedge\bigl(v=\mu(X)\text{ before }v=1\bigr), \end{aligned}$$

with $\le$ the order of $[-\infty,\infty]$, as a set of pairs, of The Extended Real Line, Its Order, and [0,∞] (iii).

The three trees are well scoped and satisfy their side conditions. The parameters standing as arguments or inside pairs, $\emptyset$, $X$ and $\infty=\mathbb{R}$, are sets. The condition $\theta_{\cup}$ is itself a well-scoped tree without values or atoms of its own, so it is the reading of a predicative formula by The Graph Reading of a Formula Tree Is Predicative and Agrees with Its Reading, So the Reading Is Predicative (i), its graph reading being itself. The condition $\theta_{\Sigma}$ is expressed by a predicative formula: $s$ is a term of type $\mathcal{S}$ under the guard $s\in\mathcal{S}$ (Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (i)), so $\sum_{m\in\mathbb{N}}s_{m}$ is a term of type $[0,\infty]$ under it (Sums of Sequences in [0,∞] as Typed Terms and as a Map (i)), and Terms and Typed Terms under a Guard (iv) applies.

Each tree also uses its values properly under every assignment of sets. Its values are read only where $\mu:\mathcal{F}\to[0,\infty]$ holds and, inside the quantifiers, only where $A$ is a sequence in $\mathcal{F}$, $s$ a sequence in $[0,\infty]$ and $m,k\in\mathbb{N}$. There $A_{m}$, $A_{k}$ and $s_{m}$ exist, and so do $\mu(\emptyset)$, $\mu(X)$ and $\mu(A_{m})$, as $\emptyset,X,A_{m}\in\mathcal{F}$. The union $\bigcup_{m\in\mathbb{N}}A_{m}$ of the family $(A_{m})_{m\in\mathbb{N}}$ is a set by The Union and Product of a Family of Sets Indexed by a Set, and the Intersection of a Family with an Inhabited Index Class, Are Sets (i), it is the only set satisfying $\theta_{\cup}$ by Indexed Families of Sets and Their Union, Intersection and Product (ii) and Axiom of Extensionality for Classes, and it lies in $\mathcal{F}$ by σ-Algebra and Measurable Space (i), so $\mu(U)$ exists. Finally $\sum_{m\in\mathbb{N}}s_{m}\in[0,\infty]$ is a set, and the only set satisfying $\theta_{\Sigma}$.

By The Graph Reading of a Formula Tree Is Predicative and Agrees with Its Reading, So the Reading Is Predicative (iii), the reading of each tree is therefore the reading of a predicative formula whose free variables are $\mu$ and class variables for the parameters. In the reading, quantifiers range over sets and every named variable takes its value. No set lies in both $A_{m}$ and $A_{k}$ if and only if $A_{m}\cap A_{k}=\emptyset$ (The Boolean Operations on Classes, Disjointness, and the Universal Class (i), The Empty Set, the Unordered Pair and the Singleton (i), Axiom of Extensionality for Classes), and sequences are sets. Hence $\Theta(\mu)$ holds if and only if $\mu:\mathcal{F}\to[0,\infty]$, $\mu(\emptyset)=0$, and for every pairwise disjoint sequence $(A_{m})$ in $\mathcal{F}$ and every sequence $s$ in $[0,\infty]$ with $s_{m}=\mu(A_{m})$ for all $m\in\mathbb{N}$,

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

(the sequence $m\mapsto\mu(A_{m})$ is the only such $s$); that is, by Measure, Measure Space, and Probability Measure (i), if and only if $\mu$ is a measure on $(X,\mathcal{F})$. Likewise $\Theta_{\mathrm{f}}(\mu)$ holds if and only if $\mu$ is a measure with $\mu(X)<\infty$ (The Extended Real Line, Its Order, and [0,∞] (iii)), a finite measure (Measure, Measure Space, and Probability Measure (iii)); and $\Theta_{1}(\mu)$ if and only if $\mu$ is a measure with $\mu(X)=1$, a probability measure (Measure, Measure Space, and Probability Measure (v)).

Let $\psi$, $\psi_{\mathrm{f}}$ and $\psi_{1}$ be predicative formulas whose readings are those of $\Theta$, $\Theta_{\mathrm{f}}$ and $\Theta_{1}$, and let

$$\mathcal{M}=\{\mu\in\Phi:\psi(\mu)\},\qquad\mathcal{M}_{\mathrm{f}}=\{\mu\in\Phi:\psi_{\mathrm{f}}(\mu)\},\qquad\mathcal{M}_{1}=\{\mu\in\Phi:\psi_{1}(\mu)\},$$

as in Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (ii). Each is a subclass of the set $\Phi$, hence 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). For a set $\mu$, $\mu\in\mathcal{M}$ if and only if $\mu\in\Phi$ and $\mu$ is a measure on $(X,\mathcal{F})$; since a measure is a function $\mathcal{F}\to[0,\infty]$, it lies in $\Phi$, so $\mu\in\mathcal{M}$ if and only if $\mu$ is a measure on $(X,\mathcal{F})$. This proves (i), and the same argument for $\mathcal{M}_{\mathrm{f}}$ and $\mathcal{M}_{1}$ proves (ii) and (iii).