Strength of Transfinite Induction on the Difference Hierarchy

Question

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

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