Proof of Predicative Formulas for Differences, Quotients, Absolute Values, Distances and the Strict Order of the Real Numbers, at Any Variable Positions

Throughout, $\mathbb{R}$, with $+$, $\cdot$, $0$, $1$ and $\le$, is an ordered field by The Real Numbers Form an Ordered Field in Which Every Nonempty Set Bounded Above Has a Supremum (i), so the ordered-field part 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 applies with $r=\mathbb{R}$. That lemma requires the variables $t_{1},\dots,t_{6}$ it provides to differ only from the displayed variables, whereas a parameter, in the sense of Conditions Expressed by a Predicative Formula, and Guards (i), must be none of $x_{0},\dots,x_{n-1}$. The class variables among $t_{1},\dots,t_{6}$ are none of $x_{0},\dots,x_{n-1}$, since set variables and class variables form disjoint lists (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (i)). The set variables among them we replace by distinct set variables that occur nowhere in the formula $\psi$ provided and are none of $x_{0},\dots,x_{n-1}$. 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), with the replaced variables as $v_{1},\dots,v_{k}$ and their replacements as $y_{1},\dots,y_{k}$, the result is again predicative, and it holds under an assignment exactly when $\psi$ holds with each replaced variable given the value of its replacement. As the equivalence the lemma provides involves the $t_{\ell}$ only through their values, the new formula is equivalent to the same condition when the new variables carry those values. So we may take $t_{1},\dots,t_{6}$ to be parameters, none of $x_{0},\dots,x_{n-1}$, with the fixed values $\mathbb{R}$, $+$, $\cdot$, $0$, $1$ and $\le$.

Differences. Apply 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) with $x=x_{0}$, $y=x_{1}$ and $z=x_{2}$. It gives a predicative formula $\psi$ whose free variables are among $x_{0},x_{1},x_{2}$ and the parameters, and which holds, under every assignment of sets to $x_{0},x_{1},x_{2}$, if and only if

$$x_{0}\in\mathbb{R},\quad x_{1}\in\mathbb{R}\quad\text{and}\quad x_{2}=x_{0}-x_{1}.$$

So $\psi$ is a predicative formula in $x_{0},x_{1},x_{2}$. Let $\sigma(0)=i$, $\sigma(1)=j$ and $\sigma(2)=k$; these indices are below $n$ and need not be distinct. By Renaming and Substituting Variables in Predicative Formulas (i), the formula $\psi(x_{i},x_{j},x_{k})$ obtained by this renaming is a predicative formula in $x_{0},\dots,x_{n-1}$, and under every assignment of sets to $x_{0},\dots,x_{n-1}$ it holds if and only if $\psi$ holds when $x_{0},x_{1},x_{2}$ are assigned the sets assigned to $x_{i},x_{j},x_{k}$, that is, if and only if $x_{i}\in\mathbb{R}$, $x_{j}\in\mathbb{R}$ and $x_{k}=x_{i}-x_{j}$. Hence $\psi(x_{i},x_{j},x_{k})$ expresses the condition in (i).

Quotients. In the same way, 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 (viii) with $x=x_{0}$, $y=x_{1}$ and $z=x_{2}$ gives a predicative formula in $x_{0},x_{1},x_{2}$ that holds exactly when $x_{0}\in\mathbb{R}$, $x_{1}\in\mathbb{R}$, $x_{1}\neq0$ and $x_{2}=x_{0}/x_{1}$. Renaming it by $\sigma(0)=i$, $\sigma(1)=j$, $\sigma(2)=k$, Renaming and Substituting Variables in Predicative Formulas (i) gives a predicative formula in $x_{0},\dots,x_{n-1}$ that holds exactly when $x_{i}\in\mathbb{R}$, $x_{j}\in\mathbb{R}$, $x_{j}\neq0$ and $x_{k}=x_{i}/x_{j}$, which proves (ii).

Absolute values. Apply 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 (v) with $x=x_{0}$ and $z=x_{1}$: it gives a predicative formula in $x_{0},x_{1}$ that holds exactly when $x_{0}\in\mathbb{R}$ and $x_{1}=|x_{0}|$. Renaming it by $\sigma(0)=i$ and $\sigma(1)=k$, Renaming and Substituting Variables in Predicative Formulas (i) gives a predicative formula in $x_{0},\dots,x_{n-1}$ that holds exactly when $x_{i}\in\mathbb{R}$ and $x_{k}=|x_{i}|$, which proves (iii).

Distances. Likewise 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 (vi) with $x=x_{0}$, $y=x_{1}$ and $z=x_{2}$ gives a predicative formula in $x_{0},x_{1},x_{2}$ that holds exactly when $x_{0}\in\mathbb{R}$, $x_{1}\in\mathbb{R}$ and $x_{2}=|x_{0}-x_{1}|$, and its renaming by $\sigma(0)=i$, $\sigma(1)=j$, $\sigma(2)=k$ is, by Renaming and Substituting Variables in Predicative Formulas (i), a predicative formula in $x_{0},\dots,x_{n-1}$ that holds exactly when $x_{i}\in\mathbb{R}$, $x_{j}\in\mathbb{R}$ and $x_{k}=|x_{i}-x_{j}|$. This proves (iv).

The strict order. The order $\le$ is a total, hence partial, order on $\mathbb{R}$ by The Real Numbers (i), so its strict relation $<$ is the class of Partial and Total Orders on a Set and the Associated Strict Relation (iii), and for sets $u$ and $v$, $u<v$ means $(u,v)\in{<}$. Let $S$ be a class variable, distinct from $x_{0},\dots,x_{n-1}$, taken as a parameter with value $<$. 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 (iii) with $s=S$, $t_{1}=x_{i}$ and $t_{2}=x_{j}$ (not necessarily distinct), the formula $(x_{i},x_{j})\in S$ is predicative, its free variables are $x_{i}$, $x_{j}$ and $S$, and when sets are assigned to $x_{i}$ and $x_{j}$ it holds if and only if $(x_{i},x_{j})\in{<}$, that is, $x_{i}<x_{j}$. So it expresses the condition in (v). For (vi), let $w$ be a set variable, distinct from $S$ and from $x_{0},\dots,x_{n-1}$, taken as a parameter with value $0$ (a set, being an element of $\mathbb{R}$ by The Real Numbers (iv)). The same lemma, with $s=S$, $t_{1}=w$ and $t_{2}=x_{j}$, shows that $(w,x_{j})\in S$ is predicative, with free variables $w$, $x_{j}$ and $S$, and that under every assignment of a set to $x_{j}$ it holds if and only if $(0,x_{j})\in{<}$, that is, $0<x_{j}$. So it expresses the condition in (vi).