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}:\mathcal{U}$ of natural numbers. The elements of $\mathbb{N}$ are constructed using $0:\mathbb{N}$ and the successor operation $\mathsf{succ}:\mathbb{N}\to\mathbb{N}$ . When denoting natural numbers, we adopt the usual decimal notation $1:\!\!\equiv\mathsf{succ}(0)$ , $2:\!\!\equiv\mathsf{succ}(1)$ , $3:\!\!\equiv\mathsf{succ}(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

	$\displaystyle f(0)$	$\displaystyle:\!\!\equiv c_{0},$
	$\displaystyle f(\mathsf{succ}(n))$	$\displaystyle:\!\!\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 $\mathsf{double}(0)$ , which is easy: we put $c_{0}:\!\!\equiv 0$ . Next, to compute the value of $\mathsf{double}(\mathsf{succ}(n))$ for a natural number $n$ , we first compute the value of $\mathsf{double}(n)$ and then perform the successor operation twice. This is captured by the recurrence $c_{s}(n,y):\!\!\equiv\mathsf{succ}(\mathsf{succ}(y))$ . Note that the second argument $y$ of $c_{s}$ stands for the result of the recursive call $\mathsf{double}(n)$ .

Defining $\mathsf{double}:\mathbb{N}\to\mathbb{N}$ by primitive recursion in this way, therefore, we obtain the defining equations:

	$\displaystyle\mathsf{double}(0)$	$\displaystyle:\!\!\equiv 0$
	$\displaystyle\mathsf{double}(\mathsf{succ}(n))$	$\displaystyle:\!\!\equiv\mathsf{succ}(\mathsf{succ}(\mathsf{double}(n))).$

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

	$\displaystyle\mathsf{double}(2)$	$\displaystyle\equiv\mathsf{double}(\mathsf{succ}(\mathsf{succ}(0)))$
		$\displaystyle\equiv c_{s}(\mathsf{succ}(0),\mathsf{double}(\mathsf{succ}(0)))$
		$\displaystyle\equiv\mathsf{succ}(\mathsf{succ}(\mathsf{double}(\mathsf{succ}(0% ))))$
		$\displaystyle\equiv\mathsf{succ}(\mathsf{succ}(c_{s}(0,\mathsf{double}(0))))$
		$\displaystyle\equiv\mathsf{succ}(\mathsf{succ}(\mathsf{succ}(\mathsf{succ}(% \mathsf{double}(0)))))$
		$\displaystyle\equiv\mathsf{succ}(\mathsf{succ}(\mathsf{succ}(\mathsf{succ}(c_{% 0}))))$
		$\displaystyle\equiv\mathsf{succ}(\mathsf{succ}(\mathsf{succ}(\mathsf{succ}(0))))$
		$\displaystyle\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 $\mathsf{add}:\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:

	$\displaystyle c_{0}$	$\displaystyle:\mathbb{N}\to\mathbb{N}$
	$\displaystyle c_{0}(n)$	$\displaystyle:\!\!\equiv n$
	$\displaystyle c_{s}$	$\displaystyle:\mathbb{N}\to(\mathbb{N}\to\mathbb{N})\to(\mathbb{N}\to\mathbb{N})$
	$\displaystyle c_{s}(m,g)(n)$	$\displaystyle:\!\!\equiv\mathsf{succ}(g(n)).$

We thus obtain $\mathsf{add}:\mathbb{N}\to\mathbb{N}\to\mathbb{N}$ satisfying the definitional equalities

	$\displaystyle\mathsf{add}(0,n)$	$\displaystyle\equiv n$
	$\displaystyle\mathsf{add}(\mathsf{succ}(m),n)$	$\displaystyle\equiv\mathsf{succ}(\mathsf{add}(m,n)).$

As usual, we write $\mathsf{add}(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:

$\mathsf{rec}_{\mathbb{N}}:\prod_{(C:\mathcal{U})}\,C\to(\mathbb{N}\to C\to C)% \to\mathbb{N}\to C$

with the defining equations

	$\displaystyle\mathsf{rec}_{\mathbb{N}}(C,c_{0},c_{s},0)$	$\displaystyle:\!\!\equiv c_{0},$
	$\displaystyle\mathsf{rec}_{\mathbb{N}}(C,c_{0},c_{s},\mathsf{succ}(n))$	$\displaystyle:\!\!\equiv c_{s}(n,\mathsf{rec}_{\mathbb{N}}(C,c_{0},c_{s},n)).$

Using $\mathsf{rec}_{\mathbb{N}}$ we can present $\mathsf{double}$ and $\mathsf{add}$ as follows:

	$\displaystyle\mathsf{double}$	$\displaystyle:\!\!\equiv\mathsf{rec}_{\mathbb{N}}\big{(}\mathbb{N},\,0,\,{% \lambda}n.\,{\lambda}y.\,\mathsf{succ}(\mathsf{succ}(y))\big{)}$		(1)
	$\displaystyle\mathsf{add}$	$\displaystyle:\!\!\equiv\mathsf{rec}_{\mathbb{N}}\big{(}\mathbb{N}\to\mathbb{N% },\,{\lambda}n.\,n,\,{\lambda}n.\,{\lambda}g.\,{\lambda}m.\,\mathsf{succ}(g(m)% )\big{)}.$		(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\mathcal{U}$ , an element $c_{0}:C(0)$ , and a function $c_{s}:\mathchoice{\prod_{n:\mathbb{N}}\,}{\mathchoice{{\textstyle\prod_{(n:% \mathbb{N})}}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:% \mathbb{N})}}}{\mathchoice{{\textstyle\prod_{(n:\mathbb{N})}}}{\prod_{(n:% \mathbb{N})}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N})}}}{\mathchoice{{% \textstyle\prod_{(n:\mathbb{N})}}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N% })}}{\prod_{(n:\mathbb{N})}}}C(n)\to C(\mathsf{succ}(n))$ ; then we can construct $f:\mathchoice{\prod_{n:\mathbb{N}}\,}{\mathchoice{{\textstyle\prod_{(n:\mathbb% {N})}}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N})}% }}{\mathchoice{{\textstyle\prod_{(n:\mathbb{N})}}}{\prod_{(n:\mathbb{N})}}{% \prod_{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N})}}}{\mathchoice{{\textstyle\prod_% {(n:\mathbb{N})}}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:% \mathbb{N})}}}C(n)$ with the defining equations:

	$\displaystyle f(0)$	$\displaystyle:\!\!\equiv c_{0},$
	$\displaystyle f(\mathsf{succ}(n))$	$\displaystyle:\!\!\equiv c_{s}(n,f(n)).$

We can also package this into a single function

$\mathsf{ind}_{\mathbb{N}}:\prod_{(C:\mathbb{N}\to\mathcal{U})}\,C(0)\to\Bigl{(% }\mathchoice{{\textstyle\prod_{(n:\mathbb{N})}}}{\prod_{(n:\mathbb{N})}}{\prod% _{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N})}}C(n)\to C(\mathsf{succ}(n))\Bigr{)}% \to\mathchoice{{\textstyle\prod_{(n:\mathbb{N})}}}{\prod_{(n:\mathbb{N})}}{% \prod_{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N})}}C(n)$

with the defining equations

	$\displaystyle\mathsf{ind}_{\mathbb{N}}(C,c_{0},c_{s},0)$	$\displaystyle:\!\!\equiv c_{0},$
	$\displaystyle\mathsf{ind}_{\mathbb{N}}(C,c_{0},c_{s},\mathsf{succ}(n))$	$\displaystyle:\!\!\equiv c_{s}(n,\mathsf{ind}_{\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\mathcal{U}$ . 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(\mathsf{succ}(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

$\mathsf{assoc}:\mathchoice{\prod_{i,j,k:\mathbb{N}}\,}{\mathchoice{{\textstyle% \prod_{(i,j,k:\mathbb{N})}}}{\prod_{(i,j,k:\mathbb{N})}}{\prod_{(i,j,k:\mathbb% {N})}}{\prod_{(i,j,k:\mathbb{N})}}}{\mathchoice{{\textstyle\prod_{(i,j,k:% \mathbb{N})}}}{\prod_{(i,j,k:\mathbb{N})}}{\prod_{(i,j,k:\mathbb{N})}}{\prod_{% (i,j,k:\mathbb{N})}}}{\mathchoice{{\textstyle\prod_{(i,j,k:\mathbb{N})}}}{% \prod_{(i,j,k:\mathbb{N})}}{\prod_{(i,j,k:\mathbb{N})}}{\prod_{(i,j,k:\mathbb{% N})}}}i+(j+k)=(i+j)+k,$

it is sufficient to supply

$\mathsf{assoc}_{0}:\mathchoice{\prod_{j,k:\mathbb{N}}\,}{\mathchoice{{% \textstyle\prod_{(j,k:\mathbb{N})}}}{\prod_{(j,k:\mathbb{N})}}{\prod_{(j,k:% \mathbb{N})}}{\prod_{(j,k:\mathbb{N})}}}{\mathchoice{{\textstyle\prod_{(j,k:% \mathbb{N})}}}{\prod_{(j,k:\mathbb{N})}}{\prod_{(j,k:\mathbb{N})}}{\prod_{(j,k% :\mathbb{N})}}}{\mathchoice{{\textstyle\prod_{(j,k:\mathbb{N})}}}{\prod_{(j,k:% \mathbb{N})}}{\prod_{(j,k:\mathbb{N})}}{\prod_{(j,k:\mathbb{N})}}}0+(j+k)=(0+j% )+k$

and

$\mathsf{assoc}_{s}:\mathchoice{\prod_{i:\mathbb{N}}\,}{\mathchoice{{\textstyle% \prod_{(i:\mathbb{N})}}}{\prod_{(i:\mathbb{N})}}{\prod_{(i:\mathbb{N})}}{\prod% _{(i:\mathbb{N})}}}{\mathchoice{{\textstyle\prod_{(i:\mathbb{N})}}}{\prod_{(i:% \mathbb{N})}}{\prod_{(i:\mathbb{N})}}{\prod_{(i:\mathbb{N})}}}{\mathchoice{{% \textstyle\prod_{(i:\mathbb{N})}}}{\prod_{(i:\mathbb{N})}}{\prod_{(i:\mathbb{N% })}}{\prod_{(i:\mathbb{N})}}}\left(\mathchoice{\prod_{j,k:\mathbb{N}}\,}{% \mathchoice{{\textstyle\prod_{(j,k:\mathbb{N})}}}{\prod_{(j,k:\mathbb{N})}}{% \prod_{(j,k:\mathbb{N})}}{\prod_{(j,k:\mathbb{N})}}}{\mathchoice{{\textstyle% \prod_{(j,k:\mathbb{N})}}}{\prod_{(j,k:\mathbb{N})}}{\prod_{(j,k:\mathbb{N})}}% {\prod_{(j,k:\mathbb{N})}}}{\mathchoice{{\textstyle\prod_{(j,k:\mathbb{N})}}}{% \prod_{(j,k:\mathbb{N})}}{\prod_{(j,k:\mathbb{N})}}{\prod_{(j,k:\mathbb{N})}}}% i+(j+k)=(i+j)+k\right)\to\mathchoice{\prod_{j,k:\mathbb{N}}\,}{\mathchoice{{% \textstyle\prod_{(j,k:\mathbb{N})}}}{\prod_{(j,k:\mathbb{N})}}{\prod_{(j,k:% \mathbb{N})}}{\prod_{(j,k:\mathbb{N})}}}{\mathchoice{{\textstyle\prod_{(j,k:% \mathbb{N})}}}{\prod_{(j,k:\mathbb{N})}}{\prod_{(j,k:\mathbb{N})}}{\prod_{(j,k% :\mathbb{N})}}}{\mathchoice{{\textstyle\prod_{(j,k:\mathbb{N})}}}{\prod_{(j,k:% \mathbb{N})}}{\prod_{(j,k:\mathbb{N})}}{\prod_{(j,k:\mathbb{N})}}}\mathsf{succ% }(i)+(j+k)=(\mathsf{succ}(i)+j)+k.$

To derive $\mathsf{assoc}_{0}$ , recall that $0+n\equiv n$ , and hence $0+(j+k)\equiv j+k\equiv(0+j)+k$ . Hence we can just set

$\mathsf{assoc}_{0}(j,k):\!\!\equiv\mathsf{refl}_{j+k}.$

For $\mathsf{assoc}_{s}$ , recall that the definition of $+$ gives $\mathsf{succ}(m)+n\equiv\mathsf{succ}(m+n)$ , and hence

	$\displaystyle\mathsf{succ}(i)+(j+k)$	$\displaystyle\equiv\mathsf{succ}(i+(j+k))\qquad\text{and}$
	$\displaystyle(\mathsf{succ}(i)+j)+k$	$\displaystyle\equiv\mathsf{succ}((i+j)+k).$

Thus, the output type of $\mathsf{assoc}_{s}$ is equivalently $\mathsf{succ}(i+(j+k))=\mathsf{succ}((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 $\mathsf{ap}_{\mathsf{succ}}:(m=_{\mathbb{N}}n)\to(\mathsf{succ}(m)=_{\mathbb{N% }}\mathsf{succ}(n))$ , so we can define

$\mathsf{assoc}_{s}(i,h,j,k):\!\!\equiv\mathsf{ap}_{\mathsf{succ}}(h(j,k)).$

Putting these together with $\mathsf{ind}_{\mathbb{N}}$ , we obtain a proof of associativity.

Title	1.9 The natural numbers
\metatable