Godel's Incompleteness Theorems

• In any consistent formal system expressing arithmetic, true but unprovable statements exist (First Theorem)
• No consistent system strong enough for arithmetic can prove its own consistency (Second Theorem)
• Truth and provability are fundamentally distinct—mathematical truth transcends what systems can prove
• Gödel numbering encodes syntax as natural numbers, enabling modern computability and complexity theory
• Hilbert's dream of complete, consistent mathematics is mathematically impossible
• Results apply to all sufficiently expressive formal systems, not just specific axiomatizations

Gödel's Incompleteness Theorems

Overview

Gödel's Incompleteness Theorems, proven by Kurt Gödel in 1931, represent one of the most profound and surprising results in mathematical logic. These theorems establish fundamental limitations on what can be proven within any formal system sufficiently powerful to encode basic arithmetic. Before Gödel's work, mathematicians pursuing Hilbert's program hoped to find a complete and consistent axiomatic system for all of mathematics—a system where every true statement could be proven and no contradictions could arise. Gödel shattered this dream by showing that such a system is impossible.

The theorems have two parts. The First Incompleteness Theorem shows that in any consistent formal system strong enough to express basic arithmetic, there exist statements that are true but unprovable within that system. The Second Incompleteness Theorem goes further, demonstrating that no sufficiently strong consistent system can prove its own consistency. These results fundamentally changed our understanding of mathematical truth, showing that truth transcends provability.

The impact extends far beyond mathematical logic. Gödel's methods introduced the technique of Gödel numbering—encoding syntactic objects as natural numbers—which became foundational for computability theory, complexity theory, and the theory of formal languages. The theorems forced a reconsideration of formalism as a philosophy of mathematics and continue to influence discussions in philosophy of mind, computer science, and epistemology.

Any formal system powerful enough to express arithmetic is either incomplete (contains true but unprovable statements) or inconsistent (can prove contradictions). Moreover, no such system can prove its own consistency—self-verification is impossible for sufficiently expressive mathematical systems.

• Consistent if there is no formula $\phi$ such that both $T⊢\phi$ and $T⊢\neg \phi$
• Complete if every sentence $\phi$ in $\mathcal{L}$ is decidable in $T$
• $\omega$-consistent if for any formula $\phi (x)$, if $T⊢\phi (\overline{n})$ for all $n\in \mathbb{N}$, then $T⊬\exists x\neg \phi (x)$

Here $\overline{n}$ denotes the numeral representing $n$ (i.e., $S(S(\cdots S(0)\cdots ))$ with $n$ applications of the successor function $S$).

Core Theory

Gödel's Incompleteness Theorems

1. $T⊬G_T$ and $T⊬\neg G_T$ (i.e., $G_T$ is undecidable in $T$)
2. If $T$ is $\omega$-consistent, then $G_T$ is true in the standard model $\mathbb{N}$

We prove the First Incompleteness Theorem. The proof proceeds in several stages.

We establish an effective coding of syntactic objects as natural numbers. Define a Gödel numbering $┌\cdot ┐:\text{Formulas}\to \mathbb{N}$ that assigns to each symbol, term, formula, and finite sequence of formulas a unique natural number. For example:

• Assign prime numbers to basic symbols: $┌0┐=2$, $┌S┐=3$, $┌+┐=5$, etc.
• For a sequence $(a_1,\dots ,a_n)$, use $┌(a_1,\dots ,a_n)┐=2^{a_1}\cdot 3^{a_2}\cdots p_n^{a_n}$ where $p_i$ is the $i$-th prime

This encoding is primitive recursive, meaning both the encoding and decoding functions are computable.

Since $T$ represents arithmetic, it can express primitive recursive relations. In particular, there exists a formula ${\text{Proof}}_T(x,y)$ in the language of $T$ such that for any formula $\phi$ and sequence of formulas $\pi$:

Define the provability predicate:

By the representability theorem, for any formula $\phi$:

• If $T⊢\phi$, then $T⊢{\text{Prov}}_T(┌\phi ┐)$

This is the technical heart of the proof. For any formula $\psi (x)$ with one free variable, there exists a sentence $\delta$ such that:

To construct $\delta$, define the diagonalization function $\text{diag}(x)$ which maps $┌\phi (x)┐$ to $┌\phi (\overline{┌\phi (x)┐})┐$. Let $D(x,y)$ represent this function in $T$. Consider:

Now set $\delta :=\theta (┌\theta ┐)$. By construction and the properties of $D$:

Apply the Diagonal Lemma to $\psi (y):=\neg {\text{Prov}}_T(y)$. This yields a sentence $G_T$ such that:

The sentence $G_T$ "says of itself" that it is not provable in $T$.

Suppose $T⊢G_T$. Then by representability of provability, $T⊢{\text{Prov}}_T(┌G_T┐)$. But $T⊢G_T\leftrightarrow \neg {\text{Prov}}_T(┌G_T┐)$, so $T⊢\neg G_T$. This contradicts consistency of $T$. Therefore $T⊬G_T$.

Now suppose $T⊢\neg G_T$. Then $T⊢{\text{Prov}}_T(┌G_T┐)$ by the biconditional. But if $T$ is $\omega$-consistent, since $T⊬G_T$, there is no proof of $G_T$, so for all $n\in \mathbb{N}$, $\mathbb{N}\models \neg {\text{Proof}}_T(\overline{n},┌G_T┐)$. By representability, $T⊢\neg {\text{Proof}}_T(\overline{n},┌G_T┐)$ for all $n$. But $\omega$-consistency then implies $T⊬\exists x{\text{Proof}}_T(x,┌G_T┐)$, i.e., $T⊬{\text{Prov}}_T(┌G_T┐)$, contradicting our assumption. Therefore $T⊬\neg G_T$.

Assuming $\omega$-consistency, we've shown $T⊬G_T$. This means there is no proof of $G_T$ in $T$, so $\mathbb{N}\models \neg {\text{Prov}}_T(┌G_T┐)$. But $G_T\leftrightarrow \neg {\text{Prov}}_T(┌G_T┐)$ holds in $\mathbb{N}$ (since the biconditional is provable in $T$ and $T$ is sound for arithmetic). Therefore $\mathbb{N}\models G_T$.

This completes the proof of the First Incompleteness Theorem. □

Additionally, the Second Incompleteness Theorem requires that $T$ can formalize enough of its own proof theory (the "Hilbert-Bernays-Löb derivability conditions"). Not every theory satisfying the First Theorem necessarily satisfies the Second.

Examples and Applications

1

Let $T=\text{PA}$, Peano arithmetic with axioms including the induction schema. We construct the explicit Gödel sentence $G_{\text{PA}}$.

First, we establish a Gödel numbering. Assign:

• Variables $v_0,v_1,v_2,\dots$ the codes $2^{2\cdot 0+1},2^{2\cdot 1+1},2^{2\cdot 2+1},\dots$
• Logical symbols: $┌\neg ┐=3$, $┌\to ┐=5$, $┌\forall ┐=7$
• Arithmetic symbols: $┌0┐=11$, $┌S┐=13$, $┌+┐=15$, $┌\cdot ┐=17$, $┌=┐=19$

For a formula like $\forall v_0(v_0+0=v_0)$, its Gödel number is computed using the sequence encoding.

The provability predicate ${\text{Prov}}_{\text{PA}}(y)$ can be written explicitly as a ${\Sigma }_1$ formula:

where $\text{IsProof}(x)$ checks that $x$ codes a valid sequence of formulas each following from previous ones by PA axioms and inference rules, and $\text{Concludes}(x,y)$ checks that the last formula in the sequence coded by $x$ is the formula coded by $y$.

The Diagonal Lemma produces $G_{\text{PA}}$ such that:

Explicitly, $G_{\text{PA}}$ is a ${\Pi }_1$ sentence (of the form $\forall x\psi (x)$ for some bounded formula $\psi$). While we cannot write out the millions of symbols in $G_{\text{PA}}$ explicitly, its structural form is determined: it asserts that no number codes a proof of itself.

By the First Incompleteness Theorem, $\text{PA}⊬G_{\text{PA}}$ and $\text{PA}⊬\neg G_{\text{PA}}$, yet $G_{\text{PA}}$ is true in $\mathbb{N}$.

2

The original Gödel sentence requires $\omega$-consistency to conclude truth. J. B. Rosser (1936) refined the construction to need only consistency.

Define a modified provability notion:

This says "$y$ is provable and its proof comes before any proof of $\neg y$."

By the Diagonal Lemma, construct $R_T$ such that:

If $T⊢\neg R_T$ via some proof with number $q$, and $q<p$, then $\mathbb{N}\models {\text{Proof}}_T(\overline{q},┌\neg R_T┐)\wedge q<p$, so $\mathbb{N}\models \neg {\text{Prov}}_T^R(┌R_T┐)$. But the equivalence gives $\mathbb{N}\models R_T\leftrightarrow \neg {\text{Prov}}_T^R(┌R_T┐)$, and we assumed $T⊢R_T$, so $\mathbb{N}\models R_T$, contradiction.

If $q>p$ (or no such $q$ exists), then $\mathbb{N}\models {\text{Prov}}_T^R(┌R_T┐)$, so $\mathbb{N}\models \neg R_T$, contradicting $\mathbb{N}\models R_T$.

Similarly, if $T⊢\neg R_T$ via proof number $q$, then by the equivalence, $T⊢{\text{Prov}}_T^R(┌R_T┐)$, meaning some proof of $R_T$ exists with number $p<q$, contradicting consistency.

The Rosser sentence thus gives undecidability from consistency alone.

Consider the theory $T_{\text{true}}=\{\phi :\mathbb{N}\models \phi \}$, the set of all true sentences of arithmetic. This theory is:

• Complete: Every sentence is decidable (either true or false)
• Consistent: No contradiction is true in $\mathbb{N}$
• Represents arithmetic: Contains all of PA

This appears to violate the First Incompleteness Theorem! The resolution: $T_{\text{true}}$ is not recursively axiomatizable. There is no computable procedure to enumerate its axioms. By Tarski's Undefinability Theorem, the set of Gödel numbers of true arithmetic sentences is not arithmetically definable, hence not recursively enumerable.

Without recursive axiomatizability, we cannot effectively construct the provability predicate ${\text{Prov}}_T(y)$ needed for the diagonal argument. The hypothesis is essential: only theories with algorithmically recognizable proofs are subject to incompleteness.

Similarly, Presburger arithmetic (arithmetic with only addition, no multiplication) is complete and consistent, but this is possible because it cannot represent all primitive recursive functions—it lacks the expressive power needed for Gödel's construction.

Gödel's construction is a formalization of the liar paradox. Consider the sentence "This sentence is false." If it's true, then it's false; if it's false, then it's true—contradiction.

Gödel's genius was to replace "false" with "unprovable in $T$," yielding "This sentence is unprovable in $T$." This is not paradoxical but merely undecidable:

• If provable, then (by soundness) true, so it says something true about itself (being unprovable), contradiction
• If disprovable, then provably false, but it says it's unprovable—inconsistency
• If unprovable, then it's true about itself, but we can't prove it in $T$

The self-reference is achieved not through vague linguistic tricks but through the rigorous mechanism of Gödel numbering, allowing formulas to "talk about" their own syntactic structure by arithmetic means. Think of it as giving each formula a social security number, then writing formulas that compute with these numbers to refer back to themselves.

Visually: imagine a computer program that contains its own source code as a string and checks whether that source code halts. The program has "self-knowledge" through encoding. Gödel sentences have mathematical self-knowledge through arithmetic encoding of syntax.

Historical Development

Kurt Gödel announced his First Incompleteness Theorem in 1930 at a conference in Königsberg, almost as an aside after a talk by John von Neumann on Hilbert's program. Von Neumann immediately grasped the significance and independently discovered the Second Incompleteness Theorem, though Gödel had already found it. The full paper, "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I" (On Formally Undecidable Propositions of Principia Mathematica and Related Systems I), appeared in 1931.

The original proof used the system of Principia Mathematica (Russell and Whitehead's formalization of mathematics) and required $\omega$-consistency. Barkley Rosser's 1936 refinement weakened this to simple consistency. The proof was significantly streamlined over subsequent decades, with important clarifications by Stephen Kleene, Alonzo Church, and Alfred Tarski.

The Second Incompleteness Theorem's proof originally required careful analysis of formalized provability. The modern approach via the Hilbert-Bernays-Löb derivability conditions was systematized in the 1950s-60s, showing that any theory proving certain basic properties of its provability predicate cannot prove its own consistency. Martin Löb's theorem (1955) gave a beautiful generalization: if $T⊢{\text{Prov}}_T(┌\phi ┐)\to \phi$, then $T⊢\phi$.

Paul Cohen's 1963 forcing technique for independence results in set theory, showing the independence of the Continuum Hypothesis from ZFC, is philosophically aligned with Gödel's work: showing that certain questions transcend particular axiom systems.

Connections to Other Areas

The First Incompleteness Theorem is intimately connected to Turing's Halting Problem. A theory $T$ is complete and consistent iff the set $\{n:T⊢{\phi }_n\}$ (where ${\phi }_n$ is the $n$-th formula) is decidable. But Gödel's theorem shows this set is undecidable for theories representing arithmetic.

More precisely, by the MRDP theorem (Matiyasevich-Robinson-Davis-Putnam), every recursively enumerable set is Diophantine. Thus the halting set $K=\{e:{\phi }_e(e)\downarrow \}$ can be represented by a polynomial Diophantine equation. If PA were complete, we could decide whether this equation has solutions, solving the halting problem—contradiction.

This connection runs deep: both incompleteness and uncomputability stem from diagonalization. The Gödel sentence uses logical diagonalization; the halting problem uses computational diagonalization. Both show inherent limitations of formal methods through self-referential constructions. This unity was recognized early: Church, Turing, and Kleene all worked on both foundations of logic and computation in the 1930s, seeing them as aspects of the same mathematical phenomenon.

What You Need First

What This Opens Up

See Also