1.9 The natural numbers

The rules we have introduced so far do not allow us to construct any infiniteMathworldPlanetmath types. The simplest infinite type we can think of (and one which is of course also extremely useful) is the type β„•:𝒰 of natural numbersMathworldPlanetmath. The elements of β„• are constructed using 0:β„• and the successor operation π—Œπ—Žπ–Όπ–Ό:β„•β†’β„•. When denoting natural numbers, we adopt the usual decimal notation 1:β‰‘π—Œπ—Žπ–Όπ–Ό(0), 2:β‰‘π—Œπ—Žπ–Όπ–Ό(1), 3:β‰‘π—Œπ—Žπ–Όπ–Ό(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 β€œinductionMathworldPlanetmath” have a more familiar meaning. To construct a non-dependent function f:β„•β†’C out of the natural numbers by recursion, it is enough to provide a starting point c0:C and a β€œnext step” function cs:β„•β†’Cβ†’C. This gives rise to f with the defining equations

f⁒(0) :≑c0,
f⁒(π—Œπ—Žπ–Όπ–Όβ’(n)) :≑cs(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:≑ℕ. We first need to supply the value of π–½π—ˆπ—Žπ–»π—…π–Ύβ’(0), which is easy: we put c0:≑0. Next, to compute the value of π–½π—ˆπ—Žπ–»π—…π–Ύβ’(π—Œπ—Žπ–Όπ–Όβ’(n)) for a natural number n, we first compute the value of π–½π—ˆπ—Žπ–»π—…π–Ύβ’(n) and then perform the successor operation twice. This is captured by the recurrence cs(n,y):β‰‘π—Œπ—Žπ–Όπ–Ό(π—Œπ—Žπ–Όπ–Ό(y)). Note that the second argument y of cs stands for the result of the recursive call π–½π—ˆπ—Žπ–»π—…π–Ύβ’(n).

Defining π–½π—ˆπ—Žπ–»π—…π–Ύ:β„•β†’β„• by primitive recursion in this way, therefore, we obtain the defining equations:

π–½π—ˆπ—Žπ–»π—…π–Ύβ’(0) :≑0
π–½π—ˆπ—Žπ–»π—…π–Ύβ’(π—Œπ—Žπ–Όπ–Όβ’(n)) :β‰‘π—Œπ—Žπ–Όπ–Ό(π—Œπ—Žπ–Όπ–Ό(π–½π—ˆπ—Žπ–»π—…π–Ύ(n))).

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

π–½π—ˆπ—Žπ–»π—…π–Ύβ’(2) β‰‘π–½π—ˆπ—Žπ–»π—…π–Ύβ’(π—Œπ—Žπ–Όπ–Όβ’(π—Œπ—Žπ–Όπ–Όβ’(0)))

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 additionPlanetmathPlanetmath 𝖺𝖽𝖽:β„•β†’β„•β†’β„• with C:≑ℕ→ℕ and the following β€œstarting point” and β€œnext step” data:

c0 :β„•β†’β„•
c0⁒(n) :≑n
cs :β„•β†’(β„•β†’β„•)β†’(β„•β†’β„•)
cs⁒(m,g)⁒(n) :β‰‘π—Œπ—Žπ–Όπ–Ό(g(n)).

We thus obtain 𝖺𝖽𝖽:β„•β†’β„•β†’β„• satisfying the definitional equalities

𝖺𝖽𝖽⁒(0,n) ≑n
𝖺𝖽𝖽⁒(π—Œπ—Žπ–Όπ–Όβ’(m),n) β‰‘π—Œπ—Žπ–Όπ–Όβ’(𝖺𝖽𝖽⁒(m,n)).

As usual, we write 𝖺𝖽𝖽⁒(m,n) as m+n. The reader is invited to verify that 2+2≑4.

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


with the defining equations

𝗋𝖾𝖼ℕ⁒(C,c0,cs,0) :≑c0,
𝗋𝖾𝖼ℕ⁒(C,c0,cs,π—Œπ—Žπ–Όπ–Όβ’(n)) :≑cs(n,𝗋𝖾𝖼ℕ(C,c0,cs,n)).

Using 𝗋𝖾𝖼ℕ we can present π–½π—ˆπ—Žπ–»π—…π–Ύ and 𝖺𝖽𝖽 as follows:

π–½π—ˆπ—Žπ–»π—…π–Ύ :≑𝗋𝖾𝖼ℕ(β„•, 0,Ξ»n.Ξ»y.π—Œπ—Žπ–Όπ–Ό(π—Œπ—Žπ–Όπ–Ό(y))) (1)
𝖺𝖽𝖽 :≑𝗋𝖾𝖼ℕ(β„•β†’β„•,Ξ»n.n,Ξ»n.Ξ»g.Ξ»m.π—Œπ—Žπ–Όπ–Ό(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 functionsMathworldPlanetmath; 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 theoryPlanetmathPlanetmath 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:ℕ→𝒰, an element c0:C⁒(0), and a function cs:∏(n:β„•)C⁒(n)β†’C⁒(π—Œπ—Žπ–Όπ–Όβ’(n)); then we can construct f:∏(n:β„•)C⁒(n) with the defining equations:

f⁒(0) :≑c0,
f⁒(π—Œπ—Žπ–Όπ–Όβ’(n)) :≑cs(n,f(n)).

We can also package this into a single function


with the defining equations

𝗂𝗇𝖽ℕ⁒(C,c0,cs,0) :≑c0,
𝗂𝗇𝖽ℕ⁒(C,c0,cs,π—Œπ—Žπ–Όπ–Όβ’(n)) :≑cs(n,𝗂𝗇𝖽ℕ(C,c0,cs,n)).

Here we finally see the connection to the classical notion of proof by induction. Recall that in type theory we represent propositionsPlanetmathPlanetmathPlanetmath 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:ℕ→𝒰. 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⁒(π—Œπ—Žπ–Όπ–Όβ’(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


it is sufficient to supply

π–Ίπ—Œπ—Œπ—ˆπ–Ό0:∏j,k:ℕ 0+(j+k)=(0+j)+k



To derive π–Ίπ—Œπ—Œπ—ˆπ–Ό0, recall that 0+n≑n, and hence 0+(j+k)≑j+k≑(0+j)+k. Hence we can just set


For π–Ίπ—Œπ—Œπ—ˆπ–Όs, recall that the definition of + gives π—Œπ—Žπ–Όπ–Όβ’(m)+nβ‰‘π—Œπ—Žπ–Όπ–Όβ’(m+n), and hence

π—Œπ—Žπ–Όπ–Όβ’(i)+(j+k) β‰‘π—Œπ—Žπ–Όπ–Όβ’(i+(j+k))  and
(π—Œπ—Žπ–Όπ–Όβ’(i)+j)+k β‰‘π—Œπ—Žπ–Όπ–Όβ’((i+j)+k).

Thus, the output type of π–Ίπ—Œπ—Œπ—ˆπ–Όs is equivalently π—Œπ—Žπ–Όπ–Όβ’(i+(j+k))=π—Œπ—Žπ–Όπ–Όβ’((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 successorsMathworldPlanetmathPlanetmathPlanetmath. (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 π–Ίπ—‰π—Œπ—Žπ–Όπ–Ό:(m=β„•n)β†’(π—Œπ—Žπ–Όπ–Ό(m)=β„•π—Œπ—Žπ–Όπ–Ό(n)), so we can define


Putting these together with 𝗂𝗇𝖽ℕ, we obtain a proof of associativity.

Title 1.9 The natural numbers