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.