Proof of Sums and Differences of Natural Numbers as Typed Terms

Terms under $\gamma$, their values and terms of a type are as in Terms and Typed Terms under a Guard (i) and Terms and Typed Terms under a Guard (ii); throughout, the parameters have their fixed values, as in Conditions Expressed by a Predicative Formula, and Guards (i).

Proof of (i). The addition $+$ of $\mathbb{N}_{0}$ is a binary operation on the set $\mathbb{N}_{0}$, that is, a map $+:\mathbb{N}_{0}\times\mathbb{N}_{0}\to\mathbb{N}_{0}$, by Addition on Omega (i), The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii) and The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (iv). By Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iv), $(s,t)$ is a term of type $\mathbb{N}_{0}\times\mathbb{N}_{0}$ under $\gamma$; so by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii), with $+$ for $F$, $+((s,t))$ is a term of type $\mathbb{N}_{0}$ under $\gamma$, and its value is the sum of the values of $s$ and $t$ by Binary Operations on a Set (ii). Now let $s$ and $t$ be of type $\mathbb{N}$. They are of type $\mathbb{N}_{0}$, since their values lie in $\mathbb{N}\subseteq\mathbb{N}_{0}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii) and the condition of Terms and Typed Terms under a Guard (iv) does not involve the type; so $s+t$ is of type $\mathbb{N}_{0}$, as just shown. Its value lies in $\mathbb{N}$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication (vi), so Terms and Typed Terms under a Guard (iii) holds for the type $\mathbb{N}$, and Terms and Typed Terms under a Guard (iv) is the condition already obtained; so $s+t$ is of type $\mathbb{N}$.

Proof of (ii). Values. Under an assignment satisfying $\gamma$, the values of $s$ and $t$ lie in $\mathbb{N}_{0}$ by Terms and Typed Terms under a Guard (iii), and $t\le s$ by hypothesis; so by The Difference of Two Natural Numbers with Zero (i) the value of $s-t$ is the unique $j\in\mathbb{N}_{0}$ with $t+j=s$. It is a set in $\mathbb{N}_{0}$ determined by the values of $s$ and $t$, hence by the sets assigned to $x_{1},\dots,x_{k}$ and the values of the parameters; so $s-t$ is a term under $\gamma$ satisfying Terms and Typed Terms under a Guard (iii) with $\mathbb{N}_{0}$.

The formula. Let $z$ be a set variable that is none of $x_{1},\dots,x_{k}$, is not free in $\gamma$ and does not occur in $s-t$, and let $Y_{+}$ be the parameter of $s-t$ with value $+$. The set variables form an infinite list by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (i), so there are distinct set variables $u$ and $v$ that are none of $x_{1},\dots,x_{k}$ and $z$ and occur neither in $\gamma$ nor in $s-t$. By Terms and Typed Terms under a Guard (iv) there are predicative formulas $\psi_{s}^{u}$ and $\psi_{t}^{v}$ expressing $\gamma\wedge u=s$ and $\gamma\wedge v=t$; by Conditions Expressed by a Predicative Formula, and Guards (ii) their free variables are among $x_{1},\dots,x_{k}$, $u$, respectively $v$, and the parameters of $\gamma$, $s$ and $t$, so $z$ is free in neither. Let $\psi$ be the formula

$$\exists u\,\exists v\,\bigl(\psi_{s}^{u}\wedge\psi_{t}^{v}\wedge((v,z),u)\in Y_{+}\bigr).$$

The formula $((v,z),u)\in Y_{+}$ is 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 (iv), so $\psi$, which applies no quantifier to a class variable, is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i); its free variables are among $x_{1},\dots,x_{k}$, $z$ and the parameters of $\gamma$ and $s-t$. Consider an assignment of sets to $x_{1},\dots,x_{k}$ and $z$. As $+$ is a binary operation on the set $\mathbb{N}_{0}$, as shown in the proof of (i), Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (xi) gives that $((v,z),u)\in{+}$ holds if and only if $v,z\in\mathbb{N}_{0}$ and $u=v+z$; so no separate condition $z\in\mathbb{N}_{0}$ is needed. By the properties of $\psi_{s}^{u}$ and $\psi_{t}^{v}$, $u$ and $v$ must be the values of $s$ and $t$; so $\psi$ holds if and only if $\gamma$ holds, $z\in\mathbb{N}_{0}$ and $t+z=s$. When $\gamma$ holds, $t\le s$, and by The Difference of Two Natural Numbers with Zero (i) the elements $z\in\mathbb{N}_{0}$ with $t+z=s$ are exactly $z=s-t$. So $\psi$ expresses $\gamma\wedge z=s-t$, Terms and Typed Terms under a Guard (iv) holds, and $s-t$ is of type $\mathbb{N}_{0}$.