Question

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.

Answer 1

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.

Answer 2

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?