Large cardinal axioms and total recursive functions

Question

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

Answer 1

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

Answer 2

Since large cardinal axioms have arithmetic consequences not provable without them, the answer to your first question is yes. For example, let $f(n)=1$, provided that $n$ is not the Goedel code of a proof of a contradiction in ZFC. Since large cardinals imply Con(ZFC), the theory ZFC+large cardinals proves that $f$ is total. But ZFC alone does not prove this (if consistent), since it is relatively consistent with ZFC that there are proofs of contradictions from ZFC.

For the more general question, suppose that the stronger theory not only proves the weaker theory, but also proves that whenever the weaker theory proves that a TM program computes a total function, then it really does. This is the situation for most large cardinals---for example the theory asserting that there is a weakly compact cardinal implies towers of smaller inaccessible cardinals, and so if a program is total inside such a $V_\kappa$, then it really is in $V$. Given this situation, let $f(n)$ be the function which first inspects all smaller $m\leq n$ to see which code proofs from the weaker theory that a certain function $g_m$ is total, and then let $f(n)$ be larger than all such $g_m(n)$. Our assumption on the stronger theory ensures that we can be confident that the computation of $g_m(n)$ converges, so $f(n)$ will be defined.