Proof of Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order

Throughout, sums of elements of $\omega$ lie in $\omega$ by Addition on Omega §addition, and $0\in\omega$ and $S(n)\in\omega$ for every $n\in\omega$ by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §inductive.

Recursion equations. Let $m\in\omega$, and let $f:\omega\to\omega$ be the map given in Addition on Omega §addition by The Recursion Theorem on Omega §recursion with $a=\omega$, $c=m$ and $g=\sigma$, so that $f(0)=m$ and $f(S(k))=\sigma((k,f(k)))=S(f(k))$ for every $k\in\omega$. By Addition on Omega §addition, $f$ is a set witnessing the formula defining $m+n$ with $z=f(n)$, so $m+n=f(n)$ for every $n\in\omega$. Hence, for all $m,n\in\omega$,

$$m+0=m\qquad\text{and}\qquad m+S(n)=S(m+n).\qquad(\ast)$$

Induction classes. Each induction below is run with Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §induction on a class $A=\{n\in\omega:\varphi\}$ (with the induction variable possibly renamed) formed by class abstraction with set parameters among $k,m,n$ and the class parameters $\omega$ and $\le$. Each $\varphi$ quantifies over set variables only, $0$ (the empty set, by The Class Omega of Natural Numbers with Zero §zero), $S(\cdot)$ (by The Successor of a Set §successor), sums (by Addition on Omega §addition) and the ordered pair in $u\le v$ being defined set symbols, whose arguments lie in $\omega$ by the conjunct $n\in\omega$ and the remarks above; so $\varphi$ is predicative as Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §comprehension requires. By Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, $n\in\omega$ lies in $A$ if and only if $\varphi$ holds of $n$. For each class we check $0\in A$ and, for $n\in\omega$, that $n\in A$ implies $S(n)\in A$; then $\omega\subseteq A$, which is the claim for every element of $\omega$.

Order facts. By Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §set, $\omega$ is a set; by The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor §well-order and Well-Orders on a Set §well-order, $\le$ is a total order on $\omega$, hence a partial order, so it is reflexive, antisymmetric and transitive on $\omega$ by Partial and Total Orders on a Set and the Associated Strict Relation §partial; and by The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor §strict, $<$ is its associated strict relation. So Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders applies with $a=\omega$ and these $\le$ and $<$.

Zero. $m+0=m$ is $(\ast)$. For $0+m=m$, let $A=\{n\in\omega:0+n=n\}$. By $(\ast)$, $0+0=0$, and if $0+n=n$ then $0+S(n)=S(0+n)=S(n)$. So $0+n=n$ for every $n\in\omega$, in particular $0+m=m$.

Successor. $m+S(n)=S(m+n)$ is $(\ast)$. For the second equation fix $m$ and let $A=\{n\in\omega:S(m)+n=S(m+n)\}$. By $(\ast)$, $S(m)+0=S(m)=S(m+0)$; and if $S(m)+n=S(m+n)$, then by $(\ast)$

$$S(m)+S(n)=S(S(m)+n)=S(S(m+n))=S(m+S(n)).$$

Finally, by $(\ast)$, $n+S(0)=S(n+0)=S(n)$.

Associative. Fix $k,m$ and let $A=\{n\in\omega:(k+m)+n=k+(m+n)\}$. By $(\ast)$, $(k+m)+0=k+m=k+(m+0)$. If $(k+m)+n=k+(m+n)$, then by $(\ast)$

$$(k+m)+S(n)=S((k+m)+n)=S(k+(m+n))=k+S(m+n)=k+(m+S(n)).$$

Commutative. Fix $m$ and let $A=\{n\in\omega:m+n=n+m\}$. By the clause zero above, $m+0=m=0+m$. If $m+n=n+m$, then by $(\ast)$ and the clause successor above (its second equation with $n$ and $m$ interchanged), $m+S(n)=S(m+n)=S(n+m)=S(n)+m$.

Cancellation. Fix $m,n$ and let $A=\{k\in\omega:(k+m=k+n\Rightarrow m=n)\}$. If $0+m=0+n$, then $m=n$ by the clause zero above. Let $k\in A$ and $S(k)+m=S(k)+n$. By the clause successor above, $S(k+m)=S(k+n)$, so $k+m=k+n$ by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §successor-injective, and $m=n$ as $k\in A$. So $S(k)\in A$.

Difference. ($\Leftarrow$) Fix $m$ and let $A=\{j\in\omega:m\le m+j\}$. By $(\ast)$ and reflexivity, $m\le m=m+0$. Let $m\le m+j$. By The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor §successor, $m+j<S(m+j)$, so $m+j\le S(m+j)=m+S(j)$ by The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor §strict and $(\ast)$, and transitivity gives $m\le m+S(j)$. Hence $m\le m+j$ for all $j\in\omega$, so $m+j=n$ implies $m\le n$.

($\Rightarrow$) Let $A=\{n\in\omega:\forall m\,(m\in\omega\wedge m\le n\Rightarrow\exists j\,(j\in\omega\wedge m+j=n))\}$. Base: if $m\in\omega$ and $m\le0$, then also $0\le m$ by The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor §zero-least, so $m=0$ by antisymmetry, and $m+0=0$ by $(\ast)$. Step: let $n\in A$, $m\in\omega$ and $m\le S(n)$. By Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders §weak-strict, $m<S(n)$ or $m=S(n)$. If $m=S(n)$, then $m+0=S(n)$ by $(\ast)$. If $m<S(n)$, then $m\le n$ by The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor §successor, so as $n\in A$ there is $j\in\omega$ with $m+j=n$, and then $m+S(j)=S(m+j)=S(n)$ by $(\ast)$, with $S(j)\in\omega$. So $S(n)\in A$, and $\omega\subseteq A$ gives the claim.

Order. First, for all $j\in\omega$, by the clauses successor and associative above,

$$k+(S(m)+j)=k+S(m+j)=S(k+(m+j))=S((k+m)+j)=S(k+m)+j.\qquad(\ast\ast)$$

Let $m<n$. By The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor §successor-below, $S(m)\le n$, so by the clause difference above $n=S(m)+j$ for some $j\in\omega$; then $k+n=S(k+m)+j$ by $(\ast\ast)$, so $S(k+m)\le k+n$ by the clause difference above, and $k+m<k+n$ by The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor §successor-below. Conversely let $k+m<k+n$. By The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor §successor-below, $S(k+m)\le k+n$, so by the clause difference above $S(k+m)+j=k+n$ for some $j\in\omega$; by $(\ast\ast)$, $k+(S(m)+j)=k+n$, so $S(m)+j=n$ by the clause cancellation above. Hence $S(m)\le n$ by the clause difference above, and $m<n$ by The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor §successor-below.

For $\le$: by Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders §weak-strict, $m\le n$ if and only if $m<n$ or $m=n$, and $k+m\le k+n$ if and only if $k+m<k+n$ or $k+m=k+n$. By the strict part just proved, $m<n$ if and only if $k+m<k+n$; and $m=n$ if and only if $k+m=k+n$, the forward direction by substitution and the converse by the clause cancellation above. So $m\le n$ if and only if $k+m\le k+n$.

Zero-sum. Let $m+n=0$. If $n\neq0$, then by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §cases $n=S(n')$ for some $n'\in\omega$, and $m+n=S(m+n')\neq0$ by $(\ast)$ and Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §successor-nonzero, a contradiction. So $n=0$, and $m=m+0=0$ by $(\ast)$.