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,


but:


$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$.



Large cardinal axioms and total recursive functions
$\def\zfc{\mathrm{ZFC}}\def\lca{\mathrm{LCA}}$Yes. Normally, $\zfc+\lca\_1$ proves not only the consistency of $\zfc+\lca\_2$, but also the uniform reflection principle of $\zfc+\lca\_2$ (at least for arithmetic formulas). In particular, the $\Sigma^0\_1$-reflection principle is a $\Pi^0\_2$ sentence provable in $\zfc+\lca\_1$ but not in $\zfc+\lca\_2$, and it can be expressed as the totality of the following function $f$: if $x$ is a code of a $\zfc+\lca\_2$ proof of a $\Sigma^0\_1$-sentence of the form $\exists u\,\theta(u)$ with $\theta\in\Delta^0\_0$, let $f(x)$ be the minimal $u$ such that $\mathbb N\models\theta(u)$, otherwise $f(x)=0$.


To see that $f$ grows faster than any provably total recursive function of $\zfc+\lca\_2$, let $g$ be such a function. We may assume without loss of generality that $g$ is increasing, and $g(x)=y$ has a $\Sigma^0\_1$-definition $\exists w\,\lambda(x,y,w)$ which is provably total and (strictly) increasing in $\zfc+\lca\_2$. Let $\theta(x,u)$ be the formula $\exists y,w\le u\,\lambda(2^x,y,w)$ (this is strictly speaking not $\Delta^0\_0$, but this is easy to fix, I'll leave it like this to simplify the presentation). Then the formulas $\exists u\,\theta(\ulcorner n\urcorner,u)$ (where $\ulcorner n\urcorner$ denotes the binary numeral of $n$) have $\zfc+\lca\_2$ proofs of Gödel number bounded by $p(n)$ for some polynomial $p$, but their smallest witnesses have magnitude at least $g(2^n)>g(p(n))$ for large enough $n$.


This argument shows that $f(m)>g(m)$ for infinitely many $m$. If we want this to hold for all sufficiently large $m$, it suffices to make the function increasing by using $f\_2(x)=\max\_{y\le x}f(y)$ instead of $f$.


