Mathematical Logic
★ ILLC DREAM · Oxford MFoCS · Cambridge Part IIIThe core of the cathedral. First-order logic is the skeleton of mathematics — every theorem, every proof, every definition rests on the syntax and semantics built in track one. From there, six tracks walk the outer limits of what can be proven: the Henkin construction, Gödel's abyss, the arithmetic of the infinite, games between structures, proofs as programs, and the arrow-language that unifies it all. This is not optional. This is the foundation.
Track 1 — FOL & Incompleteness
Enderton, A Mathematical Introduction to Logic (2nd ed., 2001) → Smullyan, Gödel's Incompleteness Theorems (1992). Read Sipser Ch. 4 in parallel — undecidability is incompleteness in disguise.
Track 2 — Modal & Epistemic
★ priorityBlackburn, de Rijke & Venema, Modal Logic (2001) → Fagin, Halpern, Moses & Vardi, Reasoning About Knowledge (1995) → van Ditmarsch, van der Hoek & Kooi, Dynamic Epistemic Logic (2008). Ends in a DEL paper formalizing one turn of the agent.
Track 3 — Set Theory
Enderton, Elements of Set Theory (1977). The diagonal argument here is the same blade Gödel used. Lindenbaum's lemma in Track 1 quietly used Zorn — now you earn it.
Track 4 — Model Theory
Marker, Model Theory: An Introduction (Springer GTM 217, 2002). Games between Spoiler and Duplicator make the limits of first-order logic concrete — and mirror the bisimulation games of Track 2.
Track 5 — Proof Theory
do lastTroelstra & Schwichtenberg, Basic Proof Theory (2nd ed., 2000). The hardest track. The Hauptsatz proof is long — five to ten pages of vault LaTeX — and beautiful.
Track 6 — Category Theory
optional · powerfulMac Lane, Categories for the Working Mathematician (2nd ed., 1998) · Riehl, Category Theory in Context (2016). Free ⊣ Forgetful explains half of modern mathematics; the other half is a limit.