computability theory - Ackermann function in the Primitive recursive arithmetic

You can express the totality of any computable function in PRA, using Kleene's T predicate, which is primitive recursive. So if you pick any index $e$ for the Ackermann function, the formula $(forall n)(exists t) T(underline{e}, n, t)$ is already in the language of PRA.

However, you cannot prove the totality of the Ackermann function in PRA. One way to see this is to note that PRA is a subtheory of $text{I-}Sigma^0_1$, modulo an interpretation of the language of PRA into $text{I-}Sigma^0_1$. The provably total functions of $text{I-}Sigma^0_1$ are well-known to be exactly the primitive recursive functions.

There is a lot of proof theory literature on provably total functions, which are also called provably recursive functions. But I don't know how much of it focuses specifically on primitive recursive arithmetic. One place to look might be Hájek and Pudlák, Metamthematics of First-Order Arithmetic.