The last appendix to Eckart Menzler-Trott’s book on Gödel is a thirty-six page essay “From Hilbert’s Programme to Gentzen’s Programme” by Jan von Plato. As you’d expect from this author, this is accurate and useful, as far as it goes. But actually, although it would have made a long book even longer, it would have been rather good to have fifteen rather than five pages on the key results about the consistency of arithmetic. For von Plato’s discussion is a bit frustratingly short of details about the proof-strategies of Gentzen’s four proofs. Students who aren’t planning to do a heavy-duty course on proof-theory will find it difficult to pick up quite enough about the basics of what is going on in the proofs to satisfy their intellectual curiosity. (All the same, like Smorynski’s piece, this essay will be well worth putting on reading lists — and so libraries should certainly get a copy of this book.)
I should add — to counterbalance remarks in an earlier posting — that Menzler-Trott’s Introduction does very clearly say “This is the story of the outer life of the mathematician and logician Dr.habil. Gerhard Gentzen; it is not a book about proof theory or its development.” (p. xviii). So perhaps we shouldn’t judge a story of the “outer life” alongside Dawson’s account of Gödel or the Fefermans on Tarksi which do try to tell something of the inner stories. But Menzler-Trott’s Preface also says “I hope that this book will be judged as a contribution to the philosophy and the history of logic and proof theory and not merely to the art of biography of mathematicians.” (p. xiv). So in the end I’m still unsure quite what the book is aiming for. But it is obviously a labour of love by its avowedly amateur author, with a great (sometimes excessive) amount of detail and — despite its oddities — it is certainly worth dipping into.