MathOverflow is a question and answer site for professional mathematicians. It only takes a minute to sign up.
Sign up to join this community
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.
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.
$(\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.)
$\endgroup$
Aug 11, 2010 at 20:01