Does Z₂ Prove the iteration theorem?

Question

iteration theorem:

Let (ℕ,0,S) be the structure of natural numbers. And let W be an arbitrary set and c be an arbitrary member of W and g be a function from W into W. Then, there is a unique function F from ℕ into W such that:

1. F(0)=c
2. F(S(n))=g(F(n))

We know that ZFC Proves the iteration theorem, but my question is, does second order arithmetic (Z₂) prove the iteration theorem?

I think the answer is positive, but I'm not entirely sure.

Answer 1

Z$_2$ cannot talk about arbitrary sets. But if $W⊆ℕ$, then of course Z$_2$ can prove this simple recursion theorem. In fact, mere ACA$_0$ suffices. (See here for a short introduction to reverse mathematics.)

$F = \{ \ ⟨k,v⟩ : k,v{∈}ℕ ∧ ∃h{∈}ℕ_{≤k}{→}ℕ\ ( \ h(0) = c ∧ ∀i{∈}ℕ_{<k}\ ( \ h(i{+}1) = g(h(i)) \ ) ∧ h(k) = v \ ) \ \}$.

I leave you to check that this can indeed be encoded (via Godel coding), and that you can construct this in ACA$_0$ and prove that it is the desired unique recursion solution. Also, if you want recursion along longer well-orderings than $⟨ℕ,<⟩$, but staying within Z$_2$, the next natural stopping point is ATR$_0$, which supports arithmetical recursion along any (countable) well-ordering. For dealing with countable structures, typically you never need anywhere as close to Z$_2$, which is way stronger than ATR$_0$.