Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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.

share|cite|improve this question

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

share|cite|improve this answer
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

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.