Skip to content

14.2 First Incompleteness Theorem

Construction of a true but unprovable statement using diagonalization and self-reference.

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:

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

which means “xx codes a valid proof of the formula with code yy”.

Using this, define the provability predicate:

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

So:

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

expresses “AA 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 φ(x)\varphi(x) with one free variable, there exists a sentence GG such that:

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

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

This is a precise form of self-reference.

Constructing the Gödel Sentence

Let:

φ(x)¬Prov(x) \varphi(x) \equiv \neg \mathrm{Prov}(x)

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

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

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

Since that formula is GG itself, we interpret this as:

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

Analysis of the Sentence

Assume the formal system is consistent.

First, suppose:

G \vdash G

Then the system proves GG. By the meaning of GG:

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

the system would also prove:

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

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

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

This leads to a contradiction. Therefore:

⊬G \not\vdash G

Now suppose:

¬G \vdash \neg G

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

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

So the system proves that GG 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:

⊬¬G \not\vdash \neg G

So neither GG nor its negation is provable.

Statement of the Theorem

Let TT be a formal system that:

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

Then there exists a sentence GG such that:

̸TGand̸T¬G \not\vdash_T G \quad \text{and} \quad \not\vdash_T \neg G

So TT is incomplete.

Truth of the Gödel Sentence

In the standard model of natural numbers:

N \mathbb{N}

the sentence GG is true.

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

So we have:

  • GG is true
  • GG 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.