Hello.


I study [primitive recursive arithmetic](http://en.wikipedia.org/wiki/Primitive_recursive_arithmetic) and have the following questions.


1) Is it possible to express in the PRA that Ackermann function is total?


2) If yes, is such expression decidable in the PRA ?


Can u suggest some literature on this topic?


Thank you.



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


