As an aside, if you look at the photo credit on that great color photo of Einstein and Gödel, it was snapped by Oskar Morgenstern, one of the fathers of game theory.
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/
Thanks for the links. I read the account. I was surprised to see that Morgenstern didn't mention Gödel's arguments. It only made a reference to the steps leading up to Gödel's own findings, like what he read on and how much time it took him, but never mentioned the substantial argument, which is what I wanted to read.
When I first became fascinated with incompleteness (following initial coursework in theory of computation), it kind of became my "religion" of sorts for a while. But as many mathematicians lament, the Incompleteness Theorem is one of the most popularly abused proofs of all time - used for non-experts to assert their own half-baked pseudo-philosophy (of course, the same goes for quantum mechanics as well).
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)
Nagel's book is a wonderful exposition (three-page-long footnotes aside). In addition to these two, I might recommend Torkel Franzén's book "Gödel's Theorem: An Incomplete Guide to Its Use and Abuse". Some of the content is fairly technical but not inaccessible by any means. If you're interested in the corner cases of how incompleteness theorems can be applied, it's a terrific resource.
Thanks! I believe I read a reference to this book once on HN, then could not find it. Unless there is another book that focuses on the misuses of the incompleteness theorem, this is the one I'm looking for.
"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."
I read this stuff in "The Emperor's New Mind" by Roger Penrose. It not only talks about this, but introduces to Relativity, Quantum Mechanics, Phase Spaces. It also builds up all the mathematics required, so if you know what complex numbers are - that will be more than enough to follow and understand the concepts introduced well enough. Very highly recommended.
The second part somehow was not as interesting though.
Another book that has several chapters related to GEB is David Deutsch's "The Beginning of Infinity." It's a very accessible read, and for me, eye-opening in more than one way.
+1, a really enjoyable but provocative read. With respect to Godel, Roger Penrose's "Shadows of the Mind" gives a pretty good insight into the implications of Godels theorems.
I have no background in CS or Math, but a lot of philosophy. In other words, I'm a highly interested layman. What's my best plan of action to understanding Godel's theory? Maybe the best approach would be an entry level book on CS?
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…
At the very least a good course in discrete mathematics is a good start (it's also a good start for anything technical as well - one of the most valuable math classes anyone can ever take, as far as I'm concerned)
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.
> At the very least a good course in discrete mathematics is a good start
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.
Knowing computer science stuff like regular languages is really not required to understand the incompleteness theorems; grasping first order logic, a little arithmetic and some elementary recursion theory is sufficient.
I repeat my objection to the Goldstein book raised elsewhere in this discussion.
I always liked "Godels Theorem Simplified". It doesn't rely on heavy technical prerequisites in mathematics or CS. It is pretty much as advertised, a simplification of Godel's original proof. Godel used a more complicated encoding scheme using prime numbers, which Gensler replaces with a simpler encoding scheme. He walks you through various less powerful formal systems, before you get to one complicated enough to have incompleteness issues. There is also discussion about the philosophical ramifications of Godel's theroems.
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 just Godel's theorem, you probably want to focus on Logic more than Math or CS. Godel's proof involves qualifying over first-order logic statements and logical properties of numbers much more than it involves computation or numerics. The most nitty-gritty part is Godel encodings, but it's not that computationally intensive, and the details actually aren't that relevant.
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.
The unsolvability of the halting problem has a slightly weaker version of Goedel's first incompleteness theorem as a trivial corollary. You can use Turing machines to prove a stronger statement very easily as well. Therefore the CS perspective is very enlightening. See http://www.scottaaronson.com/blog/?p=710.
I would recommend coming to terms with "A Transition To Advanced Mathematics". Once you feel like you can plumb Cantor's Diagonalization without nausea :), then read on Godel. GEB is excellent but frothy ( not pointed and a slog ) but is worth it for other reasons.
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.
I think it's best to go directly at the source. Wikipedia has a very understandable sketch of proof (which in itself is quite unconventional) that helps understand the motivation and the content of the theorem: http://en.wikipedia.org/wiki/Proof_sketch_for_G%C3%B6del%27s...
Whatever approach you take, be sure it includes Torkel Franzén's Gödel's Theorem: An Incomplete Guide to Its Use and Abuse. Although it's pretty good, it may not be where you want to start. But there are a lot of bogus conclusions made by people with a superficial understanding of Gödel and that is the best thing I know pointing out the flaws.
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.
The statement "this fact is not provably true under the axioms of mathematics" is not provably true under the axioms of mathematics. Therefore, it is true, but we can never prove it.
I recommend approaching this via uncomputability, and the fact that for every program there is a proof and vice versa.
"It's like an ill-designed jigsaw puzzle. No matter how you arrange the pieces, you'll always end up with some that won't fit in the end."
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.
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.
"I think the point is that if you try to add those unprovable theorems to the system to try to make it complete it becomes inconsistent."
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:
Yes, but in your example the system is still incomplete and the moment you would add an axiom that would make it complete, it would become inconsistent (so either you never finish your puzzles or you finish them and exactly the same moment they fall apart).
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.
Right, but the point here is that we're not just talking about extensions of the system, we're talking about true but unprovable statements—that is, statements that are true in the standard model of arithmetic but not provable in PA (or whatever other arithmetic theory strikes your fancy). This is why Turing looked not at single formal theories but at a hierarchy of consistency extensions of the initial theory. In other words, the game changes from formal provability to informal provability, and from provability relative to a set of axioms to absolute provability. Turing showed (very roughly) that given a tree of consistency extensions (which branches only at limit stages) every Pi_1 sentence was decided at some point a with |a| = ω + 1. Feferman then proved in the 1960s that there is a path through the tree of ordinal notations that decides every Pi_2 sentence. These are completeness results, albeit for progressions of formal systems rather than individual systems. So certainly the puzzle can never be completed within a single formal system, but by restricting to sentences of limited complexity, there is an ordinal-time operation which decides each sentence (obviously there are numerous philosophical problems with this, although I'm afraid my expertise in this area is extremely limited so I can only give a sketch of the issues involved).
But it really is mind-bending: if you, instead, add a theorem to the system (say, ZFC) which states, "ZFC is consistent", this system (ZFC+Con(ZFC)) is consistent! Even more strangely, if you instead add "ZFC is not consistent", this system (ZFC+notCon(ZFC)) is also consistent. We call these "self-hating theories."
The point must surely be that one can add the these true-but-unprovable statements to the original axioms without contradiction. They fit just fine: they're all elements of Th(N). It's a poor analogy because the natural way of thinking of a jigsaw puzzle is of a set of elements (pieces) that are consistent (every piece has a place), so if a piece doesn't fit then it's not consistent with the others. But this is false if the pieces are statements in the language of arithmetic that are true of the natural numbers.
IIRC, In "The Emperors New Mind" Penrose mentions that Godel employed Cantor's "Method of Diagonalization" to show that within a system such as the natural numbers there can be true statements(uncountably infinite) not on the list of provable statements(countably infinite).
On a related note, does anyone know where I would look to understand reducibility of formal systems to one another?
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)
'Reducibility' in general is an informal notion, and as such there are many different technically precise ways of capturing aspects of it. Mutual interpretability and bi-interpretability are two of these, but they apply to formal systems with the same underlying logic (that is, the same semantics and proof theory). There are also many other notions of translation between different logics like Gödel–Gentzen negative translation between classical logic and intuitionistic logic. I'm not sure if there is a good introduction to all of these different ways of capturing reducibility, but you could try asking on math.stackexchange.com, there are usually helpful responses to reference requests there.
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.
One of the features of first order logic is that the provability relation is recursively enumerable: given any recursive first order theory, there is a Turing machine that can list every theorem of that theory (although of course it will run forever).
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.)
Godel Escher Bach is a great book (it's entertaining and informative) for learning about formal systems. There are general rules (rules of inference) for their construction from axioms that will keep you from going wrong.
I read it a long time ago (late teens/early twenties) but it changed my intellectual world and gave me an insight into things that I might never have been introduced to. Hard to know whether it would have the same impact now or the same impact for others but I rate it very highly for personal reasons. Also - Rudy Rucker's 'Infinity and the Mind'...
"Another result that derives from Gödel's ideas is the demonstration that no program that does not alter a computer's operating system can detect all programs that do. In other words, no program can find all the viruses on your computer, unless it interferes with and alters the operating system."
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.
"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"
While that's biographically interesting, you really don't get off the hook from understanding that he used basically the same approach of Cantor's diagonalization.
Be careful. That's a naive view, and drawing more conclusion than I think you mean.
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.
Ahh, fair enough. I'd have to agree with you there. My guess is that that plus being able to inductively generate axioms from experience are largely what let us escape that particular weakness of formal systems.
Provability is relative to a formal system. Whether there are _absolutely undecidable_ statements is more controversial, and still an open question in the philosophy of mathematics. Gödel's disjunction is part of this literature: "Either … the human mind … infinitely surpasses the powers of any finite machine, or else there exist absolutely unsolvable diophantine problems." Soloman Feferman has written about this, for instance in a 2006 Philosophia Mathematica paper.
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/