First-order logic is the skeleton of mathematics. Every theorem, every proof, every definition rests on the syntax and semantics you are about to build. This is not optional. This is the foundation.
You will prove the completeness theorem. You will walk the Henkin construction. You will stare into the abyss of consistency and validity and understand why they coincide. This is the most important proof in logic — and by December, you will own it.
Nine books carry the entire logic curriculum. Each one is read in exact chapter ranges, never skimmed — every definition transcribed, every starred theorem proved into the Vault in full LaTeX. The only prerequisites are proof literacy (induction, contradiction, contraposition) and the discipline to read slowly. Tracks 1–3 open the sequence; Track 5 waits until they are done; Tracks 4 and 6 run alongside.
Ch. 2.1–2.7: syntax, structures, soundness, and the Henkin completeness proof.
Gödel numbering, the diagonal lemma, both incompleteness theorems. Sipser Ch. 4 in parallel.
Ch. 1–2: Kripke frames, frame correspondence, canonical models, bisimulation.
Ch. 1–3: knowledge, belief, common knowledge, the muddy children.
Public announcements, action models, product update — the frontier.
Ch. 1–5: ZFC, ordinals, cardinals, and the Axiom of Choice.
Ch. 1–3: elementary equivalence, types, quantifier elimination, EF games.
Ch. 2–4: sequent calculus, cut elimination, normalization, Curry–Howard.
Ch. 1–2 of each: categories, functors, universal properties. Riehl is the gentler door.
You will prove that logic captures truth — and then that it can never capture all of it. From the Henkin construction to Gödel's diagonal, this is the arc every logician walks.
Eight weeks, one destination: the Henkin proof of completeness. Everything before it — syntax, structures, satisfaction, soundness — is built so that the final construction has ground to stand on. By week 8 you will hold, in your own LaTeX, the theorem that provability and semantic consequence coincide.
A first-order language is an alphabet — variables, constants, function symbols, predicate symbols — and two recursively generated classes built over it: terms, then atomic and well-formed formulas. The technical heart of these sections is the machinery of free and bound variables and of substitution, because a single variable-capture mistake silently invalidates every later theorem about derivations. This is also where you acquire the idiom you will use all semester: proof by induction on the structure of formulas, licensed by unique readability. Nothing here is decorative; the Henkin construction in week 7 manipulates exactly these objects.
A structure M = ⟨D, I⟩ supplies a nonempty domain and an interpretation of every nonlogical symbol; an assignment s: Var → D then makes truth assignment-relative, written M ⊨ φ[s]. Tarski's satisfaction conditions define this relation by recursion on φ — one clause per connective and quantifier — and everything semantic in the whole track (models, validity, the consequence relation Γ ⊨ φ) is defined from it. The quietly crucial theorem is that satisfaction depends only on the values s gives the free variables of φ, which is what lets sentences have truth values at all. This relation is one half of the completeness theorem; the proof system of §2.6 is the other.
Enderton's Hilbert-style calculus has a small stock of logical axioms, modus ponens, and generalization; a derivation is a finite sequence justified line by line, and Γ ⊢ φ means such a sequence exists. The soundness theorem — if Γ ⊢ φ then Γ ⊨ φ — says the calculus never proves anything false in a model of Γ, and its proof is your first serious induction on derivations: verify each axiom is valid, then check that both rules preserve consequence. Alongside it you prove the workhorse lemmas — the deduction theorem above all — that the completeness proof will lean on constantly. Soundness is the easy direction; internalize its shape now, because completeness is its mirror image run in reverse.
The argument runs through five movements, and you must own all of them. First, reduce completeness to: every consistent set is satisfiable. Second, Lindenbaum's lemma: every consistent Γ extends to a maximal consistent Δ. Third, expand the language with a Henkin witness constant cφ for each formula ∃x φ, adding the axioms ∃x φ → φ[cφ/x] while preserving consistency. Fourth, build the canonical model M whose domain is the (quotiented) set of closed terms, interpreting each symbol exactly as Δ dictates. Fifth, the truth lemma — M ⊨ φ ⇔ φ ∈ Δ, proved by induction on φ, with the witnesses carrying the existential case — from which completeness, Γ ⊨ φ ⟹ Γ ⊢ φ, falls out in three lines. The standard is absolute: the entire construction, reproduced closed-book.
One week to harvest what the Henkin construction planted. Compactness and Löwenheim–Skolem are the two great corollaries of completeness — and together they expose the strange, productive weakness of first-order logic: it cannot tell infinite cardinalities apart, and that weakness is precisely what makes model theory (Track 4) possible.
Compactness says Γ is satisfiable iff every finite subset of Γ is satisfiable — an infinite consistency claim reduced to finitely many checks. From completeness the proof is almost immediate: derivations are finite objects, so an inconsistency in Γ already lives in some finite fragment. The classic application is your first taste of non-standard mathematics: add a fresh constant c and the axioms c > 0, c > 1, c > 2, … to true arithmetic; every finite subset is satisfiable in ℕ, so the whole set has a model — one containing an "infinite" number. That model is not a curiosity; it is proof that first-order axioms can never pin ℕ down.
Downward LS says any satisfiable theory in a countable language has a countable model — visible already in the Henkin proof, whose canonical model is built from countably many terms. Upward LS says a theory with an infinite model has models of every infinite cardinality, proved by compactness applied to a theory padded with κ-many fresh constants forced to be pairwise distinct. Together they are the deep insight of the week: first-order logic cannot pin down cardinality. Sit with the Skolem paradox — a countable model of set theory that internally believes in uncountable sets — until it stops feeling like a contradiction and starts feeling like a precise statement about what "countable" means inside versus outside a model.
Week 8 proved that logic captures truth; these three weeks prove it can never capture all of it. The arc runs from a coding trick — formulas as numbers — through the diagonal lemma to the two theorems that ended Hilbert's program, with Turing's halting problem read in parallel as the same result wearing different clothes.
Assign every symbol, formula, and finite proof-sequence a unique natural number, computably and reversibly — that is the entire trick, and it must be done precisely, not gestured at. Once formulas are numbers, syntactic properties like "x codes a proof of y" become arithmetic relations, and the representability theorem shows every recursive function is representable by a formula of PA. The consequence is vertiginous: arithmetic can talk about its own proofs. Every step of the incompleteness argument stands on this scaffolding, so build it with your own hands — pick a scheme, code real formulas, verify decodability.
The diagonal lemma manufactures self-reference: for any formula ψ(x) there is a sentence δ such that T proves δ ↔ ψ(⌜δ⌝). Apply it to the negation of the provability predicate and you get the Gödel sentence G, which asserts "G is unprovable in T." If T ⊇ PA is consistent, T cannot prove G (a proof of G would make G false, hence provable-and-refutable); under Smullyan's careful hypotheses T cannot refute it either — so G is true but unprovable. Notice what the theorem does not say: not that truth is mystical, but that no single consistent formal system exhausts arithmetic truth. The vault standard: the full Smullyan-method proof, every step, closed-book.
Formalize the entire first-theorem argument inside T and it yields something stranger: T proves Con(T) → G, so if T could prove Con(T), it would prove G — which it cannot. Hence no consistent theory containing enough arithmetic proves its own consistency. The technical content lives in the Hilbert–Bernays derivability conditions, the three properties of the provability predicate that make the internalization go through; identify them and the proof is a page. This is where Hilbert's program — securing infinitary mathematics by finitary consistency proofs — collapses on its own terms.
Read the halting problem alongside Gödel and watch the same diagonal turn twice: Turing diagonalizes against machines, Gödel against proofs, and Cantor (Track 3) against enumerations — one argument, three costumes. The bridge is exact: if T were a complete consistent axiomatization of arithmetic, you could decide the halting problem by searching for proofs, so undecidability forces incompleteness. This is the seam where Track 1 touches the Theory of Computation track, and the week's essay stitches it shut.
Necessity, possibility, knowledge, belief. This is the ILLC's mother tongue — and the track that connects directly to your agent work.
Four weeks to make possible-worlds semantics second nature. The payoff structure is deliberate: Kripke models give you a playground, frame correspondence gives you the dictionary between axioms and geometry, canonical models replay the Henkin construction in modal dress, and bisimulation tells you exactly what modal logic can and cannot see.
Extend propositional logic with two operators — φ ::= p | ¬φ | φ ∧ φ | □φ | ◇φ — and interpret them over a Kripke frame (W, R): a set of worlds and an accessibility relation. A model (W, R, V) adds a valuation, and truth becomes local: M, w ⊨ □φ iff M, w′ ⊨ φ for every w′ ∈ R(w), with ◇ its existential dual. The move to evaluate formulas at worlds — rather than absolutely — is the single idea underneath everything in this track, from knowledge operators to public announcements. The standard translation into first-order logic (□ becomes a guarded ∀) is worth learning immediately: it situates modal logic inside FOL and sets up van Benthem's theorem.
Each famous axiom is a first-order condition on R wearing modal clothing: T (□φ → φ) corresponds to reflexivity, 4 (□φ → □□φ) to transitivity, B (φ → □◇φ) to symmetry, 5 (◇φ → □◇φ) to euclideanness — while K, □(φ→ψ) → (□φ→□ψ), holds on every frame. Every correspondence proof has two directions and you must own both: if the frame has the property, the axiom is valid — a direct semantic argument unwinding the truth clauses — and if the axiom is valid on the frame, the frame has the property — where you cunningly choose a valuation (typically V(p) = {v : wRv}) that forces the geometry to reveal itself. Stack the axioms and the systems appear: S4 = K+T+4 makes R a preorder; S5 = K+T+5 makes it an equivalence relation, which is why S5 will model knowledge in Phase 2.
Completeness for modal logics is the Henkin construction replayed: worlds of the canonical model are maximal consistent sets of formulas, and Δ R Δ′ holds iff every □φ ∈ Δ has φ ∈ Δ′. A modal Lindenbaum lemma supplies the worlds; the existence lemma shows every ◇φ ∈ Δ is witnessed by an accessible world; and the truth lemma — Mc, Δ ⊨ φ ⇔ φ ∈ Δ — closes the loop by induction on φ. Completeness for a specific system then reduces to a frame check: prove the canonical relation of S5 is an equivalence relation and S5-completeness falls out. Feel the rhyme with week 6–8 of Track 1 — it is the same proof-shape, and recognizing that shape is half of what this semester teaches.
A bisimulation is a relation between models satisfying three clauses — atomic harmony, forth, and back — and bisimilar worlds satisfy exactly the same modal formulas. It is the precise answer to "when do two models look the same to modal eyes," and building bisimulations (or proving none exists) is a skill you will drill on concrete diagrams. The crown is the van Benthem characterization: a first-order formula is equivalent to (the translation of) a modal one iff it is invariant under bisimulation — modal logic is exactly the bisimulation-invariant fragment of FOL. File this next to the Ehrenfeucht–Fraïssé games of Track 4; they are the same idea, played over different logics.
Now the boxes acquire meaning: □ becomes Kᵢ — "agent i knows" — and the frame conditions of Phase 1 become claims about rational minds. Four weeks take you from single-agent knowledge through belief, up to common knowledge and the muddy children, and out the far side into AGM belief revision — the formal theory of changing your mind, and the ancestor of your BRAIN agent's memory update.
Read Kᵢφ as "agent i knows φ" and interpret each agent's accessibility relation as indistinguishability: wRᵢv means that in world w, agent i cannot rule out being in v. The S5 axioms then become epistemology: factivity Kᵢφ → φ (what is known must be true — this is what separates knowledge from opinion), positive introspection Kᵢφ → KᵢKᵢφ, and the boldest, negative introspection ¬Kᵢφ → Kᵢ¬Kᵢφ — the agent knows what it does not know. Each corresponds, via Phase 1's dictionary, to Rᵢ being an equivalence relation, so multi-agent epistemic models are just worlds partitioned differently by different agents. Interrogate negative introspection honestly: it is the S5 axiom most often false of humans and most nearly true of well-designed database systems and agents.
Belief is knowledge with the safety rail removed: Bᵢφ is not factive, because agents can be wrong. Drop T, keep 4 and 5, and add D — ¬(Bᵢφ ∧ Bᵢ¬φ), the demand that beliefs at least be consistent — and you get KD45, whose frames are serial, transitive, and euclidean. The single missing axiom is the entire philosophy of the system: a KD45 agent is coherent and fully introspective yet possibly deluded, which is exactly the epistemic condition of any real agent acting on a model of the world. Build models where an agent believes falsehoods confidently, and study how knowledge and belief interact when both operators live in one system.
Everyone knowing φ is weak; common knowledge Cφ — everyone knows φ, and knows that everyone knows, and so on, all the way up — is what coordination actually requires. Formally C is a fixed point: Cφ ↔ φ ∧ K₁(Cφ) ∧ K₂(Cφ) ∧ … — an infinitary operator that escapes first-order logic, evaluated semantically by reachability along the union of all agents' relations. The classic proving ground is the muddy children puzzle: three children, at least one with mud on their forehead; the parent announces "at least one of you has mud"; the question "do you know whether you are muddy?" is asked repeatedly — and each round of silence is itself an announcement, shrinking the model, until after k rounds exactly the k muddy children know. The subtlety worth savoring: if k ≥ 2 the parent's announcement tells no child anything they could not see — what it creates is common knowledge, and that alone drives the deduction.
Epistemic logic describes belief at an instant; AGM asks how a rational agent should change beliefs when new information arrives. Three operations — expansion K+φ (add and close), contraction K−φ (retract φ minimally), revision K∗φ (accept φ, restoring consistency) — are governed by the AGM postulates: closure, success, inclusion, vacuity, consistency, and extensionality, with the deep pair linked by the Levi and Harper identities. The animating principle is minimal change: surrender as little as possible of what you believed. This is your BRAIN agent's memory update wearing formal dress — µ(M, s, a) → M′, the belief state after an action, is a revision operator, and in Phase 3 DEL will give the same idea a possible-worlds semantics.
The frontier. Epistemic logic freezes a moment of knowledge; DEL sets it in motion — announcements shrink models, actions transform them, and learning becomes a model operation. Three weeks: public announcements, then arbitrary action models, then the payoff — one full turn of your own agent, formalized.
[!φ]ψ reads "after φ is truthfully, publicly announced, ψ holds," and its semantics is surgery: announcing φ deletes every ¬φ-world, and ψ is evaluated in the smaller model M|φ. The miracle of PAL is that the dynamic operator is eliminable, via the reduction axioms: [!φ]p ↔ (φ → p) for atoms, [!φ]¬ψ ↔ (φ → ¬[!φ]ψ), [!φ](ψ ∧ χ) ↔ ([!φ]ψ ∧ [!φ]χ), and the crown jewel — [!φ]Kᵢψ ↔ (φ → Kᵢ[!φ]ψ) ★ MEMORIZE THIS — knowledge after the announcement equals conditional knowledge, before it, of the announcement's consequences. Each axiom is proved by unwinding the update semantics at a world, and together they translate PAL into plain epistemic logic, which is exactly how completeness is proved. Run the muddy children through PAL and watch each round of silence become a literal announcement deleting worlds: the puzzle solves itself in three updates. Then meet Moore sentences — p ∧ ¬Kp, true but unknowable, false after being announced — the proof that announcements do not simply "add" knowledge.
Public announcement is the simplest epistemic event; action models generalize to anything agents can partially observe — private messages, suspicions, whispers. An action model A is itself a Kripke structure whose points are possible events, each with a precondition, and whose relations encode what each agent can distinguish about what happened. The new state of the world is the product update M ⊗ A: pairs (w, a) with M, w ⊨ pre(a), with (w, a) Rᵢ (v, b) iff wRᵢv in M and aRᵢb in A — uncertainty about the world composes with uncertainty about the event. Public announcement falls out as the one-point action model, and sequences of actions compose. This is the general theory of how an epistemic state evolves under observation: every agent action is an action model.
Now spend the machinery. Formalize one turn of your BRAIN agent: the agent observes O (what it learns this turn), its belief state B updates by product update with the action model representing that observation, it reasons in the resulting model using Kᵢ and Bᵢ, and it acts on the routing decision the reasoning licenses. The memory update µ(M, s, a) → M′ from Phase 2 becomes literal: M′ = M ⊗ A(a, s), and AGM's minimal-change principle becomes a constraint on which action models are admissible. Two to three pages, definitions first, one fully worked turn, every step justified — this artifact is DEL doing real work, and it is the piece of the vault that belongs in a statement of purpose aimed at the ILLC.
The ground on which all of mathematics is quietly built — nine axioms, the infinite made precise, and the one proof that ties them together: Choice.
Everything in mathematics is officially a set, and these five weeks make you a citizen of that regime rather than a tourist. First the nine axioms, stated in first-order formulas and defended one by one; then the ordinals, which extend induction past the finite; then Cantor's diagonal, which cracks the infinite open into sizes.
ZFC is a first-order theory in the single relation symbol ∈, and each axiom answers a specific question: which sets are we entitled to assume exist, and what makes two of them equal? Learn each formula together with its motivation and its danger — Separation exists as a schema restricted to subsets precisely because unrestricted comprehension yields Russell's paradox; Replacement is what Zermelo's original system was missing; Foundation forbids ∈-descending chains and gives the cumulative hierarchy its floor. The nine, stated precisely:
An ordinal is a transitive set well-ordered by ∈ — a definition so economical that the number is the set of its predecessors: 0 = ∅, 1 = {∅}, 2 = {∅,{∅}}, and upward through the first infinite ordinal ω to ω+1, ω·2, ω², and beyond. The two engines of the theory are transfinite induction — prove ∀α P(α) by showing P holds at α whenever it holds below α, with successor and limit cases handled separately — and transfinite recursion, which legitimizes defining functions on the ordinals by their behavior on all earlier values. The recursion theorem's proof — existence and uniqueness via unions of coherent approximations — is a template you will reuse verbatim in the AC ⟺ Zorn proof of Phase 2, so learn it as a method, not a fact.
The cardinal |X| is the least ordinal equinumerous with X; ℵ₀ = |ℕ| is countability, ℵ₁ the first uncountable size. Cantor's theorem — |P(X)| > |X| for every set X — is three lines that changed mathematics: given any f: X → P(X), the diagonal set D = {x ∈ X : x ∉ f(x)} can be no f(x), so no surjection exists. It is the same diagonal you met in Gödel and Turing (Track 1, week 12), now in its original habitat, and it yields 2^ℵ₀ > ℵ₀ — the reals are uncountable — immediately. Cardinal arithmetic then turns out strangely flat below the power set: ℵ₀ + ℵ₀ = ℵ₀ and ℵ₀ · ℵ₀ = ℵ₀ (the pairing function), while the continuum hypothesis — is 2^ℵ₀ = ℵ₁? — is independent of ZFC (Gödel 1938, Cohen 1963): the axioms simply do not decide it.
One axiom, three faces, and the proof that they are the same face. The equivalence AC ⟺ Zorn ⟺ well-ordering is the centerpiece of the track — a single sustained argument powered by the transfinite recursion you built in Phase 1 — and around it, the strange moral landscape of an axiom that mathematics cannot live without and cannot quite look at directly.
The Axiom of Choice says every family of nonempty sets admits a choice function; Zorn's Lemma says a poset in which every chain has an upper bound contains a maximal element; the well-ordering theorem says every set can be well-ordered. On their faces these could not look less alike — one is about selection, one about maximality, one about order — and yet all three are equivalent over ZF. Before proving the equivalence, learn each statement precisely enough to catch the standard misstatements (Zorn needs every chain bounded, including the empty one), and warm up on the easy equivalences, like AC ⟺ every product of nonempty sets is nonempty.
The cycle is proved AC ⟹ Zorn ⟹ WO ⟹ AC, and the hard arrow is the first. The strategy is transfinite recursion: given a poset where every chain is bounded, use a choice function to define, by recursion on the ordinals, a strictly increasing chain — at each stage, choose a strict upper bound of what has been built so long as one exists. If the recursion never halted it would inject the entire class of ordinals into your poset, contradicting Replacement (via Hartogs' theorem there is always an ordinal too big to embed); so it halts, and where it halts sits a maximal element. Zorn ⟹ WO applies Zorn to the poset of partial well-orderings of X, ordered by end-extension, and shows a maximal one must exhaust X; WO ⟹ AC is the two-line dessert. The vault standard: the entire cycle, closed-book, with the recursion-and-halting argument in full detail — this is THE proof of the track.
Now trace where Choice already touched your semester and where it gets strange. Lindenbaum's lemma — the beating heart of the Henkin proof in Track 1 — is Zorn applied to consistent extensions; every vector space having a basis is Zorn applied to linearly independent sets; Hahn–Banach extends functionals by the same maximality move. But the same axiom yields the Banach–Tarski paradox: a sphere decomposed, by non-measurable pieces, into two spheres of the original size — "paradox" meaning not contradiction but the price of non-constructive selection. And the axiom's status is exactly as delicate as CH's: Gödel (1938) showed ZF cannot refute AC, Cohen (1963) showed ZF cannot prove it. Constructivists decline it; nearly all of modern mathematics silently spends it. The essay asks you to take a position and defend it.
The study of the relationship between formal languages and the structures that satisfy them — where logic becomes geometry, and games decide truth.
Model theory begins where Track 1 ended: completeness and compactness in hand, you now study what first-order sentences can and cannot distinguish. This phase builds the field's basic optics — elementary equivalence, types, and the two classification theorems (omitting types, Ryll-Nardzewski) that tell you how much a theory constrains its models.
M ≡ N means M and N satisfy exactly the same first-order sentences — indistinguishable to the language, however different they look from outside. The stronger relation M ≺ N, elementary embedding, demands that N agree with M on all formulas with parameters from M: substructure plus the Tarski–Vaught condition. The canonical example carries the whole idea: (ℚ,<) ≡ (ℝ,<) — a countable and an uncountable order that first-order logic cannot tell apart, because both are dense linear orders without endpoints; while (ℕ,<) ≢ (ℚ,<), separated by the sentence asserting a minimum exists. Elementary equivalence is coarser than isomorphism by exactly the width of Löwenheim–Skolem, and learning to feel that gap is what this phase is for.
A complete type p(x) over a theory (or over parameters in a model) is a maximal consistent set of formulas in the free variable x — the most detailed first-order description a single element could satisfy. An element realizing p is a witness to that description; a model omits p if no element does. Compactness guarantees every type is realized in some elementary extension, and saturated models are the maximalists that realize every type they consistently can. Work concrete cases until types feel like objects: over (ℚ,<) with parameters, types correspond to cuts in the order; the type of an infinite element over true arithmetic is your week-9 non-standard model, reborn as a definition.
Realizing types is easy — compactness does it wholesale; the delicate art is avoiding one. The omitting types theorem says that if a countable theory does not locally force a type p — no consistent formula implies all of p — then T has a countable model omitting p. The proof is a Henkin construction with a conscience: you build a maximal consistent, witness-complete set as in Track 1, but interleave extra steps ensuring, for each term, some formula of p fails of it — a finite-injury discipline that countability makes possible. It is the first theorem where you steer the Henkin machinery toward a model with prescribed properties rather than merely any model, and that skill is model theory in miniature.
A theory is ω-categorical when it has exactly one countable model up to isomorphism — the tightest grip a first-order theory can have on its countable models. Ryll-Nardzewski characterizes this grip exactly: a countable complete theory is ω-categorical iff for each n it has only finitely many n-types. The proof braids together everything in the phase — omitting types drives one direction, a back-and-forth argument the other — and the flagship example is again (ℚ,<): Cantor's back-and-forth shows any two countable dense linear orders without endpoints are isomorphic, so DLO is ω-categorical, and its types are correspondingly few. Categoricity, types, and quantifier elimination (Phase 2) are three gauges of the same tightness.
Quantifiers are where the difficulty of a theory hides — each ∃ is a search, each ∀ a promise over the whole domain. A theory that eliminates quantifiers has no hiding places left: every question reduces to a quantifier-free calculation, and decidability often follows. This phase teaches the definition, the engine (Tarski–Vaught), and one full elimination carried out by hand.
A theory T has quantifier elimination when every formula is T-equivalent to a quantifier-free formula in the same free variables. This is a statement about the definable sets: in a QE theory, everything definable is already definable without quantifiers, so the definable sets are exactly the combinatorially simple ones — finite unions of intervals for DLO, Boolean combinations of varieties for algebraically closed fields, semialgebraic sets for real closed fields. Peano arithmetic conspicuously does not eliminate quantifiers, and that failure is the model-theoretic shadow of Gödel: arithmetic's definable sets are wild enough to encode proof itself. The general method is always the same reduction: it suffices to eliminate a single ∃ from a conjunction of literals, because the full result follows by induction on formulas.
The Tarski–Vaught test says M ≺ N iff every existential formula with parameters in M that is true in N already has a witness inside M — elementarity reduced to a single quantifier's worth of checking. Its proof is an induction on formulas in which only the ∃ case has content, and that economy is why it appears everywhere: in the downward Löwenheim–Skolem proof (build a countable set closed under witnesses), in unions of elementary chains, and as the working criterion inside quantifier-elimination arguments. Learn it as the practical instrument it is — the thing you actually check when you need M ≺ N.
Now do it with your hands: prove that DLO — the theory of dense linear orders without endpoints, the theory of (ℚ,<) — eliminates quantifiers. By the reduction it suffices to treat ∃x θ where θ is a conjunction of literals in < and =, and the elimination is honest bookkeeping: split on the constraints relating x to the parameters, and observe that density and endpointlessness guarantee a witness exists iff the parameters satisfy a quantifier-free condition (every lower bound below every upper bound). Corollaries cascade: DLO is complete (so (ℚ,<) ≡ (ℝ,<) — this time by algorithm rather than by games), and with Cantor's back-and-forth, all countable models are isomorphic. This is why the theory of dense orders is so constrained: QE leaves it nowhere to hide structure.
QE is not only structural — it is algorithmic. If the elimination procedure is effective and the quantifier-free sentences are decidable, the whole theory is decidable: to decide a sentence, eliminate its quantifiers and evaluate what remains. So (ℚ,<) is decidable, and Tarski's QE for real closed fields makes the first-order theory of the reals — all of elementary geometry — decidable, one of the great positive results of logic. Set this against Track 1's negative pole: (ℕ,+,·) is undecidable even though its logic is complete, because it is the theory, not the calculus, that resists. The pairing of Tarski's ℝ and Gödel's ℕ is the sharpest lesson in the whole semester about where the boundary of the computable runs.
The last phase turns logic into a game you can win. Ehrenfeucht–Fraïssé games characterize first-order equivalence by strategy, so proving two structures alike — or provably different — becomes a matter of outplaying an adversary. It is the most tactile mathematics in the whole track, and it closes the loop with Track 2's bisimulation.
Two players face two structures M and N. In each of n rounds, Spoiler picks an element of either structure — trying to exhibit a difference — and Duplicator answers with an element of the other, trying to mirror it; after n rounds Duplicator wins if the chosen pairs form a partial isomorphism. The EF theorem is the exact dictionary: Duplicator has a winning strategy in the n-round game iff M ≡ₙ N — the structures agree on all sentences of quantifier rank ≤ n. The proof is a double induction on n, translating quantifiers into moves: each ∃ in a formula is a Spoiler move the formula survives, and Duplicator's strategy is a witness-choosing function. Quantifier rank as "number of rounds you can survive" is an image that will reorganize how you read every formula afterward.
The theorem converts equivalence proofs into strategy design. To prove (ℚ,<) ≡ (ℝ,<) yet again — the third proof this track — hand Duplicator the interval-preserving strategy: density guarantees a response inside every gap, for any number of rounds, so the structures agree on sentences of every rank. For inexpressibility, run the logic backward: if a property P were expressed by a sentence of rank n, Duplicator winning the n-round game between a structure with P and one without would be a contradiction — hence FOL cannot express "the domain is finite," nor "cardinality = ℵ₁," and the hand-waving of week 9 ("first-order logic cannot pin down cardinality") becomes a finished proof. Collect these into a small arsenal: each inexpressibility result is one well-chosen pair of structures plus one strategy.
Put the EF theorem beside Track 2's bisimulation and the symmetry is exact: EF games are the model-comparison game for first-order logic, bisimulation games the same for modal logic — Spoiler probes, Duplicator mirrors, and the logic's expressive power is precisely what survives the mirroring. The difference in the games (free element choice versus moves along accessibility relations) is the difference between the logics, and van Benthem's characterization sits at the junction: modal logic is the bisimulation-invariant fragment of FOL. Write the comparison down carefully — this unification, comparison-games-as-semantics, is a distinctly ILLC way of seeing, and it belongs in your dossier in your own words.
Where proofs become objects of study in their own right — and, through Curry–Howard, become programs. The hardest track. Its centerpiece is beautiful.
Nine weeks inside the anatomy of proof itself. The spine of the phase is Gentzen's Hauptsatz — the longest single proof of your semester, five to ten pages of disciplined induction — and its reward is Curry–Howard: the discovery that your proofs were programs all along. Trust the ordering: rules first, then the great elimination, then its consequences, then the computational reading.
A sequent Γ ⊢ Δ asserts: if everything in Γ is true, then something in Δ is true — and LK derives sequents from axioms φ ⊢ φ by rules that are startlingly symmetric. The structural rules (weakening, contraction, exchange) manage the contexts; the logical rules introduce each connective on the left or on the right — ∧-left: from Γ, φ, ψ ⊢ Δ infer Γ, φ∧ψ ⊢ Δ; ∧-right: from Γ ⊢ φ, Δ and Γ ⊢ ψ, Δ infer Γ ⊢ φ∧ψ, Δ — with parallel pairs for ∨, →, ¬ and quantifier rules guarded by eigenvariable conditions (the fresh-variable side conditions that make ∀-right and ∃-left honest). Then there is cut: from Γ ⊢ φ, Δ and Γ, φ ⊢ Δ infer Γ ⊢ Δ — the rule that lets a proof invent and discard a lemma φ. Cut is how mathematicians actually work; the Hauptsatz will show it is, in principle, never needed.
Every LK proof transforms into a cut-free proof. The proof is a double induction, and you must hold its two dimensions apart: the outer measure is the cut-rank — the complexity (degree) of the cut formula — and the inner measure is the level, the combined height of the derivations above the cut. Permutation lemmas handle the case where the cut formula is not principal in the last rule of a premise: the cut slides upward past that rule, level decreasing, rank untouched. Reduction lemmas handle the essential case, where the cut formula was just introduced on both sides: a cut on φ∧ψ becomes cuts on φ and ψ, a cut on ∀x φ becomes a cut on an instance — strictly smaller degree, and this is where contraction makes the bookkeeping genuinely hard. The induction on rank, with the induction on level nested inside, grinds every cut out of the proof. It is long; it is the most beautiful sustained induction in logic; and the vault demands all of it, five to ten pages, in your own hand.
Once cut is gone, inspect the surviving rules: each one only ever writes down subformulas of its conclusion. Hence the subformula property — every formula anywhere in a cut-free proof is a subformula of the end-sequent — so a cut-free proof of φ stays inside φ's own vocabulary: the syntax of the proof reveals its semantics. Consistency of LK falls out in one breath: a proof of the empty sequent ⊢ would have a cut-free counterpart, but no rule can conclude ⊢ from nothing. This is Gentzen's answer to Gödel's second theorem — consistency established, but by transfinite means outside the system itself — and cut-free proofs are also why proof search (the root of logic programming and tableau methods) is possible at all.
Natural deduction replaces the sequent's symmetric left/right rules with the intro/elim rhythm of actual mathematical reasoning: ∧-intro from φ and ψ to φ∧ψ, ∧-elim projecting back out; →-intro, the soul of the calculus, discharges an assumption — suppose φ, derive ψ, conclude φ→ψ owing nothing further to φ — and →-elim is modus ponens. NJ, the intuitionistic system, is these rules alone; NK adds excluded middle (equivalently, double-negation elimination) and with it classical logic. Keeping scrupulous track of which assumptions are open and which discharged is the entire discipline here, and it is precisely the bookkeeping that Curry–Howard will re-describe as variable binding.
A detour is an introduction immediately consumed by its own elimination — build φ∧ψ by ∧-intro, then ∧-elim it back apart — and normalization removes detours until every formula in the proof earns its place; the subformula property returns, now for natural deduction. Then the veil lifts. Annotate each assumption with a variable and each rule with a term-former, and NJ proofs are simply-typed λ-terms: propositions ↔ types, proofs ↔ programs, normalization ↔ evaluation. Detour removal is exactly β-reduction, (λx.M)N → M[N/x], with η-reduction (λx.f(x) → f) its aesthetic companion. Hold the one example that makes it unforgettable: the proposition φ → (ψ → φ∧ψ) is the type α → (β → (α × β)), and its proof — assume φ, assume ψ, pair them — is λx.λy.(x,y), literally the pair constructor. Your semester of proofs has been a semester of programs.
NJ proves φ∨ψ only by proving one disjunct, and ∃x φ only by producing a witness — the disjunction and existence properties that make intuitionistic proofs constructions. NK's excluded middle buys shorter, stranger proofs (the classic: irrationals a, b with a^b rational, proved without ever saying which pair) at the cost of that computational content, and proof-theoretically the classical reductions are genuinely wilder. Under Curry–Howard the divide becomes an engineering fact: NJ is the typed λ-calculus, and classical axioms correspond to control operators — continuations — a discovery that turned an old philosophical dispute into a theorem about programming languages. The closing essay asks what a proof is for: certainty, or construction?
The language of modern mathematics — where structure itself becomes the object, and "free" and "forgetful" turn out to be two sides of one adjunction.
Category theory studies mathematics by its arrows: forget what objects are made of, keep only how they map to one another, and watch familiar constructions become theorems about composition. Five weeks build the grammar — categories, functors, natural transformations — and the habit of duality. Read Riehl for intuition, Mac Lane for authority.
A category is objects, morphisms between them, an associative composition g∘f, and an identity idₓ at every object — nothing more, and the austerity is the point. The examples span mathematics: Set (sets and functions), Grp (groups and homomorphisms), Top (spaces and continuous maps); but the small strange ones teach you most — a poset is a category with a morphism x→y exactly when x ≤ y, a monoid is a one-object category, a free category is formal paths in a graph. Working in a category means never opening the objects: every property must be phrased through arrows alone, and retraining yourself into that discipline is the actual content of the week.
A functor F: C → D sends objects to objects and morphisms to morphisms, preserving composition and identities — it is a homomorphism of categories, and the requirement that it act on arrows, not just objects, is what gives it power. The great examples are the working tools of modern mathematics: the fundamental group π₁: Top* → Grp and homology Top → Ab, which convert topological problems into algebraic ones precisely because functoriality forces continuous maps to become homomorphisms; and the humbler pair that will dominate Phase 2 — the forgetful functor Grp → Set that strips structure, and the free functor Set → Grp that generates it. Functoriality is already a theorem-prover: any functor preserves isomorphisms, so spaces with non-isomorphic fundamental groups cannot be homeomorphic.
A natural transformation η: F ⇒ G assigns to each object X a component ηₓ: F(X) → G(X) such that for every f: X → Y the naturality square — G(f)∘ηₓ = η_Y∘F(f) — commutes: the translation between the two functors is uniform, defined without arbitrary choices. This is the concept category theory was invented to state (Eilenberg and Mac Lane, 1945, formalizing "natural" in "natural isomorphism"). The worked example is abelianization: quotienting each group by its commutator subgroup gives components G → G/[G,G] natural in G — chase the square and watch uniformity become a commuting diagram. Diagram-chasing is a skill of the hands; do it until squares commute in your sleep.
When are two categories "the same"? Isomorphism of categories is too rigid to occur in nature; the right notion is equivalence — functors F: C → D and G: D → C with natural isomorphisms GF ≅ Id and FG ≅ Id — sameness up to uniform translation, and the workhorse criterion (full, faithful, essentially surjective) is how you actually verify one. Duality is the other free gift: every category C has an opposite C^op with arrows reversed, and every theorem proved arrow-theoretically yields a dual theorem at no cost — products dualize to coproducts, monos to epis, limits to colimits. Learn to take the dual of a statement mechanically; in Phase 2 it will halve your workload.
The center of the discipline. A universal property defines an object by what it does for every other object — and objects so defined are automatically unique up to unique isomorphism. Products first, then the general theory of limits, and finally adjoint functors, the concept everything else in this track has been rehearsing for.
The product X × Y comes with projections π₁, π₂ and a promise: for any object Z with maps f: Z→X and g: Z→Y, there is a unique h: Z → X×Y with π₁∘h = f and π₂∘h = g. That promise — the universal property — characterizes the product without ever mentioning elements, and the essential theorem is that it characterizes it uniquely up to unique isomorphism: two candidates map to each other by their universal properties, and uniqueness forces the composites to be identities. Dualize and the coproduct appears: disjoint union in Set, free product in Grp, direct sum in Vect — one definition, wildly different constructions, which is precisely the lesson. From now on, "the" product means the universal property, not any particular construction of it.
Products generalize: a limit of a diagram D is a universal cone — an object with compatible maps into every object of D, through which every other cone factors uniquely — and a colimit is the dual universal cocone. The zoo becomes systematic: a product is the limit of a discrete diagram, an equalizer the limit of two parallel arrows, a pullback (fiber product) the limit of a cospan; pushouts and coequalizers are their duals. The structural theorem worth internalizing: a category with all products and equalizers has all (small) limits — the whole menagerie is generated by two constructions. "Every universal construction is a limit or colimit" is not a slogan; after this fortnight it is an inventory you can verify against your own mathematics.
An adjunction F ⊣ G is a natural bijection Hom(F(X), Y) ≅ Hom(X, G(Y)), natural in both variables — maps out of the F-construction correspond exactly to maps into the G-description. The template is Free ⊣ Forgetful: a homomorphism from the free group F(S) to any group H is exactly a function from S to H's underlying set — you have used this fact since your first algebra course, and now it has a name and a calculus. Equivalently, an adjunction is a unit η: Id ⇒ GF and counit ε: FG ⇒ Id satisfying the triangle identities; proving the two definitions equivalent is the phase's centerpiece exercise. Adjoints are the deepest organizing concept in the subject — "free," "generated by," "underlying," "best approximation" are all adjunctions — and they preserve limits (right adjoints) and colimits (left adjoints) with complete reliability.
The final movement points the arrows back at logic itself. A topos is a category that behaves like the universe of sets — closely enough to do mathematics inside it — and its native logic turns out to be intuitionistic, vindicating Track 5 from an entirely unexpected direction. Then the synthesis: your whole semester, rewritten in arrows.
A topos is a category with finite limits, exponentials (function-objects Y^X), and a subobject classifier Ω — an object such that subobjects of X correspond exactly to characteristic maps X → Ω, the way subsets correspond to maps into {true, false} in Set. Set itself is the first topos; sheaves on a space and functor categories like Set^C are the ones that matter, and in them Ω is richer than two points. The astonishment: the subobjects of any object form a Heyting algebra, not a Boolean one, so the internal logic of a general topos is intuitionistic — excluded middle fails not by decree but by geometry. Gentzen's NJ, which you learned as a proof calculus, reappears as the logic that arbitrary mathematical universes actually speak.
The categorical reading of logic recasts everything from Track 1: a theory is a category, a model is a functor from it into Set (or any topos), and a homomorphism of models is a natural transformation — soundness and completeness become statements about functor categories. Quantifiers, the deepest part, are adjoints: ∃ is left adjoint and ∀ right adjoint to substitution, which is the heart of the hyperdoctrine formulation of first-order logic. Naturality becomes uniform truth across structures, and different logical systems — classical, intuitionistic, modal — become different classes of categories. You need the shape of this story rather than its full technical weight: enough to see that "logic" and "structure" were one subject wearing two costumes all semester.
Now audit the semester with categorical eyes. Groups, rings, and vector spaces live in categories; homology is a functor and its long exact sequences are natural transformations; every universal construction you have ever used — products, quotients, completions, free objects — is a limit, a colimit, or an adjunction; Lindenbaum algebras are functorial; even Kripke models (Track 2) are presheaves in disguise. "Free" and "forgetful," which you met as vocabulary, are now the two halves of an adjunction, and the essay asks you to make the case — with your own semester as the evidence — that category theory is not another subject but the grammar the other subjects were written in.
Forty-two entries across six tracks. Five of them are ★★★ centerpieces — the proofs an admissions committee at the ILLC will recognize as the real thing. What follows is not a reading list. It is a ledger of debts to be paid in ink.
Nothing here is studied in isolation. The completeness theorem feeds computability; bisimulation shakes hands with Ehrenfeucht–Fraïssé; dynamic epistemic logic walks straight into your agent research.
Gödel's incompleteness is the halting problem in disguise — Sipser Ch. 4 is read in parallel with Track 1, and quantifier elimination decides theories the way automata decide languages. Theory of Computation →
The same taste for structure — Hilbert spaces, unitary evolution, BQP inside the complexity zoo — waits on the other side of the cathedral. Quantum track →
Track 2 ends with a DEL formalization of one agent turn: observation, belief update via action-model composition, reasoning with Kᵢ and Bᵢ, action. AGM revision is your BRAIN agent's memory update, formalized.
Six logic tracks are one field of seven. See how the arc — FOL → Incompleteness → Modal → Set → Model → Category → Proof — sits inside the full semester. Return to the Atlas →
Destinations · ILLC ★ dream · Oxford · Cambridge · UvA QCS · ETH