I have admired Gödel since I read Hofstadter's: Gödel, Escher, Bach: an eternal golden braid. I hadn't read his work as a logician, but would talk with friends about it (and its implications) informally. That is, until I was chatting with Suman in 2008. He could tell that I would benefit from reading a popularization of his incompleteness theorems that dealt more directly with the content of his proof, so he and Anjali gifted me this book for my birthday (Harvey-mas).
The book was a joy to read (man have I been lucky with these books - I seem to say that they all are great). I enjoyed learning about Gödel's life - his life in Vienna, his work on the proofs, and his cherished walks with Einstein, another scientist who Rebecca Goldstein argues is intellectually exiled* by his theories/proofs - and the proof itself.
When I was an undergraduate in an introductory course on philosophy and discussing a number of important proofs, I found myself wishing for an airtight proof that the axioms of an argument were correct. Could there be assurance that I was using the right axioms? If not, I might come to the completely wrong conclusion despite using a rational argument. As you know, in any argument, the conclusions follow from the premises via rules of inference.
At the time, I constructed an argument by analogy that no such proof existed since we could not imagine removing a condition, which we could not imagine removing (e.g. one could not imagine removing from the set of axioms that a human mind is a prerequisite for rational argument). Just as a fish would not have a concept for water (since it had always been fully surrounded by water and there had never been not water for it), so too, we humans could be fully immersed in some set of beliefs or conditions which would be impossible to imagine going without.
Via Gödel's incompleteness theorems**, Gödel proved that such a program was useless: we cannot justify a set of premises in a logical system using the logic alone. If you are interested in the context from which Gödel's work arose, check out: Hilbert's program, and the Liar's paradox (i.e. "This sentence is false".
Implications of incompleteness
While many others extended the incompleteness theorems to the humanities, the computer sciences, and intelligence research (see Penrose for example), Gödel himself was more reticent to extend his theories. He does have this to say about the differences between men and machines though:
Either the human mind surpasses all machines (to be more precise it can decide more number theoretical questions than any machine) or else there exist number theoretical questions undecidable for the human mind.
By this, Gödel seems to suggest that either we are not like a machine (because our decision mechanism is not, at base, mechanical), and we have access to truths that a formal system would find unprovable; or else, we are at base complicated machines that have deluded ourselves into believing we have access to unformalizable mathematical truths.
* While both Einstein and Gödel achieved a large degree of fame for their discoveries, Goldstein argues that it was the world's subjectivist interpretations of each man's theory that lead to their respective marginalization. For Einstein and Gödel, their work bespoke the objectivist reality of Physics (physical realism) and Mathematics (Platonism).
** From Wikipedia: "For any formal effectively generated theory T including basic arithmetical truths and also certain truths about formal provability, T includes a statement of its own consistency if and only if T is inconsistent."