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.

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

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.