Gödel's Incompleteness Theorems

Gödel’s incompleteness theorems are two results in logic concerning the limitations of formal systems capable of expressing elementary arithmetic. Published by Kurt Gödel in 1931, they establish that sufficiently strong, consistent, effectively axiomatized theories cannot decide every sentence in their language and, under appropriate conditions, cannot prove their own consistency. These are precise restrictions on formal derivability, rather than claims that mathematics is contradictory or that mathematical reasoning is generally unreliable. (doi.org)

Historical setting

The theorems emerged from investigations into the foundations of mathematics, particularly Hilbert’s program, associated with David Hilbert. Its objectives included formalizing mathematics and establishing the consistency of its formal theories through finitistic reasoning. Gödel’s results imposed fundamental restrictions on this project: no consistent, effectively axiomatized theory encompassing enough arithmetic can settle every arithmetical question, and consistency proofs cannot always be carried out within the theory being justified. These restrictions helped redirect foundational research toward studying the strength and limitations of particular theories. (ic.openlogicproject.org)

Gödel presented his results in On Formally Undecidable Propositions of Principia Mathematica and Related Systems I, published in Monatshefte für Mathematik und Physik, volume 38, pages 173–198. The paper supplied a proof of the first theorem and outlined the second. (doi.org)

Conditions and terminology

A formal theory specifies a language, axioms, and rules governing formal proofs. It is consistent if it does not prove both a sentence and its negation. It is complete, in the relevant syntactic sense, if for every sentence it proves either that sentence or its negation. A sentence that is neither provable nor refutable is independent of the theory. (ic.openlogicproject.org)

Effective axiomatization means that the axioms can be enumerated by an algorithm; they need not form a finite list. Sufficient arithmetic strength means that the theory can represent the elementary numerical operations and relations needed to encode formal reasoning. A standard benchmark for the first theorem is Robinson arithmetic, usually denoted $Q$. First-order Peano arithmetic, which additionally includes an induction schema, is a central example to which both theorems apply. (web.mit.edu)

The hypotheses matter. Presburger arithmetic, the theory of natural numbers with addition but without multiplication, is complete and decidable. Conversely, the collection of all sentences true in the standard natural numbers is complete but not effectively axiomatizable. Neither example contradicts incompleteness. (people.csail.mit.edu)

First incompleteness theorem

In its standard Gödel–Rosser form, the first theorem states:

Every consistent, effectively axiomatized theory extending Robinson arithmetic contains a sentence that it can neither prove nor refute.

Gödel’s original argument used the stronger assumption of ω-consistency to establish that the constructed sentence’s negation was also unprovable. This excludes a theory’s proving that some natural number has a property while disproving that property for every individual numeral. J. Barkley Rosser modified the construction so that ordinary consistency suffices for incompleteness. (web.mit.edu)

“Unprovable” is always relative to specified axioms and inference rules. An independent sentence may become provable after adding new axioms. Nevertheless, every consistent extension that remains effectively axiomatized and sufficiently strong is itself incomplete; additional axioms do not produce a final effective theory deciding all arithmetic. (math.berkeley.edu)

Arithmetization and self-reference

The proof’s central technique is Gödel numbering: assigning natural-number codes to symbols, formulas, and proofs. Operations on expressions can then be represented by numerical operations. This converts questions about syntax—such as whether a coded sequence constitutes a proof—into questions about natural numbers. The coding does not require expressions literally to contain their own text. (web.mit.edu)

The diagonal lemma produces a sentence $G_T$ satisfying

where $\operatorname{Prov}_T(x)$ expresses provability in $T$, and $\ulcorner G_T\urcorner$ denotes the sentence’s numerical code. Informally, $G_T$ asserts its own unprovability in that particular theory. If $T$ proved it, the theory could also establish that a proof exists, contradicting what the sentence asserts. (web.mit.edu)

For the standard construction, consistency implies that $G_T$ is true in the standard natural numbers yet unprovable in $T$. Recognizing this truth relies on reasoning about the theory’s consistency from outside it, rather than on a proof within $T$. (math.berkeley.edu)

Second incompleteness theorem

A standard formulation states that a consistent, effectively axiomatized theory extending Peano arithmetic cannot prove its own conventional arithmetical consistency statement:

Here consistency is expressed as the nonexistence of a coded proof of contradiction. The formulation depends on the standard representation of provability and the relevant derivability conditions; it does not apply indiscriminately to every sentence informally described as asserting consistency. (ocw.mit.edu)

The proof formalizes enough of the first theorem’s reasoning to establish, inside $T$, that $\operatorname{Con}(T)$ implies $G_T$. An internal consistency proof would therefore yield the forbidden proof of $G_T$. Stronger theories may nevertheless prove the consistency of weaker ones. The theorem prohibits a particular kind of internal justification, not all mathematical consistency proofs. (ocw.mit.edu)

Completeness, models, and computation

Incompleteness does not conflict with Gödel’s completeness theorem for first-order logic. Logical completeness concerns deriving every sentence that follows from the axioms in all their models. An incomplete theory instead has sentences whose truth varies between models of its axioms. Truth in the intended natural-number structure therefore differs from logical consequence across all models. (ic.openlogicproject.org)

The results also connect proof theory with computability. The undecidability underlying the halting problem provides another route to arithmetic incompleteness: an effective, sound, complete arithmetic theory would permit algorithmic decisions about computations that no algorithm can universally make. The distinction remains between checking an individual finite proof and deciding every possible mathematical question. (math.berkeley.edu)