I've read a little bit about this theorem, and it's really weird and fascinating. Back in the early 1900's, Bertrand Russell and Alfred Whitehead created a system of arithmetic on which mathematics could be more firmly grounded. There was an ideal of being able to demonstrate every mathematical theorem so far accumulated in the discipline in a really rigorous fashion, building from the most fundamental pieces of set theory and logic. With a system as rigorous as the one Russell and Whitehead devised, it was hoped that every true mathematical statement could be thoroughly proved from first principles. Godel ruined the party and proved in 1931 that any sufficiently powerful system of arithmetic becomes capable of talking, not only about numbers and their properties, but about itself, which allows for paradox to creep in.
When a system becomes capable of talking about itself, it can say things like "this statement is not provable within the present system". Such a statement is true, but manifestly unprovable. If you were to find a proof for that statement, then the statement would be false, suggesting your proof contradicts the premise you're trying to demonstrate. On the other hand, if no proof exists for such a statement, then the statement is true. Godel's deathblow was to show that all similarly powerful systems of arithmetic will be capable of generating such true but unprovable statements. So the dream of being able to prove every true mathematical proposition came to an end. At least that's my understanding of it.
One question Godel has always prompted in my mind is, if truth is independent of provability, then what exactly does it mean for a mathematical statement to be true? If we say that X is true, do we just mean that no counterexamples to X exist?
Back to Prof. Walther MA460 page.
