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

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.

-

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

-
It looks like T is conservative over PA, because it doesn't prove that any sets exist. –  aaa Apr 28 '12 at 22:48
@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. –  Carl Mummert Apr 28 '12 at 22:55
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. –  aaa Apr 29 '12 at 12:11
@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. –  Carl Mummert May 1 '12 at 16:19
@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. –  Benedict Eastaugh May 1 '12 at 17:33