Gentzen introduced the use of finite sequences of formulas as a basic object, called a sequent; for the propositional case this has been described in the previous commentary General discussion of proof systems. He considered this formalization closer to the way we actually reason.
Then he turned to the question of the consistency of PA. One
consequence of Gödel's work is the fact that if one can prove the
consistency of PA, then the proof ``is not expressible in PA''.
This is understood to imply that one cannot prove the consistency of PA
by finitistic means, as had been hoped by Hilbert.
Gentzen
did succeed in proving the consistency of PA, but by using a non
finitistic framework, namely he used transfinite induction up to the ordinal
,
the limit of
.