1.9 The natural numbers

The rules we have introduced so far do not allow us to construct any infinite types. The simplest infinite type we can think of (and one which is of course also extremely useful) is the type $\mathbb{N}:𝒰$ of natural numbers. The elements of $\mathbb{N}$ are constructed using $0:\mathbb{N}$ and the successor operation $\mathrm{𝗌𝗎𝖼𝖼}:\mathbb{N}\to \mathbb{N}$. When denoting natural numbers, we adopt the usual decimal notation $1:\equiv \mathrm{𝗌𝗎𝖼𝖼}(0)$, $2:\equiv \mathrm{𝗌𝗎𝖼𝖼}(1)$, $3:\equiv \mathrm{𝗌𝗎𝖼𝖼}(2)$, ….

The essential property of the natural numbers is that we can define functions by recursion and perform proofs by induction — where now the words “recursion” and “induction” have a more familiar meaning. To construct a non-dependent function $f:\mathbb{N}\to C$ out of the natural numbers by recursion, it is enough to provide a starting point $c_0:C$ and a “next step” function $c_s:\mathbb{N}\to C\to C$. This gives rise to $f$ with the defining equations

$f(0)$ $:\equiv c_0,$

$f(\mathrm{𝗌𝗎𝖼𝖼}(n))$ $:\equiv c_s(n,f(n)).$

We say that $f$ is defined by primitive recursion.

As an example, we look at how to define a function on natural numbers which doubles its argument. In this case we have $C:\equiv \mathbb{N}$. We first need to supply the value of $\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}(0)$, which is easy: we put $c_0:\equiv 0$. Next, to compute the value of $\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}(\mathrm{𝗌𝗎𝖼𝖼}(n))$ for a natural number $n$, we first compute the value of $\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}(n)$ and then perform the successor operation twice. This is captured by the recurrence $c_s(n,y):\equiv \mathrm{𝗌𝗎𝖼𝖼}(\mathrm{𝗌𝗎𝖼𝖼}(y))$. Note that the second argument $y$ of $c_s$ stands for the result of the recursive call $\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}(n)$.

Defining $\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}:\mathbb{N}\to \mathbb{N}$ by primitive recursion in this way, therefore, we obtain the defining equations:

$\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}(0)$ $:\equiv 0$

$\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}(\mathrm{𝗌𝗎𝖼𝖼}(n))$ $:\equiv \mathrm{𝗌𝗎𝖼𝖼}(\mathrm{𝗌𝗎𝖼𝖼}(\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}(n))).$

This indeed has the correct computational behavior: for example, we have

$\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}(2)$ $\equiv \mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}(\mathrm{𝗌𝗎𝖼𝖼}(\mathrm{𝗌𝗎𝖼𝖼}(0)))$

$\equiv c_s(\mathrm{𝗌𝗎𝖼𝖼}(0),\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}(\mathrm{𝗌𝗎𝖼𝖼}(0)))$

$\equiv \mathrm{𝗌𝗎𝖼𝖼}(\mathrm{𝗌𝗎𝖼𝖼}(\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}(\mathrm{𝗌𝗎𝖼𝖼}(0))))$

$\equiv \mathrm{𝗌𝗎𝖼𝖼}(\mathrm{𝗌𝗎𝖼𝖼}(c_s(0,\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}(0))))$

$\equiv \mathrm{𝗌𝗎𝖼𝖼}(\mathrm{𝗌𝗎𝖼𝖼}(\mathrm{𝗌𝗎𝖼𝖼}(\mathrm{𝗌𝗎𝖼𝖼}(\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}(0)))))$

$\equiv \mathrm{𝗌𝗎𝖼𝖼}(\mathrm{𝗌𝗎𝖼𝖼}(\mathrm{𝗌𝗎𝖼𝖼}(\mathrm{𝗌𝗎𝖼𝖼}(c_0))))$

$\equiv \mathrm{𝗌𝗎𝖼𝖼}(\mathrm{𝗌𝗎𝖼𝖼}(\mathrm{𝗌𝗎𝖼𝖼}(\mathrm{𝗌𝗎𝖼𝖼}(0))))$

$\equiv 4.$

We can define multi-variable functions by primitive recursion as well, by currying and allowing $C$ to be a function type. For example, we define addition $\mathrm{𝖺𝖽𝖽}:\mathbb{N}\to \mathbb{N}\to \mathbb{N}$ with $C:\equiv \mathbb{N}\to \mathbb{N}$ and the following “starting point” and “next step” data:

$c_0$ $:\mathbb{N}\to \mathbb{N}$

$c_0(n)$ $:\equiv n$

$c_s$ $:\mathbb{N}\to (\mathbb{N}\to \mathbb{N})\to (\mathbb{N}\to \mathbb{N})$

$c_s(m,g)(n)$ $:\equiv \mathrm{𝗌𝗎𝖼𝖼}(g(n)).$

We thus obtain $\mathrm{𝖺𝖽𝖽}:\mathbb{N}\to \mathbb{N}\to \mathbb{N}$ satisfying the definitional equalities

$\mathrm{𝖺𝖽𝖽}(0,n)$ $\equiv n$

$\mathrm{𝖺𝖽𝖽}(\mathrm{𝗌𝗎𝖼𝖼}(m),n)$ $\equiv \mathrm{𝗌𝗎𝖼𝖼}(\mathrm{𝖺𝖽𝖽}(m,n)).$

As usual, we write $\mathrm{𝖺𝖽𝖽}(m,n)$ as $m+n$. The reader is invited to verify that $2+2\equiv 4$.

As in previous cases, we can package the principle of primitive recursion into a recursor:

$${\mathrm{𝗋𝖾𝖼}}_{\mathbb{N}}:\prod _{(C:𝒰)}C\to (\mathbb{N}\to C\to C)\to \mathbb{N}\to C$$

with the defining equations

${\mathrm{𝗋𝖾𝖼}}_{\mathbb{N}}(C,c_0,c_s,0)$ $:\equiv c_0,$

${\mathrm{𝗋𝖾𝖼}}_{\mathbb{N}}(C,c_0,c_s,\mathrm{𝗌𝗎𝖼𝖼}(n))$ $:\equiv c_s(n,{\mathrm{𝗋𝖾𝖼}}_{\mathbb{N}}(C,c_0,c_s,n)).$

Using ${\mathrm{𝗋𝖾𝖼}}_{\mathbb{N}}$ we can present $\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}$ and $\mathrm{𝖺𝖽𝖽}$ as follows:

$\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}$ $:\equiv {\mathrm{𝗋𝖾𝖼}}_{\mathbb{N}}(\mathbb{N},\mathrm{\hspace{0.17em}0},\lambda n.\lambda y.\mathrm{𝗌𝗎𝖼𝖼}(\mathrm{𝗌𝗎𝖼𝖼}(y)))$ (1)

$\mathrm{𝖺𝖽𝖽}$ $:\equiv {\mathrm{𝗋𝖾𝖼}}_{\mathbb{N}}(\mathbb{N}\to \mathbb{N},\lambda n.n,\lambda n.\lambda g.\lambda m.\mathrm{𝗌𝗎𝖼𝖼}(g(m))).$ (2)

Of course, all functions definable only using the primitive recursion principle will be computable. (The presence of higher function types — that is, functions with other functions as arguments — does, however, mean we can define more than the usual primitive recursive functions; see e.g. http://planetmath.org/node/87563Exercise 1.10.) This is appropriate in constructive mathematics; in §3.4 (http://planetmath.org/34classicalvsintuitionisticlogic),§3.8 (http://planetmath.org/38theaxiomofchoice) we will see how to augment type theory so that we can define more general mathematical functions.

We now follow the same approach as for other types, generalizing primitive recursion to dependent functions to obtain an induction principle. Thus, assume as given a family $C:\mathbb{N}\to 𝒰$, an element $c_0:C(0)$, and a function $c_s:{\prod }_{(n:\mathbb{N})}C(n)\to C(\mathrm{𝗌𝗎𝖼𝖼}(n))$; then we can construct $f:{\prod }_{(n:\mathbb{N})}C(n)$ with the defining equations:

$f(0)$ $:\equiv c_0,$

$f(\mathrm{𝗌𝗎𝖼𝖼}(n))$ $:\equiv c_s(n,f(n)).$

We can also package this into a single function

$${\mathrm{𝗂𝗇𝖽}}_{\mathbb{N}}:\prod _{(C:\mathbb{N}\to 𝒰)}C(0)\to ({\prod }_{(n:\mathbb{N})}C(n)\to C(\mathrm{𝗌𝗎𝖼𝖼}(n)))\to {\prod }_{(n:\mathbb{N})}C(n)$$

with the defining equations

${\mathrm{𝗂𝗇𝖽}}_{\mathbb{N}}(C,c_0,c_s,0)$ $:\equiv c_0,$

${\mathrm{𝗂𝗇𝖽}}_{\mathbb{N}}(C,c_0,c_s,\mathrm{𝗌𝗎𝖼𝖼}(n))$ $:\equiv c_s(n,{\mathrm{𝗂𝗇𝖽}}_{\mathbb{N}}(C,c_0,c_s,n)).$

Here we finally see the connection to the classical notion of proof by induction. Recall that in type theory we represent propositions by types, and proving a proposition by inhabiting the corresponding type. In particular, a property of natural numbers is represented by a family of types $P:\mathbb{N}\to 𝒰$. From this point of view, the above induction principle says that if we can prove $P(0)$, and if for any $n$ we can prove $P(\mathrm{𝗌𝗎𝖼𝖼}(n))$ assuming $P(n)$, then we have $P(n)$ for all $n$. This is, of course, exactly the usual principle of proof by induction on natural numbers.

As an example, consider how we might represent an explicit proof that $+$ is associative. (We will not actually write out proofs in this style, but it serves as a useful example for understanding how induction is represented formally in type theory.) To derive

$$\mathrm{𝖺𝗌𝗌𝗈𝖼}:\prod _{i,j,k:\mathbb{N}}i+(j+k)=(i+j)+k,$$

it is sufficient to supply

$${\mathrm{𝖺𝗌𝗌𝗈𝖼}}_0:\prod _{j,k:\mathbb{N}}\mathrm{\hspace{0.17em}0}+(j+k)=(0+j)+k$$

and

$${\mathrm{𝖺𝗌𝗌𝗈𝖼}}_s:\prod _{i:\mathbb{N}}(\prod _{j,k:\mathbb{N}}i+(j+k)=(i+j)+k)\to \prod _{j,k:\mathbb{N}}\mathrm{𝗌𝗎𝖼𝖼}(i)+(j+k)=(\mathrm{𝗌𝗎𝖼𝖼}(i)+j)+k.$$

To derive ${\mathrm{𝖺𝗌𝗌𝗈𝖼}}_0$, recall that $0+n\equiv n$, and hence $0+(j+k)\equiv j+k\equiv (0+j)+k$. Hence we can just set

$${\mathrm{𝖺𝗌𝗌𝗈𝖼}}_0(j,k):\equiv {\mathrm{𝗋𝖾𝖿𝗅}}_{j+k}.$$

For ${\mathrm{𝖺𝗌𝗌𝗈𝖼}}_s$, recall that the definition of $+$ gives $\mathrm{𝗌𝗎𝖼𝖼}(m)+n\equiv \mathrm{𝗌𝗎𝖼𝖼}(m+n)$, and hence

$\mathrm{𝗌𝗎𝖼𝖼}(i)+(j+k)$ $\equiv \mathrm{𝗌𝗎𝖼𝖼}(i+(j+k))\mathit{\hspace{1em}\hspace{1em}}\text{and}$

$(\mathrm{𝗌𝗎𝖼𝖼}(i)+j)+k$ $\equiv \mathrm{𝗌𝗎𝖼𝖼}((i+j)+k).$

Thus, the output type of ${\mathrm{𝖺𝗌𝗌𝗈𝖼}}_s$ is equivalently $\mathrm{𝗌𝗎𝖼𝖼}(i+(j+k))=\mathrm{𝗌𝗎𝖼𝖼}((i+j)+k)$. But its input (the “inductive hypothesis”) yields $i+(j+k)=(i+j)+k$, so it suffices to invoke the fact that if two natural numbers are equal, then so are their successors. (We will prove this obvious fact in Lemma 1 (http://planetmath.org/22functionsarefunctors#Thmlem1), using the induction principle of identity types.) We call this latter fact ${\mathrm{𝖺𝗉}}_{\mathrm{𝗌𝗎𝖼𝖼}}:(m{=}_{\mathbb{N}}n)\to (\mathrm{𝗌𝗎𝖼𝖼}(m){=}_{\mathbb{N}}\mathrm{𝗌𝗎𝖼𝖼}(n))$, so we can define

$${\mathrm{𝖺𝗌𝗌𝗈𝖼}}_s(i,h,j,k):\equiv {\mathrm{𝖺𝗉}}_{\mathrm{𝗌𝗎𝖼𝖼}}(h(j,k)).$$

Putting these together with ${\mathrm{𝗂𝗇𝖽}}_{\mathbb{N}}$, we obtain a proof of associativity.

Title	1.9 The natural numbers