Event Timeslots (1)
Wednesday
-
In 1936 Gentzen published the first consistency proof of Peano Arithmetic. To be precise, Gentzen proved the consistency of Peano arithmetic formalised in a version of his sequent calculus. Gödel’s second incompleteness theorem shows that the consistency of Peano Arithmetic cannot be proved within Peano arithmetic, if it is consistent. Consequently, Gentzen’s proof must make use of methods that do not form part of Peano arithmetic. Gentzen used transfinite induction over the complexity of proofs up to the ordinal ??0. This raises the philosophical question whether the method of proof can be regarded as finitary, as demanded by Hilbert’s Programme. Besides the proof, Gentzen’s article also contains philosophical considerations concerning this question. We’ll go through the entirety of Gentzen’s article. Time permitting, we also look at Hilbert and Bernays’ assessment of Gentzen’s proof in relation to Hilbert’s Programme.