To quote from the overview chapter in the book:
I think that the book succeeds beautifully to do just that, and will repay re-reading.
The aim of the present addition to the literature on Gödel’s theorem is to set out the content, scope and limits of the incompleteness theorem in such a way as to allow a reader with no knowledge of formal logic to form a sober and soundly based opinion of these various arguments and reflections invoking the theorem. To this end, a number of commonly occurring such arguments and reflections will be presented, in an attempt to counteract common misconceptions and clarify the issues. The formulations of these arguments and reflections, when not attributed to any specific author, are adaptations of statements found on the net, representative of many such reflections.
Torkel Franzén also maintained the page Gödel on the net, from which the book eventually originated.
You might have noticed the use of the past tense in the previous sentence. Unfortunately, I just discovered that the author passed away in 2006. He left some books that, like this one, have received praise from many sources. I certainly enjoyed reading this book, and I am feeling tempted to open my purse and purchase a copy of this volume for my personal library.
Addendum (17 November 2007): I encourage any reader who wants to catch a glimpse of what this book is about, and of the writing style of the author, to have a look at this short article Torkel Franzén wrote for the Notices of the AMS (volume 53, number 4). Here is an example of one of the many things I personally learned from the book.
Let us say that a formal system has an arithmetical component if it is possible to interpret some of its statements as statements about the natural numbers, in such a way that the system proves some basic principles of arithmetic having to do with summation and multiplication. Given this, we can produce (using Barkley Rosser’s strengthening of Gödel’s theorem in conjunction with the proof of the Matiyasevich-Davis-Robinson-Putnam theorem about the representability of recursively enumerable sets by Diophantine equations) a particular statement of the form “The Diophantine equation p(x1 , . . . , xn ) = 0 has no solution” which is undecidable in the theory, provided it is consistent.
Franzén remarks that
Wikipedia has a short list of mathematical statements that are independent of ZFC on this page. You may find it interesting.
....it is mathematically a very striking fact that any sufficiently strong consistent formal system is incomplete with respect to this class of statements,....
However, no famous arithmetical conjecture has been shown to be undecidable in ZFC.....From a logician's point of view, it would be immensely interesting if some famous arithmetical conjecture turned out to be undecidable in ZFC, but it seems too much to hope for.
Saharon Shelah's result to the effect that the Whitehead problem is undecidable in ZFC is discussed in this paper by Eklof. Shelah has also shown that the problem is independent of ZFC+CH.
There is also an interesting post on a combinatorial problem that is independent of ZFC on the complexity blog. That post also includes several pointers to pieces that are well worth reading.