# Strength of Transfinite Induction on the Difference Hierarchy

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

-

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$.
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. –  Henry Towsner Nov 27 '10 at 20:15