As ‘homework’, before writing more of the second edition of my Gödel book, I’m reading through the literature to see how others have handled the First Incompleteness Theorem, both in the early papers from Gödel on, and then in the later textbook tradition. How do is the Theorem stated? How is it proved?
I’ve started writing notes on the expository history, and here’s the first (19 page) instalment. The notes don’t at all aim to be comprehensive, though I’d like to know about significant omissions as I go along. They have been written, as much as anything, as a rather detailed aide-memoire for myself (and a source of bits and pieces I might use). I have done some joining up of the dots to make them tolerably readable, but I certainly haven’t put in the time to spell out everything out in the way a beginning student might want. Still, you shouldn’t need much background to follow the twists and turns.
The notes come in three parts. Part 1 looks at early papers by the Founding Fathers. Part 2, to follow, will look at three pivotal works, Mostowki’s Sentences Undecidable in Formalized Arithmetic and Kleene’s Introduction to Metamathematics (both from 1952), and then Tarski, Mostowski and Robinson’s Undecidable Theories (1953). Part III will continue the story on through some sixty years of textbooks.
Make what use of these notes that you will. Though the usual warning applies in spades, as I’m no historian: caveat lector! Remember how very easy it to LaTeX your work. Just because what you write then looks very pretty doesn’t mean that it is any more authoritative …
7 thoughts on “Gödel’s First Theorem, from Gödel 1931 to Kleene 1943”
The Ishi Press reprint is some sort of photo-reprint of a pre-1971 edition, an early edition I think. It contains a new forward by Michael Beeson.
Professor Smith, I wonder if you wouldn’t mind sharing any knowledge you might have on the various editions and reprints of Kleene’s Introduction to Metamathematics. I’m trying to get my hands on a copy and while this isn’t itself terribly difficult, what I do find a bit confusing is that Kleene’s book seems to have passed through several publishing houses. Most recently, the book was published by Ishi Press (and according to most accounts, this is essentially an on-demand photocopy). There is a printing from about 1980 on North Holland Press and current copies of this also seem to be “print on demand.” And it is still possible to find used copies of the third and fourth printings of what at least appears to be the original text published by D. Van Nostrand.
My question: As far as you know, is there a preferred text? (By which I mean a preferring printing on a particular press?) I’d be extraordinarily grateful to you for any insight you might have on this.
By the way, I’m very much looking forward to the second edition of your Introduction to Godel’s Theorems. It’s a wonderful book and I’ll be using it to teach an advanced undergraduate course in logic that I am developing for next year.
In footnote 1 of his short piece ‘The writing of Introduction to Mathematics‘ (in Thomas Drucker, ed., Perspectives on the History of Mathematical Logic (Birkhäuser 1991), Kleene says
So that suggests you can’t go far wrong with any printing, and any from 1971 should be the same.
By the way, there are a lot of inexpensive second-hand copies on abebooks.com
Thank you very much! I just ordered a copy from abebooks.
I wish to suggest an alternative proof related to Godel’s results, which goes back to Raymond Smullyan in his “Theory of Formal Systems”, This is an excerpt from the introduction:
Yes — I have nothing but admiration for Smullyan! I’ll certainly be discussing his Theory of Formal Systems later in the notes, as well as some of his other wonderful books.
I was having similar thoughts but with some historical threads (and this may be more like real history of the subject than you want to get into). The Smullyan material comes out of Post Canonical Systems and poor Post is often left out of these accounts. And PCSs are sort an ideal bridge between explicitly recursion theoretic accounts and the who-needs-numbers-we’re-talking-syntax accounts. (I guess the idea here is that from a PCS point of view you don’t analyze formalisms in terms of recursiveness–it’s really the other way around.) The other Smullyan thread, the one that’s more apparent in his later books (but also in some very cute technical articles) is the drive to a certain level of abstraction. I want to distinguish abstraction from generalization. Brute generalization is just, for instance, where you prove G1 for all extensions of Q. Abstraction is what Smullyan does in his GIT book or what happens when we study the modal logic provability. But those moves were all already happening in the 1930s; the HB derivability conditions being the obvious example. (I count those as initiating the abstraction route.) Feferman’s great paper (The Arithmetization of Metamathematics…) sort of converts abstraction to generalization, by (sort of) finding a way to specify the range of formalisms that do satisfy the HB derivability conditions. And that’s my potted history ramble.