Gödel’s Incompleteness Theorems

The publication of Kurt Gödel’s paper, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme (On Formally Undecidable Propositions of Principia Mathematica and Related Systems), in 1931, sent shockwaves through the foundations of mathematics. It dismantled the optimistic trajectory set by David Hilbert and changed the way we understand the limits of formal logic forever.

1. Hilbert’s Program and the Quest for Certainty

At the start of the 20th century, David Hilbert proposed a monumental task for mathematicians: to provide a solid foundation for all of mathematics by formalizing it into a set of axioms. Hilbert’s Program sought to prove that mathematics was:

1. Complete: Every mathematical statement can be either proven or disproven.
2. Consistent: No contradiction (e.g., $0=1$) can be derived from the axioms.
3. Decidable: There exists a definite procedure (algorithm) for determining the truth or falsehood of any statement.

Hilbert famously declared, “Wir müssen wissen. Wir werden wissen.” (We must know. We will know.) Gödel’s work would soon demonstrate that for many systems, we simply cannot know.

2. Formal Systems and Recursive Axiomatizability

To understand Gödel’s result, we must define what we mean by a formal system $T$. A system is typically considered “sufficiently strong” if it can encompass Peano Arithmetic (PA).

A system $T$ is recursively axiomatizable if there is an algorithm that can decide whether any given string of symbols is an axiom of the system. This requirement is crucial; it ensures that the “rules of the game” are clearly defined and computable.

A formal system consists of:

• A language $\mathcal{L}$ of symbols.
• A set of axioms (fundamental truths).
• Rules of inference (e.g., Modus Ponens) to derive theorems from axioms.

3. Arithmetization: Gödel Numbering

The core of Gödel’s technique was Arithmetization of Syntax. He realized that statements about a formal system could be mapped into the system itself by assigning unique natural numbers to symbols, formulas, and even entire proofs.

Each symbol is assigned a constant. For example:

• ’(’ $\to 1$
• ’)’ $\to 2$
• '$\neg$' $\to 3$
• '$\forall$' $\to 4$

A formula is encoded using the Fundamental Theorem of Arithmetic. If a formula consists of symbols $s_1,s_2,\dots ,s_n$ with Gödel numbers $g_1,g_2,\dots ,g_n$, its unique Gödel number $G$ is: $G=2^{g_1}\cdot 3^{g_2}\cdot 5^{g_3}\cdots \cdot p_n^{g_n}$ where $p_n$ is the $n$-th prime. Because prime factorization is unique, we can move between the syntax of logic and the arithmetic of integers without loss of information.

Python Implementation: Simple Gödel Numbering

The following script demonstrates how to map a sequence of formal symbols to a unique large integer using prime factorizations.

import sympy

def godel_encode(symbols):
    """
    Encodes a string of symbols into a unique Gödel number.
    Symbols are represented by their index in a predefined dictionary + 1.
    """
    mapping = {
        '~': 1, 'v': 2, '>': 3, '∃': 4, '=': 5, 
        '0': 6, 'S': 7, '(': 8, ')': 9, ',': 10,
        'x': 11, 'y': 12, 'z': 13
    }
    
    primes = list(sympy.primerange(2, 100))
    encoded_val = 1
    
    for i, char in enumerate(symbols):
        symbol_val = mapping.get(char, 0)
        if symbol_val == 0:
            raise ValueError(f"Symbol '{char}' not in mapping.")
        
        # Use the (i+1)-th prime raised to the symbol's value
        encoded_val *= (primes[i] ** symbol_val)
        
    return encoded_val

# Example: Encode 'S(0)=x'
formula = "S(0)=x"
# Characters: S=7, (=8, 0=6, )=9, = = 5, x=11
# Value = 2^7 * 3^8 * 5^6 * 7^9 * 11^5 * 13^11
g_number = godel_encode(formula)
print(f"The Gödel number for '{formula}' is:\n{g_number}")

4. The Diagonal Lemma

The Diagonal Lemma is the technical engine behind Incompleteness. It states that for any formula $\psi (x)$ in the language of $T$ with one free variable, there exists a sentence $G$ such that: $T⊢G\leftrightarrow \psi (┌G┐)$ where $┌G┐$ denotes the Gödel number of $G$. In essence, this allows us to construct sentences that talk about their own properties. By choosing $\psi (x)$ to be $\neg \text{Prov}(x)$ (where $\text{Prov}(x)$ means “x is the Gödel number of a provable formula”), we can construct a sentence $G$ that effectively asserts: “I am not provable.”

5. The First Incompleteness Theorem

Statement: In any consistent, recursively axiomatizable formal system $T$ that is strong enough to perform basic arithmetic, there exist statements that are true but unprovable within $T$.

Proof Sketch:

1. Construct the Gödel sentence $G$ such that $T⊢G\leftrightarrow \neg \text{Prov}(┌G┐)$.
2. If $T⊢G$, then $G$ must be true (assuming $T$ is sound). But $G$ says $G$ is not provable. This is a contradiction.
3. If $T⊢\neg G$, then $\neg G$ is true, which means $G$ is false. If $G$ is false, then $G$ is provable. But if $T$ proves $\neg G$ and $G$ is provable, $T$ is inconsistent.
4. Therefore, if $T$ is consistent, neither $G$ nor $\neg G$ can be proven in $T$.

Crucially, because $G$ is not provable, what it claims (that it is not provable) is actually true. We have found a truth that the system cannot reach.

6. The Second Incompleteness Theorem

Gödel’s second theorem is perhaps even more devastating. It addresses the question of Consistency.

Let $\text{Con}(T)$ be the formal sentence expressing that “System $T$ is consistent,” defined as the absence of a proof for a contradiction (e.g., $\neg \text{Prov}(┌0=1┐)$).

Statement: A consistent, recursively axiomatizable formal system $T$ (of sufficient strength) cannot prove its own consistency. That is: $T/⊢\text{Con}(T)$

If we want to prove that arithmetic is consistent, we must use a system stronger than arithmetic (like Set Theory). But then we need to prove the consistency of that system, leading to an infinite regress. There is no “ultimate” foundation that can verify itself.

7. Impact on Foundations and Computation

The theorems marked the end of Logicism (the attempt to reduce all math to logic) and severely limited Formalism.

Connection to Computation: The Halting Problem

Alan Turing later generalized these ideas into the realm of computer science. The Halting Problem—proving whether a given program will eventually stop or run forever—is undecidable. There is a deep isomorphism between Gödel’s unprovable sentences and Turing’s uncomputable functions.

If there were a general algorithm to decide mathematical truth, we could solve the Halting Problem, which we know is impossible. Thus, Gödel’s Incompleteness is the logical ancestor of the limits of modern computation.

8. Conclusion

Gödel did not show that mathematics is “broken.” Rather, he showed that mathematical truth is a larger concept than mathematical proof. A formal system is like a flashlight in a dark room: no matter how bright it is, there will always be corners it cannot illuminate. The richness of mathematics arises precisely because it cannot be contained within a single finite box.

Knowledge Check