1
$\begingroup$

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.

$\endgroup$
21
  • 5
    $\begingroup$ 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. $\endgroup$
    – David Roberts
    Apr 19, 2012 at 7:35
  • 1
    $\begingroup$ 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$. $\endgroup$ Apr 19, 2012 at 11:15
  • 3
    $\begingroup$ 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. $\endgroup$ Apr 20, 2012 at 13:24
  • 1
    $\begingroup$ @Andreas: I agree. @eugenpros: No one is using any semantic arguments here, your "proof" violates the syntactic constraints on (not only) the induction rule. PRA is not an extensible jelly, it is a particular formal system with a fixed language and a fixed set of axioms and derivation rules. (Except that different authors use different, but generally equivalent, versions of these particulars.) For example formal descriptions of PRA, see projecteuclid.org/euclid.pjm/1102905993 or dx.doi.org/10.1002/malq.19870330210 (the latter calls the theory $\mathcal A$). $\endgroup$ Apr 20, 2012 at 15:21
  • 1
    $\begingroup$ @eugepros: Since you wish to avoid semantics and rely on syntax, and since you say that, from the syntax point of view $\varphi_A$ and $K$ are simply symbols, (part of) the problem with your proof can be explained by observing that these two symbols, $\varphi_A$ and $K$, are not symbols of PRA. $\endgroup$ Apr 21, 2012 at 1:17

3 Answers 3

8
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ 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? $\endgroup$
    – eugepros
    Apr 18, 2012 at 5:42
  • $\begingroup$ 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. $\endgroup$ Apr 18, 2012 at 10:07
  • 1
    $\begingroup$ 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^-$. $\endgroup$ Apr 18, 2012 at 11:48
-1
$\begingroup$

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.

$\endgroup$
4
  • 2
    $\begingroup$ Your formula $\varphi_A$ starts with an unbounded quantifier $\exists k$. You cannot write that in a quantifier-free way. $\endgroup$ Apr 18, 2012 at 11:51
  • $\begingroup$ 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? $\endgroup$
    – eugepros
    Apr 18, 2012 at 14:03
  • 3
    $\begingroup$ 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). $\endgroup$ Apr 19, 2012 at 9:54
  • 2
    $\begingroup$ 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. $\endgroup$ Apr 19, 2012 at 10:51
-1
$\begingroup$

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

$\endgroup$
3
  • $\begingroup$ 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. $\endgroup$ Apr 19, 2012 at 11:04
  • 1
    $\begingroup$ Thanks for taking the time to rewrite the proof in this way. $\endgroup$ Apr 19, 2012 at 11:06
  • $\begingroup$ 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). $\endgroup$ Apr 19, 2012 at 12:27

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