Is there a total recursive function $f:N \to N$ such that for no $\Sigma_1$ formula $\phi(x,y)$ which defines it (i.e., defines its graph), is it true that PA proves that "$\phi$ defines a total function".
For instance, is this true for Paris-Harrington's function? (There, we know that if we take $\phi$ to define the function in the intended form, it cannot be proved to be complete, but maybe another formula will do the trick.)

  • 1
    $\begingroup$ No $\Sigma_1$-sound r.e. extension of arithmetic can represent all recursive functions in a provably total way, and yes, for PA you can take the Paris-Harrington function: the usual arguments that PA doesn't prove $\forall x\exists y\phi(x,y)$ actually apply to PA + the set of all true $\Pi_1$ sentences, hence to all possible definitions of the same function. $\endgroup$ – Emil Jeřábek May 9 '15 at 17:56

There indeed are such functions. I cannot confirm that function arising from Paris-Harrington theorem has this property (though I suspect it does) but existence and other example follow from the following theorem:

If PA proves that a given recursive function is total, then this function is primitively recursive in $H_\alpha$ for some $\alpha<\varepsilon_0$.

In particular, $H_{\varepsilon_0}$ cannot be proven total, no matter what formula we choose to define it.

Mentioned result is proven e.g. in "Classifying the provably total functions of PA" by Weiermann.

  • $\begingroup$ Thanks! that was fast! I looked at the paper, I guess the point is that $H_{\epsilon_0}$ is still recursive and total but not bounded by any other $H_\alpha$. Thanks again, I thought this would be open for a long time :) $\endgroup$ – ikp May 9 '15 at 18:09
  • $\begingroup$ Yes, that is perfectly true. Using the recursion theorem one easily proves that $H_{\varepsilon_0}$ is total. Moreover if $\alpha<\beta\leq\varepsilon_0$ then $H_\alpha$ is eventually dominated by $H_\beta$. $\endgroup$ – Andreas Weiermann Aug 9 '15 at 9:25

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.