7
$\begingroup$

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.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
15
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • 4
    $\begingroup$ 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.) $\endgroup$
    – Andreas Blass
    Commented Aug 11, 2010 at 20:01
  • 1
    $\begingroup$ 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. $\endgroup$
    – Carl Mummert
    Commented Aug 11, 2010 at 23:34

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .