13
$\begingroup$

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

Improve this question
$\endgroup$
11
  • $\begingroup$ My immediate guess for a): Take a model of PA, now prove that you can add a second order part to it by naming the arithmetically defined sets. This gives a model of $ACA_0$. Thus every first order consequence of $ACA_0$ must hold in every model of PA. I'm not sure I understand b) at all. Regarding c): My guess would be to try to take a proof in $ACA_0$ and replace occurrences of second order variables "X" by their arithmetically defining formulae. $\endgroup$
    – Uri Andrews
    Commented May 6, 2010 at 22:10
  • $\begingroup$ To clarify b). Consider the proof of a) and give that proof in a formal logic. What kind of logic do you need? If you take a model of PA, you need a second order logic. However, the question itself is of first order + PA. So, question b) is, whether the proof of a) can be given in first order + PA. For the algorithm. It isn't that easy. If you have higher order quantifier introduction, then it must be eliminated (because the end proof is first order). The tricky situation occurs when introduction appears after elimination in the proof. $\endgroup$
    – Lucas K.
    Commented May 6, 2010 at 22:30
  • 1
    $\begingroup$ I'll try to post a full answer when I have time: (a) Uri's guess is correct; (b) please rewrite that question in a meaningful way as in your comment above; (c) I don't think cleverness will help because of Gödel's Speed-Up Theorems - plato.stanford.edu/entries/goedel/#SpeUpThe $\endgroup$
    – François G. Dorais
    Commented May 6, 2010 at 22:45
  • $\begingroup$ I don't think the Speed-Up Theorems apply. We're not bounding the length of a proof of $\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. $\endgroup$
    – Chad Groft
    Commented May 7, 2010 at 0:18
  • $\begingroup$ I was thinking too quickly. Chad is right about the Speed-Up Theorems: they would apply for ACA vs PA, but not ACA_0 vs PA. $\endgroup$
    – François G. Dorais
    Commented May 7, 2010 at 1:02

3 Answers 3

Reset to default
8
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Thanks for the answers. I have enough material to continue for now. I will also look at proof-normalization and cut-elimination as suggested by alexod.<br/><br/> To answer your question on why I want this. If I have an algorithm then I can also apply it on a full second order proof, which is not ACA<sub>0</sub>. It should end on using the induction axiom with a second order induction hypothesis. At least some of those uses can be reduced by using the constructive (or finitist) omega rule. I have the believe that Hilbert's program can be carried out in modified form. PA + COR is very strong. $\endgroup$
    – Lucas K.
    Commented May 9, 2010 at 9:46
13
$\begingroup$

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

  1. The model-theoretic proof in Simpson's book that Charles Stewart refers to.

  2. A proof-theoretic proof is given in Shoenfield's paper "A Relative Consistency Proof", Journal of Symbolic Logic 19 (1) 21-28, 1954.

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

Improve this answer
$\endgroup$
6
  • 1
    $\begingroup$ More: In Petr Hájek and Pavel Pudlák's book "Metamathematics of First-Order Arithmetic", they give the model-theoretic proof (Theorem III.1.16) and show that it is formalisable in $I \Sigma_1$, the subtheory of PA in which induction is restricted to $\Sigma_1$-formulas (Theorem IV.4.10). $\endgroup$
    – user7247
    Commented Jul 5, 2010 at 13:35
  • 1
    $\begingroup$ @robin-adams : This is very elegant, thanks. Also, many thanks for all the references. I knew of Shoenfield's argument (which I needed in a course, since I wanted to prove a result about PA arguing about ACA${}_0$ within PA), and of course I knew the model theoretic argument (your item 1), but wasn't aware of the others. $\endgroup$
    – Andrés E. Caicedo
    Commented Nov 5, 2010 at 4:14
  • 1
    $\begingroup$ How do you create a cut-free proof when PA has induction axioms that don't allow for cut-elimination? $\endgroup$
    – Russell O'Connor
    Commented May 8, 2011 at 15:33
  • 1
    $\begingroup$ I meant $\Delta$ to be a cut-free proof in pure predicate logic (LK) of a sequent of the form $\Gamma, \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$, where \Gamma is some finite sequence of axioms of PA. $\endgroup$
    – user7247
    Commented May 27, 2011 at 16:10
  • 3
    $\begingroup$ Actually, what I wrote way back last July is not quite correct, since free set variables might occur in the induction axioms used in $ACA_0$. But it's reparable. $\Delta$ is a cut-free proof of $\Gamma, \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$, where $\Gamma$ is some finite sequence of the non-comprehension axioms of $ACA_0$. Replace $t \in X_i$ with $[t/x_i]\phi_i$, and $t \in Y$ with $t = t$ for every other set variable $Y$. $\endgroup$
    – user7247
    Commented May 27, 2011 at 16:46
6
$\begingroup$

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

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .