PA proves that functions are total

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

• 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. – Emil Jeřábek May 9 '15 at 17:56

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.
• 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 :) – ikp May 9 '15 at 18:09
• 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$. – Andreas Weiermann Aug 9 '15 at 9:25