01Overview
In 1928 Hilbert posed the Entscheidungsproblem: is there an algorithm that decides whether any first-order statement is provable? He believed mathematics could be fully formalised, and that the formalisation could itself be proved consistent.
In 1931 Gödel encoded “this statement is unprovable” as an arithmetic sentence: every symbol, formula and proof received a unique number, so the system could talk about itself. Two theorems followed: any consistent system containing arithmetic has undecidable statements, and no such system can prove its own consistency. This was not only an earthquake in logic; it directly pushed Turing to redefine what a mechanical procedure is.
02History
- 1928
Hilbert poses the Entscheidungsproblem
He asks for a decision procedure for predicate logic.
- 1931
The incompleteness theorems
Self-reference and coding expose the intrinsic limits of formal systems.
- 1936
Turing defines computability
The Turing machine reformulates 'algorithm' and proves the halting problem undecidable.
- 1953
Rice's theorem
Every non-trivial semantic property of programs is undecidable.
03Core concepts
Formal system
Symbols, axioms and inference rules, forming proofs a machine can check.
Gödel numbering
Maps symbols and proofs to natural numbers so the system can talk about itself.
Self-reference
Constructing a statement that points at itself is the core trick of the proof.
04Hands-on
Do it once — it beats reading it ten times
Hand-encode the formula 0=0 as a Gödel number, walking through symbol → number → formula number
05Self-check
Say it in your own words first, then open the answer. Whatever you cannot explain is what to review next.
Can you explain "Formal system"?
Symbols, axioms and inference rules, forming proofs a machine can check.
Can you explain "Gödel numbering"?
Maps symbols and proofs to natural numbers so the system can talk about itself.
Can you explain "Self-reference"?
Constructing a statement that points at itself is the core trick of the proof.
What problem did it solve, and why was there nothing better at the time?
Go back to the history section: how was this done before, and what did it cost?
If you had to build it today, how would you break it down?
Use the hands-on task above: write a plan of at most three steps before you start.
06Key people
Kurt Gödel
1906 – 1978
Author of the incompleteness theorems and of a rotating-universe solution.
David Hilbert
1862 – 1943
Set out the formalist programme and its 23 problems.
07Further reading
- On Formally Undecidable Propositions of Principia Mathematica and Related Systems
- Gödel, Escher, Bach