Textbook of AI

Gödel's incompleteness theorems, proved by Kurt Gödel in 1931 in his paper Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I, are two of the most celebrated results in mathematical logic.

The first incompleteness theorem states that any consistent formal system F that is rich enough to express elementary arithmetic contains true statements that cannot be proved within F. Gödel's proof constructs an explicit such statement, informally, "this sentence is not provable in F", using Gödel numbering to encode formulas as natural numbers, so that statements about provability become statements about arithmetic and hence expressible inside F itself.

The second incompleteness theorem strengthens this: a sufficiently rich consistent system F cannot prove its own consistency. The hope at the heart of Hilbert's programme, that mathematics could be set on a finite, complete, provably-consistent foundation, was therefore unattainable.

The theorems shaped twentieth-century logic and the philosophy of mathematics. Their relevance to AI is direct: Roger Penrose has argued that Gödel's theorems imply human mathematical insight cannot be captured by any algorithm, an argument vigorously contested by AI researchers including Hilary Putnam and Marvin Minsky. The Gödel-numbering technique itself anticipated the universal-machine constructions of Turing and Church and is the conceptual ancestor of every interpreter, every reflection mechanism, and every self-reference in computer science.