Gödel's first incompleteness theorem

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

AI ALIGNMENT FORUM
AF

Proof of Gödel's first incompleteness theorem

Weak form

Strong form

AI ALIGNMENT FORUM
AF

Proof of Gödel's first incompleteness theorem

Weak form

Strong form