proved his theorem
(in the language
) 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.