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.

-
There is a subtle difference between the two, though: with the infinitary rule, you can deduce $\forall n . P(n)$ as soon as you have proofs for $P (n)$ for all standard natural numbers $n$. So for example, if you have proofs of sufficiently high complexity (probably $> \epsilon_0$) you could deduce in the infinitary system that $$\forall n . n \text{ does not code the proof of an inconsistency in PA}$$ or something like that. – Zhen Lin Feb 28 '13 at 20:01
For induction, you need strong normalization of typed lambda calculus with "inductors", that is in some dependent type theory with inductive datatype (or at least the datatype of numbers) — but the standard proofs for that only works for intuitionistic systems (this stands at the foundation of Coq, Agda and other proof assistants). – Blaisorblade Apr 15 '14 at 7:16
And as a computer scientist, I'm not really familiar with the details of the proof. However, from some answers I suspect that cut elimination corresponds only to beta-reduction for function types, and not to generic reduction ("unrolling induction N times" is not beta-reduction, just the computation rule for the eliminator for natural numbers). – Blaisorblade Apr 15 '14 at 8:19
As I realized when answering @BenStandeven, compared to a dependently-typed presentation, Peano arithmetic lacks a recursion form – "given n and an inductive step, or more generally an implication, apply the implication n times". – Blaisorblade Apr 15 '14 at 8:28

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

-
In general, the way that cut elimination works is that the logical axioms cause no problems - which is why first-order logic with no axioms at all has cut elimination. For an arbitrary theory, we have to worry about the cuts that are introduced when we apply the axioms of the theory. Induction axioms in particular tend to require us to move from finitary deductions to infinitary deductions in order to eliminate the cuts. – Carl Mummert Feb 28 '13 at 20:40

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.

-
I don't feel I understand any more from his answer. what you've said about quantifiers seems to be the essential point (but then System F has universal quantifiers and you can prove its SN with candidats which seems finitary to me..) - but I'd like to understand why now. Thanks to you all. – user58512 Mar 5 '13 at 17:22

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.

-
"with the original induction rule, we would be stuck" - couldn't one simply have an elimination rule for naturals, saying "apply an implication t times, if t is a natural"? That's what one does in dependently-typed proof theories (Agda, Coq, and so on). In a strong normalization proof, that construct can later be reduced when t reduces to a normal form if it that normal form is closed (that is, a number literal) by applying the induction step t times (as you would do when proving strong normalization)? – Blaisorblade Apr 15 '14 at 8:25