Proof of The Finite Signed Measures on a Measurable Space Form a Set

The argument is that of The Measures, the Finite Measures and the Probability Measures on a Measurable Space Form Sets, with real values in place of values in $[0,\infty]$.

Throughout, $\Phi=\mathbb{R}^{\mathcal{F}}$ and $\mathcal{S}=\mathbb{R}^{\mathbb{N}}$ are sets whose elements are exactly the functions $\mathcal{F}\to\mathbb{R}$ and the sequences in $\mathbb{R}$, 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 $\mathbb{R}$ are sets, so quantifiers over sets reach all of them. Further, $\emptyset\in\mathcal{F}$ by Closure Properties of σ-Algebras, Intersections and Traces of σ-Algebras, and the Generated σ-Algebra (vi), and unions of sequences in $\mathcal{F}$ and pairwise disjointness are as in Measure, Measure Space, and Probability Measure, as Finite Signed Measures takes them.

Sums of real series. Let $\theta_{\Sigma}(s,\sigma)$ be the condition "$s\in\mathcal{S}$, the series $\sum_{m=1}^{\infty}s_{m}$ converges, and $\sigma=\sum_{m=1}^{\infty}s_{m}$". It is expressed by the predicative formula

$$s\in\mathcal{S}\wedge\exists p\,\bigl(\forall n\,\forall w\,((n,w)\in p\Rightarrow\mathrm{it}(w,n,s))\wedge\kappa(p,\sigma)\bigr),$$

where $\mathrm{it}$ is the formula of Iterated Operations Are Given by a Predicative Formula (i) for the addition of $\mathbb{R}$, placed at the variables $w$, $n$ and $s$ by a renaming of variables (Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (i)), and $\kappa(p,\sigma)$ is the formula of Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (i) for the metric space $(\mathbb{R},d_{\mathbb{R}})$ of Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (iv), with $p$ and $\sigma$ for $s$ and $z$. Indeed, let $s\in\mathcal{S}$. By Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (iv), $\kappa(p,\sigma)$ already says that $p$ is a sequence in $\mathbb{R}$, so only $p:\mathbb{N}\to\mathbb{R}$ need be considered. For $n\in\mathbb{N}$, $s$ is a function from $\mathbb{N}\supseteq[n]$ to $\mathbb{R}$, so the conjunct with $\mathrm{it}$ holds if and only if $p(n)=\sum_{k=1}^{n}s_{k}$ for every $n\in\mathbb{N}$, that is (the sum over the interval $\{1,\dots,n\}$ of Sums and Products over a Finite Set and over an Interval (iv), defined as the addition of $\mathbb{R}$ is associative and commutative by The Real Numbers Form an Ordered Field in Which Every Nonempty Set Bounded Above Has a Supremum (i), agreeing there with the iterated sum), if and only if $p$ is the sequence of partial sums of $s$, which exists by Sequences of Real Numbers Built from Given Ones: Partial Sums, Index Shifts, Predecessor Reindexing, Absolute Values and Termwise Operations (i). By Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (iv), $\kappa(p,\sigma)$ holds if and only if $p$ converges to $\sigma\in\mathbb{R}$. So the formula holds if and only if $s$ is a sequence in $\mathbb{R}$ whose sequence of partial sums converges to $\sigma$, that is, by Series of Real Numbers: Partial Sums, Convergence, the Sum and Absolute Convergence (ii) and The Limit of a Convergent Sequence (i), if and only if $\theta_{\Sigma}(s,\sigma)$. In particular, if $s\in\mathcal{S}$ and its series converges, then exactly one set satisfies $\theta_{\Sigma}(s,\cdot)$, the sum, a real number by Sums of Series: a Convergent Series Has a Real Sum, and a Bound on All Partial Sums Bounds the Sum in [0,∞] (i); and the condition $\gamma_{\Sigma}(s)$, "$s\in\mathcal{S}$ and the series $\sum_{m=1}^{\infty}s_{m}$ converges", is expressed by the predicative formula $\exists\sigma\,\theta_{\Sigma}(s,\sigma)$.

The formula tree. Consider the following formula tree in the set variable $\nu=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. 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(\nu,A,s)&:\ \forall m\,\bigl(m\in\mathbb{N}\Rightarrow(t=s_{m}\text{ before }a=A_{m}\text{ before }u=\nu(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}=\nu(A_{m})$ for every $m\in\mathbb{N}$, with $A_{m}=A(m)$, $A_{k}$, $s_{m}=s(m)$ and $\nu(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),$$

where $\varphi\Leftrightarrow\psi$ abbreviates $(\varphi\Rightarrow\psi)\wedge(\psi\Rightarrow\varphi)$, let

$$\begin{aligned} \Theta(\nu):\ \ &\nu:\mathcal{F}\to\mathbb{R}\ \wedge\ \bigl(c=\nu(\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\mathbb{R}\Rightarrow\varepsilon(\nu,A,s)\Rightarrow\Bigl(\gamma_{\Sigma}(s)\ \wedge\\ &\quad\bigl(U=\textstyle\bigcup_{m\in\mathbb{N}}A_{m}\text{ with }\theta_{\cup}\text{ before }v=\nu(U)\text{ before }\sigma=\textstyle\sum_{m=1}^{\infty}s_{m}\text{ with }\theta_{\Sigma}\text{ before }v=\sigma\bigr)\Bigr)\Bigr)\Bigr), \end{aligned}$$

with $0$ the zero of $\mathbb{R}$ and $\gamma_{\Sigma}(s)$ an atom of its own.

The tree is well scoped and satisfies its side conditions. The only parameter standing as an argument or inside a pair, $\emptyset$, is a set. 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; and $\gamma_{\Sigma}$ and $\theta_{\Sigma}$ are expressed by predicative formulas, as shown above.

The tree also uses its values properly under every assignment of sets. Its values are read only where $\nu:\mathcal{F}\to\mathbb{R}$ holds and, inside the quantifiers, only where $A$ is a sequence in $\mathcal{F}$, $s$ a sequence in $\mathbb{R}$ and $m,k\in\mathbb{N}$. There $A_{m}$, $A_{k}$ and $s_{m}$ exist, and so do $\nu(\emptyset)$ and $\nu(A_{m})$, as $\emptyset,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 $\nu(U)$ exists. Finally, the value $\sigma$ is read only where $\gamma_{\Sigma}(s)$ holds, and there $\sum_{m=1}^{\infty}s_{m}$ is a set and the only set satisfying $\theta_{\Sigma}$.

The reading. By The Graph Reading of a Formula Tree Is Predicative and Agrees with Its Reading, So the Reading Is Predicative (iii), the reading of $\Theta$ is therefore the reading of a predicative formula $\psi$ whose free variables are $\nu$ 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(\nu)$ holds if and only if $\nu:\mathcal{F}\to\mathbb{R}$, $\nu(\emptyset)=0$, and for every pairwise disjoint sequence $(A_{m})$ in $\mathcal{F}$ and every sequence $s$ in $\mathbb{R}$ with $s_{m}=\nu(A_{m})$ for all $m\in\mathbb{N}$, the series $\sum_{m=1}^{\infty}s_{m}$ converges and

$$\nu\Bigl(\bigcup_{m\in\mathbb{N}}A_{m}\Bigr)=\sum_{m=1}^{\infty}s_{m}$$

(the sequence $m\mapsto\nu(A_{m})$, which exists by Maps and Relations Given by Formulas (i), is the only such $s$); that is, by Finite Signed Measures (i), if and only if $\nu$ is a finite signed measure on $(X,\mathcal{F})$.

The set. Let

$$\mathcal{M}=\{\nu\in\Phi:\psi(\nu)\},$$

as in Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (ii). It 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 $\nu$, $\nu\in\mathcal{M}$ if and only if $\nu\in\Phi$ and $\nu$ is a finite signed measure on $(X,\mathcal{F})$; since a finite signed measure is a function $\mathcal{F}\to\mathbb{R}$, it lies in $\Phi$, so $\nu\in\mathcal{M}$ if and only if $\nu$ is a finite signed measure on $(X,\mathcal{F})$. This proves (i).