I always wondered how to describe Gödel's Incompleteness Theorems in a nutshell, without all the technicalities, but still very close to what its idea is. I am interested to read if my description nails the idea of the Incompleteness Theorems or where I commit serious errors or confusions.

p.s. I did this a while ago already, but I think my new version is better than the old one. Please only answer if you somehow familiar with the theorems!

First Incompleteness Theorem

We assume a consistent formal system S where we can syntactically correct formulate the following statement G: G <-> ~Proof(G). There are two cases within S:

(1) G is provable, but then G is not provable (~Proof(G)) which is a contradiction and therefore impossible,

(2) ~G is provable which means (~G & Proof(G)) v (G & ~Proof(G)), but that means in either case G will be proven which is a contradiction and therefore impossible.

So our (consistent) system S cannot prove G or ~G and is therefore incomplete (or it could prove G or ~G if it was inconsistent for trivial reasons). Within S we can't decide if G or ~G is true, but of course from a meta-view we know that G is true. Gödel's "only" accomplishment was to show that G can be formulated syntactically correct in a special S called PM and therefore "infects" whole math (and yes, that was genius).

Second Incompleteness Theorem

Let's assume our system S again, this time strong enough to prove its First Incompleteness Theorem, i.e. if S is consistent then G which says G <-> ~Proof(G). Let's assume we could prove the consistency of S in S. Then by mp we could prove in S that G which is impossible due to the First Incompleteness Theorem, therefore the assumption must be false.