Comment by vyodaiken

What made the theorem hard is not the details, which are simple, it's the conceptual leap to thinking about mathematical statements as mathematical objects - something that is much easier for us than for mathematicians of Godel's time because we are familiar with programs and computers. Much of the text is taken up with proving things that were surprising to mathematicians of the era, but are now commonplace: e.g. that we can treat numbers as encoding mathematical propositions so that for every proposition P expressible in some formal logic L, there is a number #P which encodes P in some unambiguous way - as long as L is expressive enough to formalize some basic arithmetic. Then we can start making trouble by asking if we can construct a proposition Q so that Q(#P) is true iff the proposition #P encodes, P, is provable in our system. If so, we should be able to prove Q(#P) or NOT Q(#P) if L is complete, but things don't work out well because it's possible to encode paradoxical statements. In short.