It is provable that every primitive recursive function is total in 1st order PA. Some non primitive recursive functions are also provably total in PA.
Can we show that a function is totally provable in PA but it doesn't has a recursive definition ? Somehow we need to diagonalize over all the provably total recursive functions , but that function should be uncomputable since turning machines can only compute total and recursive functions, yet one could show that the diagonalized function is representable in PA and also is provably total...