3 Clarified b)

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 - The theory 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 thinkunderstand, and is can be expressed in First Order logic + PA. Is there also a proof in First Order logic + PAof this?

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

Lucas

2 edited tags
1

# Reducing ACA₀ proof to First Order PA

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 - The theory itself is a ∏02 question I think, and is there a proof in First Order logic + PA of this?

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