Are there known relationships between large cardinal axioms (say Mahlo or Woodin cardinals) and total recursive functions (over the natural numbers) of the type:
$ZFC$ + large cardinal axiom $\vdash$ $f$ is a total recursive function,
$ZFC \not\vdash$ $f$ is a total recursive function,
like this is known for different axiom systems of reverse mathematics, e.g.:
$ATR_0 \vdash$ the Goodstein function $G$ is total recursive,
but for the weaker system $ACA_0$ we have:
$ACA_0 \not\vdash$ the Goodstein function $G$ is total recursive.
Or, more generally asked, is there a relationship of the following kind:
If $LCA_1$ (large cardinal axiom 1) is stronger (wrt. consistency strength) than $LCA_2$, then $ZFC + LCA_1$ proves the totality of a recursive function $f$ which grows faster than all recursive functions having totality proofs in $ZFC + LCA_2$?
This question arises in investigations of the relationship between learnability and provability, where provably total recursive functions are used to schedule the learning process. A learning systems $\Lambda(\Sigma_1)$ using $\Sigma_1$ as a background theory is stronger than a learning system $\Lambda(\Sigma_2)$, if $\Sigma_1$ allows totality proofs of recursive functions growing faster than all recursive functions having totality proofs in $\Sigma_2$.