Hello. I already asked the question here. The main point is that I tried to prove in Primitive recursive arithmetic (PRA) the totality of the Ackerman function, and I found, that the single thing which can prevent it - nonapplicability of the Deduction theorem to PRA. But I know, that totality of the Ackerman function is unprovable in PRA. Does it mean, that the Deduction theorem is non-applicable to PRA?
People commented, that: "the main reason that PRA does not prove the Ackerman function is total is that PRA does not include enough induction axiom". That's obviously right! I know, that PRA contains only rule of inference for the mathematical induction. And I also know, that transfinite induction up to the ordinal number $\omega^2$, by which we can prove totality of the Ackerman function, in first-order logic is equivalent to double mathematical induction. But the language of PRA is not first-order language of full value. And I tried to use double mathematical induction directly and to find out problems.
Please look to my proof and say where it can be wrong. Now I see the only problem: I used Deduction meta-theorem in the form: $(PRA \wedge a \vdash b) \to (PRA \vdash a \to b)$. As far as I know, this meta-theorem for infinitely many axioms can be proven only if we use mathematical induction (in meta-theory) and thus - it is unobvious.
Emil Jeřábek, you are right: Outer induction is on a $\Pi_2^0$ formula when expressed in the language of Peano arithmetic. We can see it from this post. Induction axiom, used at the last (7) step, is a $\Pi_2^0$ formula.
But the proof in PRA - without quantifiers - instead of this axiom uses inference rule: $[PRA \vdash \psi(0)] \wedge [PRA \vdash \psi(m) \to \psi(m+1)] \to [PRA \vdash \psi(m)]$, where $\psi(m) \equiv \varphi_A(m,1) \wedge \varphi_A(m,K(m))$.
Emil Jeřábek:
Yes, it is wrong. I don’t know how exactly you intended to use the T-predicate, but basically: the T-predicate itself (and the U-function) is primitive recursive, hence equivalent to an open formula of PRA. Then $n=f(m)$ can be expressed by the existential formula $\exists w\,(T(e,m,w)\land U(w)=n), and \exists n\,n=f(m)$ is equivalent to the existential formula $\exists w\,T(e,m,w)$, but there is no way to eliminate these existential quantifiers in PRA (this would imply that f is primitive recursive).
Thank you, it resolves the largest part of the problem! But one else thing remains, that I cannot understand:
Supposing, we consider $\varphi_A$ just as the new predicate symbol, and axioms (1), (2), (3) - as the definition of the predicate. Can't we treat it namely as the predicate of existence for Ackerman function value? And if it's so, why cannot we consider the foregoing proof as the proof of totality of the Ackerman function?
Carl Mummert:
There are two ways of handling PRA in the literature. The first is to use no quantifiers at all; the second is to use quantifiers, just like Peano arithmetic. In the latter sense, totality can be expressed in the language of PRA, of course.
PRA with quantifiers sounds very strange. As far as I know, every unbounded quantifier changes a theory in essence.
Emil Jeřábek:
The language of PRA consists of a handful of initial functions, and it allows defining new functions by composition and primitive recursion. It does not allow adding new functions by Skolemization
It sounds absurdly: How can a language restrict this? If syntax allows infinitely many functional and infinitely many predicate symbols, how can grammar analyzer verify, that they are primitive recursive?
As far as I know, an axioms set (not language!) of PRA is limited by only axioms for primitive recursive functions. OK, we won't treat the definition of Ackerman function as a part of the "PRA's set of axioms".
P.S. Sorry, I again cannot add comment to the thread.
I want to illustrate by an example my last assertion that the verification whether an object is primitive recursive or not is out of the scope of syntax.
How can we prove in PRA associativity of addition: $x+(y+z)=(x+y)+z$?
From the axiom $x+0=x$ we have:
1) $x+(y+0)=(x+y)+0$
By substitution $z$ for $S(z)$ we have:
2) $x+(y+z)=(x+y)+z \to x+(y+S(z))=(x+y)+S(z)$
And (attention!) by the rule of induction from (1) and (2) we have:
3) $x+(y+z)=(x+y)+z$
Is there any kind of verification that $+$ is primitive recursive function before we can apply the rule of induction? NO.
Now let us add to the theory the binary functional symbol $\circ$. We didn't add axioms, defining it. Did we change the theory? I think - no. It's called "conservative extension". Can we prove some new statements about the function $\circ$? Yes. One of statements which we can prove is:
$n \circ 0= n \to x \circ (y \circ z)=(x \circ y) \circ z$
The scheme of the proof is exactly the same as for addition. Please pay attention: Actually I know nothing about operation $\circ$. Maybe $x \circ y = x + y$ or maybe $x \circ y = max(x,y)$. I even don't know, whether it is primitive recursive or not. But the foregoing statement is true in any interpretation, because nothing can prevent us to use the rule of induction for proving it.
