According to the Wikipedia ACA0 is a conservative extension of First Order logic + PA.
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,