Proof of 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

Each result cited is universally quantified over the data in its own statement.

Predicativity and free variables. 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 §pair-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 §operation-membership, for variables $q_{1}$, $q_{2}$, $q_{3}$ and $s$ of either kind the formulas $(q_{1},q_{2})\in s$ and $((q_{1},q_{2}),q_{3})\in s$ are predicative and, when sets are assigned to $q_{1}$, $q_{2}$ and $q_{3}$, hold if and only if the corresponding ordered pair is an element of the value of $s$. They are formed in the statement 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 by eliminating ordered pairs as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-set-symbols, which introduces only bound variables, and then renaming as in Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity §renaming; so their free variables are among $q_{1}$, $q_{2}$, $q_{3}$ and $s$. Every formula displayed in the statement or below is built from atomic formulas as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §formula, from $\varphi$, from the formula $\Phi$ 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 §function and from such pair formulas by $\neg$, $\wedge$, $\vee$, $\Rightarrow$, and $\exists$ and $\forall$ applied to set variables only. By Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §formula, $\vee$, $\Rightarrow$ and $\forall v$ abbreviate strings built with $\neg$, $\wedge$ and $\exists v$, and the elimination of abbreviations in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-symbols acts on atomic parts, so after it no part of such a formula has the form $\exists X\,\psi$ with $X$ a class variable: each such formula is predicative by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §predicative. Its free variables are among those of its parts, less the variables quantified over. Since Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §formula forms only parenthesised binary conjunctions, a chain $\psi_{1}\wedge\psi_{2}\wedge\dots\wedge\psi_{n}$ is read nested from the left, as $(\dots((\psi_{1}\wedge\psi_{2})\wedge\psi_{3})\dots\wedge\psi_{n})$; by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §reading it holds if and only if each $\psi_{i}$ holds.

The clause value-substitution. Let $z'$ be a set variable other than $x$, $z$ and $F$ and not occurring in $\varphi$, let $\theta$ be $(x,z)\in F$, and let $\gamma$ be $\Phi(F)\wedge\exists z'\,((x,z')\in F)$, with $\Phi(F)$ 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 §function, which holds if and only if the value $F$ is a function; $\theta$ and $\gamma$ are predicative by the first paragraph. Under an assignment in which $\gamma$ holds, $F$ is a function, and by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §value the sets $c$ with $(x,c)\in F$ are exactly those with $x\in\operatorname{dom}F$ and $c=F(x)$; as one such set exists, exactly one set $z$ satisfies $\theta$, namely $F(x)$. So Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §elimination, with $k=1$, $v_{1}$ the variable $x$, and the free variables of $\theta$, $\gamma$ and $\varphi$ other than $x$ and $z$ as parameters, gives: whenever $\gamma$ holds, $\varphi(F(x))$, $\exists z\,(\theta\wedge\varphi)$ and $\forall z\,(\theta\Rightarrow\varphi)$ are equivalent. Now fix an assignment in which $F$ is a function, so that $\Phi(F)$ holds. If $x\in\operatorname{dom}F$, then $F(x)$ is a set by Functions, Values of a Function, and Functions from One Class to Another §value and $(x,F(x))\in F$ by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §value, so $\gamma$ holds, and both formulas hold if and only if $\varphi(F(x))$. If $x\notin\operatorname{dom}F$, then by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §value no set $c$ satisfies $(x,c)\in F$, so by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §reading $\exists z\,(\theta\wedge\varphi)$ fails and $\forall z\,(\theta\Rightarrow\varphi)$ holds, as the clause asserts. Both formulas are predicative by the first paragraph.

The clause operation-substitution. If $x$ and $y$ are the same variable, read $v_{1},v_{2}$ below as that one variable, with $k=1$. Let $z'$ be a set variable other than $x$, $y$, $z$ and $\ast$ and not occurring in $\varphi$, let $\theta$ be $((x,y),z)\in\ast$, and let $\gamma$ be $\Phi(\ast)\wedge\exists z'\,(((x,y),z')\in\ast)$, predicative by the first paragraph. Under an assignment in which $\gamma$ holds, $\ast$ is a function 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 §function, the ordered pair $(x,y)$ is a set by The Ordered Pair of Two Sets and Nested Tuples §pair, and by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §value the sets $c$ with $((x,y),c)\in\ast$ are exactly those with $(x,y)\in\operatorname{dom}\ast$ and $c=\ast((x,y))$; as one such set exists, exactly one set $z$ satisfies $\theta$. So Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §elimination, with $k=2$, $v_{1}$ and $v_{2}$ the variables $x$ and $y$, and the free variables of $\theta$, $\gamma$ and $\varphi$ other than $x$, $y$ and $z$ as parameters, gives: whenever $\gamma$ holds, $\varphi(\ast((x,y)))$, $\exists z\,(\theta\wedge\varphi)$ and $\forall z\,(\theta\Rightarrow\varphi)$ are equivalent. Now fix an assignment in which $a$ is a set and $\ast$ a binary operation on $a$; then $\ast$ is a function by Binary Operations on a Set §operation and Functions, Values of a Function, and Functions from One Class to Another §map, so $\Phi(\ast)$ holds, and by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §operation, for every set $c$: $((x,y),c)\in\ast$ if and only if $x\in a$, $y\in a$ and $c=x\ast y$. If $x\in a$ and $y\in a$, then $x\ast y=\ast((x,y))$ is a set with $((x,y),x\ast y)\in\ast$ by Binary Operations on a Set §notation, so $\gamma$ holds, and both formulas hold if and only if $\varphi(x\ast y)$. Otherwise no set $c$ satisfies $((x,y),c)\in\ast$, so $\exists z\,(\theta\wedge\varphi)$ fails and $\forall z\,(\theta\Rightarrow\varphi)$ holds, as the clause asserts. Both formulas are predicative by the first paragraph.

The field clauses. Let $t_{1},\dots,t_{6}$ be distinct variables, other than $x$, $y$, $z$ and the bound variables used below, to which $r$, $+$, $\cdot$, $0$, $1$ and $\le$ are assigned, in this order. Let $w$ and $w'$ be distinct set variables other than $x$, $y$, $z$ and $t_{1},\dots,t_{6}$. Fix an assignment under which $t_{1},\dots,t_{6}$ have the values $r$, $+$, $\cdot$, $0$, $1$ and $\le$, and sets are assigned to the remaining set variables. By Ordered Fields §ordered-field, $r$, with $+$, $\cdot$, $0$ and $1$, is a field and $\le$ is a total order on $r$; by the framing of Fields §field, $r$ is a set, $+$ and $\cdot$ are binary operations on $r$ and $0,1\in r$, and by Fields §field, $r$, with $+$, $\cdot$, $0$ and $1$, is a commutative ring. The elements of $r$ are sets by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §objects; this is used below without further mention. By Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §operation, applied to $r$ and $+$ and to $r$ and $\cdot$:

$$\text{for all sets }u,v,c:\quad((u,v),c)\in{+}\iff(u\in r\wedge v\in r\wedge c=u+v),\qquad((u,v),c)\in{\cdot}\iff(u\in r\wedge v\in r\wedge c=u\cdot v).\qquad(\mathrm{E})$$

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 §operation-membership and $(\mathrm{E})$, a formula $((q_{1},q_{2}),q_{3})\in t_{2}$ holds if and only if the values of $q_{1}$ and $q_{2}$ lie in $r$ and the value of $q_{3}$ is their sum, and likewise for $t_{3}$ and products. 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 §pair-membership, for every set $u$ the formula $(t_{4},u)\in t_{6}$, with $u$ assigned to a set variable in the second place, holds if and only if $(0,u)\in{\le}$, that is, $0\le u$ in the relation notation of Relations, Domain, Range, Inverse and Composition §relation. As in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-set-symbols, where the left conjunct of $x\in A\wedge\varphi$ is among the hypotheses under which a defined set symbol in $\varphi$ is used, the conditions of the field clauses are read from left to right: $-x$, $x-y$, $|x|$, $|x-y|$, $y^{-1}$ and $x/y$ are used under the conjuncts to their left, and a condition whose left conjunct fails is false. Below, letters standing for set variables also stand for the sets assigned to them, and each formula is predicative with free variables among the displayed ones and $t_{1},\dots,t_{6}$, by the first paragraph.

(i) Negatives. For distinct set variables $u$ and $v$ among $x$, $y$, $z$, $w$ and $w'$, let $\nu(u,v)$ be the formula $v\in t_{1}\wedge((u,v),t_{4})\in t_{2}$. It holds if and only if $u\in r$ and $v=-u$. Indeed, $\nu(u,v)$ holds if and only if $v\in r$, $u\in r$ and $0=u+v$. If $u\in r$ and $v=-u$, then by Negatives, Differences, Reciprocals and Quotients §negative $v$ is an element of $r$ with $u+v=0$, so $\nu(u,v)$ holds. Conversely, if $\nu(u,v)$ holds, then $u\in r$, $v\in r$ and $u+v=0$; by Additive and Multiplicative Inverses Are Unique §negative exactly one element of $r$ has sum $0$ with $u$, and by Negatives, Differences, Reciprocals and Quotients §negative it is $-u$, so $v=-u$. In particular $\nu(x,z)$ holds if and only if $x\in r\wedge z=-x$ does, which proves the clause negative-formula.

(ii) Differences. For distinct set variables $u$, $v$ and $v'$ among $x$, $y$, $z$ and $w'$, let $\delta(u,v,v')$ be the formula $\exists w\,(\nu(v,w)\wedge((u,w),v')\in t_{2})$. It holds if and only if $u\in r$, $v\in r$ and $v'=u-v$. Indeed, if $u,v\in r$ and $v'=u-v$, then $-v\in r$ and $\nu(v,-v)$ by (i), and $v'=u+(-v)$ by Negatives, Differences, Reciprocals and Quotients §negative, so $((u,-v),v')\in{+}$ by $(\mathrm{E})$, and $-v$ witnesses $\exists w$. Conversely, if a set $w$ satisfies $\nu(v,w)$ and $((u,w),v')\in{+}$, then $v\in r$ and $w=-v$ by (i), and $u\in r$ and $v'=u+w=u+(-v)$ by $(\mathrm{E})$, which is $u-v$ by Negatives, Differences, Reciprocals and Quotients §negative. In particular $\delta(x,y,z)$ holds if and only if $x\in r\wedge y\in r\wedge z=x-y$ does, which proves the clause difference-formula.

(iii) Absolute values. For distinct set variables $u$ and $v$ among $x$, $z$ and $w'$, let $\alpha(u,v)$ be the formula

$$u\in t_{1}\wedge\bigl(((t_{4},u)\in t_{6}\wedge v=u)\vee(\neg((t_{4},u)\in t_{6})\wedge\nu(u,v))\bigr).$$

It holds if and only if $u\in r$ and $v=|u|$. Indeed, let $u\in r$. If $0\le u$, then $|u|=u$ by Absolute Value in an Ordered Field §absolute-value, the second disjunct fails, and the first holds if and only if $v=u$; so $\alpha(u,v)$ holds if and only if $v=|u|$. If not $0\le u$, then $|u|=-u$ by Absolute Value in an Ordered Field §absolute-value, the first disjunct fails, and the second holds if and only if $\nu(u,v)$, that is, by (i), if and only if $v=-u$; so again $\alpha(u,v)$ holds if and only if $v=|u|$. If $u\notin r$, then $\alpha(u,v)$ fails. In particular $\alpha(x,z)$ holds if and only if $x\in r\wedge z=|x|$ does, which proves the clause absolute-value-formula.

(iv) Distances. The formula $\exists w'\,(\delta(x,y,w')\wedge\alpha(w',z))$ holds if and only if $x\in r\wedge y\in r\wedge z=|x-y|$ does. Indeed, if $x,y\in r$ and $z=|x-y|$, then $-y\in r$ by Negatives, Differences, Reciprocals and Quotients §negative, so $x-y=x+(-y)$ lies in $r$ by Binary Operations on a Set §notation; it witnesses $\exists w'$, as $\delta(x,y,x-y)$ holds by (ii) and $\alpha(x-y,z)$ by (iii). Conversely, if a set $w'$ satisfies $\delta(x,y,w')$ and $\alpha(w',z)$, then $x,y\in r$ and $w'=x-y$ by (ii), and $z=|w'|=|x-y|$ by (iii). This proves the clause distance-formula.

(v) Reciprocals. For distinct set variables $u$ and $v$ among $y$, $z$ and $w$, let $\rho(u,v)$ be the formula $u\in t_{1}\wedge\neg(u=t_{4})\wedge v\in t_{1}\wedge((u,v),t_{5})\in t_{3}$. It holds if and only if $u\in r$, $u\neq0$ and $v=u^{-1}$. Indeed, $\rho(u,v)$ holds if and only if $u\in r$, $u\neq0$, $v\in r$ and $1=u\cdot v$. If $u\in r$, $u\neq0$ and $v=u^{-1}$, then by Negatives, Differences, Reciprocals and Quotients §reciprocal $v$ is an element of $r$ with $u\cdot v=1$, so $\rho(u,v)$ holds. Conversely, if $\rho(u,v)$ holds, then $u\in r$, $u\neq0$, $v\in r$ and $u\cdot v=1$; by Additive and Multiplicative Inverses Are Unique §reciprocal exactly one element of $r$ has product $1$ with $u$, and by Negatives, Differences, Reciprocals and Quotients §reciprocal it is $u^{-1}$, so $v=u^{-1}$. In particular $\rho(y,z)$ holds if and only if $y\in r\wedge y\neq0\wedge z=y^{-1}$ does, which proves the clause reciprocal-formula.

(vi) Quotients. The formula $\exists w\,(\rho(y,w)\wedge((x,w),z)\in t_{3})$ holds if and only if $x\in r\wedge y\in r\wedge y\neq0\wedge z=x/y$ does. Indeed, if $x,y\in r$, $y\neq0$ and $z=x/y$, then $y^{-1}\in r$ and $\rho(y,y^{-1})$ by (v), and $z=x\cdot y^{-1}$ by Negatives, Differences, Reciprocals and Quotients §reciprocal, so $((x,y^{-1}),z)\in{\cdot}$ by $(\mathrm{E})$, and $y^{-1}$ witnesses $\exists w$. Conversely, if a set $w$ satisfies $\rho(y,w)$ and $((x,w),z)\in{\cdot}$, then $y\in r$, $y\neq0$ and $w=y^{-1}$ by (v), and $x\in r$ and $z=x\cdot w=x\cdot y^{-1}$ by $(\mathrm{E})$, which is $x/y$ by Negatives, Differences, Reciprocals and Quotients §reciprocal. This proves the clause quotient-formula.

The formulas of (i) to (vi) do not depend on the assignment, and the free variables of each are among the set variables displayed in its condition and $t_{1},\dots,t_{6}$, the variables $w$ and $w'$ being bound in them: $x$ and $z$ for (i) and (iii), $y$ and $z$ for (v), and $x$, $y$ and $z$ for (ii), (iv) and (vi).