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


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


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.

  • 1
    $\begingroup$ $f$ is the constant $1$ function, hence provably total in ZFC. $\endgroup$ – Emil Jeřábek Jun 8 '12 at 10:39
  • 2
    $\begingroup$ @Joel: Yes, different definitions of the same function may differ in their totality. Consider this as a feature. Essentially, the p.t.r.f. of a theory describe the $\Pi^0_2$ fragment of $T+\operatorname{Th}_{\Pi^0_1}(\mathbb N)$. $\endgroup$ – Emil Jeřábek Jun 8 '12 at 13:00
  • 2
    $\begingroup$ Emil, you are saying that when studying provable totality, one always throws the $\Pi^0_1$-theory of $\mathbb{N}$ into the theory? Why is this? The question seems to be perfectly sensible for theories not containing this extra stuff. $\endgroup$ – Joel David Hamkins Jun 8 '12 at 13:24
  • 5
    $\begingroup$ You can study provably total algorithms (TM) if you wish, it’s perfectly sensible. I was simply pointing out that the (fairly traditional) definition of a provably total function does not distinguish different algorithms computing the same function. The rationale, I suppose, is that this characteristic of the theory is a set of combinatorial objects (functions), which can be studied with tools unrelated to logic. (The situation is akin to ordinals of a theory, there you also abstract away different definitions of the same ordinal.)... $\endgroup$ – Emil Jeřábek Jun 8 '12 at 13:47
  • 2
    $\begingroup$ First of all, thanks a lot for your quick and enlightening answers! Also the discussion about intensional and extensional definitions raises an important point for further contemplation. As Francois has correctly remarked, in my context the intensional view seems to be appropriate, because I deal with programs executed on a universal reference TM. It is fascinating, that these large cardinals, which are directly concerned with unfathomable infinities, have such interesting implications for effective objects. $\endgroup$ – Joerg Zimmermann Jun 8 '12 at 16:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.