Goedelian Memoirs

I have just finished a charming little book by Gaisi Takeuti:

Memoirs of a Proof Theorist; Mariko Yasugi and Nicholas Passell

The book is a translation of "Goedel'', written in Japanese by Takeuti and translated bu Mariko Yasugi and Nicholas Passell. The book consists, predominantly, of a series of articles about Goedel's life and work. Takeuti offers several personal insights into Goedel, having worked with him at IAS in Princeton.

In proof theoretic circles, Takeuti's name is inextricably linked to his fundamental conjecture' of a cut elimiantion theorem for second order logic, about which I have written previously. Since this conjecture was such a dominating aspect of Takeuti's work at the time of his friendship with Goedel, it is a thread which repeats throughout the book. In this english translation, an appendix has been added in which Takeuti very quickly takes the reader from the definition of a sequent, via Gentzen's consistency proof of arithmetic, to the statement of the fundamental conjecture in a mere 14 pages. It is a testament to Takeuti's deep understanding of this subject that he is able to illuminate all of these results in so brief an exposition.

Takeuti writes of how he managed to arouse Goedel's interest in the conjecture, saying:

His view of my fundamental conjecture was that counter-examples would be discovered by the method of his Incompleteness Theorem or by nonstandard methods'

This comment came back to haunt Takeuti, who relays an exerpt from a referee's report of a paper on the conjecture:

The author claims that the consistency of number theory can be derived from the fundamental conjecture, but this is obvioously inconsistent with Goedel's incompleteness theorem.'

The belief that one cannot establish cut elimination for second order logic was, perhaps, forgiveable given the close temporal proximity with the proof of the incompleteness theorem. The controversy arises since second order logic is the proof theoretic incarnation of set theory. The reason is that, just as first order predicates are equivalent to sets, so second order predicates allow one to state properties of sets. Second order quantification then means, of course, that one can quantify over sets.

Since one can express set theory in second order logic, it is certainly possible to formalise Peano Arithmetic, hence the controversy. However, Gentzen's consistency proof of arithmetic shows that it is equivalent to the accessibility of the first epsilon number, which is the ordinal corresponding to an exponential stack of omega's, of height omega. Here, accessibility means that any strictly decreasing chain of ordinals below this ordinal is finite. This claim, which is justifiable on semantic grounds is, nevertheless, not provable in peano arithmetic. So, there is no clash with the Incompleteness Theorem - we are using an extension of arithmetic in order to prove the consistency of arithmetic.

The book is filled with descriptions both of Goedel's work and his professional relationships. Takeuti is remarkably candid at times when discussing Goedel's work, particularly his early result of the completeness of first order logic and offers many fascinating insights. The choice of title for the english translation is somewhat unfortunate. It is the memoirs of neither Goedel nor Takeuti. But perhaps this complaint is a tad glib - one could, perhaps, see it as the memoirs of Goedel's proof theoretic life.

On an administrative note, I have regular internet access over the next two weeks and have several posts lined up for this period.