I'm wondering if a particular theory of second order arithmetic has been studied or is known to be equivalent to some other theory.

Consider the formulas generated by $\Pi^1_1$ and $\Sigma^1_1$ formulas by propositional combinations (the title refers to this, rather informally, as the difference hierarchy, since these formulas are essentially the difference between two $\Pi^1_1$ formulas, the difference between two such, and so on). Let's call this class of formulas $\Delta$, for convenience.

My question is what the strength (either reverse mathematical or proof theoretic) of $\Delta-TI_0$, the theory which allows transfinite induction along any well-ordering for $\Delta$ formulas, is. This has proof theoretic strength strictly greater than $\Pi^1_2-TI_0$ (Rathjen and Weierman's proof that $\Pi^1_2-TI_0$ implies well-foundedness of $\psi\Omega^{\Omega^n}$ goes through, and furthermore this theory can carry out the key induction internally), and strictly less than $\Pi^1_1-CA_0$ (the standard argument that $\Pi^1_1-CA_0$ proves the existence of a $\beta$-model of $\Pi^1_\infty-TI_0$ suffices).


1 Answer 1


I hope it's not too tacky to answer my own question now that I've had a few days and train rides to think about it.

The answer is that the proof theoretic ordinal of $\Delta-TI_0$ is the Howard-Bachmann ordinal (the ordinal of $\Pi^1_1-CA_0^-$, $\Pi^1_\infty-TI_0$, $ID_1$, and $KP\omega$).

The upper bound is easy to see ($\Delta-TI_0$ is a subtheory of $\Pi^1_\infty-TI_0$). (In fact, each instance of $\Delta-TI_0$ is provable in $\Pi^1_1-CA_0^-$, modulo some work to handle parameters in the formulas in $\Delta$.)

For the lower bound, consider the easy embedding of $ID_1$ into the language of second order arithmetic, in which arithmetic formulas map to arithmetic formulas and the least fixed point in $ID_1$ is mapped to a $\Pi^1_1$ formula. Then all formulas of $ID_1$ map to $\Delta$ formulas, so every axiom of $ID_1$ becomes a theorem of $\Delta-TI_0$ (the point here is that the only instances of induction axioms appearing in $ID_1$ are induction on $\Delta$ formulas). In particular, the proof of well-foundedness below the Howard-Bachmann ordinal can be carried out, unchanged, in $\Delta-TI_0$.

  • $\begingroup$ @Henry : What would be some good/reasonable references to learn more on this topic? $\endgroup$ Nov 27, 2010 at 19:46
  • $\begingroup$ The starting place is certainly Simpsons' book, Subsystems of Second Order Arithmetic. Chapter 3 of Pohlers' article in the Handbook of Proof Theory has a fairly systematic discussion of the relationship between first-order theories like $ID_1$, second order theories of comprehension, and admissible set theory. I haven't actually read Pohlers' new book, but (based on his previous book) it's probably the best reference for the actual detailed work with the ordinals. $\endgroup$ Nov 27, 2010 at 20:15
  • $\begingroup$ @Henry : Thanks! I'll begin with the Handbook paper and check Pohlers book. $\endgroup$ Nov 27, 2010 at 20:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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