On Formally Undecidable Propositions of Principia Mathematica and Related Systems

The paper contains Gödel's incompleteness theorems, now fundamental results in logic that have many implications for consistency proofs in mathematics.

The main results established are Gödel's first and second incompleteness theorems, which have had an enormous impact on the field of mathematical logic.

Gödel showed that the classical paradoxes of self-reference, such as "This statement is false", can be recast as self-referential formal sentences of arithmetic.

The fact that such self-reference can be expressed within arithmetic was not known until Gödel's paper appeared; independent work of Alfred Tarski on his indefinability theorem was conducted around the same time but not published until 1936.

In the preface to the volume van Heijenoort noted that Gödel was one of four authors who had personally read and approved the translations of his works.

Between them they "exchanged a total of seventy letters and met twice in Gödel's office in order to resolve questions concerning subtleties in the meanings and usage of German and English words."

This appears as On Undecidable Propositions of Formal Mathematical Systems (Davis 1965:39ff) and represents the lectures as transcribed by Stephen Kleene and J. Barkley Rosser while Gödel delivered them at the Institute for Advanced Study in Princeton, New Jersey in 1934.

This version is also notable because in it Gödel first describes the Herbrand suggestion that gave rise to the (general, i.e. Herbrand–Gödel) form of recursion.