Godel's proof for dummies Can someone give me as simple-a-proof as possible for Godel's Incompleteness Theorem?
I'd love to understand it more.
 A: I try to keep it very short - for more I also highly recommend Nagel-Newman's book Goedel's Theorem.
There are two two main observations:


*

*A sufficiently rich formal system $\mathscr T$ can make statements about itself: there is a computable translation of meta-theoretic/natural language statements $\phi$ about $\mathscr T$ (e.g., some formula in $\mathscr T$ is provable, $\mathscr T$ is consistent, ...)  into formulas $\lceil\phi\rceil$  in $\mathscr T$. The translation is sound in the sense that whenever $\phi$ holds in the meta-theory, then $\lceil\phi\rceil$ is provable within $\mathscr T$.
In particular, given any formula $\psi$ of $\mathscr T$ you get, in a 'computable' way (this e.g. would need to be made more precise), another formula $\lceil\psi\text{ is not provable in }{\mathscr T}\rceil$, expressing that $\psi$ is not provable in $\mathscr T$.
How: Encode meta-theoretic objects like formulas, proofs, ... by natural numbers via Goedel numberings.

*Very roughly any suitably computable operation $\textbf O$ on $\mathscr T$-formulas has a fixed point, i.e. a formula $\psi$ of $\mathscr T$ such that ${\textbf O}(\psi)$ and $\psi$ are equivalent.
How: One realizes that the self-interpretability of $\mathscr T$ gives rise to an (at least informal) interpretation of $\lambda$-calculus, and one imitates a fixed point combinator from $\lambda$-calculus to get the desired fixed points. See https://cstheory.stackexchange.com/questions/27322/fixed-points-in-computability-and-logic
Given these two observations, you get Goedel's theorem as follows: first, choose a fixed point of $$\psi\mapsto \lceil\psi\text{ is not provable in }{\mathscr T}\rceil.$$ In words, $\psi$ is equivalent to the formalization (within $\mathscr T$) of the statement that $\psi$ is not provable; this is what corresponds to the formalization of I am not provable which you often find in  introductions to Goedel's theorem.
Now, suppose $\psi$ can be proved from $\mathscr T$. Then, the soundness of translation says that also $$\lceil\psi\text{ is provable in }{\mathscr T}\rceil,\quad\text{ or equivalently }\quad\neg \lceil\psi\text{ is not provable in }{\mathscr T}\rceil$$ can be proved from $\mathscr T$. However, by construction, the provability of the latter is equivalent to provability of $\neg\psi$ by our choice of $\psi$. Hence, if $\psi$ is provable, then also $\neg\psi$, hence $\mathscr T$ is inconsistent. So we arrive at:
Conclusion: If $\mathscr T$ is consistent, then $\psi$ (from above) is not provable.
On the other hand, the translation of the right hand side into $\mathscr T$ is again equivalent to $\psi$, so we finally obtain:
Theorem: If $\mathscr T$ is consistent, then there is a true formula $\psi$ in $\mathscr T$ (true in the sense that it is the translation of a true statement in the meta-theory) which is not provable from $\mathscr T$. 
