Sums and Differences of Natural Numbers as Typed Terms

This helper adopts the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices; (i) and (ii) are statements of the metatheory about expressions. Let $k\ge0$, the distinct set variables $x_{1},\dots,x_{k}$, the parameters with their fixed values, and assignments be as in Conditions Expressed by a Predicative Formula, and Guards (i); let $\gamma$ be a guard; and let terms under $\gamma$ and their values, and terms of type $A$ under $\gamma$ for a class $A$, be as in Terms and Typed Terms under a Guard (i) and Terms and Typed Terms under a Guard (ii). Sums, the order and differences of elements of $\mathbb{N}_{0}$ are those of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (iv), The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (v) and The Difference of Two Natural Numbers with Zero (i), formed in $\mathbb{N}_{0}$.

(i) Let $s$ and $t$ be terms of type $\mathbb{N}_{0}$ under $\gamma$, and let $s+t$ stand for the term $+((s,t))$ of Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii), written with a parameter $+$ whose value is the addition of $\mathbb{N}_{0}$; its value under each assignment satisfying $\gamma$ is the sum of the values of $s$ and $t$. Then $s+t$ is a term of type $\mathbb{N}_{0}$ under $\gamma$; and if $s$ and $t$ are terms of type $\mathbb{N}$ under $\gamma$, then $s+t$ is a term of type $\mathbb{N}$ under $\gamma$.

(ii) Let $s$ and $t$ be terms of type $\mathbb{N}_{0}$ under $\gamma$ such that $t\le s$ under every assignment satisfying $\gamma$, and let $s-t$ be the term under $\gamma$, written with $s$, $t$ and a parameter whose value is the addition of $\mathbb{N}_{0}$, whose value under each assignment satisfying $\gamma$ is the difference of the values of $s$ and $t$. Then $s-t$ is a term of type $\mathbb{N}_{0}$ under $\gamma$. That is, its value under every assignment satisfying $\gamma$ lies in $\mathbb{N}_{0}$; and for every set variable $z$ that is none of $x_{1},\dots,x_{k}$, is not free in $\gamma$ and does not occur in $s-t$, the condition $\gamma\wedge z=s-t$ on $x_{1},\dots,x_{k}$ and the displayed variable $z$ is expressed by a predicative formula.