Proving the First Incompleteness Theorem

Gödel's First Incompleteness Theorem stands as one of the most profound results in mathematical logic. In this lesson, we'll work through the complete proof step by step, examining each component and understanding how they combine to establish this remarkable result.

Statement of the Theorem

Gödel's First Incompleteness Theorem: Any consistent formal system that is sufficiently powerful to express basic arithmetic contains statements that are true but unprovable within the system.

More formally: If T is a consistent theory that includes Robinson arithmetic (Q), then there exists a sentence φ such that neither φ nor ¬φ is provable in T.

Key Components of the Proof

1. Arithmetization of Syntax

The first crucial step is Gödel numbering - a way to encode syntactic objects (formulas, proofs) as natural numbers.

// Example of Gödel numbering for basic symbols
const godelNumbers = {
  '0': 1,
  'S': 2,  // successor function
  '+': 3,
  '*': 4,
  '=': 5,
  '¬': 6,
  '∧': 7,
  '∨': 8,
  '→': 9,
  '∀': 10,
  '∃': 11,
  '(': 12,
  ')': 13
};

// Function to compute Gödel number of a formula
function godelNumber(formula: string): number {
  let result = 1;
  for (let i = 0; i < formula.length; i++) {
    const char = formula[i];
    const prime = nthPrime(i + 1);
    const code = godelNumbers[char] || charCodeToGodel(char);
    result *= Math.pow(prime, code);
  }
  return result;
}

2. Representability in Arithmetic

We need to show that syntactic relations can be expressed arithmetically. Key predicates include:

• Form(x): "x is the Gödel number of a formula"
• Proof(x, y): "x is the Gödel number of a proof of the formula with Gödel number y"
• Provable(y): "∃x Proof(x, y)"

3. The Diagonal Lemma

This is the heart of the construction. For any formula φ(x) with one free variable, there exists a sentence ψ such that:

T ⊢ ψ ↔ φ(⌜ψ⌝)

where ⌜ψ⌝ is the Gödel number of ψ.

// Conceptual representation of the diagonal construction
function diagonalLemma(phi: Formula): Formula {
  // Create a formula that says "the formula obtained by
  // substituting its own Gödel number into position x is not provable"
  const psi = constructSelfReference(phi);
  return psi;
}

4. Construction of the Gödel Sentence

Apply the diagonal lemma to the formula ¬Provable(x):

Let G be the sentence such that: T ⊢ G ↔ ¬Provable(⌜G⌝)

This sentence G essentially says "I am not provable in T".

The Proof

Step 1: G is true if T is consistent

Suppose T is consistent. We show that G is true in the standard model of arithmetic.

Case 1: Suppose T ⊢ G

• Then Provable(⌜G⌝) is true in the standard model
• By the equivalence, ¬Provable(⌜G⌝) is true
• This gives us both Provable(⌜G⌝) and ¬Provable(⌜G⌝), contradiction
• Therefore, T ⊬ G

Case 2: Since T ⊬ G, we have that ¬Provable(⌜G⌝) is true

• By the equivalence T ⊢ G ↔ ¬Provable(⌜G⌝), G is true

Step 2: G is not provable in T

From Case 1 above, we already established T ⊬ G.

Step 3: ¬G is not provable in T

Suppose for contradiction that T ⊢ ¬G.

• Since G ↔ ¬Provable(⌜G⌝), we have T ⊢ ¬¬Provable(⌜G⌝)
• So T ⊢ Provable(⌜G⌝)
• By the correctness of the provability predicate, T ⊢ G
• But then T proves both G and ¬G, contradicting consistency
• Therefore, T ⊬ ¬G

Computational Perspective

From a computability viewpoint, the theorem can be understood as follows:

// If we could decide all true arithmetic statements
function decideArithmetic(statement: ArithmeticStatement): boolean {
  // This function cannot exist for all statements
  // due to the incompleteness theorem
  throw new Error("Cannot decide all arithmetic truths");
}

// The Gödel sentence creates a paradox similar to the halting problem
function godelParadox(system: FormalSystem): boolean {
  const godelSentence = constructGodelSentence(system);
  // If provable, then false (by construction)
  // If not provable, then true but unprovable
  return !system.canProve(godelSentence) && isTrueInStandardModel(godelSentence);
}

Significance and Implications

The proof establishes several crucial points:

1. Incompleteness: No consistent formal system containing arithmetic can prove all arithmetic truths
2. Undecidability: There's no algorithm to determine the truth of all arithmetic statements
3. Limitations of Formalization: Mathematics cannot be completely formalized in any single consistent system

The construction is remarkably elegant - it uses the system's own expressive power to construct a statement that the system cannot decide. This self-referential aspect connects to many other fundamental results in logic and computer science.

Conclusion

Gödel's proof technique introduced revolutionary ideas about self-reference in formal systems. The diagonal lemma and arithmetization became standard tools, influencing developments in computability theory, proof theory, and the foundations of mathematics. Understanding this proof provides deep insight into the fundamental limitations of formal mathematical systems.