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

In the setting of Class Theory NBG: the Axioms, Standing Conventions and Basic Notation, formulas may be written with abbreviations and predicative is meant as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-symbols, with set variables, class variables and free variables as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §symbols and Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §free, to which sets and classes are assigned as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §reading.

In the clauses value-substitution and operation-substitution, $\varphi$ is a predicative formula in which $z$ and further variables of either kind may occur free; under an assignment, each variable also denotes its value, and for a set $c$, $\varphi(c)$ states that $\varphi$ holds when $c$ is assigned to $z$ and the other free variables keep their values.

¶ Let $x$ and $z$ be set variables and $F$ a variable of either kind, $x$, $z$ and $F$ pairwise distinct, and let $(x,z)\in F$ be 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 §pair-membership. The formula $\exists z\,((x,z)\in F\wedge\varphi)$ is predicative, and, under every assignment in which the value of $F$ is a function, it holds if and only if $x$ lies in the domain $\operatorname{dom}F$ and $\varphi(F(x))$, with the value $F(x)$; the formula $\forall z\,((x,z)\in F\Rightarrow\varphi)$ is predicative, and, under every such assignment, it holds if and only if $\varphi(F(x))$ whenever $x\in\operatorname{dom}F$.

¶ Let $x$, $y$ and $z$ be set variables, $x$ and $y$ not necessarily distinct, and $a$ and $\ast$ variables of either kind, $\ast$ distinct from $x$, $y$ and $a$, and $z$ distinct from $x$, $y$, $a$ and $\ast$, and let $((x,y),z)\in\ast$ be 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 §operation-membership. The formula $\exists z\,(((x,y),z)\in\ast\wedge\varphi)$ is predicative, and, under every assignment in which the value of $a$ is a set $a$ and the value of $\ast$ is a binary operation $\ast$ on $a$, it holds if and only if $x\in a$, $y\in a$ and $\varphi(x\ast y)$, with $x\ast y$ as in Binary Operations on a Set §notation; the formula $\forall z\,(((x,y),z)\in\ast\Rightarrow\varphi)$ is predicative, and, under every such assignment, it holds if and only if $\varphi(x\ast y)$ whenever $x\in a$ and $y\in a$.

In the remaining clauses, let $r$, with $+$, $\cdot$, $0$, $1$ and $\le$, be an ordered field, whose negative and difference, reciprocal and quotient and absolute value are meant, and let $x$, $y$ and $z$ be distinct set variables. Each condition below, in the set variables it displays and with $r$, $+$, $\cdot$, $0$, $1$ and $\le$ as parameters, is equivalent to a predicative formula: there are distinct variables $t_{1},\dots,t_{6}$, other than the displayed ones, and a predicative formula $\psi$ whose free variables are among the displayed set variables and $t_{1},\dots,t_{6}$, such that under every assignment in which $t_{1},\dots,t_{6}$ have the values $r$, $+$, $\cdot$, $0$, $1$ and $\le$, $\psi$ holds if and only if the condition holds.

¶ $x\in r\wedge z=-x$.

¶ $x\in r\wedge y\in r\wedge z=x-y$.

¶ $x\in r\wedge z=|x|$.

¶ $x\in r\wedge y\in r\wedge z=|x-y|$.

¶ $y\in r\wedge y\neq0\wedge z=y^{-1}$.

¶ $x\in r\wedge y\in r\wedge y\neq0\wedge z=x/y$.