4
$\begingroup$

Following on from my question about $\omega$-models, I'm interested in the interaction between subsystems of second order arithmetic with restricted induction such as $\mathsf{RCA}_0$ and those which additionally satisfy the full second order induction scheme, that is, the universal closure of

$$(\varphi(0) \wedge \forall{n}( \varphi(n) \rightarrow \varphi(n + 1))) \rightarrow \forall{n} \; \varphi(n)$$

for all formulae $\varphi$ in the language of second order arithmetic $\mathrm{L}_2$, such as $\mathsf{RCA}$. Specifically, do the unsubscripted systems prove the consistency of their subscripted counterparts, in all or some cases?

I believe that in the case of $\mathsf{ACA}$ and $\mathsf{ACA}_0$ then this does hold, since $\mathsf{ACA}$ proves the consistency of $\mathrm{PA}$, which is equiconsistent with $\mathsf{ACA}_0$—but I can't remember where I heard that, nor why it's true. As a stab in the dark I would guess that perhaps one could formalise a truth predicate for first order arithmetic in second order arithmetic and then proceed by induction in the length of proofs, but that may be a rather wild guess.

  • 0
    I know this is an old post but I was looking for the answer to this very question. I subsequently found http://www.logicmatters.net/resources/pdfs/SubsystemsRevised.pdf that has a brief sketch of the proof that ACA proves Con(PA), but of course I'm totally not qualified to answer your question.2016-08-05

1 Answers 1

4

I realized that the argument I had in mind for my original answer is flawed, and after some more thought I don't know how to fix it or even whether it is correct. It may be better to un-accept this answer to see if someone else can respond to the full question before I can.

I can answer the part about ACA and PA. It is true that ACA proves the consistency of PA. This is because ACA is able to define a truth predicate for formulas of PA, using $\Sigma^1_1$ induction. It can't make the entire truth predicate, because this predicate is not in the minimal $\omega$-model of ACA consisting of just the arithmetical sets, but ACA can prove by $\Sigma^1_1$ induction that for each $n$ there is a truth predicate $T_n$ for $\Sigma^0_n$ formulas. Then ACA can use these partial truth predicates to verify that the axioms of PA are all true and $0=1$ is false, so PA is consistent. The difference with $\mathsf{ACA}_0$ is that $\mathsf{ACA}_0$ cannot prove that for every $n$ there is a satisfaction predicate for $\Sigma^0_n$ formulas, it can only prove the existence for each fixed standard $n$.

  • 0
    It looks like T is conservative over PA, because it doesn't prove that any sets exist.2012-04-28
  • 0
    @aaa: the induction scheme in PA is limited to formulas with no set variables, while induction in T is for all formulas in the language of second-order arithmetic. Since T proves Con(PA), T cannot be even $\Pi^0_1$ conservative over PA.2012-04-28
  • 0
    But T doesn't prove there are any sets. In models where there aren't any sets, every formula in the language of second-order arithmetic is equivalent to one with no set variables. Also, you say that T proves the consistency of $\Pi^1_k-CA$, but T is a subtheory of $\Pi^1_k-CA$, so this would violate Gödel's theorem.2012-04-29
  • 0
    @aaa: I see what you mean in the last sentence. I was using the fact that $Z_2$ does prove, for each $k$, that there is a $\beta$-model of $\Pi^1_k\text{-CA}_0$. But $Z_2$ won't prove that these are models of full induction, as I was mistakenly thinking when I wrote the original answer.2012-04-29
  • 0
    Thanks @Carl, that's really helpful. Do you know any sources that discuss this further? I kind of expected it to be covered in _Subsystems of Second Order Arithmetic_, but it doesn't seem to be, although I may have missed it.2012-05-01
  • 1
    @Benedict: I don't know of anywhere that it is discussed, it's just "one of those things". But I would guess that it was known to Feferman and Friedman, and probably others, back in the 1960s.2012-05-01
  • 1
    @Carl that sounds right. Looking at early papers in what became reverse maths, Friedman's 1975 paper 'Some Systems of Second Order Arithmetic and Their Use' uses full induction, but he was already addressing systems with restricted induction at that time.2012-05-01
  • 0
    @Carl could you give me a hint as to what the problem was with your original answer? Sorry for dredging this back up after a month and a half, I didn't realise you'd edited your post until yesterday.2012-07-04
  • 0
    @Benedict: Sorry about that. I mistakenly thought adding the definable sets to a model satisfying the full induction scheme would give a model of $Z_2$. I now think that claim is false. At the time I checked only whether the extension model would still satisfy full induction, which it would. Later I realized that I can't prove that the extension model satisfies full comprehension, because the collection of definable sets may change when new sets are added to the model. But the collection of arithmetical sets will remain the same, so the extension will satisfy $\mathsf{ACA}$ at least.2012-07-04
  • 0
    I found a result in _SoSOA_ that backs up your revised view: $\mathsf{ATR}_0 \vdash \mathrm{Con}(\mathsf{ACA})$. It's listed as corollary VIII.1.14, p. 313 of the second edition. $\mathsf{ATR}_0$ is a subtheory of $\Pi^1_1\mathsf{-CA}_0$ so it can't be the case that $\mathsf{ACA} \vdash \mathrm{Con}(\Pi^1_1\mathsf{-CA}_0)$.2012-07-11
  • 0
    Can you see whether there is anything wrong with my proof that ACA proves Con(ACA0)? Within PA first prove by induction that every proof over ACA0 can be converted (uniformly) to a proof that does not use the set-existence axioms, by syntactic transformations. Finally prove that every proof over ACA0 that only uses axioms of PA cannot use ∃set-intro, and hence cannot use ∀set-elim either, so all second-order deductions can be eliminated as well, leaving a proof over PA. Within ACA we can clearly do the same proof and then prove Con(PA) as in your answer, to finally deduce Con(ACA0).2017-12-24
  • 0
    I'm not sure, but there is a standard proof that Con(PA) implies Con(ACA_0) - I am sure it must be in Simpson's book. So then ACA would prove both of those consistency statements.2017-12-25
  • 0
    (Somehow I didn't get pinged.) I see. I just thought your answer would be complete once you add that fact in. =) Or did you mean that you believe the answer is yes for all the systems in the big five?2017-12-25
  • 0
    @user21820 : What were you thinking about the other five subsystems? The equiconsistency of ACAo and PA relies on the fact that class of arithmetical sets is closed under relative arithmetical definability, in some sense.2017-12-25
  • 0
    Benedict asks: "do the unsubscripted systems prove the consistency of their subscripted counterparts, in all or some cases?". He goes on to say that he believes ACA proves Con(ACA0). Your answer plus provable equivalence between Con(PA) and Con(ACA0) over PA settles the latter, but not the former. That's all. =)2017-12-25