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.

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.

-
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 2010 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 2010 at 23:34

Carl, can I ask you one more question concerning the topic?

I thought about the reasons why we cannot prove in PRA totality of the Ackerman function $A(m,n)$, directly using double mathematical induction for $n$ then for $m$, and came to a conclusion, that it's because the deduction theorem is nonapplicable to PRA. Please correct me if the following reasoning is wrong.

First, let us define in the PRA language, using Kleene's T predicate, the predicate $\varphi_A(m,n)$, which means: $\exists k ~ k=A(m,n)$.

Second, using the definition of $A(m,n)$, let us amplify the PRA by the next three axioms:

1) $\varphi_A(0,n)$

2) $\varphi_A(m,1) \to \varphi_A(m+1,0)$

3) $\varphi_A(m,K(m)) \to [\varphi_A(m+1,n) \to \varphi_A(m+1,n+1)]$

The axiom (3) is the result of Skolemization of the next assertion:

$\forall m ~ [\forall k ~ \varphi_A(m,k)] \to [\forall n ~ \varphi_A(m+1,n) \to \varphi_A(m+1,n+1)]$

where $K$ is the new functional symbol.

Third, notice that $\varphi_A(m,1) \wedge \varphi_A(m,K(m))$ implies both $\varphi_A(m+1,0)$ and $\varphi_A(m+1,n) \to \varphi_A(m+1,n+1)$:

4) $[\varphi_A(m,1) \wedge \varphi_A(m,K(m))] \to \varphi_A(m+1,0)$

5) $[\varphi_A(m,1) \wedge \varphi_A(m,K(m))] \to [\varphi_A(m+1,n) \to \varphi_A(m+1,n+1)]$

Here we used deduction theorem, but only in trivial form: $(a \wedge b \vdash c) \to (a \vdash b \to c)$, which is independent of the PRA axioms. Joining (4) with (5):

6) $[\varphi_A(m,1) \wedge \varphi_A(m,K(m))] \to (\varphi_A(m+1,0) \wedge [\varphi_A(m+1,n) \to \varphi_A(m+1,n+1)])$

Here we can see a premise of mathematical induction for $n$ - in the right part of the implication.

We have not proven assertion $\varphi_A(m+1,0) \wedge [\varphi_A(m+1,n) \to \varphi_A(m+1,n+1)]$ yet. But if we could use deduction theorem in the form: $(PRA \wedge a \vdash b) \to (PRA \vdash a \to b)$, then we could continue the proof.

So, let us suppose, that we can use deduction theorem in the form: $(PRA \wedge a \vdash b) \to (PRA \vdash a \to b)$.

Fourth, let us suppose $\varphi_A(m,1) \wedge \varphi_A(m,K(m))$. It implies $\varphi_A(m+1,0) \wedge [\varphi_A(m+1,n) \to \varphi_A(m+1,n+1)]$, and the last, using mathematical induction for $n$, implies $\varphi_A(m+1,n)$. Thus, by the deduction theorem we have:

7) $\varphi_A(m,1) \wedge \varphi_A(m,K(m)) \to \varphi_A(m+1,n)$

Fifth, using substitution $n$ for $1$ and for $K(m+1)$, we can conclude from $\varphi_A(m+1,n)$ the next: $\varphi_A(m+1,1) \wedge \varphi_A(m+1,K(m+1))$. Thus, using (7), we can conclude the last from $\varphi_A(m,1) \wedge \varphi_A(m,K(m))$. Using deduction theorem again (but only in "trivial" form, which is independent of the PRA axioms), we have:

8) $\varphi_A(m,1) \wedge \varphi_A(m,K(m)) \to \varphi_A(m+1,1) \wedge \varphi_A(m+1,K(m+1))$

Sixth, from (1) we can conclude:

9) $\varphi_A(0,1) \wedge \varphi_A(0,K(0))$

Seventh, from (8) and (9), using mathematical induction for $m$, we can conclude:

10) $\varphi_A(m,1) \wedge \varphi_A(m,K(m))$

Eighth, from (7) and (10) we can conclude:

11) $\varphi_A(m+1,n)$

Jointly with (1) it means $\varphi_A(m,n)$ - assertion about totality of the Ackerman function.

Knowing, that it's undecidable in PRA, I can see only one used assumption, which can be wrong: That we can use deduction theorem in the form: $(PRA \wedge a \vdash b) \to (PRA \vdash a \to b)$. So we cannot use deduction theorem in this form?

-
I haven't had a chance to look at this in great detail, but the main reason that PRA does not prove the Ackerman function is total is that PRA does not include enough induction axioms. PRA itself, being just a first-order theory without any additional inference rules, does satisfy the usual deduction theorem. There are indeed formal systems that do not satisfy the deduction theorem, but these must have additional rules of inference in addition to the usual inference rules for first-order logic, because the usual proof of the deduction theorem applies to all first-order theories. – Carl Mummert Apr 17 2012 at 14:45
First, additional questions should be posted as new questions (with links to old ones, if appropriate), not as answers. Second, as far as I can see, the problem with your proof is not the deduction theorem but the use of induction for a formula involving $\varphi_A$ and $K$. I don't think PRA includes enough induction to justify this. – Andreas Blass Apr 17 2012 at 14:51
Regarding the induction, the usual way I would prove that the Ackermann function total would involve the inductive hypothesis "If $\lambda n.A(m,n)$ is total then $\lambda n.A(m+1,n)$ is total". The naive computation makes that hypothesis $\Delta^0_3$, but PRA has the same strength as $\Sigma^0_1$ induction when it comes to proving that computable functions are total. – Carl Mummert Apr 17 2012 at 14:51
I completely agree with Andreas that this would be better as a separate question. – Carl Mummert Apr 17 2012 at 14:53