In T. Taos *Analysis 1* book, on page 26, we have a proposition that tells us that recursive definitions are actually well-defined.



> 
> Proposition 2.1.16: *Suppose for each naturla number $n$, wh have some function $f\_n:\mathbb{N}\rightarrow\mathbb{N}$. Let $c$ be a natural number. Then we can assign a unique natural number $a\_n$ to each natural number $n$, such that $a\_0=c$ and $a\_{n+1}=f\_n(a\_n)$ for each natural number $n$.*
> 
> 
> 


At this point only the axioms of the natural numbers are known. Now the author goes then on to develop set theory and explains how the natural numbers can be realized inside set theory and *then* says that now we can establish a rigorous version of the above proposition (as an exercise):



> 
> Exercise 3.5.12: *This exercise will establish a rigorous version of Proposition 2.1.16. Let $f:\mathbb{N}\times\mathbb{N}\rightarrow\mathbb{N}$ be a function an $c$ a natural number. Show that there exists a function $a:\mathbb{N}\rightarrow\mathbb{N}$ such that $$a(0)=c$$and$$a(n+1)=f(n,a(n)).$$*
> 
> 
> 


Question: *Supposing* that we had already defined exactly what a function is an so on, then Proposition 2.1.16 seems to me to be a perfectly rigorous statement and its proof (via induction and the use of the Peano axioms) - which is much simpler than the proof of the exercise - a perfectly valid (i.e. not informal) proof. Is that true ?


(Does the other maybe say that Proposition 2.1.16 isn't rigorous and it's proof is only informal only because at that stage we don't have developed set theory ?) 



An informal version of the recursion theorem
The proof of 2.1.16 uses an informal notion of induction. The induction axiom 2.5 says that 


* if P(n) is a property, such that P(0) holds etc etc… then P(n) holds for all n.


Now the "proof" of 2.1.16 does not define any property P(n), so it does not use induction in a formal way. 


In Exercise 3.5.12, on the other hand, an explicit property P(n) appears, namely
the property that there is a unique function defined on all numbers up to n such that ...


