Best Books on Godel's Incompleteness Theorems, in Order
Two results, endlessly misquoted. This path establishes what Godel actually proved before letting you near anything that invokes him, then teaches the logic the proofs assume, then works through the proofs themselves in full. The middle stage is the corrective one: more nonsense is written about incompleteness than about any other theorem in mathematics, and the books that say so are worth reading before the technical ones. By the end you should be able to state both theorems precisely, follow the arithmetisation of syntax, and explain why the second theorem is the harder and more consequential of the two.
What the theorems say
BeginnerState both incompleteness theorems accurately and understand the sketch of the proof, with no formal logic assumed
▸ Study plan for this stage
Pace: 3 to 4 weeks, about 710 pages, and all three are books for the general reader — no formal logic is assumed anywhere in this stage. Nagel and Newman's Godel's Proof is 104 pages and should be read twice: once now and once after stage four, because it is compressed enough to reward a second pass. Rebe
- State the first theorem carefully: any consistent formal system strong enough to express elementary arithmetic contains a true sentence it cannot prove. The qualifications are not decoration — drop any one and the theorem is false.
- The second theorem: such a system cannot prove its own consistency. It is the harder result and the more consequential one, and most popular accounts skate over it.
- The proof strategy in outline: encode statements about the system as statements about numbers, then build a sentence that says of itself that it is unprovable.
- Effectively axiomatised, consistent, and sufficiently strong are three separate conditions. Knowing which one each abuse of the theorem violates is most of what stages one and two are for.
- Nagel and Newman's hundred pages remain the best short account of the first theorem for a reader with no logic at all, and it is deliberately silent on the biography and philosophy.
- Goldstein supplies what they omit: Vienna Circle positivism, Godel's own Platonism, and the fact that he took his theorem to support very nearly the opposite of what the logical positivists around him wanted from it.
- Budiansky is optional if you only want the mathematics, but he corrects the myth-making that Goldstein's book, being partly a philosophical essay, does not set out to address.
- Godel's Platonism is a philosophical position he held, not a consequence of his theorems. Keeping the two apart is a habit worth forming immediately.
- State both incompleteness theorems precisely, with every hypothesis. Then say what each hypothesis is doing.
- What does 'true but unprovable' mean, and true in what? A precise answer to this disposes of a large fraction of the nonsense in stage two.
- Why is the second theorem harder to prove than the first, given that it seems to follow from it?
- What did Godel himself think his theorems showed about mathematics and about the mind, and on what grounds?
- Where do Goldstein and Budiansky disagree about Godel, and is the disagreement about facts or about emphasis?
- After Nagel and Newman, write out the construction of the Godel sentence in your own words on one side of paper, without looking. Keep it; you will compare it against Peter Smith's formal construction in stage four and the differences will be instructive.
- Write both theorems on a card with all hypotheses. Every time you meet a claim about incompleteness for the rest of this path, check it against the card before evaluating it.
- List every informal analogy Nagel and Newman use — the map, the mirror, self-reference in ordinary language — and mark for each one where it will break down. Doing this now inoculates you against the analogies in Hofstadter.
- Using Goldstein and Budiansky together, write a paragraph on what the Vienna Circle wanted from foundations of mathematics and why Godel's result disappointed them. The philosophical stake is what makes the theorem famous rather than merely important.
Next up: You now know what the theorems claim; the next stage is the corrective, because more nonsense is written about incompleteness than about any other theorem in mathematics.
Nagel and Newman's hundred-page classic, still the best short account of the first theorem for a reader with no logic. Read it first and re-read it after stage four; it is compressed enough that it rewards a second pass.
The biographical and philosophical setting — Vienna Circle positivism, Godel's Platonism, and why he thought his own theorem supported the opposite of what the logical positivists wanted. Read it second, for the context Nagel and Newman deliberately omit.
The fullest modern biography, and honest about the decline and the paranoia. Optional if you want only the mathematics, but it corrects the myth-making that Goldstein's book, being partly a philosophical essay, does not set out to address.
What the theorems do not say
IntermediateRecognise the standard abuses of incompleteness on sight, and understand the one serious philosophical argument built on it
▸ Study plan for this stage
Pace: 5 to 6 weeks, about 1,200 pages, but the distribution is extreme. Torkel Franzen's book — published as Godel's Theorem: An Incomplete Guide to Its Use and Abuse and catalogued here under the short title — is 172 pages and is the only genuinely essential item in the stage; it is written for a general
- The standard abuses fall into recognisable families: theological arguments, postmodern appeals to undecidability, claims about physics or economics, and the Lucas-Penrose argument that minds are not machines.
- Most abuses fail on one of three things — the system is not effectively axiomatised, not strong enough for arithmetic, or not a formal system at all.
- Franzen works the misuses one at a time and is rigorous rather than merely dismissive: he takes the serious versions seriously and shows exactly where they break.
- The Lucas-Penrose argument is the one philosophically serious construction built on the theorems, and it remains genuinely disputed rather than settled — Franzen sets out the objections without pretending the debate closed.
- Smullyan's knights, knaves and self-referential reasoners are a route into the second theorem: a reasoner who believes in his own consistency turns out to be inconsistent, which is Lob's theorem in disguise.
- Forever Undecided is also the gentlest possible introduction to provability logic, which is the whole subject of the last stage on this path.
- Godel, Escher, Bach made incompleteness famous and is the source of a good many of the claims Franzen spends his book refuting, which is precisely why the path puts it after the corrective.
- Hofstadter's analogies between formal systems, canons and self-copying structures are a book-length argument about mind, not a proof of anything about it. Enjoy them while keeping the mathematics and the speculation separate.
- Take three claims of the form 'Godel showed that...' from ordinary reading and locate the exact page in Franzen that addresses each. Which of the three conditions does each violate?
- What is the Lucas-Penrose argument, precisely, and what is the strongest objection to it?
- Why does a reasoner who believes in his own consistency end up inconsistent, in Smullyan's terms?
- Which specific claims in Godel, Escher, Bach does Franzen contradict, and is Hofstadter making a mathematical claim or an analogical one in each case?
- Does incompleteness say anything at all about the limits of human knowledge? Give the careful answer, not the popular one.
- Collect five real invocations of Godel from books, articles or talks you have encountered, and for each one write which hypothesis it violates. Franzen supplies the tools; the collection has to be yours to be useful.
- Work Smullyan's chapters on reasoners of type 4 and the Lob's theorem puzzles all the way through, doing the puzzles rather than reading the solutions. This is the only place on the path where the second theorem is genuinely easy.
- In Godel, Escher, Bach, read the chapters on the MIU system and the Typographical Number Theory dialogues and check Hofstadter's informal proof sketch against Nagel and Newman's. Note the two places where his exposition is doing something theirs is not.
- Write a one-page refutation, in your own words and citing the relevant hypothesis, of the strongest bad Godel argument you can construct yourself. Building it before demolishing it is the exercise.
Next up: You can now tell a use from an abuse informally; the next stage supplies the logic that lets you check the proofs themselves rather than taking them on report.
Published as Godel's Theorem: An Incomplete Guide to Its Use and Abuse and catalogued under the short title. The indispensable corrective — Franzen works through the postmodern, theological and Lucas-Penrose misuses one at a time, and is rigorous rather than merely dismissive.
Smullyan's puzzle route to the second theorem, via knights, knaves and reasoners who believe their own consistency. The most painless way into the self-reference that stage four handles formally, and it is genuinely funny.
The book that made incompleteness famous, and the source of a great many claims Franzen spends his own book refuting. Read it here, after the corrective, so you can enjoy the analogies while keeping the mathematics and the speculation separate.
The logic the proofs assume
IntermediateWork comfortably with first-order logic, formal systems, recursive functions and the completeness theorem — everything the proofs take for granted
▸ Study plan for this stage
Pace: 16 to 20 weeks, and by far the longest stage — these are three genuine mathematics textbooks and the work is in the exercises, not the page count. Boolos, Burgess and Jeffrey's Computability and Logic is 304 pages and the right starting point: computability first, then logic, then incompleteness as
- First-order logic: syntax, structures, satisfaction, and the difference between a sentence being true in a structure and being derivable in a system.
- The completeness theorem — every logically valid sentence is provable — which is Godel's other famous result and is routinely confused with incompleteness. Getting the two apart is a prerequisite for everything after.
- Computability: Turing machines or recursive functions, the Church-Turing thesis, and decidable versus effectively enumerable sets.
- Why recursive function theory comes first: arithmetisation of syntax is possible because provability is an effectively enumerable relation on numbers, and that is a computability fact.
- Representability — the fact that every recursive function can be defined inside arithmetic — is the technical heart of the whole business, and the place where the proofs actually get hard.
- Robinson arithmetic and Peano arithmetic, and how little strength is actually needed for the first theorem to bite.
- The compactness and Lowenheim-Skolem theorems, which Enderton does properly and which set the context in which incompleteness is surprising.
- Shoenfield's role here is as a reference, not a course: use it to check a statement, not to learn one.
- State the completeness theorem and the first incompleteness theorem side by side and explain precisely why they are compatible.
- Prove that the set of theorems of an effectively axiomatised theory is effectively enumerable.
- What does it mean for a function to be representable in a theory, and why does representability rather than mere definability matter?
- How weak can a theory be and still be subject to the first incompleteness theorem?
- State the Lowenheim-Skolem theorem and explain what is paradoxical about it and why the paradox dissolves.
- What is the difference between a theory being complete and a logic being complete?
- Work the exercises in Boolos, Burgess and Jeffrey's chapters on recursive functions and on representability in full. These two chapters are the actual prerequisite for stage four; the rest of the book can be read more lightly.
- Prove the completeness theorem following Enderton's Henkin construction, writing out the term model yourself rather than reading the construction through.
- Show that the halting problem is undecidable, then write a paragraph connecting that proof to the diagonal construction you sketched in stage one. They are the same move.
- Take a short arithmetical formula and check, term by term, that Boolos's representability argument applies to a specific simple recursive function such as addition or the predecessor function.
- Look up one theorem you have just proved in Shoenfield and compare his statement with the one you worked from. The compression is a fair warning about what a graduate reference is for.
Next up: With computability, first-order logic and representability in hand, the proofs of both theorems are finally readable line by line.
Boolos, Burgess and Jeffrey is the standard bridge: computability first, then logic, then incompleteness as the payoff. Start here rather than with a pure logic text, because recursive function theory is what makes arithmetisation possible.
The cleanest treatment of first-order logic, soundness and completeness. Read it alongside or after Boolos when you want the model theory done properly rather than briskly.
The graduate reference — terse, complete, and the book the others cite. Do not start here; come to it when you want a statement of the results with nothing left informal.
The proofs in full
BeginnerFollow the arithmetisation of syntax, the diagonal lemma, and both theorems line by line, including the derivability conditions
▸ Study plan for this stage
Pace: 12 to 16 weeks, about 960 pages, and the stage that depends most heavily on stage three being done properly. Peter Smith's An Introduction to Godel's Theorems is 376 pages and is the central book of the path: a full modern treatment that builds Robinson arithmetic and the representability results ca
- Arithmetisation of syntax: assigning numbers to symbols, formulas and proofs so that syntactic relations become arithmetical ones.
- The diagonal lemma, which produces for any formula a sentence asserting that the formula applies to its own Godel number. This is the technical engine of both theorems.
- The Godel sentence itself, and why its truth follows from the system's consistency without being provable in it.
- Rosser's improvement, which weakens the hypothesis from omega-consistency to plain consistency, and why Godel's original argument needed the stronger assumption.
- The Hilbert-Bernays-Lob derivability conditions, which are what actually make the second theorem work and which most popular accounts omit entirely.
- Smullyan's abstract treatment of self-reference generalises the results well past Godel's original setting, which is what makes it a genuinely different second reading rather than a shorter one.
- Godel's 1931 paper had to build its machinery from nothing, and reading it after a modern proof shows how much of the standard presentation is later tidying by other people.
- Turing's 1936 paper, also in the Davis collection, arrives at an equivalent limitation from computability, which is the connection stage three was preparing.
- Prove the diagonal lemma. Then state exactly which properties of the Godel numbering it uses.
- Why does the first theorem need omega-consistency in Godel's original form, and how does Rosser's sentence avoid it?
- State the three derivability conditions and show how the second theorem follows from them.
- Which step of the proof of the second theorem is the one that is hard to verify in detail, and why do most textbooks decline to do it?
- How does Smullyan's abstract framework generalise the results, and what does the generalisation buy?
- Reading Godel's 1931 paper, which parts of the argument does he prove that a modern text assumes, and which does he assume that a modern text proves?
- Carry out the Godel numbering of a short formula by hand using Smith's own scheme, then compute the number for a two-line proof. Doing this once, painfully, is the only way arithmetisation stops being a slogan.
- Prove both theorems from Smith's development without looking, then compare your proof of the second with his. The gap will be in the derivability conditions, which is exactly where it should be.
- Reread the informal construction you wrote in stage one and mark every place where the formal proof does something your version glossed over. Keeping both versions is the single most useful artefact this path produces.
- Work through Smullyan's abstract self-reference chapter and identify which of Smith's concrete lemmas each of his abstract results specialises to.
- Read Godel's 1931 paper in the Davis collection with Smith open beside it and map each of Godel's forty-six definitions to its modern counterpart. Not all of them have one.
Next up: With both proofs verified in detail, incompleteness stops being an endpoint and becomes the start of a research programme.
The best modern full treatment for a reader who has done stage three — Smith builds Robinson arithmetic and the representability results carefully, then proves both theorems and discusses what they mean. This is the central book of the path.
Smullyan's austere Oxford Logic Guide, notable for its abstract treatment of self-reference and for generalising the results well past Godel's original setting. Read it after Smith as the second, sharper pass.
Davis's collection of the primary papers — Godel 1931 alongside Church, Turing, Rosser and Kleene. Once you have followed a modern proof, read the original and see how much of the machinery Godel had to build from nothing.
What incompleteness became
BeginnerSee the theorems as the start of a research programme — provability logic and the fine structure of incompleteness — rather than as a terminus
▸ Study plan for this stage
Pace: 10 to 14 weeks, about 420 pages, and both books are specialist research monographs rather than courses — the page counts are misleading and the reading rate will be very slow. George Boolos's The Logic of Provability is 275 pages and assumes the second theorem and its derivability conditions cold, p
- Provability logic treats 'is provable in the system' as a modal operator, which converts the derivability conditions into axioms of a modal system.
- GL, the Godel-Lob system, is that modal logic, and Lob's theorem is its characteristic axiom. The derivability conditions stop looking technical and start looking inevitable.
- Solovay's arithmetical completeness theorem — GL proves exactly the modal principles that hold for provability in Peano arithmetic — is the result that makes the whole subject respectable.
- Lob's theorem itself: if a system proves that provability of a sentence implies the sentence, then it proves the sentence. It is a strengthening of the second theorem and much stranger.
- Interpretability between theories, which gives a way of comparing the strength of systems and is one of the organising notions of Lindstrom's book.
- Degrees of incompleteness and the fine structure of the phenomenon: incompleteness is not a single fact but a landscape with structure in it.
- Reflection principles, which formalise 'this system is sound' inside the system and produce hierarchies of extensions.
- The point of the stage: incompleteness is a live area of mathematical logic, not a settled curiosity from 1931.
- State Lob's theorem and derive the second incompleteness theorem from it.
- What are the axioms of GL, and how does each correspond to a derivability condition?
- What does Solovay's completeness theorem actually claim, and why is it surprising?
- What does it mean for one theory to be interpretable in another, and how does interpretability give a notion of relative strength?
- How does a reflection principle differ from a consistency statement, and what does adding one to a theory get you?
- Having read the whole path, restate both incompleteness theorems in one paragraph for a reader who knows first-order logic. Compare it with the card you wrote in stage one.
- Derive Lob's theorem in GL from the axioms, then derive it arithmetically from the derivability conditions, and set the two derivations side by side. The modal proof is three lines and the arithmetical one is not, which is the argument for provability logic in a single exercise.
- Work Boolos's exercises on Kripke models for GL, and construct a model demonstrating that a specific modal formula is not a theorem.
- Return to Smullyan's Forever Undecided from stage two and identify which of its puzzles are now recognisable as GL theorems. Almost all of them are, which is what the puzzle book was for.
- Using Lindstrom, write a one-page summary of what is known about degrees of interpretability, at whatever level of detail you can honestly support. The exercise is partly a measurement of how far the path has taken you.
- Reread Nagel and Newman, as stage one instructed. A hundred pages that took a week at the start should now take an afternoon, and the places where you disagree with their exposition are the record of everything in between.
Next up: This is the last stage: you can state both theorems precisely, prove them, recognise their misuse, and read the research literature that grew out of them.
Provability as a modal operator, with Lob's theorem at the centre. The single most elegant thing to read after the second incompleteness theorem, and it makes the derivability conditions feel inevitable rather than technical.
The specialist's survey of what happened next — interpretability, degrees of incompleteness, the fine structure of the phenomenon. A hard closing book, and the clearest evidence that incompleteness is a live field rather than a settled curiosity.
Discussion
Keep reading
Paths that share books, cover the same subject, or open a related topic.
