It is surprising that there is lack of information on Gentzen's consistency proof – sure, there are some contents on Gentzen's first consistency proof of Peano axioms, but not on what we usually say Gentzen's consistency proof. Thus the question: what would be rough descriptions of Gentzen's consistency proof?
What I can start with is this: what Gentzen wanted to do is to start from a weaker system than PA so that consistency claims will not be controversial. But a weaker system cannot prove consistency of PA, so one needs to add something, but one needs to make sure that such addition can be well-accepted and the resulting system is not stronger than PA. That addition is quantifier-free induction up to $\varepsilon_0$, and the system being used is PRA.
My question thus now is, how would PRA and this induction principle connect to establish consistency proof? While a good reference, preferably existing on Internet, is OK, I think it would be better if this question is directly answered, as it can serve as a good reference for other people as well.
(In addition, it is a bit hard for me to see how we can form base case for $n=0$. What would be the base case here?)
Best Answer
In very rough outline, Gentzen's proof is as follows. He defines primitive recursive (with respect to standard codings) functions $C$ from proofs in PA to ordinals $<\epsilon_0$ and $E$ from proofs to proofs, with the following properties, for all proofs $p$. (1) If $C(p)>0$ then $C(E(p))<C(p)$. (2) The conclusion of $E(p)$ is the same as that of $p$. (3) If the conclusion of $p$ is $0=1$ then $C(p)>0$. These three properties are proved by finitary reasoning formalizable in PRA.
Given this information plus the well-ordering property of $\epsilon_0$, he gets the consistency of PA as follows. Suppose there were a PA-proof of $0=1$. Then we can generate more proofs of $0=1$ by iterating $E$: $p_0=p$ and $p_{n+1}=E(p_n)$. All $p_n$ are proofs of $0=1$ by (2); $C(p_n)>0$ by (3); and $C(p_{n+1})<C(p_n)$ by (1). But an infinite decreasing sequence of ordinals $C(p_n)$ contradicts the well-ordering assumption. So there cannot be a PA-proof of $0=1$.
Note that well-ordering was used only in the weaker form "There is no infinite, decreasing, primitive recursive sequence in $\epsilon_0$."
A little more about $C$ and $E$: In the deductive systems used by Gentzen, a particular rule called "cut" is responsible for most of the proof-theoretic complexity. In particular, it is trivial that $0=1$ cannot be proved without using cut (property (3) above). $C(p)$ measures "how much" cut is involved in the proof $p$; this is not just a matter of the number of applications of the cut-rule in $p$ but also the complexity of the formulas to which this rule is applied. $E(p)$ is the result of one step in a process called cut-elimination. The whole process would, as its name says, get rid of the applications of the cut rule in a proof, while maintaining the correctness and the conclusion of the proof (property (2) above). One step of the process, i.e., $E$, only reduces the cut-rank, i.e., property (1) above.