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.)
$\begingroup$
$\endgroup$
1
-
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řábekCommented May 9, 2015 at 17:56
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
2
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$– ikpCommented May 9, 2015 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$ Commented Aug 9, 2015 at 9:25