                                              Notes prepared by
                                                 Stanley Burris
                                                   July 3, 2001

The Consistency of Arithmetic: Gentzen

Gerhard Gentzen (1909–1945)

1934 - Investigations on logical deduction.
1936 - The consistency of number theory.

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.^{1} 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 ε_{0}, the limit of ω, ω^{ω}, ω^{ω^{ω}}, · · ·.

References

[1] G. Gentzen, Untersuchung über das logische Schliessen. Math. Z. 39 (1934), 176–210, 405–431.

[2] G. Gentzen, Die Widerspruchsfreiheit der reinen Zahlentheorie. Math. Ann. 112 (1936), 493–565.

1In the foreword to Hilbert and Bernays two volumes on logic Hilbert says that there is a widespread and incorrect assumption that Gödel’s results have proved his program of proving the consistency of mathematics by finitistic means to be hopeless.