Weak form

The weak Gödel's first incompleteness theorem states that every -consistent axiomatizable extension of minimal arithmetic is incomplete.

Let $T$ extend minimal_arithmetic, and let $P r v_{T}$ be the standard provability predicate of $T$ .

Then we apply the diagonal lemma to get $G$ such that $T ⊢ G ⟺ \neg P r v_{T} (G)$ .

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

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

Now, suppose that $T ⊢ \neg G$ . Then $T ⊢ P r v_{T} (G)$ . But then as $T$ is consistent there cannot be a standard proof of $G$ , so if $P r v_{T} (x)$ is of the form $\exists y P r o o f_{T} (x, y)$ then for no natural number $n$ it can be that $T ⊢ P r o o f_{T} (┌ G ┐, n)$ , so $T$ is $ω$ -inconsistent, in contradiction with the hypothesis.

Strong form

Every consistent and axiomatizable extension of minimal_arithmetic is incomplete.

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