Consistency of Analysis (second order arithmetic)

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

Update:

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

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
• @MattF. Proof theoretic ordinals are computable ordinals defined using a system of ordinal notations - en.wikipedia.org/wiki/Ordinal_notation – 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