Is there a proof of the consistency of Analysis (second order arithmetic), which is similar to Gentzen's proof of the consistency of arithmetic?


Which (different) methods can be used to prove the consistency of Analysis? and where can I find such proofs?

up vote 14 down vote accepted

I believe the answer is "no": certainly the proof-theoretic ordinal (the optimal object taking the role of "$\epsilon_0$" in Gentzen's proof) is totally unknown, and my understanding is that there is no non-trivial upper bound on it, either. See also Proof-Theoretic Ordinal of ZFC or Consistent ZFC Extensions?; in particular, my understanding is that we only know the actual proof-theoretic ordinals of theories up to (something around) $\Pi^1_2$-comprehension, and I suspect we don't even have upper bounds for proof-theoretic ordinals as high as $\Pi^1_3$-comprehension.

That said, I also believe this is the only obstacle - that is, if we had the proof-theoretic ordinal $\alpha$ in hand, then we would have a proof of "Analysis is consistent" from "$T$+'induction along $\alpha$'", where $T$ is some reasonable weak base theory and "induction along $\alpha$" is properly formulated. So in some sense, the only real difference between analysis and arithmetic is in the complexity of finding the proof-theoretic ordinal.

. . . however, the use of the word "only" there can be extremely misleading: finding proof-theoretic ordinals of stronger and stronger theories requires increasingly deep ideas, and not just the continued turning of a well-understood crank. So on the one hand, while it's valuable to localize all the difficulty around a single object, it's also true that this is a vastly complex object, and that saying "all we need to do is understand the proof-theoretic ordinal" is less meaningful than it might sound.

  • I like the answer; it makes me wonder: What does it mean to have the ordinal "in hand"? Presumably you mean something more that a formula uniquely defining it, perhaps a formula of a certain form. But what form? – Matt F. Mar 8 '14 at 14:59
  • 2
    @MattF. Proof theoretic ordinals are computable ordinals defined using a system of ordinal notations - – François G. Dorais Mar 8 '14 at 16:52

As Noah says, the direct successor of Gentzen's method, cut-elimination, has been generalized up to $\Pi^1_2$-comprehension. This was shown separately by Rathjen and Arai; the full results have never been published, but fragments have appeared in various papers. Rathjen published "An ordinal analysis of parameter free $\Pi^1_2$-comprehension", which covers a fairly strong subtheory of $\Pi^1_2$-comprehension. The strongest results of Arai's I'm finding actually published only go up to $\Pi_3$ reflection, "Proof theory for theories of ordinals II: $\Pi_3$-reflection". My paper, "Ordinal analysis by transformations", is rather vague about the comparison between the system it's analyzing and usual hierarchy, but I now think the system it analyzes is around the strength of parameter free $\Pi^1_2$-comprehension.

However the consistency of analysis has been shown by other means. First, as Carl mentions, Spector's proved the consistency of analysis in "Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics". Spector's proof is considered non-constructive (it uses bar recursion).

Girard gave a constructive consistency proof of analysis: he proves strong normalization proof for System F, which is an equivalent system. This proof can be found written up quite nicely in his book, Proofs and Types.

Although the proof-theoretic ordinal of second-order arithmetic is very hard to determine, there is another standard method for the proving consistency of arithmetic: Gödel's Dialectica interpretation. This was originally used by Gödel to give a different relative consistency proof of Peano arithmetic by reducing its consistency to the consistency of a quantifier-free theory of functionals of finite type known as system $T$.

This work was later extended by Spector and Howard to give a relative consistency proof for second-order arithmetic. The weaker system used is the same system $T$ augmented with bar recursion. The details are spelled out in section 6 of Gödel's Functional ("Dialectica") Interpretation by Jeremy Avigad and Solomon Feferman from the Handbook of Proof Theory.

Although this is not a Gentzen-style analysis, it does have a certain analogy. Gentzen showed that the consistency of Peano Arithmetic reduces to that of a weak theory augmented with transfinite induction. The Dialactica-style relative consistency proof for second-order arithmetic reduces its consistency to that of a (different) weaker theory $T$ augmented with bar recursion, which can be seen as a scheme for constructing objects by transfinite recursions. The induction scheme dual to bar recursion, bar induction, is a kind of transfinite induction scheme. The proof also gives a characterization of the provably total computable functions of second-order arithmetic, much like the consistency proof for Peano arithmetic does.

  • Thanks a lot, I just was asking for the methods for the consistency of Analysis. – Mohammad Golshani Mar 8 '14 at 13:40

Your Answer


By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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