Defining Operations on ℕ

Once we have naturals, we want to do things with them. We define operations
by defining equations that mirror the Peano construction.

Addition $\oplus$:
- $m \oplus 0 = m$
- $m \oplus s(n) = s(m \oplus n)$

Multiplication $\odot$:
- $m \odot 0 = 0$
- $m \odot s(n) = (m \odot n) \oplus m$

Exponentiation $m^n$:
- $m^0 = s(0)$
- $m^{s(n)} = m^n \odot m$

These are recursive definitions: each one reduces $n$ until it reaches $0$.
That gives us a mechanical way to compute — apply the rules as rewrite
rules until no more apply. This is the replacement rule.

For example, to compute $2 \oplus 1$:

The greatest common divisor gcd(a, b) is the largest natural dividing both a and b. On unary naturals, gcd is defined by Euclid's algorithm:

where $a \bmod b$ is the remainder when $a$ is divided by $b$.

Step-by-step (working with peano numerals):

For $\gcd(s(s(s(o))), s(s(o)))$ (i.e. $\gcd(3, 2)$):
1. $b \neq 0$: compute $\gcd(b, a \bmod b) = \gcd(2, 3 \bmod 2)$.
2. $3 \bmod 2 = 1$: compute $\gcd(1, 2 \bmod 1)$.
3. $2 \bmod 1 = 0$: compute $\gcd(1, 0)$.
4. $b = 0$: return $a = 1$. So $\gcd(3, 2) = 1$. ✓

Predecessor. To compute $a \bmod b$ we need the predecessor function $p$ with $p(s(n)) = n, p(o) = o$. Defined recursively:
- $p(o) = o$
- $p(s(n)) = n$

The proof of correctness for gcd uses induction on $b$. Euclid's algorithm always terminates because the second argument strictly decreases.