# 14.2 First Incompleteness Theorem
14.2 First Incompleteness Theorem

The goal is to construct a sentence that talks about its own provability. This requires combining arithmetization with a method for controlled self-reference.

Representing Provability

From the previous section, we have an arithmetic relation:

$$
\mathrm{Proof}(x,y)
$$

which means “$x$ codes a valid proof of the formula with code $y$”.

Using this, define the provability predicate:

$$
\mathrm{Prov}(y) ;\equiv; \exists x, \mathrm{Proof}(x,y)
$$

So:

$$
\mathrm{Prov}(\ulcorner A \urcorner)
$$

expresses “$A$ is provable”.

This formula lives inside arithmetic. It does not refer to syntax externally.

Diagonalization

We now build a sentence that refers to its own code. The key tool is the diagonal lemma.

It states that for any formula $\varphi(x)$ with one free variable, there exists a sentence $G$ such that:

$$
G \leftrightarrow \varphi(\ulcorner G \urcorner)
$$

The sentence $G$ substitutes its own Gödel number into $\varphi$.

This is a precise form of self-reference.

Constructing the Gödel Sentence

Let:

$$
\varphi(x) \equiv \neg \mathrm{Prov}(x)
$$

Apply the diagonal lemma. There exists a sentence $G$ such that:

$$
G \leftrightarrow \neg \mathrm{Prov}(\ulcorner G \urcorner)
$$

So $G$ says: “the formula with my code is not provable”.

Since that formula is $G$ itself, we interpret this as:

$$
\text{$G$ says: “$G$ is not provable.”}
$$

Analysis of the Sentence

Assume the formal system is consistent.

First, suppose:

$$
\vdash G
$$

Then the system proves $G$. By the meaning of $G$:

$$
G \leftrightarrow \neg \mathrm{Prov}(\ulcorner G \urcorner)
$$

the system would also prove:

$$
\neg \mathrm{Prov}(\ulcorner G \urcorner)
$$

But since $\vdash G$, the system can verify that $G$ has a proof, so:

$$
\vdash \mathrm{Prov}(\ulcorner G \urcorner)
$$

This leads to a contradiction. Therefore:

$$
\not\vdash G
$$

Now suppose:

$$
\vdash \neg G
$$

Then the system proves that $G$ is false. From the definition of $G$, this implies:

$$
\vdash \mathrm{Prov}(\ulcorner G \urcorner)
$$

So the system proves that $G$ is provable. In many standard systems, this leads again to inconsistency.

Under a mild strengthening of consistency, often called $\omega$-consistency or simply soundness for this context, we conclude:

$$
\not\vdash \neg G
$$

So neither $G$ nor its negation is provable.

Statement of the Theorem

Let $T$ be a formal system that:

* is consistent
* can represent basic arithmetic
* can express the provability predicate

Then there exists a sentence $G$ such that:

$$
\not\vdash_T G
\quad \text{and} \quad
\not\vdash_T \neg G
$$

So $T$ is incomplete.

Truth of the Gödel Sentence

In the standard model of natural numbers:

$$
\mathbb{N}
$$

the sentence $G$ is true.

It states that $G$ is not provable. Since we have shown that $G$ is not provable, the statement holds.

So we have:

* $G$ is true
* $G$ is not provable

This is the separation between truth and provability.

Interpretation

The theorem does not depend on any particular formula. It applies to any sufficiently strong formal system.

It shows that no such system can capture all truths about natural numbers.

The construction is robust:

* encoding syntax as numbers
* expressing provability inside arithmetic
* using diagonalization to create self-reference

These three steps produce a sentence that escapes the system’s proving power.

Perspective

The incompleteness phenomenon arises from the system’s ability to talk about itself.

If a system can express statements about its own proofs, then diagonalization can produce a sentence that avoids proof.

This is closely related to other diagonal arguments in logic and computation, including the halting problem.

The next section strengthens this result by showing that a system cannot prove its own consistency.