# Ackermann function in the Primitive recursive arithmetic

Hello.

I study 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.

-

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.
Different indices $e$ for the same function might lead to different formulations $(\forall n)(\exists t)T(e,n,t)$ of totality. Carl's answer is fine because, for the Ackermann function, no choice of $e$ will make totality provable in PRA. But for other functions, you could have two indices of the same function such that totality for one is provable in PRA while totality for the other is not provable even in ZFC. (In fact, the constant zero function has two such indices.) –  Andreas Blass Aug 11 '10 at 20:01
Good point - in general you have to take a "natural" index for the computable function you want to prove is total. Of course you also have to take a "natural" primitive recursive index for the $T$ predicate, or it might be that your theory can't prove any computable function is total. It's an endemic problem with formalization. –  Carl Mummert Aug 11 '10 at 23:34