http://en.wikipedia.org/wiki/Oskar_Morgenstern

Morgenstern and Einstein were Gödel's closest friends, I've just now learned. It gives me goosebumps looking at that photo and imagining the three of them on that lawn.

Semi-related, here's an account of Gödel's "pent-up lecture" about the inconsistencies in the American constitution that he told to his citizenship examiner: http://morgenstern.jeffreykegler.com/

These are a few books I recommend:

"Incompleteness - The proof and paradox of Kurt Gödel" by Rebecca Goldstein

"Gödel's Proof" by Ernst Nagel (it's a tiny book, not too technical, but technical enough for anyone with a solid CS background to appreciate and understand)

http://news.ycombinator.com/item?id=3991687

http://www.logicomix.com/en/

Mentioned in glowing terms here on HN many times:

http://www.hnsearch.com/search#request/all&q=logicomix

http://news.ycombinator.com/item?id=846451

http://news.ycombinator.com/item?id=870762

http://news.ycombinator.com/item?id=874471

http://news.ycombinator.com/item?id=3690254

It was my present for proofing an early draft of "Here's Looking at Euclid" / "Alex's Adventures in Numberland"

I really don't understand this analogy. The first incompleteness theorem shows that there are statements true of the natural numbers which aren't provable from any sufficiently strong recursive theory. It's more like Th(N) (the set of statements true of the natural numbers) being a jigsaw puzzle from which many pieces will always be missing if you start with a recursive set of pieces and try to lay down only those pieces which a provable from your initial set. Nothing "won't fit": there aren't inconsistencies or incompatibilities at work here, but incompleteness.

I'm really interested by questions like:

Why is second order logic irreducible to first order logic if I could use first order logic to reason about the behavior of a turing machine running a second order logic theorem prover with whatever inputs I like?

How do I get something that can do what I can do, which is to say take any formal system and prove theorems with it? How do you determine what formal systems are "valid" logics? (Leading to sensible conclusions rather than nonsense like A & ~A)

http://www.damtp.cam.ac.uk/events/strings02/dirac/hawking/

I think I just heard a 'pop'ping sound.. but really, writers try too hard sometimes to make this stuff accessible to people. I don't think someone who is going to get a whole half-way into the article is going to need such reductionism to catch their interest; I'd honestly be more excited if the actual symbolic definition of the theorem was shown to me at that point.

Wait, what?! Anyone have a ref?

Edit: Thanks to andyjohnson and vbtemp. TIA for others too.

Thanks for posting this article.