Russell and Godel - What's so important?

A former student emailed me about Russell's discovery of the inconsistency inherent in considering the set of all sets that don't contain themselves. "What's all the fuss?", he asked.

I mentioned how this led Godel to the discovery and proof that in any formal system (like geometry) there are statements that have been proved to be true, statements that have not yet been proved to be true but are provable, and, unfortunately (and this is the big shocker!) true statements that will never be able to be proved to be true (and we won't know which of the unproved statements belong in this category.)

He still wondered why this was so important. Here's my response.

Imagine you have some organized system, like geometry. You start with some axioms (assumptions), and derive theorems. Each of the theorems is proved. You KNOW therefore that your system is consistent. Sometimes you make lucky guesses by seeing patterns, so you propose new theorems, but you call them postulates because you haven't proved them yet (like the Four Colour Map Postulate or the Congruence Postulates). Eventually, either a counter-example is discovered so the postulate is dumped, or you prove the theorem. The FCM postulate is now the FCM Theorem because it has been proved. The conguence postulates remain unproved. We use them, though, but in the back of our minds we have that tiny reservation that everything proven using congruent triangles as an intermediate step is suspect. Our dream, of course, is completion: we prove all true theorems in our system.

What if the system has an infinite number of possible theorems. OK, so we can't get completion in a finite time, but completion (at the end of time!) is possible in principle.

BUT, suppose (heaven forbid!) that there are true theorems in the system that are forever unprovable and YOU DON'T KNOW WHICH ONES THEY ARE!

You would be calling them postulates because you haven't proved them yet, but you have a gut feeling that they are true, so you are devoting time to proving them. This time will be ultimately wasted, even if you devote an INFINITE amount of time, because the statement you are trying to prove happens to be one of the unprovable statements.

Russell/Godel's work showed that this horrendous situation exists in ALL formal systems. (Formal=axiom/theorem/ proof system.) There will ALWAYS be true but unprovable statements, so you will never know the system is complete. Persistance is futile!

This was a great shock to mathematicians and logicians. It's like discovering that the earth is not the centre of the universe, or that humans evolved from non-humans. Ever since Euclid, mathematicians delighted in thinking of their discipline has solid and objective. Opposite angles are equal not because we want them to be so, or some king demands them to be so, but because we can PROVE them to be so. What fantastic advances came from the development of formal systems: number theory, set theory, calculus, etc. I think it's more than just the worry that a mathematician might be wasting time trying to prove a true-bue-unprovable-theorum. It's deeper. What makes THAT theorem (i.e. the unprovable one) different from the other proveable theorems? No one will ever know! --sigh--