In Odifreddi, General Recursion Theory, Vol. II, p. 325, I find the following claim:
Notice that, due to the connection between induction and $\mu$-recursion discussed in Section I.1, proving totality of a function defined by $\mu$-recursion amounts to proving induction for the formula used in the $\mu$-recursion. Thus, which recursive functions are provably total in [the theory] $\mathcal{F}$ strongly depends on the inductive strength of $\mathcal{F}$.
I don't quite understand this claim. By Gödel's representation theorem, every recursive function is numeralwise representable by a $\Sigma_1$ formula, but of course not every total recursive function is provably recursive in I$\Sigma_1$.
Now, part of the point here is surely that in order to be allowed to introduce $f$ by $\mu$-recursion on a predicate $P(\vec{x}, y)$, we must already have shown that $P$ is regular, i.e., $\forall \vec{x} \exists y P(\vec{x}, y)$. And IF we have proved this, THEN application of induction (in form of the least number principle) of course ensures us that $f$ is total. But it seems to me that this last step is much "easier" than proving the antecedent of this IF...THEN. I.e., the "hard" part seems to me proving in $\mathcal{F}$ that $P$ is a regular predicate in the first place. And I don't see why this should "amount to proving induction for the formula used in the $\mu$-recursion".
So, if I understand correctly, the claim Odifreddi CAN make is this:
If
$\mathcal{F} \vdash \forall \vec{x} \exists y P(\vec{x}, y)$
and
$f(\vec{x}) := \mu yP(\vec{x}, y)$,
then $f$ is provably recursive in $\mathcal{F}$ if $\mathcal{F}\vdash$ Ind$(P)$.
This is true, but (I would think) trivial.
But this doesn't quite seem to be what the above quote is actually saying ("proving totality ... amounts to proving induction for the formula used in the $\mu$-recursion"). Rather, it seems that he is saying something stronger, namely:
If $\mathbb{N}\models \forall \vec{x} \exists y P(\vec{x}, y)$
and
$f(\vec{x}) := \mu yP(\vec{x}, y)$,
then $f$ is provably recursive in $\mathcal{F}$ iff $\mathcal{F}\vdash$ Ind$(P)$.
And as we see from the representation theorem, this should be false.
My question is this: is there something interesting "in between" these two trivially true, respectively trivially false readings that Odifreddi is getting at?