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

Question

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?

Answer 1

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}$.

[1] Simpson, S. G. (2009). Subsystems of second order arithmetic (Vol. 1). Cambridge University Press.