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