[Math] Ackermann function in the Primitive recursive arithmetic

computability-theorylo.logicproof-theory

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.

Best Answer

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.

Related Question