# What subsystem of second-order arithmetic is needed for the recursion theorem?

In its simplest version, the recursion theorem states that for any $$m\in\mathbb{N}$$ and any function $$g:\mathbb{N}\rightarrow\mathbb{N}$$, there exists a function $$f:\mathbb{N}\rightarrow\mathbb{N}$$ such that $$f(0)=m$$ and $$f(n+1) = g(f(n))$$. There are many more complicated versions, with multiple variables and parameters and course-of-values recursion and so on. But that’s the gist of it.

Now the recursion theorem, no matter which version of it you take, is a statement in the language of second-order arithmetic. And I'm pretty sure that it’s provable in $$Z_2$$, i.e. full second-order arithmetic. But my question is, what is the weakest subsystem of second-order arithmetic capable of proving it?

Do different versions of the recursion theorem require different subsystems to prove it?

• It looks to me like any such version should be provable in RCA_0. Jul 21 '20 at 9:58

As Wojowu already pointed out $$\mathsf{RCA}_0$$ proves recursion theorem. You could find a proof in Simpson's book [1], Section II.3.
In fact primitive recursion theorem is equivalent to $$\Sigma^0_1\textsf{-Ind}$$ over $$\mathsf{RCA}_0^{\star}$$. Here $$\mathsf{RCA}_0^{\star}$$ is $$\mathsf{EA}+\Delta^0_1\text{-}\mathsf{CA}+\Delta^0_0\text{-}\mathsf{Ind}$$ and $$\mathsf{RCA}_0=\mathsf{RCA}_0^{\star}+\Sigma^0_1\text{-}\mathsf{Ind}$$. So we need to prove in $$\mathsf{RCA}_0^{\star}+\mathsf{PrimRec}$$ any given instance $$\exists y\;\varphi(0,y)\land \forall x\;(\exists y\;\varphi(x,y)\to \exists y\;\varphi(x+1,y))\to \forall x\;\exists y\varphi(x,y)$$ of $$\Sigma^0_1\textsf{-Ind}$$, where $$\varphi$$ is $$\Delta^0_0$$.
Indeed let us reason in $$\mathsf{RCA}_0^{\star}+\mathsf{PrimRec}$$. We assume $$\exists y\;\varphi(0,y)\land \forall x\;(\exists y\;\varphi(x,y)\to \exists y\;\varphi(x+1,y))$$ and claim $$\forall x\;\exists y\varphi(x,y)$$ and claim that $$\forall x\exists y\varphi(x,y)$$. Using $$\Delta^0_1\textsf{-CA}$$ and premise of induction we form the following function $$g(x)$$: $$g(x)=\begin{cases}\langle y_0,\ldots,y_{n-1},\min\{y_{n}\mid \varphi(n,y_{n})\}\rangle &\text{, if x=\langle y_0,\ldots,y_{n-1}\rangle and}\\ & \text{\;\;\; \varphi(i,y_i), for all i< n}\\ 0&\text{, otherwise}\end{cases}$$ We applying primitive recursion to $$g$$ and put $$f(0)=\langle \rangle$$. The resulting $$f$$ maps $$n$$ to a sequence $$\langle y_0,\ldots,y_{n-1}\rangle$$ such that $$\varphi(0,y_0),\ldots,\varphi(n-1,y_{n-1})$$. Note that the latter fact could be verified by $$\Delta^0_0\textsf{-Ind}$$. Thus we prove the instance of $$\Sigma^0_1\textsf{-Ind}$$.