Gödel's incompleteness theorems
In plain wordsTwo famous results from 1931 showing that any consistent set of rules for doing arithmetic leaves some true statements unprovable, and cannot prove that it is itself free of contradictions.
A pair of results in mathematical logic, published by Kurt Gödel in 1931, that limit what formal proof can achieve. The first states that any consistent, effectively axiomatized formal system able to express elementary arithmetic is incomplete: some sentence of its language can be neither proved nor refuted within it. Gödel built such a sentence by encoding formulas and proofs as numbers (Gödel numbering), so that the system can express a statement asserting, in effect, its own unprovability. The second states that such a system cannot prove its own consistency. With Alan TuringAlan Turing, prop. n.: A British mathematician who worked out what computers can do in principle, helped break German codes in the Second World War, and proposed the best-known test of machine intelligence.'s related proof that the halting problem is undecidable (1936), the theorems set limits on what any algorithmTuring machine, n.: An imaginary, extremely simple computer — a read-write head moving along an endless tape — that Alan Turing used in 1936 to define exactly what can be computed at all. or proof system can establish. In AI they are invoked in the Lucas–Penrose argumentLucas–Penrose argument, n.: An argument that human minds cannot be computers because, using a famous result in logic, people can see that certain statements are true that no fixed computer program could prove. that minds are not machines; in the Löbian obstacle, a difficulty for agents that must trust proofs produced by their own successors; and in Gödel machinesGödel machine, n.: A purely theoretical design, proposed by Jürgen Schmidhuber, for a program allowed to change anything about itself, including how it learns, but only once it has proved that the change is an improvement., self-improving programs that rewrite themselves only after proving a change beneficial.
The verifier's logic cannot prove its own consistency; by the second incompleteness theorem, that assurance must come from a stronger system.
Origin
Announced by Kurt Gödel at a conference in Königsberg in September 1930 and published in 1931 in Monatshefte für Mathematik und Physik as 'On Formally Undecidable Propositions of Principia Mathematica and Related Systems I'. The results ended David Hilbert's hope of proving mathematics consistent by finitary means; Alan Turing discussed them as 'the mathematical objection' to thinking machines in 1950.
Usage note
Often overstated: the theorems concern formal systems of a particular kind, not knowledge in general, and a stronger system can prove the Gödel sentence of a weaker one. Most logicians and philosophers reject the inference from incompleteness to the conclusion that human thought is non-mechanical.
Related
- Lucas–Penrose argumentLucas–Penrose argument, n.: An argument that human minds cannot be computers because, using a famous result in logic, people can see that certain statements are true that no fixed computer program could prove.
- Turing machineTuring machine, n.: An imaginary, extremely simple computer — a read-write head moving along an endless tape — that Alan Turing used in 1936 to define exactly what can be computed at all.
- Gödel machineGödel machine, n.: A purely theoretical design, proposed by Jürgen Schmidhuber, for a program allowed to change anything about itself, including how it learns, but only once it has proved that the change is an improvement.
- formal verificationformal verification, n.: Using mathematics, not just testing, to prove that a computer system always behaves as specified — for example, that a chip never adds wrongly or that a program can never crash in a particular way.
- Computing Machinery and IntelligenceComputing Machinery and Intelligence, prop. n.: Alan Turing's 1950 essay asking whether machines can think. It proposed a conversation test in place of that question, answered objections to thinking machines and suggested that machines might learn like children.
- embedded agencyembedded agency, n.: The puzzle of how an agent should reason when it is itself part of the world it is trying to understand and change, rather than standing outside it.
Sources
- Gödel, K. (1931). Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik 38.
- Nagel, E. & Newman, J. R. (1958). Gödel's Proof. New York University Press.