Gödel proved his

theorem by

*constructing* (in the

language of

arithmetic) a

statement which states "

*this statement cannot be proven in arithmetic*".

Obviously, if arithmetic is consistent then the statement is *true*: if it were false, then it would be provable, and then arithmetic could prove a falsehood -- inconsistency! Hence it is true and unprovable *in arithmetic* (we've just seen it's true, but we weren't doing that bit in arithmetic but in some larger world).

So what's all the noise about?

That something like this can be *said* in the language of arithmetic. The point of formalism is to create a formal language free of the ambiguities that plague natural language. "Cute" statements like this node's title clearly show that self reference is such a harmful ambiguity, but who says we can't create a formal language that will *bar the way* to such ambiguity?

Gödel does. Specifically, he showed that *any* language which is powerful enough to state even mildly interesting things about arithmetic (about at the level of defining the basic properties of multiplication!) can formulate this statement; in fact, he gives a precise construction of this statement.

Sufficiently simple systems of formal logic are still immune to this disease. Unfortunately, they're so simple as to be useless -- they cannot say anything interesting.

In fact there exist *other* types of unprovable statements, with no overt self reference, but it took more than 30 years after Gödel's work to find the first "natural" examples.