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://math.stanford.edu/~feferman/papers/lrb.pdf (full text)
"Those who are fascinated by Gödel's theorems—and the general idea of limits to what we can know—may still hunger for a more universal view of their possible significance. But they should not be satisfied with Goldstein's 'vast and messy' goulash, hers is not a recipe for true understanding."
The second part somehow was not as interesting though.
It is a good biography though, covering the roots in the Vienna circle and the disagreements with Wittgenstein.
Edit: Thanks for posting that pdf though, I enjoyed reading it.
Then get Smith's book An Introduction to Gödel's Theorems. It explains Gödel's results in great detail and doesn't assume too much background knowledge. A certain amount of perseverance will, of course, be required…
There's some supplementary material on his website: http://www.logicmatters.net/igt/
Following that, a good class in the theory of computing: understanding what exactly a generative grammar is, properties of classes of languages (e.g., understanding what "regular languages are closed under complimentation" means), pumping lemma, diagnalization proofs, halting problem. The incompleteness theorem is intimately tied to this. This is the "CS-route" to getting a good understanding in Incompleteness, I'm sure math or physics majors come to approach it in each their own way.
Being a little blunt, a background in philosophy (whether it's academic or not) without a solid discrete math background, doesn't help you out at all. This isn't philosophy, it's just a fact about properties of formal systems of sufficient complexity. If you're looking for philosophy you won't find anything too deep in the proof of Incompleteness. The philosophical implications are not clear.
However, I do recommend Rebecca Goldstein's book. It's not technical, and she's a Princeton philosopher who will indulge you with possible philosophical ramifications of the theorem (along with a good narrative). I also recommend her other books as well, especially her first novella "The Mind-Body Problem". From a philosophical perspective, the dispute between Goedel and Wittgenstein who never accepted the Incompleteness Theorem "whereof we cannot speak we must pass over in silence", which, ironically, speaks of something of which we cannot speak.
I believe that the best starting point to get to incompleteness is formal logic. This is the basic set of concepts that lets us make terms, statements and finally proofs the subject of formal mathematical study, thus tying the loop (formally mathematically defined reasoning about formally mathematically defined reasoning :-) ) that leads to Goedels proof.
Discrete mathematics is helpful but it is rather low level, the core concepts in incompleteness come from formal logic.
I repeat my objection to the Goldstein book raised elsewhere in this discussion.
"Godel, Escher, Bach" is another interesting read, but that volume does have a lot of extraneous fluff.
Hey, now. Gödel, Escher, Bach has character and is IMO a very fun book. You might have to read it more then once, though.. it's self-referential and strange-loopy in that way.
If you want to understand the ramifications of Godel's theory, it impacts math more directly than CS. The most directly impacted branches of math are the more "fundamental" ones like Set Theory. Limitations of CS has a lot more to do with Turing's theorems than Godel's.
I think that Godel was more important from a social perspective - there is a strong correlation between Postivism and much of the evils in the 20th Century.
It was aimed at math students, but I don't think I assumed prior knowledge of anything esoteric. Parts of it might be hard to follow without math or CS, I'm not sure.
I recommend approaching this via uncomputability, and the fact that for every program there is a proof and vice versa.
Mentioned in glowing terms here on HN many times:
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.
See for example:
Moreover, Gödel's second incompleteness theorem shows that the consistency of sufficiently strong effective theories of arithmetic can be tested in a particular way. Such a theory is consistent if and only if it does not prove a particular sentence, called the Gödel sentence of the theory, which is a formalized statement of the claim that the theory is indeed consistent.
Eh? No it doesn't! If you add Con(PA) to the axioms of Peano arithmetic you obtain a stronger system. That system can't prove its own consistency, of course, but if you have a proof that the system PA + Con(PA) is inconsistent then you're probably in line for a Fields Medal.
Alan Turing worked on precisely this issue, developing ordinal logics in his PhD thesis (with Alonzo Church) to try to overcome incompleteness. Soloman Feferman, who in the 1960s proved a stronger result than Turing obtained, has written about this extensively. An accessible paper is this one:
From Wikipedia again:
Gödel's theorem shows that, in theories that include a small portion of number theory, a complete and consistent finite list of axioms can never be created, nor even an infinite list that can be enumerated by a computer program. Each time a new statement is added as an axiom, there are other true statements that still cannot be proved, even with the new axiom. If an axiom is ever added that makes the system complete, it does so at the cost of making the system inconsistent.
Pieces already put together = proved true statements.
Pieces that won't fit = true but unprovable statements.
Of course every analogy breaks down somewhere but I thought this one was pretty good.
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)
Second order logic does not have a complete proof theory, so your Turing machine will not be able to compute the consequences of a theory formulated in second order logic. This can be avoided by employing Henkin semantics, but then you're not working with full second order logic anymore. Stewart Shapiro's 2000 book, Foundations without Foundationalism: A Case for Second-Order Logic has the technical details should you be interested.
Is this different from saying that second order logic contains unprovable true statements / that the incompleteness theorem applies?
Also thanks for the really well informed response!
Additionally, first order logic is complete: for every statement true in all models of a theory, there is a proof of the statement from the theory.
These two constraints cannot both be satisfied in a sound deductive system for second order logic. To see that this is so, consider that in second order logic we can prove Dedekind's categoricity theorem: there is only one model (up to isomorphism) of the second order Peano axioms (PA2). Let's assume that the provability relation for second order logic is recursively enumerable. We know from Gödel's incompleteness theorem that the set of first order sentences true of the natural numbers is not recursively enumerable. So take a sentence of the form "If PA2 then _" for some sentence _ which is in that set but not in the extension of the provability relation (this is a legitimate statement since the PA2 axioms are finite so we can just take their conjunction). This should be a logical truth of second order logic, but it's not provable (by the argument just given), so second order logic is incomplete: there are statements which are logical consequences yet are unprovable. So in other words, yes, the incompleteness theorem is very much at play in this limitation of second order logic.
For the technical details I very much recommend chapters 3 and 4 of Shapiro's book; it's not terribly expensive, and any decent university library should have a copy.
(A small footnote to my earlier post: Shapiro's book originally came out in 1991, not 2000—that's just the date of the paperback edition, and I'm unsure as to whether there are any substantial differences between the two.)
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.
"This solution has many strange properties, discussed below, in particular the existence of closed timelike curves which would allow for a form of time travel in the type of universe described by the solution. Its definition is somewhat artificial (the value of the cosmological constant must be carefully chosen to match the density of the dust grains), but this spacetime is regarded as an important pedagogical example"
I.e., "Closed timelike curves". I'm not expert in this matter, but it's a conceptual possibility that fits into general relativity.
Thanks for posting this article.
This it more like it: For any consistent, finite axiomatized formal system that is sufficiently expressive (such as the Principia Mathematica), you can construct a sentence in the language of that formal system that asserts its own un-provability. Therefore, there does not exist a mechanistic method for enumerating over all true statements in the language of that formal system.
By stating "there are some true things that cannot be proved" goes too philosophy deep, and is outside of our pay-grade. Just consider: humans don't reason based on mechanistic principles - and there's no proof as to the expressability of natural language (though we can be sure it's aggravatingly inconsistent)
EDIT: I just want to say that in general, if someone does not really grasp the technical notion of a formal system, consistency, expressiveness, provability, soundness, or recursive enumeration, then it is basically impossible for them to appreciate the incompleteness theorems, and they are very likely to grossly misrepresent it.
Do you support an empiricist view of logic then (http://en.wikipedia.org/wiki/Is_logic_empirical%3F) ? That we justify logical rules because they so strongly correspond with our own experiences?