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:
which means “ codes a valid proof of the formula with code ”.
Using this, define the provability predicate:
So:
expresses “ 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 with one free variable, there exists a sentence such that:
The sentence substitutes its own Gödel number into .
This is a precise form of self-reference.
Constructing the Gödel Sentence
Let:
Apply the diagonal lemma. There exists a sentence such that:
So says: “the formula with my code is not provable”.
Since that formula is itself, we interpret this as:
Analysis of the Sentence
Assume the formal system is consistent.
First, suppose:
Then the system proves . By the meaning of :
the system would also prove:
But since , the system can verify that has a proof, so:
This leads to a contradiction. Therefore:
Now suppose:
Then the system proves that is false. From the definition of , this implies:
So the system proves that is provable. In many standard systems, this leads again to inconsistency.
Under a mild strengthening of consistency, often called -consistency or simply soundness for this context, we conclude:
So neither nor its negation is provable.
Statement of the Theorem
Let be a formal system that:
- is consistent
- can represent basic arithmetic
- can express the provability predicate
Then there exists a sentence such that:
So is incomplete.
Truth of the Gödel Sentence
In the standard model of natural numbers:
the sentence is true.
It states that is not provable. Since we have shown that is not provable, the statement holds.
So we have:
- is true
- 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.