Proof of The Borel Sets of ℝⁿ, Lebesgue Measure on ℝⁿ and Integrals against It Are Predicative in the Dimension

Proof sketch. Throughout, the guard is $n\in\mathbb{N}$; under it $\mathbb{R}^{n}=\mathbb{R}^{[n]}$ is a typed term (Countability as a Predicative Condition, and Finite Powers of a Set as a Typed Term (ii)), $[n]$ is given by a predicative formula (Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness (i)), values of maps are typed terms and equations and memberships between typed terms are predicative (Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii), Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (v), Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (vi)), being a map is predicative (Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii)), and the strict order and differences of real numbers are predicative (Predicative Formulas for Differences, Quotients, Absolute Values, Distances and the Strict Order of the Real Numbers, at Any Variable Positions (v), Predicative Formulas for Differences, Quotients, Absolute Values, Distances and the Strict Order of the Real Numbers, at Any Variable Positions (i)).

Step 1 (open boxes). The condition "$n\in\mathbb{N}$, $a,b\in\mathbb{R}^{n}$ and $U=R(a,b)$" is predicative: by Open Boxes in ℝⁿ (i), $U=R(a,b)$ says that for every set $x$,

$$x\in U\iff x\in\mathbb{R}^{[n]}\ \text{and}\ a(i)<x(i)<b(i)\ \text{for every}\ i\in[n],$$

a formula built from the predicative pieces listed above.

Step 2 (proof of (i)). By Existence and Uniqueness of Lebesgue Measure on ℝⁿ (i), $\mathcal{B}(\mathbb{R}^{n})=\sigma(\mathcal{R}_{n})$, and by The σ-Algebra Generated by a Set of Subsets (i) and The σ-Algebra Generated by a Set of Subsets (ii) a set $B$ belongs to $\sigma(\mathcal{R}_{n})$ if and only if $B\subseteq\mathbb{R}^{n}$ and $B\in G$ for every $\sigma$-algebra $G$ on $\mathbb{R}^{n}$ containing every open box $R(a,b)$. "$G$ is a $\sigma$-algebra on $Y$", for a variable $Y$, is predicative by Borel Sets of a Variable Metric Space as a Predicative Condition, and the Families of σ-Algebras Generated by Random Elements and of Their Composites (iv); substituting the term $\mathbb{R}^{[n]}$ for $Y$ and using Step 1 for "$R(a,b)\in G$", the condition "for every set $B$: $B\in\mathcal{G}$ if and only if $B\in\sigma(\mathcal{R}_{n})$" is predicative, and it is $\mathcal{G}=\mathcal{B}(\mathbb{R}^{n})$.

Step 3 (proof of (ii)). By Lebesgue Measure on $\mathbb{R}^n$ (i) and the uniqueness in Existence and Uniqueness of Lebesgue Measure on ℝⁿ (iii), for $n\in\mathbb{N}$ we have $\kappa=\lambda_{n}$ if and only if $\kappa$ is a measure on $(\mathbb{R}^{n},\mathcal{B}(\mathbb{R}^{n}))$ and

$$\kappa\bigl(R(a,b)\bigr)=\prod_{i=1}^{n}c(i)\qquad\text{for all }a,b\in\mathbb{R}^{n}\text{ with }a(i)<b(i)\ (i\in[n]),$$

where $c:[n]\to\mathbb{R}$ is the map with $c(i)=b(i)-a(i)$. Accordingly the clause is expressed by

$$n\in\mathbb{N}\wedge\exists\mathcal{G}\,\Bigl(\beta(n,\mathcal{G})\wedge\operatorname{ms}(n,\mathcal{G},\kappa)\wedge\forall a\,\forall b\,\bigl(\chi(n,a,b)\Rightarrow\exists U\,\exists c\,\exists p\,(\rho(n,a,b,U)\wedge\delta(n,a,b,c)\wedge\mathrm{it}(p,n,c)\wedge(U,p)\in\kappa)\bigr)\Bigr).$$

Here $\beta(n,\mathcal{G})$ is the formula of (i) for "$n\in\mathbb{N}$ and $\mathcal{G}=\mathcal{B}(\mathbb{R}^{n})$". $\operatorname{ms}(n,\mathcal{G},\kappa)$ says that $\kappa$ is a measure on $(\mathbb{R}^{[n]},\mathcal{G})$; by Measure, Measure Space, and Probability Measure (i): $\kappa$ is a map $\mathcal{G}\to[0,\infty]$, $\kappa(\emptyset)=0$, and for every pairwise disjoint map $A:\mathbb{N}\to\mathcal{G}$, $\kappa(\bigcup_{m}A_{m})$ equals the sum of the sequence $\kappa\circ A$ in $[0,\infty]$, a typed term by Sums of Sequences in [0,∞] as Typed Terms and as a Map (i). $\chi(n,a,b)$ says that $a,b\in\mathbb{R}^{[n]}$ and $a(i)<b(i)$ for every $i\in[n]$; $\rho(n,a,b,U)$ is the formula of Step 1 for $U=R(a,b)$; $\delta(n,a,b,c)$ says that $c$ is a map $c:[n]\to\mathbb{R}$ and $c(i)=b(i)-a(i)$ for every $i\in[n]$, the difference by Predicative Formulas for Differences, Quotients, Absolute Values, Distances and the Strict Order of the Real Numbers, at Any Variable Positions (i), its values read after the guards $a,b\in\mathbb{R}^{[n]}$, "$c$ is a map on $[n]$" and $i\in[n]$; and $\mathrm{it}(p,n,c)$ is the formula of Iterated Operations Are Given by a Predicative Formula (i) for the product of $\mathbb{R}$, saying $p=\prod_{i=1}^{n}c(i)$. Each is predicative by the opening paragraph and Step 1. Where $\beta$, $\operatorname{ms}$ and $\chi$ hold, $R(a,b)\in\mathcal{R}_{n}\subseteq\sigma(\mathcal{R}_{n})=\mathcal{G}$ by Existence and Uniqueness of Lebesgue Measure on ℝⁿ (i), so $\kappa(R(a,b))$ exists; $U$, $c$ and $p$ exist and are unique, so the bracket says $\kappa(R(a,b))=\prod_{i=1}^{n}c(i)$. Hence the displayed formula holds exactly when $n\in\mathbb{N}$ and $\kappa=\lambda_{n}$.

Step 4 (proof of (iii)). We write the clause as an explicit formula, following the construction behind The Simple, Nonnegative, Integrable and Signed Integrals Are Predicative in the Measure and the Function, at Any Variable Positions (ii) with its parameters $X$ and $\mathcal{F}$ made set variables $E$ and $\mathcal{G}$. Its atoms are: $\alpha(E,\mathcal{G})$, the formula of Borel Sets of a Variable Metric Space as a Predicative Condition, and the Families of σ-Algebras Generated by Random Elements and of Their Composites (iv) for "$\mathcal{G}$ is a $\sigma$-algebra on $E$"; $\varphi(D)$ and $\Sigma(D,h,v)$, the formulas of Predicative Formulas for the Vocabulary of Finite Combinatorics, at Any Variable Positions (i) and Predicative Formulas for the Vocabulary of Finite Combinatorics, at Any Variable Positions (vii) (second form, for the sum $+$ of $[0,\infty]$, associative and commutative with neutral element $0$ by the setting's background), saying that $D$ is finite, respectively that $D$ is finite, $h$ is a map $h:D\to[0,\infty]$ and $v=\sum_{c\in D}h(c)$; and $\sigma(S,r)$, the formula of Predicative Formulas for Suprema and Infima, and Maps Defined by Suprema and Infima (i) for $[-\infty,\infty]$ with its order, a partial order by the setting's background. For parameters $Y$, a set, and $\mathcal{C}$, a set of subsets of $Y$, let $M_{Y,\mathcal{C}}(E,\mathcal{G},f)$ be

$$f:E\to Y\ \wedge\ \forall B\,\Bigl(B\in\mathcal{C}\Rightarrow\exists w\,\bigl(\forall a\,(a\in w\Leftrightarrow(a\in E\wedge\exists y\,(y\in B\wedge(a,y)\in f)))\wedge w\in\mathcal{G}\bigr)\Bigr),$$

which says that $f$ is a map $E\to Y$ with $f^{-1}(B)\in\mathcal{G}$ for every $B\in\mathcal{C}$ (The Image and the Preimage of a Class under a Class (ii), Measurable Map, and the Set of Measurable Maps (i)). Let

$$\pi(E,\mathcal{G},s):\quad M_{\mathbb{R},\mathcal{B}(\mathbb{R})}(E,\mathcal{G},s)\wedge\exists D\,\bigl(\forall c\,(c\in D\Leftrightarrow\exists a\,(a\in E\wedge(a,c)\in s))\wedge\varphi(D)\bigr)\wedge\forall a\,\forall c\,\bigl((a,c)\in s\Rightarrow0\le c\bigr),$$ $$\Phi_{S}(E,\kappa,s,v):\quad\exists D\,\exists h\,\Bigl(\forall c\,(c\in D\Leftrightarrow\exists a\,(a\in E\wedge(a,c)\in s))\wedge\Sigma(D,h,v)\wedge\forall c\,\bigl(c\in D\Rightarrow h(c)=c\cdot\kappa(s^{-1}(\{c\}))\bigr)\Bigr),$$

where $s^{-1}(\{c\})$ is named as the set $w$ with $\forall a\,(a\in w\Leftrightarrow(a\in E\wedge(a,c)\in s))$, and

$$\begin{aligned} \Phi(E,\mathcal{G},\kappa,g,r):\quad&\alpha(E,\mathcal{G})\wedge\kappa:\mathcal{G}\to[0,\infty]\wedge M_{[0,\infty],\mathcal{B}([0,\infty])}(E,\mathcal{G},g)\\ &\wedge\exists S\,\Bigl(\forall v\,\Bigl(v\in S\Leftrightarrow\exists s\,\bigl(\pi(E,\mathcal{G},s)\wedge\forall x\,(x\in E\Rightarrow s(x)\le g(x))\wedge\Phi_{S}(E,\kappa,s,v)\bigr)\Bigr)\wedge\sigma(S,r)\Bigr). \end{aligned}$$

$\Phi$ is predicative. Written with these abbreviations, $\Phi$ is a formula tree (Formula Trees with Values: Syntax, Two Readings, and Definedness (i)) whose atoms of their own are the predicative formulas $\alpha$, $\varphi$, $\Sigma$ and $\sigma$, its other abbreviations being predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i); it is well scoped and its side conditions hold. It uses its values properly (Formula Trees with Values: Syntax, Two Readings, and Definedness (vi)) under every assignment, because each value is named only where the conjuncts before it hold, and there it exists: $s(x)$ and $g(x)$ where $\pi(E,\mathcal{G},s)$, the third conjunct of $\Phi$ and $x\in E$ hold, which make $s$ and $g$ maps on $E$; $h(c)$ where $\Sigma(D,h,v)$ and $c\in D$ hold; the set $s^{-1}(\{c\})$, a subset of $E$ and by extensionality the only set $w$ so described, under every assignment; $\kappa(s^{-1}(\{c\}))$ where moreover $\alpha(E,\mathcal{G})$, $\kappa:\mathcal{G}\to[0,\infty]$ and $\pi(E,\mathcal{G},s)$ hold, since then $s\in\mathcal{S}^{+}(E,\mathcal{G})$, as shown below, and $s^{-1}(\{c\})\in\mathcal{G}$ by Simple Functions, Nonnegative Simple Functions, and the Simple Integral (iv); and $c\cdot\kappa(s^{-1}(\{c\}))$ there too, as $c\in D\subseteq[0,\infty)\subseteq[0,\infty]$. So $\Phi$ is predicative by The Graph Reading of a Formula Tree Is Predicative and Agrees with Its Reading, So the Reading Is Predicative (iii).

What $\Phi$ says. Where $\alpha(E,\mathcal{G})$ holds, $\pi(E,\mathcal{G},s)$ says that $s$ is a measurable map $E\to\mathbb{R}$ with finite image, the only possible $D$, and nonnegative values, that is, $s\in\mathcal{S}^{+}(E,\mathcal{G})$ (Simple Functions, Nonnegative Simple Functions, and the Simple Integral (ii), Simple Functions, Nonnegative Simple Functions, and the Simple Integral (iii)). Now let $n\in\mathbb{N}$, $E=\mathbb{R}^{[n]}$, $\mathcal{G}=\mathcal{B}(\mathbb{R}^{n})$ and $\kappa=\lambda_{n}$. The first two conjuncts of $\Phi$ hold, and the third says $g\in\mathcal{M}^{+}(\mathbb{R}^{n},\mathcal{B}(\mathbb{R}^{n}))$ (Nonnegative Measurable Maps and Their Lebesgue Integral (i)). For $s\in\mathcal{S}^{+}(\mathbb{R}^{n},\mathcal{B}(\mathbb{R}^{n}))$, $\Phi_{S}$ forces $D=s[\mathbb{R}^{n}]$ and $h$ the map $c\mapsto c\cdot\lambda_{n}(s^{-1}(\{c\}))$ on it, which exists, so $\Phi_{S}(E,\kappa,s,v)$ says $v=I_{\lambda_{n}}(s)$ (Simple Functions, Nonnegative Simple Functions, and the Simple Integral (iv)). Hence the first part of the bracket says that $S$ is the set $\{I_{\lambda_{n}}(s):s\in\mathcal{S}^{+},\ s\le g\}$ of Nonnegative Measurable Maps and Their Lebesgue Integral (ii), and $\sigma(S,r)$ then says that $r$ is its supremum (Predicative Formulas for Suprema and Infima, and Maps Defined by Suprema and Infima (i)), that is, $r=\int_{\mathbb{R}^{n}}g\,d\lambda_{n}$ (Nonnegative Measurable Maps and Their Lebesgue Integral (ii)).

The clause. With $\beta(n,\mathcal{G})$ as in Step 3 and $\Lambda(n,\kappa)$ the formula of (ii), the clause is expressed by

$$n\in\mathbb{N}\wedge\exists E\,\exists\mathcal{G}\,\exists\kappa\,\bigl(E=\mathbb{R}^{[n]}\wedge\beta(n,\mathcal{G})\wedge\Lambda(n,\kappa)\wedge\Phi(E,\mathcal{G},\kappa,g,r)\bigr),$$

predicative by the opening paragraph for the equation $E=\mathbb{R}^{[n]}$. For $n\in\mathbb{N}$ the only witnesses are $E=\mathbb{R}^{n}$, $\mathcal{G}=\mathcal{B}(\mathbb{R}^{n})$ and $\kappa=\lambda_{n}$, which exist, so by the previous paragraph the formula holds exactly when $g\in\mathcal{M}^{+}(\mathbb{R}^{n},\mathcal{B}(\mathbb{R}^{n}))$ and $r=\int_{\mathbb{R}^{n}}g\,d\lambda_{n}$.