Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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.

share|improve this question

closed as not a real question by Andres Caicedo, Andreas Blass, Emil Jeřábek, François G. Dorais Apr 21 '12 at 13:32

It's difficult to tell what is being asked here. This question is ambiguous, vague, incomplete, overly broad, or rhetorical and cannot be reasonably answered in its current form. For help clarifying this question so that it can be reopened, visit the help center.If this question can be reworded to fit the rules in the help center, please edit the question.

5  
It would be better if you edited your own question if you need to add significant amounts of text rather than adding a new answer each time. Just make it clear where each addition starts and stops and when you added it. –  David Roberts Apr 19 '12 at 7:35
    
The formula is $\Pi^0_2$ WHEN EXPRESSED IN THE LANGUAGE OF PRIMITIVE RECURSIVE ARITHMETIC. It cannot be expressed by a quantifier-free formula. There is no $K$-function in PRA so you cannot use it, you have to replace it with a (universal) quantifier, and as explained many times below, the $\phi_Ai$ formula itself includes an existential quantifier, so your $\psi$ is only $\Pi^0_2$. –  Emil Jeřábek Apr 19 '12 at 11:15
    
Regarding the new addition: the problem is that you are trying to apply the induction scheme in PRA to a formula that is not included in that scheme. The formula $\phi_A$ still has an existential quantifier. In the case of this scheme it does not matter whether it is written as an axiom scheme or as an inference rule; the only reason people write it as an inference rule is to work with open formulas. In any case, the induction scheme or rule in PRA only applies to open formulas, even if we work in the version of PRA that does have quantifiers. –  Carl Mummert Apr 19 '12 at 11:17
    
@Emil Jeřábek: I think that $K$ function is harmless - we could pretend the entire proof is in a weak second-order arithmetic, and then $K$ is just a free variable. Of course we would have to ask whether the induction scheme includes formulas with free variables (cf. the difference between induction in PA and induction in $\mathsf{ACA}_0$) but in this case the existential quantifier in $\phi$ overshadows that problem. –  Carl Mummert Apr 19 '12 at 11:19
2  
It seems to me that the many comments by Carl and Emil are not doing much good for eugepros, though they provided useful information for me and probably for other readers. So I've just voted to close this question. –  Andreas Blass Apr 20 '12 at 13:24

3 Answers 3

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.

share|improve this answer
    
Thank you for your comment. But you are right: I don't understand something. As far as I know, the formula $\varphi_A(m,n)$ for totality of the Ackerman function is expressible in the language of PRA. What is a problem? Mathematical induction for it is implemented by the inference rule of PRA, just as for any other PRA formula: $[PRA \vdash \varphi(0)] \wedge [PRA \vdash \varphi(n) \to \varphi(n+1)] \to [PRA \vdash \varphi(n)]$ Where exactly my reasoning was wrong? –  eugepros Apr 18 '12 at 5:42
    
PRA only includes induction for quantifier-free formulas. The formula $\phi_A$ from your other post is $\Sigma_0^1$. Of course $\Sigma^0_1$ induction won't prove the totality of the Ackermann function, either, so something else is strange. 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. –  Carl Mummert Apr 18 '12 at 10:07
1  
The Skolem function is a sneaky way to lower the complexity of the formula. The outer induction (in step 10) is on a $\Pi^0_2$ formula when expressed in the language of arithmetic. Eliminating this invalid device yields more or less the standard proof of totality of the Ackermann function in $I\Sigma_1+I\Pi_2^-$. –  Emil Jeřábek Apr 18 '12 at 11:48

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.

share|improve this answer
2  
Your formula $\varphi_A$ starts with an unbounded quantifier $\exists k$. You cannot write that in a quantifier-free way. –  Emil Jeřábek Apr 18 '12 at 11:51
    
I understand, that every statement of totality actually is $\Pi_2^0$, because it looks like $\forall m \exists n ~ n=f(m)$, where quantifiers are unbounded. But I relied on the assertion, that using Kleene's T-predicate it can be written in the language of PRA. Is it wrong? –  eugepros Apr 18 '12 at 14:03
2  
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). –  Emil Jeřábek Apr 19 '12 at 9:54
1  
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. –  Carl Mummert Apr 19 '12 at 10:51

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)]$

share|improve this answer
    
The issue I see is in (6). Ignoring the $\forall m$ quantifier, this has the general form $(\forall \exists) \to (\forall \exists)$, in other words the property is $\Delta^0_3$. The induction axiom for that formula isn't in PRA. Now I think I see why you are interested in the deduction theorem, because you want to get rid of the hypothesis of the induction formula, reducing it to $(\forall \exists)$. That does work to reduce the complexity of the induction formula, but PRA still doesn't have induction for $\Pi^0_2$ formulas. –  Carl Mummert Apr 19 '12 at 11:04
1  
Thanks for taking the time to rewrite the proof in this way. –  Carl Mummert Apr 19 '12 at 11:06
    
The induction formula in (6) is just $\varphi_A(m+1,n)$ (where $n$ is the induction variable, and $m$ is a parameter), i.e., it is an instance of the $\Sigma^0_1$-induction axiom (which is still not available in PRA, but it’s close). –  Emil Jeřábek Apr 19 '12 at 12:27

Not the answer you're looking for? Browse other questions tagged or ask your own question.