Ackermann function in the Primitive recursive arithmetic - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-22T17:42:48Z http://mathoverflow.net/feeds/question/35217 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/35217/ackermann-function-in-the-primitive-recursive-arithmetic Ackermann function in the Primitive recursive arithmetic Dan 2010-08-11T12:37:25Z 2012-04-18T05:12:18Z <p>Hello.</p> <p>I study <a href="http://en.wikipedia.org/wiki/Primitive_recursive_arithmetic" rel="nofollow">primitive recursive arithmetic</a> and have the following questions.</p> <p>1) Is it possible to express in the PRA that Ackermann function is total?</p> <p>2) If yes, is such expression decidable in the PRA ?</p> <p>Can u suggest some literature on this topic?</p> <p>Thank you.</p> http://mathoverflow.net/questions/35217/ackermann-function-in-the-primitive-recursive-arithmetic/35219#35219 Answer by Carl Mummert for Ackermann function in the Primitive recursive arithmetic Carl Mummert 2010-08-11T12:56:33Z 2010-08-11T12:56:33Z <p>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. </p> <p>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. </p> <p>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, <em>Metamthematics of First-Order Arithmetic</em>. </p> http://mathoverflow.net/questions/35217/ackermann-function-in-the-primitive-recursive-arithmetic/94291#94291 Answer by eugepros for Ackermann function in the Primitive recursive arithmetic eugepros 2012-04-17T13:52:34Z 2012-04-17T14:10:22Z <p>Carl, can I ask you one more question concerning the topic?</p> <p>I thought about the reasons why we cannot prove in <a href="http://en.wikipedia.org/wiki/Primitive_recursive_arithmetic" rel="nofollow">PRA</a> totality of the <a href="http://en.wikipedia.org/wiki/Ackerman_function" rel="nofollow">Ackerman function</a> $A(m,n)$, directly using double mathematical induction for $n$ then for $m$, and came to a conclusion, that it's because the <a href="http://en.wikipedia.org/wiki/Deduction_theorem" rel="nofollow">deduction theorem</a> is nonapplicable to PRA. Please correct me if the following reasoning is wrong.</p> <p>First, let us define in the PRA language, using <a href="http://en.wikipedia.org/wiki/Kleene%27s_T_predicate" rel="nofollow">Kleene's T predicate</a>, the predicate $\varphi_A(m,n)$, which means: $\exists k ~ k=A(m,n)$.</p> <p>Second, using the definition of $A(m,n)$, let us amplify the PRA by the next three axioms:</p> <p>1) $\varphi_A(0,n)$</p> <p>2) $\varphi_A(m,1) \to \varphi_A(m+1,0)$</p> <p>3) $\varphi_A(m,K(m)) \to [\varphi_A(m+1,n) \to \varphi_A(m+1,n+1)]$</p> <p>The axiom (3) is the result of <a href="http://en.wikipedia.org/wiki/Skolem_normal_form" rel="nofollow">Skolemization</a> of the next assertion:</p> <p>$\forall m ~ [\forall k ~ \varphi_A(m,k)] \to [\forall n ~ \varphi_A(m+1,n) \to \varphi_A(m+1,n+1)]$</p> <p>where $K$ is the new functional symbol.</p> <p>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)$:</p> <p>4) $[\varphi_A(m,1) \wedge \varphi_A(m,K(m))] \to \varphi_A(m+1,0)$</p> <p>5) $[\varphi_A(m,1) \wedge \varphi_A(m,K(m))] \to [\varphi_A(m+1,n) \to \varphi_A(m+1,n+1)]$</p> <p>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):</p> <p>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)])$</p> <p>Here we can see a premise of mathematical induction for $n$ - in the right part of the implication.</p> <p>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.</p> <p>So, let us <strong>suppose</strong>, that we can use deduction theorem in the form: $(PRA \wedge a \vdash b) \to (PRA \vdash a \to b)$.</p> <p>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, <strong>by the deduction theorem</strong> we have: </p> <p>7) $\varphi_A(m,1) \wedge \varphi_A(m,K(m)) \to \varphi_A(m+1,n)$</p> <p>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:</p> <p>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))$</p> <p>Sixth, from (1) we can conclude:</p> <p>9) $\varphi_A(0,1) \wedge \varphi_A(0,K(0))$</p> <p>Seventh, from (8) and (9), using mathematical induction for $m$, we can conclude:</p> <p>10) $\varphi_A(m,1) \wedge \varphi_A(m,K(m))$</p> <p>Eighth, from (7) and (10) we can conclude:</p> <p>11) $\varphi_A(m+1,n)$</p> <p>Jointly with (1) it means $\varphi_A(m,n)$ - assertion about totality of the Ackerman function.</p> <p>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?</p>