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?

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?