MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

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

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

share|cite|improve this question
up vote 2 down vote accepted

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

share|cite|improve this answer
@Henry : What would be some good/reasonable references to learn more on this topic? – Andrés E. Caicedo Nov 27 '10 at 19:46
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
@Henry : Thanks! I'll begin with the Handbook paper and check Pohlers book. – Andrés E. Caicedo Nov 27 '10 at 20:49

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.