4
$\begingroup$

A total recursive function $f(x)$ is provably total in $PA$ if there's some formula $\phi(x,y)$ such that

  1. $f(x)=y \iff PA\vdash \phi(x,y)$ and
  2. $PA\vdash \forall x \exists y \phi(x,y)$

I know (not in much detail) that a total recursive function is not provably total if it grows as fast as/faster than $f_{\epsilon_0}$ in a fast growing hierarchy, where $\epsilon_0=\omega^{\omega^{\omega^....}}$ (the Goodstein sequence would be an example). My question is, is the converse also true, i.e., every total recursive function dominated by $f_{\epsilon_0}$ is provably total in $PA$?


Edit: By Gro-Tsen's comment and Henry's answer, I know the answer to my above question is (almost trivially) no ... But if I strength my requirement a bit, and consider a total recursive function $f_\alpha$ with $\alpha<\epsilon_0$. If the fundamental sequences here leading up to $\epsilon_0$ are computable, is $f_\alpha$ guarantee to be provably total then? And how do we prove (or disprove) it?

$\endgroup$
3
  • 2
    $\begingroup$ $\lceil\log_2 f_{\varepsilon_0}\rceil$ is dominated by $f_{\varepsilon_0}$ but is not provably total in $\mathsf{PA}$ because the latter shows that $n\mapsto 2^n$ is total. $\endgroup$
    – Gro-Tsen
    Feb 25, 2017 at 10:40
  • $\begingroup$ I think the question needs some eidt. You are talking about provable, but your definition is also about definable. You can have a function defined in a Turing complete language that returns 0 for every input, but is not provable total in PA (if you translate the function to a PA definition). Still a function can be defined in PA, that is provable to be total. That makes also a difference for comment above. $\endgroup$
    – Lucas K.
    Feb 25, 2017 at 11:54
  • $\begingroup$ @LucasK.,I tried to make it more specific. The original question seems almost trivial now. $\endgroup$
    – Eric
    Feb 25, 2017 at 13:47

1 Answer 1

7
$\begingroup$

I think usually one adds the condition that $\phi$ be a $\Delta_1$ (i.e. computable) formula.

As Gro-Tsen has pointed out, the answer is no: there are lots of functions which are provably total, dominated by $f_{\epsilon_0}$, but not provably total in PA. First of all, you're not stating the sharpest version of the theorem. The theorem is that any function provably total in PA is eventually dominated by some $f_\alpha$ with $\alpha<\epsilon_0$. So any function which grows faster than all the $f_\alpha$ but slower than $\epsilon_0$ is still not provably total in PA. One can get many of these by the method Gro-Tsen's comment suggests: taking $f_{\epsilon_0}$ and slow it down just a little: none of $\lceil \log_2f_{\epsilon_0}\rceil$, $f_{\epsilon_0}/2$ and $f_{\epsilon_0}-1$ are provably total in PA.

Similarly, one can modify the definition of $f_{\epsilon_0}$ to diagonalize the $f_\alpha$ more slowly: recall that $f_{\epsilon_0}(n)=f_{\omega_n}(n)$ (where $\omega_n$ is a tower of exponentials of $\omega$ of height $n$). Consider the function $g(n)=f_{\omega_{\lfloor \log_2 n\rfloor}}(n)$, or replace $\log_2$ with any other function (possibly one which grows very slowly): one still diagonalizes all the $f_\alpha$, but one can do this very, very slowly.

Speaking of slow growing functions, consider the inverse of $f_{\epsilon_0}$: $h(n)$ is the least $m$ such that $f_{\epsilon_0}(m)>n$. This function is clearly total recursive, but actually grows too slowly to be provably total in PA.

Additionally, there are functions which, despite being slow growing, are just fundamentally too complicated to be provably total in PA. A function might have only $0$ and $1$ values, and therefore be dominated by the constant function, and yet not be provable in PA. For instance, consider the following. First, pick a pairing function $p:\mathbb{N}\rightarrow\mathbb{N}^2$. Given $n$, let $p(n)=(a,b)$; if $a$ is not the Gödel code of a $\Delta_1$ formula whose only free variables are $x,y$, $f(n)=0$. Suppose $a$ is the Gödel code of $\phi(x,y)$; if there is a proof in PA with $<f_{\epsilon_0}(n)$ steps that $\phi(n,0)$ holds, $f(n)=1$. Otherwise, $f(n)=0$.

$\endgroup$
2
  • $\begingroup$ Thank you for the clear answer. Please have a look at my edit of the original question. $\endgroup$
    – Eric
    Feb 25, 2017 at 13:44
  • 2
    $\begingroup$ @Eric: if you have another question, it's better to ask it separately. The standard representation of the functions f_alpha are provably total in PA. A trace of the computations in the standard description of f_alpha gives a descending sequence below alpha*omega. One then shows that PA proves this ordinal is well-founder. By choosing a very weird fundamental sequence (say, omega[n]=f_epsilon_0(n)), one changes the function and can get one not probably total in PA. $\endgroup$ Feb 25, 2017 at 13:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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