A little recursion theory can make Gödel's Theorems intuitively easy.
Let A be the set of <M> such that M does not accept the input <M>. By
diagonalization techniques we can show A is not recursively
enumerable.
Now let us fix a logical theory like ZFC set theory. The actual theory
does not matter much. Let B be the set of <M> such that there is a
proof in ZFC of the statement "M does not accept input <M>."
B is recursively enumerable since we can just try all possible proofs.
Now B is clearly a subset of A so there must be an input <M> in
A-B. For this <M>, we have that M does not accept input <M> but
there is no proof of this fact. We now have a true mathematical
statement with no proof. This is Gödel's first theorem.
We can be more constructive. Since B is recursively enumerable there
is some Turing machine N that computes B. Suppose that N accepts
<N>. This means <N> is in B which implies there is a proof that <N>
does not accept N, a contradiction.
So <N> cannot accept N which means <N> is not in B. So we have now
constructed an N such that the statement "N does not accept
<N>" is true but not provable.
But wait a minute, didn't I just give a proof that N does not accept
<N>? Actually I had to make the assumption that ZFC is
consistent. If ZFC is inconsistent then every statement (true or
false) is provable so B would not be a subset of A and my whole
argument falls apart.
If ZFC could prove that ZFC is consistent then I would not have to
make any assumption and would have a contradiction. Thus ZFC cannot prove its
own consistency. This is Gödel's second theorem.
Logicians tell me I'm cheating: I had to assume something technically
stronger than consistency for this argument to work. Still these proofs
illustrate the amazing power of Turing machines to make Gödel's
theorems easier to understand.