# The recursion theorem

From Peano’s axioms, we prove the following theorem, which serves as the basis for all definitions by induction, in particular the definitions of the addition and the multiplication of natural numbers.

**Theorem 1 (Recursion theorem)**

If is an application from a set into itself and , then there exists a unique application such that and for all .

**Demonstration**

The demonstration is done in two steps.

i) We show by induction that for all , there exists a unique application such that and for all , .

For , the only function such that (the second condition is “empty”) is defined by this condition, so the property is verified at rank .

Let us suppose that it is verified at rank : there exists a unique function such that and for all . Let us define a function by putting for all and . We have , and for all , by induction hypothesis; since by definition, has the desired property.

Suppose that is another function with these properties: in particular, we have and for any , and by induction hypothesis, being unique with these properties the restriction of to is equal to . It also follows that , so finally and uniqueness is also proved at rank . We conclude by induction that the property is verified for all .

ii) We deduce that there exists a unique application such that and for all , .

For this, let : by (i) there exists a unique function with the given properties, and we then define as . We thus obtain a function . By definition, we have , and for any , we have (because by uniqueness in (i), we have ) , so has the desired properties.

As for uniqueness, if is an application such that and for all , we easily prove by induction that is the whole set , and thus that , and the theorem is proved.

In practice, the definition by induction proceeds by a “construction” of the graph of the sequence , that is to say a functional relation on , for which for any , there exists with .

In principle, one defines (one chooses an element of starting from an essential property, and one describes a process (the function ) which makes it possible to define from , in the form of an expression which translates the constraints of definition of the function .

By Theorem 1, the unique function having the desired properties is the sequence defined by induction.

**Example 1**

Let us define by induction the expression , for a real number and a natural number: we let and . Here we define a mapping , which associates to the natural number the real number . The application which is appropriate is the “multiplication by “, which associates to the real number . By putting (the value of ), Theorem 1 assures us that there exists a single function such that and for all : this is the function we are seeking.