Gentzen and Normalisation

Recently, Arché and the St Andrews computer science department (with Roy Dyckhoff) jointly organised a one-day symposium celebrating the centennial of Gerhard Gentzen's birth, November 24th, 1909. The event showcased cross-disciplinary work in computer science, philosophy and logic in short instalments. As keynote speaker, we invited Jan von Plato (Helsinki), proof-theorist and Gentzen scholar. Arguably, he was responsible for a rather significant upset in our little logic community.

I'm a huge Gentzen fan, in fact I think he deserves a place together with Gödel and Tarski in the history of 20th century logic. Even more than the two latter, Gentzen's work contributed to the formation of an entirely new discipline in mathematical logic, a discipline that now completely dominates theoretical computer science, and contributes significantly to both philosophy and linguistics. Yet, biographically, I knew a great deal more about Gödel and Tarski. (If you want a Gentzen biography, this is what you need.)

One thing I didn't know about Gentzen was that there are hundreds of unpublished pages, stenographed in Gabelsberger shorthand. The transcription of Gentzen's notes is a substantial task, but hopefully in the near future we'll be able to see the full scope and significance of his Nachlass. One thing that has already been uncovered, however, but which surprised me quite a bit, is that Gentzen proved normalisation for intuitionistic logic in 1932. In other words, over 30 years before the result was published in Dag Prawitz's dissertation!

Of course we knew all along that Gentzen must have been on to something like normalisation: After all, that appears to be part of the motivation for him looking for, and proving, the cut elimination theorem (the Hauptsatz) for classical logic, and there are some revealing remarks indicating that he had looked at conversions for intro- and elim-rule pairs. Yet, it is astonishing to learn that a result that wasn't known to logicians until 1965, was not only proved by Gentzen while working on his dissertation, but also excluded from the final version of his dissertation. One explanation, offered by von Plato, is that Gentzen thought the direct proof of normalisation unnecessary as he had the corresponding proof of cut elimination in the sequent calculus.

It gets worse. Not only had Gentzen already proved normalisation for intuitionistic logic (and probably failed to do the same for classical natural deduction), but his handwritten manuscript was in his supervisor's (Bernay's) possession after the war. In fact, and here is the real killer, Bernays showed the manuscript to M. E. Szabo, the editor of The Collected Papers of Gerhard Gentzen, and the latter proceeded to use a picture of the manuscript on a cover page of the edition. Szabo used page two, but if he had used page nine instead, we would all have been staring at the start of the normalisation proof. From von Plato's paper Gentzen's Proof of Normalization for Natural Deduction:

Remarkably, most of page 2 of Gentzen's manuscript is reproduced photographically among the frontmatter of Gentzen's Collected Papers of 1969. The editor indicates that the source for the manuscript is Bernays. It is astonishing that he did not mention in this connection, say, the complete set of detour convertibilities that stand very prominently on top of page 9 of the manuscript, or the announcement of the proof of normalization in Gentzen's summary of his further results at the end of the first introductory chapter, and its realization in chapter three. (249)

The paper by von Plato also includes a translation of the handwritten manuscript. An obvious question is to ask to which extent Gentzen's had figured out the details of normalisation. The answer is that his proof is as detailed as what you find in standard textbooks today, complete with conversions and examples. He calls the maximum formula of a non-normal proof a 'Hügel' (translated by von Plato as 'hillock'). I leave the reader to marvel at the details in von Plato's translation.