On Formally Undecidable Propositions of Principia Mathematica and Related Systems (1931)

In 1931 Kurt Godel published “Uber formal unentscheidbare Satze der Principia Mathematica und verwandter Systeme,” translated into English as “On Formally Undecidable Propositions of Principia Mathematica and Related Systems.” The paper proved what are now called the incompleteness theorems and reshaped the foundations of mathematics.

The hosted English translation by B. Meltzer carries the full title and Godel’s name on its title page. The paper takes aim at the formal system of Whitehead and Russell’s Principia Mathematica and similar systems, asking whether every truth expressible in such a system can be proved within it.

Godel’s central technique was to assign numbers to the symbols, formulas, and proofs of the formal system, so that statements about provability could themselves be written as arithmetical statements. Using this encoding, now known as Godel numbering, he constructed a sentence that, in effect, asserts its own unprovability, and showed that the system can neither prove nor disprove it without contradiction.

As the Stanford Encyclopedia of Philosophy summarizes the result, any consistent system strong enough for elementary arithmetic is incomplete, and such a system cannot prove its own consistency. The idea of treating logical statements and proofs as data within the same system foreshadowed the encoding of programs as numbers, a theme central to the theory of computability that Alan Turing and Alonzo Church developed a few years later.