Proof of Gödel's first incompleteness theorem

Weak form

The weak Gödel's first incompleteness theorem states that every [ $~$\omega$~$-consistent] [ axiomatizable] extension of minimal arithmetic is incomplete.

Let $~$T$~$ extend [-minimal_arithmetic], and let $~$Prv_{T}$~$ be the standard provability predicate of $~$T$~$.

Then we apply the diagonal lemma to get $~$G$~$ such that $~$T\vdash G\iff \neg Prv_{T}(G)$~$.

We assert that the sentence $~$G$~$ is undecidable in $~$T$~$. We prove it by contradiction:

Suppose that $~$T\vdash G$~$. Then $~$Prv_ {T}(G)$~$ is correct, and as it is a $~$\exists$~$-rudimentary sentence then it is [every_true_e_rudimentary_sentence_is_provable_in_minimal_arithmetic provable in minimal arithmetic], and thus in $~$T$~$. So we have that $~$T\vdash Prv_ {T}(G)$~$ and also by the construction of $~$G$~$ that $~$T\vdash \neg Prv_{T}(G)$~$, contradicting that $~$T$~$ is consistent.

Now, suppose that $~$T\vdash \neg G$~$. Then $~$T\vdash Prv_{T}(G)$~$. But then as $~$T$~$ is consistent there cannot be a standard proof of $~$G$~$, so if $~$Prv_{T}(x)$~$ is of the form $~$\exists y Proof_{T}(x,y)$~$ then for no natural number $~$n$~$ it can be that $~$T\vdash Proof_ {T}(\ulcorner G\urcorner,n)$~$, so $~$T$~$ is $~$\omega$~$-inconsistent, in contradiction with the hypothesis.

Strong form

Every consistent and [-axiomatizable] extension of [-minimal_arithmetic] is [complete incomplete].

This theorem follows as a consequence of the [ undecidability of arithmetic] combined with the lemma stating that [ any complete axiomatizable theory is undecidable]