4.3 Arithmetic[0NN]
We will define the addition operation between natural numbers, formally
\[ ⋅+⋅ : ℕ×ℕ→ℕ \quad ,\quad (h,k)↦ h+k \quad . \]
Definition
11
This operation is commutative and associative, as shown below.
Note that \(h+0=f_ h(0)=h\) (basis of recursion); also \(0+n=f_ 0(n)=n\) (shows easily by induction).
To prove that it is commutative, we first show that
Lemma
12
Proposition
13
At this point we can give a name to \(1=S(0)\) and notice that \(S(n)=n+1\). So from now on we could do without the symbol \(S\).
With similar procedures we show that addition is associative.
Proposition
14
Multiplication is similarly defined.
Definition
15
Exercises
In the following we will simply write \(nm\) instead of \(n× m\).