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