Franzén, Torkel. Gödel's theorem: an incomplete guide to its use and abuse. Wellesley, Massachusetts: A K Peters, 2005. ISBN 1-56881-238-8.
Summary: A careful analysis of Gödel's incompleteness theorem and related results shows that, although it has significant implications in mathematical logic and raises some fundamental questions about the nature and methodology of logic and mathematics, it is an exaggeration to describe it as a revolution in human thought. Moreover, it is often misleading to extrapolate from it, or to extend it metaphorically, into other disciplines. It properly applies only to formal systems in which statements of elementary arithmetic can be expressed, and it says that, if such a formal system is consistent, then it is incomplete -- some statements of elementary arithmetic can be formulated, but neither proved nor disproved, within the formal system.
Of the formal systems to which this theorem applies, some are known to be consistent (and hence, by the theorem, incomplete), some are known to be inconsistent, and some are neither known to be consistent nor known to be inconsistent. Many interpreters of Gödel's theorem imply that it somehow gives us statements that are not provable in a given formal system but are nevertheless known to be true. This happens only when the formal system is known to be consistent. For instance, Peano arithmetic is known to be consistent (since its axioms are known to be true and its rules of inference are known to be sound, so that all of its theorems are true). Gödel's theorem does indeed show us how to construct a statement that is true, and indeed can be proved to be true, but cannot be proved or disproved within Peano arithmetic.
Formal systems that are known to be inconsistent are not of much interest, but there are some very interesting and important ones that fall in the third class -- formal systems that seem to be consistent, but have never been proved consistent. By applying the proof of Gödel's theorem to such a formal system, one can construct a statement that is true but not provable in that formal system provided that it is consistent. This does not yet show that the formal system is incomplete or that it contains unprovable truths; these conclusions follow only with the additional premise that the formal system is consistent.