In 1931 the Austrian logician Kurt Godel published the paper whose German title transliterates as “Uber formal unentscheidbare Satze der Principia Mathematica und verwandter Systeme I,” meaning “On Formally Undecidable Propositions of Principia Mathematica and Related Systems I.” It appeared in the journal Monatshefte fur Mathematik und Physik, volume 38, pages 173 to 198. The manuscript was received in November 1930 and printed the following year. The source cited here is the scan of the original German paper held at the Internet Archive.
Godel’s two incompleteness theorems answered, in the negative, the hope that David Hilbert had set out as his second Paris problem of 1900. The first theorem shows that any consistent formal system rich enough to express ordinary arithmetic must contain statements that are true but cannot be proved within the system. Godel built such a statement by encoding logical formulas as numbers, a technique now called Godel numbering, and then constructing a sentence that in effect says of itself “this statement is not provable.” If the system could prove it, the system would be inconsistent; if it cannot, the statement is true and yet unprovable. The second theorem goes further: no such system can prove its own consistency.
These results were aimed squarely at the great formal systems of the day, above all the one in Whitehead and Russell’s Principia Mathematica, which is named in Godel’s title. Hilbert had wanted a proof that the axioms of arithmetic could never lead to a contradiction, demonstrated by safe finite means from inside mathematics itself. Godel showed that this is impossible. Completeness and a self-contained consistency proof cannot both be had.
For the history of computing, the importance is that incompleteness made the limits of mechanical reasoning a precise mathematical subject rather than a matter of philosophy. The encoding tricks and the careful treatment of what a formal system can and cannot derive fed directly into the 1936 work of Alonzo Church and Alan Turing, who turned the question into one about computation and proved that no general procedure can decide every mathematical statement. Godel’s theorems are the hinge between Hilbert’s program and the birth of the theory of computation.