Incompleteness
Can a system prove its own consistency?
Mathematics spent the early twentieth century trying to put itself on a footing that could not fail. The attempt produced a theorem saying the attempt cannot succeed — and a great deal of nonsense has been written about what that theorem means, so this subject proves it and then says carefully what it does not show.
Formal systems
What if the rules are the object of study?
Mathematics as a game with marks on paper
Strip away meaning and a proof becomes a sequence of symbol manipulations. That is a loss until you realise it makes proof itself something you can prove things about.
What a system can say about numbers
Peano arithmetic is strong enough to be interesting and weak enough to be analysed. The document establishes exactly how much it can express.
Gödel numbering
Can a theory talk about itself?
Turning statements into numbers
Encode every formula as a number and arithmetic becomes capable of discussing its own proofs. The film does the encoding on a short formula, by hand.
The two theorems
What exactly did Gödel prove, and what did he not?
This sentence is not provable
The diagonal lemma builds a statement asserting its own unprovability, and then the argument is short. The film stops before the consequences.
What the theorems are not about
Gödel's results have been used to argue for things they do not touch. The document separates the theorem from its folklore, and is deliberately careful.
Computability
Is there a problem no procedure can settle?
Incompleteness, as one volume
Every document in this subject is a chapter of the same book, compiled from one source with live cross-references and continuous numbering. Download the whole thing, or take chapters as you go — the page numbers and theorem references agree either way.
Download Volume XIII ↓