Proof of Addition and Multiplication of Real Numbers Are Binary Operations: Values and Membership

Each result cited is universally quantified over the data in its own statement, and is applied to the data named where it is cited. By The Real Numbers §reals, $\mathbb{R}=C$ with $C$ as in Construction of the Dedekind Cuts: They Form a Set Totally Ordered by Inclusion, Closed under Sums, Negatives and Products of Nonnegative Cuts §cuts, and $\mathbb{R}$ is a set by Construction of the Dedekind Cuts: They Form a Set Totally Ordered by Inclusion, Closed under Sums, Negatives and Products of Nonnegative Cuts §set. For a set $x$, $0^{*}\subseteq x$ is the defined predicate $\forall v\,(v\in0^{*}\Rightarrow v\in x)$; write $\pi(x)$ for this formula.

Values (clause values). Let $x,y\in\mathbb{R}$. Then $x+y=x\oplus y\in\mathbb{R}$ by The Real Numbers §operations and Construction of the Dedekind Cuts: They Form a Set Totally Ordered by Inclusion, Closed under Sums, Negatives and Products of Nonnegative Cuts §sum. If $0^{*}\subseteq x$, then $|x|_{C}=x$; otherwise $|x|_{C}=\ominus x$, which lies in $\mathbb{R}$ by Construction of the Dedekind Cuts: They Form a Set Totally Ordered by Inclusion, Closed under Sums, Negatives and Products of Nonnegative Cuts §negative and satisfies $0^{*}\subseteq\ominus x$ by Construction of the Dedekind Cuts: They Form a Set Totally Ordered by Inclusion, Closed under Sums, Negatives and Products of Nonnegative Cuts §absolute. In both cases $|x|_{C}\in\mathbb{R}$ and $0^{*}\subseteq|x|_{C}$, and likewise for $y$. Hence $p=|x|_{C}\odot|y|_{C}$ lies in $\mathbb{R}$ by Construction of the Dedekind Cuts: They Form a Set Totally Ordered by Inclusion, Closed under Sums, Negatives and Products of Nonnegative Cuts §product, and so does $\ominus p$ by Construction of the Dedekind Cuts: They Form a Set Totally Ordered by Inclusion, Closed under Sums, Negatives and Products of Nonnegative Cuts §negative; the product $x\cdot y$ of The Real Numbers §operations is $p$ or $\ominus p$, so $x\cdot y\in\mathbb{R}$. In particular $x+y$, $|x|_{C}$, $|x|_{C}\odot|y|_{C}$ and $x\cdot y$ are sets.

Defining formulas. We construct explicit predicative formulas $\Theta_{+}(z,x,y)$ and $\Theta_{\cdot}(z,x,y)$, in the set variables $x$, $y$ and $z$, whose only abbreviations are ordered pairs, and show that, for all sets $x$, $y$ and $z$, $\Theta_{+}(z,x,y)$ holds if and only if $x\in\mathbb{R}$, $y\in\mathbb{R}$ and $z=x+y$, and $\Theta_{\cdot}(z,x,y)$ holds if and only if $x\in\mathbb{R}$, $y\in\mathbb{R}$ and $z=x\cdot y$. Their parameters are the sets $\mathbb{Q}$, $\mathbb{R}$, $0$ and $0^{*}$, where $0^{*}$ is a set since $0^{*}\in C$ by Construction of the Dedekind Cuts: They Form a Set Totally Ordered by Inclusion, Closed under Sums, Negatives and Products of Nonnegative Cuts §rational, and the classes named next.

Write $+_{\mathbb{Q}}$, $\cdot_{\mathbb{Q}}$, $-_{\mathbb{Q}}$ and $\le$ for the sum, product, negation and order of $\mathbb{Q}$, which by The Integers and the Rational Numbers, with the Natural Numbers and the Integers Identified with Subsets of the Rationals §rationals, The Rational Numbers §operations and Construction of the Rationals: Pairs of an Integer and a Natural Number up to Equal Ratios, with Sum, Product, Negation and Order §operations are two binary operations on $\mathbb{Q}$, a map from $\mathbb{Q}$ to $\mathbb{Q}$ and a relation on $\mathbb{Q}$; and let $<$ be the strict relation of $\le$, as in Construction of the Dedekind Cuts: They Form a Set Totally Ordered by Inclusion, Closed under Sums, Negatives and Products of Nonnegative Cuts §cuts. For $u,v\in\mathbb{Q}$, $u-v=u+(-v)$ by The Rational Numbers §operations, and $u\le v$ and $u<v$ mean $(u,v)\in{\le}$ and $(u,v)\in{<}$ by Partial and Total Orders on a Set and the Associated Strict Relation §partial and Partial and Total Orders on a Set and the Associated Strict Relation §strict. For all sets $u$, $v$ and $w$ with $u,v\in\mathbb{Q}$: $w=u+v$ if and only if $((u,v),w)\in{+_{\mathbb{Q}}}$, and $w=u\cdot v$ if and only if $((u,v),w)\in{\cdot_{\mathbb{Q}}}$, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §operation; and $w=-u$ if and only if $(u,w)\in{-_{\mathbb{Q}}}$, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §value, since $\operatorname{dom}{-_{\mathbb{Q}}}=\mathbb{Q}$ by Functions, Values of a Function, and Functions from One Class to Another §map. These formulas, and $(u,v)\in{\le}$ and $(u,v)\in{<}$, are predicative 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 §operation-membership 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 §pair-membership. Let

$$\sigma_{\oplus}(w,x,y):\quad w\in\mathbb{Q}\wedge\exists u\,\exists v\,(u\in\mathbb{Q}\wedge v\in\mathbb{Q}\wedge u\in x\wedge v\in y\wedge((u,v),w)\in{+_{\mathbb{Q}}}),$$ $$\sigma_{\ominus}(w,x):\quad w\in\mathbb{Q}\wedge\exists v\,\bigl(v\in\mathbb{Q}\wedge(0,v)\in{<}\wedge\exists n\,\exists n'\,\exists m\,((w,n)\in{-_{\mathbb{Q}}}\wedge(v,n')\in{-_{\mathbb{Q}}}\wedge((n,n'),m)\in{+_{\mathbb{Q}}}\wedge m\notin x)\bigr),$$ $$\sigma_{\odot}(w,x,y):\quad w\in0^{*}\vee\bigl(w\in\mathbb{Q}\wedge\exists u\,\exists v\,(u\in\mathbb{Q}\wedge v\in\mathbb{Q}\wedge u\in x\wedge v\in y\wedge(0,u)\in{\le}\wedge(0,v)\in{\le}\wedge((u,v),w)\in{\cdot_{\mathbb{Q}}})\bigr).$$

In $\sigma_{\ominus}$ the bound variable $u$ of $\ominus x$ is renamed $w$. For $w,v\in\mathbb{Q}$, $-w-v$ is $(-w)+(-v)$ by The Rational Numbers §operations, a nested use of the defined set symbols $-$ and $+$ of $\mathbb{Q}$, used properly under the guards $w\in\mathbb{Q}$ and $v\in\mathbb{Q}$, since $-w,-v\in\mathbb{Q}$ as $-_{\mathbb{Q}}$ maps $\mathbb{Q}$ to $\mathbb{Q}$. Eliminating these terms from the atomic part $-w-v\notin x$, innermost first, by the rule of Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-set-symbols, and rewriting each defining formula by the equivalences above, $-w-v\notin x$ holds if and only if $\exists n\,\exists n'\,\exists m\,((w,n)\in{-_{\mathbb{Q}}}\wedge(v,n')\in{-_{\mathbb{Q}}}\wedge((n,n'),m)\in{+_{\mathbb{Q}}}\wedge m\notin x)$, the witnesses being $n=-w$, $n'=-v$ and $m=n+n'$. By the equivalences listed above and this one, $\sigma_{\oplus}$, $\sigma_{\ominus}$ and $\sigma_{\odot}$ are the defining formulas of $x\oplus y$, $\ominus x$ and $x\odot y$ in Construction of the Dedekind Cuts: They Form a Set Totally Ordered by Inclusion, Closed under Sums, Negatives and Products of Nonnegative Cuts §constructions, written without the rational symbols, the union in $x\odot y$ being the class term of The Boolean Operations on Classes, Disjointness, and the Universal Class §operations and $\{w\in\mathbb{Q}:\dots\}$ that of Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §restricted. So, for $x,y\in\mathbb{R}$, $x\oplus y$ has the same elements as the class abstraction $\{w:\sigma_{\oplus}(w,x,y)\}$, and $\ominus x$ and $x\odot y$ the same elements as $\{w:\sigma_{\ominus}(w,x)\}$ and $\{w:\sigma_{\odot}(w,x,y)\}$, by the preceding equivalences; hence they are equal to these abstractions by Axiom of Extensionality for Classes. Hence, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §class-terms, applied to these abstractions, for $x,y\in\mathbb{R}$ and every set $z$: $z=x\oplus y$ if and only if $\alpha(z,x,y)$, $z=\ominus x$ if and only if $\nu(z,x)$, and $z=x\odot y$ if and only if $\mu(z,x,y)$, where

$$\alpha(z,x,y):\ \forall w\,(w\in z\Leftrightarrow\sigma_{\oplus}(w,x,y)),\qquad\nu(z,x):\ \forall w\,(w\in z\Leftrightarrow\sigma_{\ominus}(w,x)),\qquad\mu(z,x,y):\ \forall w\,(w\in z\Leftrightarrow\sigma_{\odot}(w,x,y)).$$

Let moreover

$$\beta(a,x):\ (\pi(x)\wedge a=x)\vee(\neg\pi(x)\wedge\nu(a,x)),\qquad\chi(z,p,x,y):\ ((\pi(x)\Leftrightarrow\pi(y))\wedge z=p)\vee(\neg(\pi(x)\Leftrightarrow\pi(y))\wedge\nu(z,p)).$$

All of $\pi$, $\sigma_{\oplus}$, $\sigma_{\ominus}$, $\sigma_{\odot}$, $\alpha$, $\nu$, $\mu$, $\beta$ and $\chi$ are built from atomic formulas and the predicative formulas above by $\neg$, $\wedge$, $\vee$, $\Rightarrow$, $\Leftrightarrow$ and quantifiers over set variables, so they are predicative by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §predicative.

The sum. By The Real Numbers §operations, $x+y=x\oplus y$ for $x,y\in\mathbb{R}$; so, for all sets $x$, $y$ and $z$, $x\in\mathbb{R}\wedge y\in\mathbb{R}\wedge z=x+y$ holds if and only if the predicative formula $\Theta_{+}(z,x,y):\ x\in\mathbb{R}\wedge y\in\mathbb{R}\wedge\alpha(z,x,y)$ holds.

The product. Let $x,y\in\mathbb{R}$. If $\pi(x)$, then $\beta(a,x)$ holds exactly for $a=x$; otherwise exactly for the sets $a$ with $\nu(a,x)$, that is, for $a=\ominus x$. So $|x|_{C}$, a set by the clause values, is the only set $a$ with $\beta(a,x)$, and likewise $|y|_{C}$ for $\beta(b,y)$. For $a,b\in\mathbb{R}$ with $\pi(a)$ and $\pi(b)$, $a\odot b$ lies in $\mathbb{R}$ by Construction of the Dedekind Cuts: They Form a Set Totally Ordered by Inclusion, Closed under Sums, Negatives and Products of Nonnegative Cuts §product, so it is a set and the only set $p$ with $\mu(p,a,b)$. For $p\in\mathbb{R}$, $\nu(z,p)$ holds if and only if $z=\ominus p$; so, by The Real Numbers §operations, $z=x\cdot y$ holds if and only if $\chi(z,|x|_{C}\odot|y|_{C},x,y)$. Three applications of Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §elimination remove $|x|_{C}\odot|y|_{C}$, $|y|_{C}$ and $|x|_{C}$ in turn. Each application below is made with the parameters $\mathbb{Q}$, $\mathbb{R}$, $0$, $0^{*}$, $+_{\mathbb{Q}}$, $\cdot_{\mathbb{Q}}$, $-_{\mathbb{Q}}$, $\le$ and $<$ at their fixed values, for which the stated uniqueness holds.

First, with $k=2$, $v_{1},v_{2}$ the variables $a,b$, the eliminated variable $p$, $\theta=\mu(p,a,b)$, $\gamma(a,b):\ a\in\mathbb{R}\wedge b\in\mathbb{R}\wedge\pi(a)\wedge\pi(b)$ and $\varphi=\chi(z,p,x,y)$, the sets $x$, $y$ and $z$ being parameters: for $a,b$ satisfying $\gamma$, exactly one set $p$ satisfies $\mu(p,a,b)$, namely $a\odot b$, as shown above. So $\psi_{1}(a,b):\ \gamma(a,b)\wedge\exists p\,(\mu(p,a,b)\wedge\chi(z,p,x,y))$ is predicative, and, for $a,b$ satisfying $\gamma$, $\psi_{1}(a,b)$ holds if and only if $\chi(z,a\odot b,x,y)$. We use this at $a=|x|_{C}$ and $b=|y|_{C}$ for $x,y\in\mathbb{R}$, which satisfy $\gamma$ by the clause values.

Second, with $k=0$, the eliminated variable $b$, $\theta=\beta(b,y)$, the guard $y\in\mathbb{R}$ and $\varphi=\psi_{1}(a,b)$, the sets $a$, $x$, $y$ and $z$ being parameters: if $y\in\mathbb{R}$, exactly one set $b$ satisfies $\beta(b,y)$, namely $|y|_{C}$. So $\psi_{2}(a):\ y\in\mathbb{R}\wedge\exists b\,(\beta(b,y)\wedge\psi_{1}(a,b))$ is predicative, and, if $y\in\mathbb{R}$, $\psi_{2}(a)$ holds if and only if $\psi_{1}(a,|y|_{C})$.

Third, with $k=0$, the eliminated variable $a$, $\theta=\beta(a,x)$, the guard $x\in\mathbb{R}\wedge y\in\mathbb{R}$ and $\varphi=\psi_{2}(a)$, the sets $x$, $y$ and $z$ being parameters: if $x,y\in\mathbb{R}$, exactly one set $a$ satisfies $\beta(a,x)$, since $x\in\mathbb{R}$; it is $|x|_{C}$. So

$$\Theta_{\cdot}(z,x,y):\ x\in\mathbb{R}\wedge y\in\mathbb{R}\wedge\exists a\,\Bigl(\beta(a,x)\wedge y\in\mathbb{R}\wedge\exists b\,\bigl(\beta(b,y)\wedge a\in\mathbb{R}\wedge b\in\mathbb{R}\wedge\pi(a)\wedge\pi(b)\wedge\exists p\,(\mu(p,a,b)\wedge\chi(z,p,x,y))\bigr)\Bigr),$$

which is $x\in\mathbb{R}\wedge y\in\mathbb{R}\wedge\exists a\,(\beta(a,x)\wedge\psi_{2}(a))$, is predicative, and, if $x,y\in\mathbb{R}$, it holds if and only if $\psi_{2}(|x|_{C})$.

Hence, for all sets $x$, $y$ and $z$: if $x\in\mathbb{R}$ and $y\in\mathbb{R}$, then $\Theta_{\cdot}(z,x,y)$ holds if and only if $\psi_{1}(|x|_{C},|y|_{C})$, that is, if and only if $\chi(z,|x|_{C}\odot|y|_{C},x,y)$, that is, if and only if $z=x\cdot y$; and otherwise $\Theta_{\cdot}(z,x,y)$ fails. So $\Theta_{\cdot}(z,x,y)$ holds if and only if $x\in\mathbb{R}$, $y\in\mathbb{R}$ and $z=x\cdot y$.

Defined set symbols. Thus, for $x,y\in\mathbb{R}$, the sum $x+y$ is the unique set $z$ with $\Theta_{+}(z,x,y)$ and the product $x\cdot y$ the unique set $z$ with $\Theta_{\cdot}(z,x,y)$, both being sets by the clause values. So $x+y$ and $x\cdot y$ are defined set symbols with set arguments $x$ and $y$ and the predicative defining formulas $\Theta_{+}$ and $\Theta_{\cdot}$; they are used properly at arguments $v\in\mathbb{R}$ and $w\in\mathbb{R}$, since there the hypotheses $v\in\mathbb{R}$ and $w\in\mathbb{R}$ ensure that exactly one such set exists. So Maps and Relations Given by Formulas §binary applies with $t(v,w)$ these symbols, as follows.

Binary operations (clause operation). By the clause values, $t(v,w)\in\mathbb{R}$ for all $v,w\in\mathbb{R}$, so Maps and Relations Given by Formulas §binary applies with $b=c=d=\mathbb{R}$, first with $t(v,w)=v+w$ and then with $t(v,w)=v\cdot w$. It gives exactly one map $f:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ with $f((x,y))=x+y$ for all $x,y\in\mathbb{R}$, and exactly one map $g:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ with $g((x,y))=x\cdot y$ for all $x,y\in\mathbb{R}$. In the statement, $+$ and $\cdot$ are the maps $\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ with these values; by the uniqueness in Maps and Relations Given by Formulas §binary they are well determined, $+=f$ and $\cdot=g$, and they are the only maps $\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ with these values. Since $\mathbb{R}$ is a set, they are binary operations on $\mathbb{R}$ by Binary Operations on a Set §operation, with values $x+y$ and $x\cdot y$ at $(x,y)$ for $x,y\in\mathbb{R}$.

Membership (clause membership). Let $x$, $y$ and $z$ be sets. By Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §operation, applied with $a=\mathbb{R}$ and the binary operation $+$, $((x,y),z)\in{+}$ if and only if $x\in\mathbb{R}$, $y\in\mathbb{R}$ and $z$ is the value of $+$ at $(x,y)$, which is the sum $x+y$ of The Real Numbers §operations by the clause operation. Likewise, applied with the binary operation $\cdot$, $((x,y),z)\in{\cdot}$ if and only if $x\in\mathbb{R}$, $y\in\mathbb{R}$ and $z$ is the value of $\cdot$ at $(x,y)$, which is the product $x\cdot y$ of The Real Numbers §operations by the clause operation.