Gödel's First Incompleteness Theorem (Formal Statement)

We state and prove the precise version of Gödel's first incompleteness theorem, which establishes the existence of undecidable sentences in any consistent, sufficiently strong formal system.

Statement

Theorem6.1Gödel's First Incompleteness Theorem

Let $T$ be a consistent, recursively axiomatized theory in the language of arithmetic that extends Robinson arithmetic $Q$ . Then there exists an arithmetic sentence $G$ such that $T \not\vdash G$ and $T \not\vdash \neg G$ .

Proof

Step 1: Representability. Since $T$ extends $Q$ , every computable function is representable in $T$ , and every c.e. relation is $\Sigma_1$ -definable in $T$ .

Step 2: Formalizing provability. The set $\{n : T \vdash \sigma_n\}$ (provable sentences, indexed by Gödel number) is c.e. Hence there exists a $\Sigma_1$ formula $\mathrm{Prov}_T(x)$ such that $T \vdash \sigma \iff \mathbb{N} \models \mathrm{Prov}_T(\ulcorner \sigma \urcorner)$ .

Step 3: Diagonal lemma. Apply the diagonal lemma to $\neg \mathrm{Prov}_T(x)$ : there exists $G$ with $T \vdash G \leftrightarrow \neg \mathrm{Prov}_T(\ulcorner G \urcorner)$ .

Step 4: $G$ is not provable. Suppose $T \vdash G$ . Then $\mathbb{N} \models \mathrm{Prov}_T(\ulcorner G \urcorner)$ , so $T \vdash \mathrm{Prov}_T(\ulcorner G \urcorner)$ (since $\Sigma_1$ truths are provable in $T$ ). But $T \vdash G \leftrightarrow \neg \mathrm{Prov}_T(\ulcorner G \urcorner)$ gives $T \vdash \neg G$ , contradicting consistency.

Step 5: $\neg G$ is not provable (Rosser version). Define a Rosser sentence $R$ : " $R$ is provable only if a shorter proof of $\neg R$ exists." If $T \vdash \neg R$ , a proof of $\neg R$ exists, so (by construction) a proof of $R$ shorter than it exists, giving $T \vdash R$ , contradicting consistency. $\square$

■

RemarkTrue but Unprovable

If $T$ is sound (all its theorems are true in $\mathbb{N}$ ), then $G$ is true in $\mathbb{N}$ (since $G$ is not provable, $\neg \mathrm{Prov}_T(\ulcorner G \urcorner)$ holds, which is what $G$ says). Thus $G$ is a true but unprovable sentence. This shows that truth and provability diverge in any sufficiently strong system.

ExampleConcrete Independent Statements

Paris and Harrington (1977) found a "natural" independent statement: a variant of the finite Ramsey theorem that is provably true but not provable in PA. Goodstein's theorem provides another example: the Goodstein sequence starting from any positive integer eventually reaches 0, but PA cannot prove this.