Proof of Predicative Formulas for Upper and Lower Darboux Sums, and the Maps and Sets of Darboux Sums over All Partitions

Auxiliary formulas. By Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field (iv), applied to the ordered field $\mathbb{R}$ (The Real Line: Standing Notation and Background for Calculus on Intervals (ii)), with its variables $t_{1},\dots,t_{6}$ renamed to the parameters $\mathbb{R}$, $+$, $\cdot$, $0$, $1$ and $\le$ of $\mathbb{R}$ by 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), there is a predicative formula $D(u,v,w)$ whose free variables are among the distinct set variables $u$, $v$, $w$ and these parameters, such that for all sets $u$, $v$ and $w$: $D(u,v,w)$ holds if and only if $u,v\in\mathbb{R}$ and $w=u-v$. Let $\mathrm{seg}(s,m)$ be the formula of Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness (i) and $\mathrm{fin}(A)$ that of Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness (ii), with the parameters $\mathbb{N}_{0}$, $\mathbb{N}$ and the order of $\mathbb{N}_{0}$ put for their class variables; and let $\mathrm{it}(w,m,g)$ be the formula of Iterated Operations Are Given by a Predicative Formula (i), with the parameters $\mathbb{R}$, the addition of $\mathbb{R}$, $\mathbb{N}$, and the order and the addition of $\mathbb{N}_{0}$ put for its class variables $X$, $F$, $Y$, $R$ and $P$. Let $\Phi$, $\mu$, $\iota$ and $\sigma$ be the formulas of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vi), 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), Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (viii) and Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (ix). Pair memberships $(u,v)\in F$ and $((u,v),w)\in F$ are the formulas of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iii) and Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iv); so are $u\le v$ and $u<v$, read as $(u,v)\in\,\le$ and $(u,v)\in\,<$ for the parameters $\le$ and $<$ (of $\mathbb{R}$ unless said otherwise), and $u+v=w$ in $\mathbb{N}_{0}$, read as $((u,v),w)\in+$ for the addition of $\mathbb{N}_{0}$. All these formulas are used with other set variables put for their displayed ones, by 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 the letters $c$, $C$, $d$, $e$, $g$, $i$, $j$, $m$, $n$, $p$, $q$, $s$, $t$, $u$, $v$, $w$ and $x$ below are set variables distinct from each other, from $a$, $b$, $f$, $P$, $z$ and from the parameters.

Proof of (i). The formula. Write $\langle t\rangle_{ab}$ for $t\in\mathbb{R}\wedge a\le t\wedge t\le b$. Let

$$\beta(a,b,f):\quad a\in\mathbb{R}\wedge b\in\mathbb{R}\wedge a<b\wedge\Phi(f)\wedge\forall t\,(\langle t\rangle_{ab}\Leftrightarrow\exists v\,((t,v)\in f))\wedge\forall t\,\forall v\,((t,v)\in f\Rightarrow v\in\mathbb{R})\wedge\exists c\,\exists C\,\bigl(c\in\mathbb{R}\wedge C\in\mathbb{R}\wedge\forall t\,\forall v\,((t,v)\in f\Rightarrow(c\le v\wedge v\le C))\bigr),$$ $$\pi(a,b,P):\quad\mathrm{fin}(P)\wedge\forall t\,(t\in P\Rightarrow\langle t\rangle_{ab})\wedge a\in P\wedge b\in P,$$ $$\lambda(P,n,x):\quad n\in\mathbb{N}\wedge\exists m\,\exists s\,\Bigl(((n,1),m)\in+\wedge\mathrm{seg}(s,m)\wedge\mu(x,s,P)\wedge\iota(x)\wedge\sigma(x,P)\wedge\forall i\,\forall j\,\forall u\,\forall v\,\bigl(((i,u)\in x\wedge(j,v)\in x\wedge(i,j)\in\,\le\wedge\neg\,i=j)\Rightarrow u<v\bigr)\Bigr),$$

the order and the addition in $\lambda$ being those of $\mathbb{N}_{0}$ except in $u<v$, and

$$\eta(x,i,p,q):\quad\exists j\,\bigl(((i,1),j)\in+\wedge(i,p)\in x\wedge(j,q)\in x\bigr),$$

with the addition of $\mathbb{N}_{0}$. In $\lambda$ and $\eta$, the $1$ in $((n,1),m)\in+$ and in $((i,1),j)\in+$ is the element $1$ of $\mathbb{N}_{0}$, taken as a parameter. Let $\Sigma(f,p,q,v)$ abbreviate $\exists t\,((t,v)\in f\wedge p\le t\wedge t\le q)$, and let

$$\sigma_{U}(f,p,q,w):\quad w\in\mathbb{R}\wedge\forall v\,(\Sigma(f,p,q,v)\Rightarrow v\le w)\wedge\forall c\,\bigl((c\in\mathbb{R}\wedge\forall v\,(\Sigma(f,p,q,v)\Rightarrow v\le c))\Rightarrow w\le c\bigr),$$

and $\sigma_{L}$ the formula obtained by replacing $v\le w$, $v\le c$ and $w\le c$ in it by $w\le v$, $c\le v$ and $c\le w$. For $\ast\in\{U,L\}$ let

$$\chi_{\ast}(f,n,x,g):\quad\exists s\,\Bigl(\mathrm{seg}(s,n)\wedge\mu(g,s,\mathbb{R})\wedge\forall i\,\forall e\,\bigl((i,e)\in g\Rightarrow\exists p\,\exists q\,\exists w\,\exists d\,(\eta(x,i,p,q)\wedge\sigma_{\ast}(f,p,q,w)\wedge D(q,p,d)\wedge((w,d),e)\in\cdot)\bigr)\Bigr),$$

with the multiplication $\cdot$ of $\mathbb{R}$, and

$$\psi_{\ast}(a,b,f,P,z):\quad\beta(a,b,f)\wedge\pi(a,b,P)\wedge\exists n\,\exists x\,\exists g\,\bigl(\lambda(P,n,x)\wedge\chi_{\ast}(f,n,x,g)\wedge\mathrm{it}(z,n,g)\bigr).$$

The free variables of $\psi_{U}$ and $\psi_{L}$ are among $a$, $b$, $f$, $P$, $z$ and the parameters.

Predicativity. The formulas $D$, $\mathrm{seg}$, $\mathrm{fin}$, $\mathrm{it}$, $\Phi$, $\mu$, $\iota$, $\sigma$ and the pair memberships are predicative by the results cited above, and $\psi_{U}$ and $\psi_{L}$ are built from them, from memberships and from equations by connectives and by quantifiers over set variables only; so no quantifier in them is applied to a class variable, and they are predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i).

Meaning. Fix sets $a$, $b$, $f$, $P$ and $z$, and let $\ast$ be $U$ or $L$. If $a,b\in\mathbb{R}$ and $a<b$, then $\langle t\rangle_{ab}$ holds exactly for $t\in[a,b]$ (Intervals of the Real Line (ii)).

First, $\beta(a,b,f)$ holds if and only if $a,b\in\mathbb{R}$, $a<b$ and $f$ is a bounded map $f:[a,b]\to\mathbb{R}$. Indeed, its conjuncts after $a<b$ other than the last are those of $\mu(f,[a,b],\mathbb{R})$ with $t\in[a,b]$ written out, so by 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) they hold if and only if $f$ is a map $f:[a,b]\to\mathbb{R}$; and then, by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i), the last conjunct says that there are $c,C\in\mathbb{R}$ with $c\le f(t)\le C$ for every $t\in[a,b]$. This holds with $c=-B$ and $C=B$ if $|f(t)|\le B$ for every $t$; conversely, if it holds, then $|f(t)|\le|c|+|C|$ for every $t\in[a,b]$.

Second, for $a,b\in\mathbb{R}$ with $a<b$, $\pi(a,b,P)$ holds if and only if $P$ is finite, $P\subseteq[a,b]$, $a\in P$ and $b\in P$, that is, by Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness (ii), Partitions of a Closed Interval, the Set of Partitions, and Refinements (i) and Partitions of a Closed Interval, the Set of Partitions, and Refinements (ii), if and only if $P\in\Pi_{a,b}$.

Let now $\beta(a,b,f)$ and $\pi(a,b,P)$ hold; otherwise $\psi_{\ast}(a,b,f,P,z)$ and the condition both fail. By Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness (i), Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (x) and Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i), $\lambda(P,n,x)$ holds if and only if $n\in\mathbb{N}$ and $x$ is a bijection $x:[n+1]\to P$ with $x_{i}<x_{j}$ for all $i,j\in[n+1]$ with $i<j$; so, by The Increasing Listing of a Partition: Endpoints, Lengths, Covering, Unions, Inserting a Point, Concatenation and Uniform Partitions (i), exactly for the $n$ and the increasing listing $x$ of $P$ used in Upper and Lower Darboux Sums of a Bounded Function on a Partition. For these $n$ and $x$ and for $i\in[n]$, $\eta(x,i,p,q)$ holds if and only if $p=x_{i}$ and $q=x_{i+1}$, by The Increasing Listing of a Partition: Endpoints, Lengths, Covering, Unions, Inserting a Point, Concatenation and Uniform Partitions (ii) and Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i). For $p=x_{i}$ and $q=x_{i+1}$, $\Sigma(f,p,q,v)$ holds if and only if $v=f(t)$ for some $t\in[x_{i},x_{i+1}]$, as the first components of the pairs in $f$ lie in $[a,b]\subseteq\mathbb{R}$; that is, by Upper and Lower Darboux Sums of a Bounded Function on a Partition (i), if and only if $v\in S_{i}$. Hence, by Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (i) and Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (iv), $\sigma_{U}(f,x_{i},x_{i+1},w)$ holds if and only if $w$ is an upper bound of $S_{i}$ in $\mathbb{R}$ below every upper bound, that is, $w=\sup S_{i}=M(i)$; and $\sigma_{L}(f,x_{i},x_{i+1},w)$ holds if and only if $w=\inf S_{i}=m(i)$, with $M$ and $m$ as in Upper and Lower Darboux Sums of a Bounded Function on a Partition (i). So, writing $M_{\ast}$ for $M$ if $\ast$ is $U$ and for $m$ if $\ast$ is $L$, and using Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness (i), 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 Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i), $\chi_{\ast}(f,n,x,g)$ holds if and only if $g$ is a map $g:[n]\to\mathbb{R}$ with $g(i)=M_{\ast}(i)\,(x_{i+1}-x_{i})$ for every $i\in[n]$; such a map exists by Upper and Lower Darboux Sums of a Bounded Function on a Partition (i) and Sets and Maps: Ordinary Notation (v), and it is unique by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv). Finally, for this $n\in\mathbb{N}$ and this map $g$ from $[n]$ to $\mathbb{R}$, $\mathrm{it}(z,n,g)$ holds if and only if $z=\sum_{i=1}^{n}g(i)$, by Iterated Operations Are Given by a Predicative Formula (i) and Iterated Operations: Finite Sums and Finite Products (iii), that is, by Upper and Lower Darboux Sums of a Bounded Function on a Partition (ii) and Upper and Lower Darboux Sums of a Bounded Function on a Partition (iii), if and only if $z=U(f,P)$, respectively $z=L(f,P)$.

So, under every assignment, $\psi_{U}(a,b,f,P,z)$ holds if and only if $a,b\in\mathbb{R}$, $a<b$, $f$ is a bounded map $f:[a,b]\to\mathbb{R}$, $P\in\Pi_{a,b}$ and $z=U(f,P)$: $\psi_{U}$ expresses this condition, as in Conditions Expressed by a Predicative Formula, and Guards (ii), and $\psi_{L}$ expresses the condition with $L(f,P)$. When $a$ and $b$ are taken as parameters with fixed values $a<b$ in $\mathbb{R}$, the same formulas, whose free variables are then among $f$, $P$, $z$ and the parameters, express the conditions on $f$, $P$ and $z$.

Proof of (ii). Let $\ast$ be $U$ or $L$, and take $a$, $b$ and $f$ as parameters with their given values. By (i), for every $R\in\Pi_{a,b}$ and every set $z$, $\psi_{\ast}(a,b,f,R,z)$ holds if and only if $z=\ast(f,R)$, which is a real number by Upper and Lower Darboux Sums of a Bounded Function on a Partition (ii) and Upper and Lower Darboux Sums of a Bounded Function on a Partition (iii). Let

$$\Gamma_{\ast}=\{p\in\Pi_{a,b}\times\mathbb{R}:\exists R\,\exists z\,(p=(R,z)\wedge\psi_{\ast}(a,b,f,R,z))\},$$

with $p=(R,z)$ the formula of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (ii); its formula is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i), so $\Gamma_{\ast}$ is a set by Sets and Maps: Ordinary Notation (iii), $\Pi_{a,b}\times\mathbb{R}$ being a set by Sets and Maps: Ordinary Notation (iv). Its elements are the pairs $(R,\ast(f,R))$ with $R\in\Pi_{a,b}$. Hence $\Gamma_{\ast}$ is a relation whose domain is $\Pi_{a,b}$, each $R\in\Pi_{a,b}$ is the first component of exactly one of its pairs, and its second components lie in $\mathbb{R}$; so $\Gamma_{\ast}$ is a map $\Gamma_{\ast}:\Pi_{a,b}\to\mathbb{R}$ with $\Gamma_{\ast}(R)=\ast(f,R)$ for every $R\in\Pi_{a,b}$, by Functions, Values of a Function, and Functions from One Class to Another (iii) and Functions, Values of a Function, and Functions from One Class to Another (ii). Every map from $\Pi_{a,b}$ to $\mathbb{R}$ with these values equals $\Gamma_{\ast}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv).

The class $\{\ast(f,R):R\in\Pi_{a,b}\}$ is $\{s:\exists R\,(R\in\Pi_{a,b}\wedge\psi_{\ast}(a,b,f,R,s))\}$, formed by class abstraction from a predicative formula; by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (viii) and (i), a set $s$ is an element of it if and only if $s=\ast(f,R)$ for some $R\in\Pi_{a,b}$. All its elements lie in $\mathbb{R}$, so it has the same elements as the set $\{s\in\mathbb{R}:\exists R\,(R\in\Pi_{a,b}\wedge\psi_{\ast}(a,b,f,R,s))\}$ of Sets and Maps: Ordinary Notation (iii), and it equals that set, by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation (ii); so it is a set and a subset of $\mathbb{R}$.