On Formally Undecidable Propositions of Principia Mathematica and Related Systems

Gödel's central claim is that any consistent formal system sufficiently powerful to express elementary arithmetic is incomplete: there exist true arithmetical propositions that the system cannot prove, and the system cannot prove its own consistency. The paper rejects the logicist and formalist assumption that a single formal system could capture all mathematical truth or provide a finitary proof of its own consistency. Gödel proves this by arithmetizing syntax—assigning natural numbers to formulas and proofs—and constructing a sentence that asserts its own unprovability. The result is not a defect of any particular system but a structural limit on formalization as such, provided the system is consistent and recursively axiomatizable.

Gödel numbering is a method for assigning a unique natural number to every symbol, formula, and proof in a formal system, thereby allowing the system to talk about its own syntax through arithmetic. This arithmetization of metamathematics was the essential innovation that made the incompleteness proof possible: it enabled Gödel to construct a sentence that says, in effect, 'this sentence is not provable.' The technique has since become standard in mathematical logic, and the paper includes a list of 45 explicit primitive recursive functions and relations used to manipulate Gödel numbers . Without this device, the self-referential construction that generates the undecidable sentence could not be formalized within the system itself.

The first incompleteness theorem states that any consistent formal system strong enough for arithmetic contains a true sentence that is not provable in the system. The second incompleteness theorem states that such a system cannot prove its own consistency—more precisely, if the system is consistent, the arithmetical formula expressing its consistency is not provable in it. Both theorems appear in the 1931 paper, as Theorems VI and XI respectively . The second theorem is the one with the most direct bearing on Hilbert's program, because it shows that a finitary consistency proof of arithmetic, of the kind Hilbert sought, cannot be carried out within the system whose consistency is at issue.

Gödel submitted the paper on 17 November 1930, and it was published in German in 1931 in Monatshefte für Mathematik und Physik, volume 38, pages 173–198 . The first English translation, by B. Meltzer of the University of Edinburgh, was published in 1962 by Oliver & Boyd, with an introduction by R. B. Braithwaite of Cambridge . A Dover reprint of the 1963 translation appeared in 1992, making the edition widely available . The paper is also reprinted, with the original German facing the English translation and an introductory note by Stephen Kleene, in Volume I of Gödel's Collected Works .

The impact on Hilbert's program is a matter of ongoing scholarly debate, though the second incompleteness theorem is widely regarded as a decisive obstacle to the program in its original form. Hilbert sought a finitary consistency proof for classical mathematics, but Gödel showed that no such proof can be formalized within the system whose consistency is in question. Some scholars, such as Detlefsen, have argued that Hilbertian instrumentalism can survive the first theorem by denying that ideal mathematics must be conservative over the real part . Others, such as Smorynski, argue that the first theorem already defeats the program . What is not disputed is that Gödel's results redirected proof theory toward relative consistency proofs and ordinal analysis.

A common misreading takes the theorems to show that mathematics is inconsistent, or that human reason is fundamentally limited in a way that makes mathematical knowledge impossible. Neither follows. The first theorem applies only to consistent systems, and it shows that they are incomplete, not inconsistent. The second theorem shows that a system cannot prove its own consistency from within, but it does not show that the system is inconsistent, nor that consistency cannot be proved by other means—such as by a stronger system, or by non-formizable arguments. Another misreading treats the theorems as applying to any informal reasoning whatsoever; in fact, they apply to formal systems meeting specific conditions of strength and recursive axiomatizability.