Gödel's incompleteness theorems

The first incompleteness theorem shows that any consistent formal system F that contains a certain minimal amount of arithmetic (typically Robinson arithmetic Q) is incomplete: there exists a sentence G_F (the Gödel sentence) that is true in the standard model of arithmetic but not provable in F. Moreover, neither G_F nor its negation is provable.¹ The second incompleteness theorem, a corollary of the first, shows that F cannot prove its own consistency (assuming F is consistent and sufficiently strong).² These theorems overturned Hilbert's program, which aimed to prove the consistency of all of mathematics using finitary, provable methods.

The incompleteness theorems have deep implications for the foundations of mathematics. They demolish the hope of a complete, consistent, and decidable axiomatization of arithmetic. Hilbert's program, which sought to banish all uncertainty, was shown to be impossible in its original form.³ In philosophy, the theorems are often cited in debates about mechanism, consciousness, and the limits of human reasoning—though such interpretations are disputed.⁴ The theorems also influenced early computer science: the undecidability of the halting problem (Turing, 1936) is closely related to the first incompleteness theorem.⁵

Gödel originally proved the theorems under the assumption of ω-consistency (a stronger condition than plain consistency).⁶ In 1936, J. Barkley Rosser improved the first theorem to require only consistency, by constructing a more complex self-referential sentence.⁷ Another lesser-known result is that the first theorem does not prevent the existence of a consistent, complete theory of arithmetic if we drop the requirement that the axioms be recursively enumerable—but such a theory would be non‑constructive. The second theorem is often misinterpreted: it does not say that a system's consistency cannot be proved at all, but only that it cannot be proved within the system itself (if the system is consistent). For example, the consistency of Peano arithmetic can be proved in ZF set theory.² Gödel's original paper used a complicated numbering of formulas; the modern presentation using Gödel numbering is simpler but retains the same idea.

The proof of the first incompleteness theorem proceeds by constructing a self-referential sentence that asserts its own unprovability. Gödel devised a method of encoding expressions of a formal language as natural numbers (Gödel numbers). Using this, he could express the syntactic property of being a proof of a sentence as an arithmetical predicate. The Gödel sentence G is then defined as the fixed point of the formula “there is no proof of the sentence with Gödel number y”. Assuming the system is consistent, G is neither provable nor refutable, yet it is true in the standard interpretation.¹ The second theorem follows by formalizing the proof of the first theorem within the system itself, showing that if the system could prove its own consistency, it would also prove G—a contradiction.

Gödel numbering

A mapping of formulas and proofs to natural numbers, enabling the formal language to talk about itself.

ω-consistency

A stronger condition than consistency: a system is ω-consistent if it does not prove both ∃x P(x) and ¬P(n) for every natural number n.

Formal system

A set of axioms and inference rules in a formal language, used to derive theorems.

Recursive axiomatization

A set of axioms whose membership can be effectively decided by a mechanical procedure.