Gentzen Cut elimination: Why do we have to "go infinite"? I found some slides here that say you can't do cut elimination on PA with axioms like $$\frac{P(Z)\;\;\;\;\;\forall n,\,P(n) \implies P(Sn)}{\forall n,\,P(n)}$$ (which denotes infinitely many axioms each of which $P$ is replaced by some formula) because they have arbitrarily high complexity.
I don't understand that, why can't we just do cut elimination on this anyway?
The suggestion is to "go infinite" by replacing these axioms with ones of type
$$\frac{P(Z)\;\;\;\;\;P(SZ)\;\;\;\;\;P(SSZ)\;\;\;\;\;P(SSSZ)\;\;\;\;\;\cdots}{\forall n,\,P(n)}$$
and then restricting the notion of a valid proof tree to one which can be assigned a small ordinal. This is absolutely horrible, why would cut elimination work for this if it doesn't for the other axiomatization of induction?

I doubt the claim in the slides because I think strong normalization of typed lambda calculus with typed recursors on natural numbers can be proved directly (without introducing an infinitary axiom and showing equivalence).
Furthermore How can we call Gentzen's consistency proof "by finitary means" if it uses this infinitary logical axiom. I was under the impression that the only infinite part was the use of a single $\epsilon_0$ induction.
 A: I feel that Carl's answer has already pretty much answered this, but since you asked why the proof is harder than that of strong normalization for typed lambda calculus with recursion, I can maybe make suggestion about why this is.
The types in typed lambda calculus are analogous to propositions and reductions are analogous to proofs under the formulas-as-classes isomorphism. However, in the simply typed lambda calculus you can only form types using implication, so in particular the types only correspond to quantifier free formulas.
If you restrict the usage of quantifiers in induction in arithmetic then you do indeed get much weaker theories. For example, requiring that every quantifier is bounded results in $I \Delta_0$, which has strength only $\omega^2$ and presumably has easier proofs of cut elimination. Similarly, adding dependent types, product types and sum types (corresponding to universal and existential quantifiers) to the lambda calculus increases the consistency strength.
A: Firstly: why does cut elimination work on the infinity rule when it fails on the induction rule? Say we have proofs of $P(\llcorner k \lrcorner)$ for each number-term $\llcorner k\lrcorner$, produced from the proof of $\forall n.(P(n) \implies P(n+1))$, and we have a cut-free proof of $\neg\forall n.P(n)$. So we must have proved $\neg P(t)$ for some term $t$; we must have $t=\llcorner k\lrcorner$ for some $k$ and, thanks to our infinitary reformulation, can thus cut $\neg P(t)$ against $P(t)$. (But with the original induction rule, we would be stuck.)
Second: why doesn't the proof of strong normalization go through? It depends on an infinite set of proofs of $\forall n.P(n)$, which can't be formalized in $\mathcal{PA}$ because the $P$ can be arbitrarily complicated. (There's also the subtlety that $\mathcal{PA}$ is classical, so not confluent; this makes the proof of strong normalization trickier.) But the behavior of the infinite system $\mathcal{PA}_\omega$ can be formalized in $\mathcal{PA}$; you just can't prove the bounds you need.
Third: why is Gentzen's argument considered finitary? Because his proof didn't involve the detour through $\mathcal{PA}_\omega$; instead he showed how to eliminate cuts and inductions simultaneously. It's harder to do it this way; but I seem to recall that Harvey E. Rose's Subrecursion: Functions and Hierarchies gave such a proof. Failing that, you could try Kleene's Introduction to Metamathematics; I'm pretty sure that this book has the finitary proof.
A: The claim on the slides is well known: Peano arithmetic does not admit cut elimination with finitary deductions. It's theorem 10.4.12 in Basic Proof Theory by Troelstra and Schwichtenberg. 
In the comments, Zhen Lin pointed out that $\text{PA}_\omega$, which is PA augmented by the $\omega$-rule, proves Con(PA). This is correct - $\text{PA}_\omega$ is much stronger than PA. 
However, there is a second subtlety in the cut elimination proof. Looking at the embedding theorem, slide 30 of the linked slides, we see that if $\text{PA} \vdash \Gamma \to \Delta$ then not only does $\text{PA}_\omega$ prove $\Gamma \to \Delta$, in fact $\text{PA}_\omega \vdash^{\omega + m}_k  \Gamma \to \Delta$ for some $k,m < \omega$. This latter fact is key to the actual ordinal analysis of $\text{PA}$. This is proved in detail in sections 10.3 and 10.4 in Troelstra and Schwichtenberg, although they use $Z$ for PA and $Z^\infty$ for $\text{PA}_\omega$. 
