# An informal version of the recursion theorem

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 ?)

• It's fine if you believe that Peano arithmetic is consistent. One reason you might believe that Peano arithmetic is consistent is that you can construct a model of it in ZF and you believe that ZF is consistent. Nov 25, 2013 at 20:34
• (Actually I would guess that most of what is informal about Proposition 2.1.16 is that Tao hadn't defined a function by that point. Is my guess right? I don't have this book.) Nov 25, 2013 at 21:41
• You seem to have a typo in the proposition, since you introduce the $f_n$'s, but then refer to $f$ with no subscript. Nov 25, 2013 at 21:42
• Sorry to all for the late response, I had some problems with the login credentials. For the sake of correctness, the typo is now corrected. Jan 15, 2014 at 19:18