Gödel's Incompleteness Theorems

Let be a Theory which encodes natural numbers (e.g. or )
We can encode formulas and proofs in with these numbers
so that every proof and/or formula is just a number in
Define

Theorem 1

There is some formula such that if
then and .

Proof

Define a relation on given by if and only if is a proof of
(where is decoded as a proof, and is decoded as a formula)
For any and a formula with one Free Variable,
let be the encoding of and let

i.e. if and only if is not the proof of
Note that

means that (if is an encoding of with one Free Variable)
and it is itself a formula in one Free Variable.
Let be the encoding of

Then

says that is not a proof of i.e. is not a proof of

Let
Then says that there is no proof of:

i.e. says that there is no proof of .
If then this is a contradiction, as we found a proof of .
If , then there is some such that ,
i.e. there is some such that
i.e. there is some proof of .
But then .
We conclude that if then

Theorem 2

Proof

Suppose

Then proves that

from the first theorem.
In particular proves that any is not a proof of
i.e. for any fixed , proves that

and thus:

but then which is a contradiction.