According to the Wikipedia ACA_{0} 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 ACA_{0} 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 ∏^{0}_{2} 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 ACA_{0} formal proof that ends in a theorem that is part of First Order logic + PA, is there an algorithm that reduces the ACA_{0} proof to First Order + PA proof?

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

`$\phi$`

in terms of the length of`$\phi$`

, we're bounding one type of proof in terms of another type. I would guess that there is some sort of recursive construction of a first-order proof from a second-order proof. You'd want to prove a super-theorem like "if`$\mathrm{ACA}_0 \vdash \phi$`

, then there is a proof whose formulae all have no more 2nd-order variables or quantifiers than`$\phi$`

itself", by eliminating steps which decreased QC or variable count. – Chad Groft May 7 '10 at 0:18