Gödel's incompleteness theorem  recommended reading
Websites
Information about Kurt Gödel
The Kurt Gödel Society website has information about Gödel as well as organising conferences on mathematical logic.
SimplyGödel is a new site with interviews with authors who have written about Gödel and his work.
Formalized proofs
Freek Wiedijk has a list of formalizations of significant theorems
Russell O’Connor describes his constructive proof of the Gödel's theorem using the Coq proof assistant.
The Hilbert II links page has plenty more links to relevant sites.
General Resources
Alan Shapiro sees this project as a
step towards a New Computer Science
General Books
forever Undecided
Raymond Smullyan  Oxford University Press, 1987  ISBN: 0192801414

This book gives a gentle introduction to the deep results of Gödel's incompleteness theorems via a series of puzzles for the reader to ponder.



Mathematical Fallacies and Paradoxes
Bryan Bunch  Dover Publications, 1982  ISBN: 0486296644

In this book Brian Bunch describes some of the unexpected results of mathematics, including reasons why you might need to watch your step. The book includes a look at self reference and the paradoxes of set theory, leading up to a well written explanation of Gödel's incompleteness theorem.
Reviews of Mathematical Fallacies and Paradoxes



Godel, Escher, Bach
Douglas Hofstadter  Penguin, 1979  ISBN: 0140289208

Hofstadter's classic work, looking at a wide range of topics concerning the mind, patterns and selfreference, and of course Gödel's incompleteness theorem.
Reviews of Godel, Escher, Bach



I am a strange loop
Douglas Hofstadter  Basic books, 2007  ISBN: 0465030785

In this book Hofstadter expands on one of the ideas of his earlier work, the parallelism between Gödel's incompleteness theorem and the emergence of mind and the self. In looks at Gödel's theorem from several different angles, providing a number of intruiging analogies of its strange type of mixing of levels.
Reviews of I am a strange loop



Godel's proof
Ernest Nagel and James R Newman  Routledge, 1958  ISBN: 0415355281

This book gives a clear explanation of the basics of the proof of Gödel's incompleteness theorem. It would be useful for those wishing to get a clear idea of Gödel's theorem without getting too technical, and to go further than what is given in most popular treatments of the subject Reviews of Godel's proof



Godel's theorem : an incomplete guide to its use and abuse
Torkel Franzen  Peters, 2005  ISBN: 1568812388

One of my reasons for working on this project was to show that Gödel's theorem isn't about some mysterious notion of self reference, but leads to a definite statement which is unprovable from a given set of axioms.
In this book Torkel Franzen examines various ways that this theorem has been wrongly quoted, and tries to set the reader straight on what it is really about. He looks at what has been said about incompleteness in physics, in theology and of course in various postmodern ramblings. It would be useful for those readers who want to go beyond the usual popular accounts and get Gödel's theorem clear in their minds.
Reviews of Godel's theorem : an incomplete guide to its use and abuse



Meta Math!:The Quest for Omega
Gregory Chaitin  Atlantic Books, 2005  ISBN: 1843545241

Gregory Chaitin is also trying to remove some of the mystery of Gödel's incompleteness theorem, showing that it is part of a more general principle of how computability is limited by complexity (rather than being based on mysterious ideas of selfreference). In this book he gives an account of some of his work. Reviews of Meta Math!:The Quest for Omega



Biographies of Gödel
Logical dilemmas
John W Dawson  Peters, 1997  ISBN: 1568810253

John W Dawson has sifted through the massive amounts of paperwork that Gödel left, to produce this detailed but readable account of Gödel's life.
Reviews of Logical dilemmas



A madman dreams of Turing machines
Janna Levin  Oxford University Press, 2008  ISBN: 978029764546

Janna Levin gives a partially fictional account of the lives of two of the most prominent mathematicians of the 20^{th} century, Kurt Godel and Alan Turing.



Textbooks
The Foundations of Mathematics
Ian Stewart and David Tall  Oxford University Press, 1977  ISBN: 0198531656

If you want to understand whats going on with my applets or any other proof of Gödel's theorem, you will need some knowledge of axioms and the structure of number systems. This book gives an excellent introduction to these subjects.
Reviews of The Foundations of Mathematics



Metamathematics, machines, and Godel's proof
N Shankar  Cambridge University Press, 1994  ISBN: 052142027X

There have been other computer based proofs of Gödel's incompleteness theorem, although none have actually produced the undecidable sentence for the reader  rather their purpose is the extra rigor that a computer based proof can provide. This book describes the construction of such a proof, based on the LISP programming language Reviews of Metamathematics, machines, and Godel's proof



Introduction to mathematical logic
Elliot Mendelson  Chapman and Hall, 1997  ISBN: 0412808307

This is not the simplest way of approaching Gödel's theorems  it goes into a lot of detail of quantification theory before getting on to its application to arithmetics. But in chapter 3 it does actually use the axioms of arithmetic to derive a number of proofs, and for that reason alone it's worth taking a look at.
Reviews of Introduction to mathematical logic



Gödel's's incompleteness theorems
Raymond Smullyan  Oxford University Press, 1992  ISBN: 0195046722

This isn't the easiest introduction to Gödel's work, but it sticks to the point rather than trying to deal with the whole of mathematical logic, and so provides a comprehensive treatment of Gödel's and related theorems in a concise book
Reviews of Gödel's incompleteness theorems



On formally undecidable propositions of Principia mathematica and related systems
Kurt Gödel  Dover Publications, 1931  ISBN: 0486669807

This is a reprint of one of the most significant of all mathematical papers  Gödel's proof of his incompleteness theorem.


