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



Strength of Transfinite Induction on the Difference Hierarchy
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$.


