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