Applicability of Deduction theorem to Primitive recursive arithmetic - MathOverflow [closed]

Applicability of Deduction theorem to Primitive recursive arithmetic

2012-04-17T20:24:31Z

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.

Answer by Andreas Blass for Applicability of Deduction theorem to Primitive recursive arithmetic

2012-04-17T21:30:46Z

Both Carl Mummert and I answered your previous question, in comments, but it seems you haven't understood what we wrote. The problem is with induction, not with the deduction theorem. Your argument applies the principle of mathematical induction in a way that is not justified in PRA. The difficulty is not, as you seem to assume in the present question, the length of the induction ($\omega^2$ versus $\omega$) but the complexity of the formula being proved by induction. Although there are different formalizations of PRA in the literature, they all share the property that mathematical induction is available only for very limited classes of formulas, classes that do not include the formulas involved in your argument.

Answer by eugepros for Applicability of Deduction theorem to Primitive recursive arithmetic

2012-04-18T11:31:01Z

The formula $\varphi_A$ from your other post is $\Sigma_0^1$

As far as I can see from the topic about Ackerman function, using T-predicate, we can express this formula in the syntax of PRA - which means: without quantifiers. Perhaps, I don't understand something?

But the way that that proof is written makes it difficult to follow. Can you write it in the usual way without adding a new Skolem function, and with explicit quantifiers instead of free variables? I suspect that doing that will expose the flaw in the proof.

Yes, if it may be helpful, I write the proof with quantifiers a bit later. But it's very strange: Using quantifiers, we'll have usual Peano arithmetic proof, in which there is no any flaws. It will be merely double mathematical induction, which is similar to transfinite induction up to $\omega^2$.

I supposed, that the problem was specifically in restrictions of PRA syntax. That was the reason why I tried to write the proof without quantifiers.

P.S. Sorry, I cannot add comment to the last post of Carl Mummert: errors emerge.

Answer by eugepros for Applicability of Deduction theorem to Primitive recursive arithmetic

2012-04-19T06:43:45Z

But the way that that proof is written makes it difficult to follow. Can you write it in the usual way without adding a new Skolem function, and with explicit quantifiers instead of free variables?

Carl, as you asked me, I'm writing the proof in Peano arithmetic syntax - with explicit quantifiers.

Here is three axioms, which define Ackerman function:

A) $\forall n ~ A(0,n) = n+1$
B) $\forall m ~ A(m+1,0) = A(m,1)$
C) $\forall m,n ~ A(m+1,n+1) = A(m, A(m+1,n))$

If we define predicate $\varphi_A(m,n)$, which means: $\exists k ~ k=A(m,n)$, then the three base statements are true:

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

Hereafter the proof as such:

4) $\forall m ~ [\forall k ~ \varphi_A(m,k)] \to \varphi_A(m+1,0)$ - from (2), by substitution $1$ in place of $k$.
5) $\forall m ~ [\forall k ~ \varphi_A(m,k)] \to [\varphi_A(m+1,0) \wedge \forall n ~ \varphi_A(m+1,n) \to \varphi_A(m+1,n+1)]$ - from (3) and (4)
6) $\forall m ~ [\forall k ~ \varphi_A(m,k)] \to [\forall n ~ \varphi_A(m+1,n)]$ - from (5), using the induction axiom:
$\forall m ~ [\varphi_A(m+1,0) \wedge \forall n ~ \varphi_A(m+1,n) \to \varphi_A(m+1,n+1)] \to [\forall n ~ \varphi_A(m+1,n)]$
7) $\forall m,n ~ \varphi_A(m,n)$ - from (1) and (6), using the induction axiom:
$\forall n ~ \varphi_A(0,n) \wedge \forall m ~ [\forall n ~ \varphi_A(m,n) \to \forall n ~ \varphi_A(m+1,n)] \to \forall m ~ [\forall n ~ \varphi_A(m,n)]$