How does adding the full second order induction scheme affect the consistency strength of subsystems of second order arithmetic?

438 Views Asked by At

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.

1

There are 1 best solutions below

15
On

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