Mathematics

Gödel's Incompleteness Theorems: The Limits of Formal Systems

We explain Gödel's two incompleteness theorems — why any consistent formal system strong enough to express arithmetic contains true statements it cannot prove, and why it cannot prove its own consistency.

Logic Foundations

The Theorems

First Incompleteness Theorem (Gödel, 1931)

Any consistent formal system $\mathcal{F}$ that is capable of expressing basic arithmetic contains a sentence $G$ such that neither $G$ nor $\neg G$ is provable in $\mathcal{F}$ .

Second Incompleteness Theorem (Gödel, 1931)

Any consistent formal system $\mathcal{F}$ that is capable of expressing basic arithmetic cannot prove its own consistency. That is, if $\operatorname{Con}(\mathcal{F})$ denotes the statement " $\mathcal{F}$ is consistent," then:

$\mathcal{F} \nvdash \operatorname{Con}(\mathcal{F})$

What the Theorems Actually Say

A formal system consists of:

A language — symbols and rules for forming well-formed formulas.
Axioms — a recursively enumerable set of starting truths.
Rules of inference — mechanical procedures for deriving new theorems from old ones.

The system is consistent if it does not prove both $\phi$ and $\neg \phi$ for any sentence $\phi$ . It is complete if for every sentence $\phi$ , either $\phi$ or $\neg \phi$ is provable.

Gödel's First Theorem says: no consistent system capable of basic arithmetic can be complete. There will always be true-but-unprovable statements.

The theorem applies to any system at least as strong as Peano Arithmetic (PA), including ZFC set theory, type theory, and any reasonable foundation for mathematics. You cannot escape incompleteness by choosing a cleverer axiom system — any consistent extension still has its own Gödel sentence.

Gödel Numbering

The key technical innovation is Gödel numbering: encoding every symbol, formula, and proof as a natural number.

Assign a unique number to each symbol:

$\ulcorner 0 \urcorner = 1, \quad \ulcorner S \urcorner = 2, \quad \ulcorner + \urcorner = 3, \quad \ulcorner \times \urcorner = 4, \quad \ulcorner = \urcorner = 5, \quad \ulcorner ( \urcorner = 6, \quad \ldots$

A formula $\phi = s_1 s_2 \cdots s_k$ gets the Gödel number:

$\ulcorner \phi \urcorner = 2^{\ulcorner s_1 \urcorner} \cdot 3^{\ulcorner s_2 \urcorner} \cdot 5^{\ulcorner s_3 \urcorner} \cdots p_k^{\ulcorner s_k \urcorner}$

where $p_k$ is the $k$ -th prime. This encoding is injective (by the fundamental theorem of arithmetic) and allows the system to talk about its own formulas and proofs.

The Diagonal Lemma

The heart of the proof is the diagonal lemma (also called the fixed-point lemma):

Diagonal Lemma. For every formula $\phi(x)$ with one free variable in system $\mathcal{F}$ , there exists a sentence $G$ such that:

$\mathcal{F} \vdash G \leftrightarrow \phi(\ulcorner G \urcorner)$

The sentence $G$ "says of itself" that it has the property $\phi$ .

This is the formal version of self-reference — the sentence $G$ contains its own Gödel number as a parameter.

Proof Sketch of the First Theorem

Proof sketch.

Step 1 — Define the provability predicate.

Since proofs are finite sequences of formulas, there is an arithmetic formula $\operatorname{Prov}(x)$ that holds if and only if $x$ is the Gödel number of a provable sentence.

Step 2 — Apply the diagonal lemma.

Apply the diagonal lemma with $\phi(x) = \neg \operatorname{Prov}(x)$ to obtain a sentence $G$ such that:

$\mathcal{F} \vdash G \leftrightarrow \neg \operatorname{Prov}(\ulcorner G \urcorner)$

In plain language, $G$ says: "I am not provable in $\mathcal{F}$ ."

Step 3 — $G$ is not provable.

If $\mathcal{F} \vdash G$ , then $\operatorname{Prov}(\ulcorner G \urcorner)$ holds. But $G$ says $\neg \operatorname{Prov}(\ulcorner G \urcorner)$ , so $\mathcal{F} \vdash \neg G$ . This makes $\mathcal{F}$ inconsistent — contradicting our assumption.

Step 4 — $\neg G$ is not provable.

If $\mathcal{F} \vdash \neg G$ , then $\mathcal{F} \vdash \operatorname{Prov}(\ulcorner G \urcorner)$ . But $G$ is not actually provable (from Step 3), so $\operatorname{Prov}(\ulcorner G \urcorner)$ is false. Since $\mathcal{F}$ proves a false statement, $\mathcal{F}$ is $\omega$ -inconsistent — contradicting our assumption.

Conclusion. Neither $G$ nor $\neg G$ is provable. The system is incomplete. $\square$

Proof Sketch of the Second Theorem

The second theorem follows from a careful internalization of the first theorem's proof.

Proof sketch.

The consistency statement $\operatorname{Con}(\mathcal{F})$ can be expressed as:

$\operatorname{Con}(\mathcal{F}) \equiv \neg \operatorname{Prov}(\ulcorner 0 = 1 \urcorner)$

The proof of the first theorem showed: if $\mathcal{F}$ is consistent, then $G$ is not provable, i.e., $\neg \operatorname{Prov}(\ulcorner G \urcorner)$ , i.e., $G$ is true.

This argument can be formalized within $\mathcal{F}$ :

$\mathcal{F} \vdash \operatorname{Con}(\mathcal{F}) \to G$

If $\mathcal{F} \vdash \operatorname{Con}(\mathcal{F})$ , then $\mathcal{F} \vdash G$ by modus ponens. But we proved $G$ is not provable. Contradiction.

Therefore $\mathcal{F} \nvdash \operatorname{Con}(\mathcal{F})$ . $\square$

The Liar Paradox Connection

Gödel's construction is reminiscent of the Liar Paradox:

"This sentence is false."

The Liar leads to paradox. Gödel's sentence $G$ , which says "This sentence is not provable," avoids paradox because there is a crucial difference between truth and provability. The sentence $G$ is true but unprovable — no contradiction arises.

What the Theorems Do NOT Say

Common misinterpretations:

"Mathematics is broken." No. The theorems say there are limits to formal systems, not to mathematical truth.
"We can never know if mathematics is consistent." Not exactly. We cannot prove consistency within the system itself. We can (and do) prove consistency of PA using stronger systems like ZFC.
"Gödel proved that AI can't think." This is a philosophical leap that the theorems do not support. Gödel himself was cautious about such claims.
"Every true statement is undecidable." Only very specific self-referential statements are undecidable. The vast majority of mathematical theorems are perfectly provable.

Examples of Unprovable Statements

Beyond Gödel's self-referential sentence, there are natural mathematical statements independent of standard axioms:

The Continuum Hypothesis is independent of ZFC (Gödel 1940, Cohen 1963).
The Paris-Harrington Theorem (1977): a combinatorial statement about Ramsey theory that is true but unprovable in Peano Arithmetic.
Goodstein's Theorem (1944): every Goodstein sequence eventually reaches zero — provable in ZFC but not in PA.
The Consistency of PA ( $\operatorname{Con}(\text{PA})$ ) is itself unprovable in PA (by the Second Theorem).

Historical Context

Kurt Gödel proved the incompleteness theorems in 1931, when he was only 25 years old. The paper, "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I," shattered Hilbert's program — the ambitious goal of finding a complete, consistent, decidable foundation for all of mathematics.

Hilbert had proclaimed in 1930: "Wir müssen wissen. Wir werden wissen." ("We must know. We shall know.") Gödel showed that this dream, in its strongest form, was impossible.

The results had immediate impact:

Alonzo Church and Alan Turing (1936) proved that the Entscheidungsproblem (decision problem) is unsolvable.
Alfred Tarski (1933) proved the undefinability of truth.
Paul Cohen (1963) developed forcing, extending Gödel's methods to prove the independence of the Continuum Hypothesis.

The Incompleteness Theorems at a Glance

\begin{aligned} &\textbf{First Theorem:} \\[4pt] &\text{Consistent } + \text{ expresses arithmetic} \implies \text{incomplete} \\[12pt] &\textbf{Second Theorem:} \\[4pt] &\text{Consistent } + \text{ expresses arithmetic} \implies \text{cannot prove own consistency} \\[12pt] &\textbf{Gödel sentence } G: \\[4pt] &G \leftrightarrow \neg\operatorname{Prov}(\ulcorner G \urcorner) \\[4pt] &\text{"I am not provable"} \implies \text{true but unprovable} \end{aligned}

References

Gödel, K., "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I," Monatshefte für Mathematik und Physik, 38, 173–198, 1931.
Smullyan, R., Gödel's Incompleteness Theorems, Oxford University Press, 1992.
Nagel, E. and Newman, J., Gödel's Proof, revised edition, NYU Press, 2001.
Smith, P., An Introduction to Gödel's Theorems, 2nd edition, Cambridge University Press, 2013. Free draft
Wikipedia — Gödel's incompleteness theorems
Stanford Encyclopedia of Philosophy — Gödel's Incompleteness Theorems

Back to all posts