Let $T$ be a first order theory that can define the naturals. Let's say it can interpret $\sf PA$.
Let $\phi$ be a one place predicate symbol definable in the language of $T$, let $f$ be a function symbol in the language of $T$; suppose $T$ proves:
$\forall x: \phi(x) \implies \exists y: y=f(x) \land \phi(y)$
Suppose we have an object $a$ such that $\phi(a)$, then is it always granted to have a function symbol $K$ such that:
$K(0)=a \\ K(n+1)= f(K(n))$
If that is not always granted, then what we exactly must have for such functions to be granted?