Reducing ACA₀ proof to First Order PA - MathOverflow

Reducing ACA₀ proof to First Order PA

2010-05-06T21:39:01Z

According to the Wikipedia ACA₀ 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₀ 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 ∏⁰₂ 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₀ formal proof that ends in a theorem that is part of First Order logic + PA, is there an algorithm that reduces the ACA₀ 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₀ 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₀ 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

Answer by Charles Stewart for Reducing ACA₀ proof to First Order PA

2010-05-08T09:33:04Z

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; maybe you will find this of use? Kohlenbach's works in general are relevant to this kind of question, see his publications page and his book, Applied proof theory: proof interpretations and their use in mathematics (2009) Springer Verlag.

Answer by robin-adams for Reducing ACA₀ proof to First Order PA

2010-07-01T12:24:42Z

There are three published proofs of this result that I know of:

The model-theoretic proof in Simpson's book that Charles Stewart refers to.
A proof-theoretic proof is given in Shoenfield's paper "A Relative Consistency Proof", Journal of Symbolic Logic 19 (1) 21-28, 1954.
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: http://arxiv.org/abs/0906.1726

Of the three, only Shoenfield's proof actually gives an algorithm for converting a proof in ACA0 into a proof in PA.

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.

Suppose $ACA_0 \vdash \alpha$, where $\alpha$ is an arithmetic sentence. Let the instances of the comprehension axiom used in the proof be

$\exists X \forall x (x \in X \leftrightarrow \phi_1), \ldots, \exists X \forall x (x \in X \leftrightarrow \phi_n)$.

Then we have

$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$

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

Replace every atomic formula $t \in X_i$ throughout $\Delta$ with $[t/x_i]\phi_i$. The result is a proof of

$PA + { \forall x_1 (\phi_1 \leftrightarrow \phi_1), \ldots, \forall x_n (\phi_n \leftrightarrow \phi_n) } \vdash \alpha$

in which no set variables appear. Therefore, $PA \vdash \alpha$.

Answer by Emil Jeřábek for Reducing ACA₀ proof to First Order PA

2011-02-03T16:41:04Z

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