Reducing ACA₀ proof to First Order PA - MathOverflow most recent 30 from http://mathoverflow.net 2013-06-19T02:13:36Z http://mathoverflow.net/feeds/question/23788 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/23788/reducing-aca-proof-to-first-order-pa Reducing ACA₀ proof to First Order PA Lucas K. 2010-05-06T21:39:01Z 2011-02-03T16:41:04Z <p>According to the Wikipedia ACA<sub>0</sub> is a conservative extension of First Order logic + PA.</p> <p><a href="http://en.wikipedia.org/wiki/Reverse_Mathematics" rel="nofollow">http://en.wikipedia.org/wiki/Reverse_Mathematics</a></p> <p>First of all I have a few questions about the proof:<br/> a - What is the general sketch of this proof, is it based on models?<br/> b - Consider the theorem that ACA<sub>0</sub> is a conservative extension of First Order + PA, and the proof of that theorem is proven in a formal system, what kind of logic is needed? If the proof is based on models, then it requires second order logic. However, the theorem itself is a &prod;<sup>0</sup><sub>2</sub> question as far as I understand, and can be expressed in First Order logic + PA. Is there also a proof in First Order logic + PA?</p> <p>Then I am interested in the following:<br/> c - Given an ACA<sub>0</sub> formal proof that ends in a theorem that is part of First Order logic + PA, is there an algorithm that reduces the ACA<sub>0</sub> proof to First Order + PA proof?</p> <p>One could just do a breath first search on First Order logic + PA and given the fact that ACA<sub>0</sub> is a conservative extension, it is guaranteed to end. So, the answer to question c is definitely "yes", but I am looking for something more clever.</p> <p>I am struggling with this algorithm for months. In general an ACA<sub>0</sub> proof, with a First Order + PA end theorem reduces rather easier. However, there are some non-trivial cases. If the answer to question b is "yes", then that proof might give hints for constructing the algorithm.</p> <p>I want to use this algorithm to reduce proofs of full second order, such that the reduced proof is First Order logic + PA, or contains the use of the induction scheme with a second order induction hypothesis.</p> <p>In many cases the use of second order induction hypothesis, can be reduced by using the "Constructive Omega Rule". I want to understand the limitations of this (if any).</p> <p>Thanks in advance,</p> <p>Lucas</p> http://mathoverflow.net/questions/23788/reducing-aca-proof-to-first-order-pa/23922#23922 Answer by Charles Stewart for Reducing ACA₀ proof to First Order PA Charles Stewart 2010-05-08T09:33:04Z 2010-05-08T09:33:04Z <p>Chapter nine of Simpson (1999) <em>Subsystems of Second-Order Arithmetic</em> proves (a) by showing how to construct a second-order model for ACA0 from a first-order model of PA.</p> <p>(b) The "second-order" we are talking about is really first-order multi-sorted logic, i.e., the second-order quantifiers have Henkin semantics. So it's all first order, all the way down.</p> <p>(c) Yes, you are right in your thoughts about getting PA proofs from ACA0. Why do you want to do this? Proofs in PA of a given theorem may be much longer than in ACA0, to the extent that they may useless as witness objects. Paulo Oliva, a student of Kohlenbach's, has studied the application of Kohlenbach's "proof mining" to subsystems of second-order arithmetic in his PhD dissertation, <a href="http://www.brics.dk/DS/03/12/BRICS-DS-03-12.pdf" rel="nofollow">Proof Mining in Subsystems of Analysis</a>; maybe you will find this of use? Kohlenbach's works in general are relevant to this kind of question, see <a href="http://www.mathematik.tu-darmstadt.de/~kohlenbach/" rel="nofollow">his publications page</a> and his book, <em>Applied proof theory: proof interpretations and their use in mathematics</em> (2009) Springer Verlag.</p> http://mathoverflow.net/questions/23788/reducing-aca-proof-to-first-order-pa/30175#30175 Answer by robin-adams for Reducing ACA₀ proof to First Order PA robin-adams 2010-07-01T12:24:42Z 2010-07-01T12:24:42Z <p>There are three published proofs of this result that I know of:</p> <ol> <li><p>The model-theoretic proof in Simpson's book that Charles Stewart refers to.</p></li> <li><p>A proof-theoretic proof is given in Shoenfield's paper "A Relative Consistency Proof", Journal of Symbolic Logic 19 (1) 21-28, 1954.</p></li> <li><p>Another proof-theoretic proof fell out as a corollary of my recent work on type theory, quite unexpectedly. I give it as Theorem 6.2 in my paper "Classical Predicative Logic-Enriched Type Theories", to appear in APAL. Preprint available here: <a href="http://arxiv.org/abs/0906.1726" rel="nofollow">http://arxiv.org/abs/0906.1726</a></p></li> </ol> <p>Of the three, only Shoenfield's proof actually gives an algorithm for converting a proof in ACA0 into a proof in PA.</p> <p>It is also possible to prove it using cut-elimination, but I don't know anywhere where this has been published. Here's a sketch proof.</p> <p>Suppose $ACA_0 \vdash \alpha$, where $\alpha$ is an arithmetic sentence. Let the instances of the comprehension axiom used in the proof be</p> <p>$\exists X \forall x (x \in X \leftrightarrow \phi_1), \ldots, \exists X \forall x (x \in X \leftrightarrow \phi_n)$.</p> <p>Then we have</p> <p>$PA + { \forall x_1 (x_1 \in X_1 \leftrightarrow \phi_1), \ldots, \forall x_n (x_n \in X_n \leftrightarrow \phi_n) } \vdash \alpha$</p> <p>Using cut-elimination, construct a cut-free proof $\Delta$ of the above. Since the proof is cut-free, it involves no set variables other than $X_1, \ldots, X_n$.</p> <p>Replace every atomic formula $t \in X_i$ throughout $\Delta$ with $[t/x_i]\phi_i$. The result is a proof of</p> <p>$PA + { \forall x_1 (\phi_1 \leftrightarrow \phi_1), \ldots, \forall x_n (\phi_n \leftrightarrow \phi_n) } \vdash \alpha$</p> <p>in which no set variables appear. Therefore, $PA \vdash \alpha$.</p> http://mathoverflow.net/questions/23788/reducing-aca-proof-to-first-order-pa/54212#54212 Answer by Emil Jeřábek for Reducing ACA₀ proof to First Order PA Emil Jeřábek 2011-02-03T16:41:04Z 2011-02-03T16:41:04Z <p>To elaborate on robin-adams' answer, the proof of the conservation using cut elimination produces an algorithm running in superexponential time (i.e., $t(n)$ is $n$-times iterated exponentiation; that's the complexity of cut elimination), and it can be formalized in $I\Delta_0+SUPEXP$. This is essentially optimal, as a result of Solovay states that $\mathrm{ACA}_0$ has non-elementary speed-up over PA (i.e., a finite tower of exponentials won't do).</p>