According to the Wikipedia ACA0 is a conservative extension of First Order logic + PA.


<http://en.wikipedia.org/wiki/Reverse_Mathematics>


First of all I have a few questions about the proof:  

a - What is the general sketch of this proof, is it based on models?  

b - Consider the theorem that ACA0 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 ∏02 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?


Then I am interested in the following:  

c - Given an ACA0 formal proof that ends in a theorem that is part of First Order logic + PA, is there an algorithm that reduces the ACA0 proof to First Order + PA proof?


One could just do a breath first search on First Order logic + PA and given the fact that ACA0 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.


I am struggling with this algorithm for months. In general an ACA0 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.


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.


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).


Thanks in advance,


Lucas



Reducing ACA₀ proof to First Order PA
Chapter nine of Simpson (1999) *Subsystems of Second-Order Arithmetic* proves (a) by showing how to construct a second-order model for ACA0 from a first-order model of PA.


(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.


(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, [Proof Mining in Subsystems of Analysis](http://www.brics.dk/DS/03/12/BRICS-DS-03-12.pdf); maybe you will find this of use? Kohlenbach's works in general are relevant to this kind of question, see [his publications page](http://www.mathematik.tu-darmstadt.de/~kohlenbach/) and his book, *Applied proof theory: proof interpretations and their use in mathematics* (2009) Springer Verlag.


