13

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

Lucas K.
  • 1,659
  • 1
  • 13
  • 24
  • 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.

     – Uri Andrews May 06 '10 at 22:10
  • 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.

     – Lucas K. May 06 '10 at 22:30
  • 1
    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 - http://plato.stanford.edu/entries/goedel/#SpeUpThe – François G. Dorais May 06 '10 at 22:45
  • 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.

     – Chad Groft May 07 '10 at 00:18
  • 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. – François G. Dorais May 07 '10 at 01:02
  • @Chad: I don't understand this part of your objection: "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." – François G. Dorais May 07 '10 at 01:14
  • @Lucas: when you have higher-order quantification, you can do that in PA. You can quantify over formulas by using their G"odel codes. I think it works because $ACA_0$ doesn't let you quantify over any sets that PA doesn't already know about. – Uri Andrews May 07 '10 at 02:30
  • Thanks for the comments! Question b is more clear now.

    @Uri, where do I have to take the Gödel numbers? For a) or c)? I don't see how I can use it in the algorithm.

    @François, I am rather confident that I can make the algorithm of c. I wanted to know if it is known science.

    If it is not possible, it means there is a ACA0 proof with a First Order final theorem, which does not give a clue of the First Order counterpart. A kind of minimal example of such non-reducible proof would be nice, because it gives a better understanding what higher order logic is about.

     – Lucas K. May 07 '10 at 16:42
  • @Lucas: I mean in (c): when the $ACA_0$ proof refers to the variable X, we translate it into a PA proof referring to Godel codes. In particular, we can mimic quantification over sets by quantifying over Godel codes for formulas. I think that should give you a PA proof from an ACA_0 one. – Uri Andrews May 07 '10 at 19:36
  • I think Uri is right, the argument can be carried out using $\Sigma_n$ truth definitions but it is not uniform; the argument doesn't seem to go through in PA, which would answer (b). A good test case for the algorithm would be the statements $Con(I\Sigma_n)$. The standard proofs in ACA_0 and PA are essentially the same: find a truth definition for $\Sigma_n$ formulas. Since ACA_0 can work with sets instead of explicit formulas, the proof is much more uniform. My guess is that ACA_0 will have a sizable speed-up over PA for these formulas. – François G. Dorais May 07 '10 at 21:46
  • For c) I suppose if you apply a proof normalization (or cut elimination) to a proof of say a $\Pi^0_2$-statement in $ACA_0$, second order quantification will vanish and the proof will become first order. – alexod May 08 '10 at 08:44

3 Answers3

13

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

user7247
  • 306
  • 1
    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). – user7247 Jul 05 '10 at 13:35
  • Thanks for the answer. I am now convinced, that the key factor in proof-strength is the things you allow in the induction hypothesis. This interesting (and maybe well known), but it has never been the focus of education of principles of mathematics or logic. What I want to do, is to extend FO PA with an additional construct/axiom, such that the proof strength becomes equal to full second order logic, without fully defining an higher order logic within the FO PA. The expressivenss of the system remains FO PA. – Lucas K. Jul 09 '10 at 21:00
  • 1
    @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. – Andrés E. Caicedo Nov 05 '10 at 04:14
  • 1
    How do you create a cut-free proof when PA has induction axioms that don't allow for cut-elimination? – Russell O'Connor May 08 '11 at 15:33
  • 1
    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. – user7247 May 27 '11 at 16:10
  • 3
    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$. – user7247 May 27 '11 at 16:46
8

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.

Charles Stewart
  • 2,283
  • 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.

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

     – Lucas K. May 09 '10 at 09:46
6

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

Emil Jeřábek
  • 44,710