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]