Schola Arcana — Mathematical Logic

You have first-order logic. Syntax, semantics, structures, truth. That is the foundation — you are already standing at the right door. What lies ahead is the proof that formal provability and semantic truth coincide. That is the completeness theorem, and it is beautiful.

phase 1 · months 1–2

The completeness theorem

This is the target. Every valid first-order sentence — true in every model — is formally provable. The proof constructs a canonical model from a maximal consistent set of sentences. This is the Henkin construction, and it is the specific argument the ILLC admissions board will expect you to know.

PHASE 01

Enderton — A Mathematical Introduction to Logic

Chapter 2 is your entire world for two months

primary text ▼

§2.1 — 2.3

First-order languages

Variables, constants, function symbols, predicate symbols, terms, atomic formulas, well-formed formulas. The grammar of formal thought.

week 1–2

§2.4 — 2.5

Structures and truth

What it means for a sentence to be true in a structure. Satisfaction, models, validity. The semantic side of the theorem.

week 3–4

§2.6

Formal proofs and soundness

Axioms, rules of inference, formal derivations. Soundness: everything provable is valid. The easy direction — but you must know it precisely.

week 5

§2.7

The completeness theorem

The Henkin construction. Build a maximal consistent set. Construct the term model. Every valid sentence is provable. This is the crown of Phase 1.

week 6–8

How to work through Enderton

each sessionread the section once, then immediately do every exercise before moving on

oliartbring your written proofs every week — especially §2.7. work through the Henkin construction with him specifically

proof vaultevery exercise you complete goes into the vault as a LaTeX file — timestamped, public

stuck?reread the definitions from the beginning of the relevant section. in logic, confusion is almost always a sign that a definition wasn't absorbed fully

End of month 2: you can state and prove the completeness theorem from memory, reconstruct the Henkin construction, and explain why compactness follows immediately. Oliart can confirm this in his letter. The ILLC requirement is closed.

First-order syntaxTerms, formulas, sentences, free and bound variables
§2.1–2.2
Structures and satisfactionWhat it means for M ⊨ φ. The semantic definition of truth.
§2.4
Validity and logical consequence⊨ φ, Γ ⊨ φ. Universal truth vs contextual truth.
§2.5
Formal proof systemsHilbert-style axioms, modus ponens, derivations, ⊢ φ
§2.6
Soundness theoremIf Γ ⊢ φ then Γ ⊨ φ. Proof by induction on derivation length.
§2.6
Consistency and maximal consistent setsLindenbaum's lemma — every consistent set extends to a maximal one.
§2.7
Henkin constants and witnessesAdding witnesses for existential sentences. The Henkin extension.
§2.7
The completeness theoremIf Γ ⊨ φ then Γ ⊢ φ. Every valid sentence is provable. The full proof.
§2.7 ★

phase 2 · month 3

Consequences of completeness

Completeness is not the end — it is the beginning. From it, two of the most powerful theorems in all of logic fall out almost immediately.

PHASE 02

Compactness + Löwenheim-Skolem

The two great consequences · still Enderton Ch. 2–3

consequences ▼

compactness theorem

If every finite subset of Γ is satisfiable, then Γ is satisfiable

Falls directly out of completeness. Has wild consequences — you can produce non-standard models of arithmetic from it.

month 3, week 1

Löwenheim-Skolem theorem

If a theory has an infinite model it has models of every infinite cardinality

No first-order theory can pin down a unique infinite cardinality. Deeply strange. Essential for model theory.

month 3, week 2

non-standard models

Arithmetic has non-standard models

Using compactness, construct a model of Peano arithmetic containing infinite natural numbers. Write about it.

month 3, week 3

optional deepening

Ebbinghaus — Mathematical Logic

Alternative proof style. More algebraic in flavor. Good for proof vault variety.

supplementary

Compactness theorem — statement, proof from completeness, and at least two applications
§2.8
Downward Löwenheim-Skolem — every satisfiable theory has a countable model
§2.8
Upward Löwenheim-Skolem — models of every infinite cardinality
§2.8
Non-standard models of arithmetic — compactness applied to Peano axioms
application

End of month 3: completeness, compactness, and Löwenheim-Skolem all under your belt. Model theory is now open to you.

phase 3 · month 3–4

Gödel's incompleteness theorems

You have completeness — now you need incompleteness. These are not contradictions. They operate in different domains and together define the shape of mathematical knowledge.

PHASE 03

Smullyan — Gödel's Incompleteness Theorems

The crown · connects to recursion theory and TOC

the crown ▼

Gödel numbering

Encoding syntax as arithmetic

Every formula, proof, and symbol gets a unique natural number. Arithmetic can then talk about its own proofs. Connects directly to Turing machines.

week 1

First incompleteness theorem

No consistent system proves all arithmetical truths

There exists a sentence that is true but unprovable. The Gödel sentence: "I am not provable."

week 2–3

Second incompleteness theorem

No consistent system proves its own consistency

Hilbert's program collapses here. The most devastating theorem in the history of mathematics.

week 3–4

connection to Sipser

Incompleteness ↔ undecidability

Gödel's proof and Turing's halting problem are the same idea in different clothes. Read Ch. 4–5 again after Gödel.

synthesis

Gödel numbering — encoding formulas and proofs as natural numbers
foundations
Representability in arithmetic — recursive functions representable in Peano arithmetic
key lemma
The Gödel sentence — construction of a sentence that asserts its own unprovability
★ first theorem
First incompleteness theorem — full proof for any consistent, sufficiently strong system
★ first theorem
Second incompleteness theorem — Con(T) is not provable in T if T is consistent
★ second theorem
Connection to the halting problem — incompleteness as undecidability in disguise
synthesis

End of Phase 3: you understand why Hilbert's program failed, what it means for mathematics to have true but unprovable sentences, and how this connects to computability. Write the synthesis essay. That is your artifact.

why this track exists

The native language of ILLC

→ Track 1 gives you classical logic. This track gives you the logic ILLC actually speaks. Van Benthem, Baltag, and Smets — the people who will read your application — built their careers in Kripke frames and dynamic epistemic logic. If your paper speaks this language, it lands differently. Start this track no later than month 3, overlapping with Track 1's Phase 3.

Modal logic extends classical logic with operators for necessity (□) and possibility (◇). Epistemic logic interprets these as knowledge and belief. Dynamic epistemic logic adds update operators — formal descriptions of how knowledge changes when new information arrives. This is the formal home of your agent paper's belief revision mechanism.

PHASE 01 · months 3–4

Kripke semantics and the modal cube

Blackburn, de Rijke & Venema — Modal Logic · Ch. 1–2

foundation ▼

primary text

Blackburn, de Rijke & Venema — Modal Logic

The canonical text. Van Benthem is a co-author. This is the book ILLC students are expected to know. Chapters 1–3 are your core. Treat it like you treat Enderton.

start here

accessible companion

van Benthem — Modal Logic for Open Minds

Written by the person who will likely read your application. More conversational than Blackburn. Read a chapter here when Blackburn feels dense. Shows you the philosophy behind the formalism.

parallel read

Kripke frames

Possible worlds semantics

A Kripke frame is a pair (W, R) — a set of worlds and an accessibility relation. A formula □φ is true at world w iff φ is true at every world accessible from w. This is the core move.

week 1–2

the modal cube

K, T, S4, S5 and their frame conditions

Each axiom schema corresponds to a frame property. T: reflexivity. 4: transitivity. B: symmetry. S5: equivalence relation. The correspondence theorem is the modal analog of completeness.

week 3–4

Syntax of modal logic — propositional logic + □ and ◇ operators
Ch. 1
Kripke frames and models — (W, R, V), truth at a world, validity
Ch. 1
Frame correspondence — each axiom encodes a frame property. T ↔ reflexivity. 4 ↔ transitivity.
Ch. 2
Completeness for K, T, S4, S5 — canonical model construction. The modal analog of Henkin.
Ch. 2 ★
Bisimulation — when two Kripke models are modally equivalent. The key invariance notion.
Ch. 2

End of Phase 1: you can define a Kripke model, evaluate modal formulas at worlds, state the correspondence between axioms and frame conditions, and prove completeness for S5. Modal logic is now a language, not a mystery.

PHASE 02 · months 5–6

Epistemic logic — knowledge and belief

Fagin, Halpern, Moses & Vardi — Reasoning About Knowledge · Ch. 1–3

epistemic ▼

primary text

Fagin, Halpern, Moses & Vardi — Reasoning About Knowledge

The definitive text on epistemic logic. Formalizes what agents know, believe, and know that they know. Directly relevant to your agent paper. Chapters 1–3 are sufficient for your purposes.

primary

key distinction

Knowledge (K) vs belief (B)

K is factive — Kᵢφ implies φ is true. B is not — Bᵢφ can be false. Your agent paper hinges on this: the agent has beliefs about user intent, not knowledge. S5 for knowledge, KD45 for belief.

foundational

multi-agent

Common knowledge and group epistemics

Cφ means every agent knows φ, and knows that every agent knows φ, and so on infinitely. This is the formal notion needed for your multi-agent open problem from the BRAIN paper.

Ch. 2

for your paper

Epistemic states as belief revision

AGM belief revision axioms: when an agent learns φ, how should their belief set change? This is the formal version of your memory update function µ(M, s, a) → M′ from BRAIN.

paper connection

Knowledge operators Kᵢ — S5 axioms, introspection, the KK thesis
Ch. 1
Belief operators Bᵢ — KD45 system, difference from knowledge
Ch. 1
Common knowledge C — definition, fixed-point characterization
Ch. 2
AGM belief revision — the six rationality postulates for belief update
Ch. 3 ★
Muddy children puzzle — common knowledge in action. Know this cold — it appears in interviews.
classic

End of Phase 2: you can formalize the difference between knowledge and belief, define common knowledge, state the AGM axioms, and connect belief revision to your agent's memory update function. Your paper now has its logical foundation.

PHASE 03 · months 6–7 · the frontier

Dynamic epistemic logic — knowledge that changes

van Ditmarsch, van der Hoek & Kooi — Dynamic Epistemic Logic

★ paper foundation ▼

primary text

van Ditmarsch, van der Hoek & Kooi — Dynamic Epistemic Logic

DEL adds action operators to epistemic logic. [A]φ means after action A is performed, φ holds. Public announcement logic (PAL) is the simplest instance. This is where your paper lives.

primary

the key move

Public announcement logic

[!φ]ψ — after publicly announcing φ, ψ holds. The update operator changes the model by restricting to φ-worlds. This is belief revision made dynamic and compositional.

PAL

for your agent

Action models and epistemic events

More general than PAL — models private communications, partial observations, and uncertain announcements. Every turn in your car agent is a DEL action that updates the agent's belief state.

paper section

synthesis

Your paper's formal claim

The agent's memory update µ(M, s, a) → M′ is a DEL action model composition. The orchestrator's routing is a policy restricted to epistemically permissible actions. This is your contribution.

★ the claim

Public announcement logic — syntax, semantics, reduction axioms
Ch. 2 ★
Product update — action models composed with epistemic models
Ch. 4
Reduction axioms — [!φ]Kᵢψ ↔ (φ → Kᵢ(φ → [!φ]ψ)). Memorize this.
Ch. 2 ★
Completeness for PAL — reduction to epistemic logic, the translation method
Ch. 3
Arbitrary announcement logic — knowing whether a formula could be announced
Ch. 5
Application to your agent — formalize one full agent turn as a DEL event model
★ paper

How to work through DEL

each weekone DEL theorem proved in LaTeX — reduction axiom proofs are the best exercises

connectafter every chapter, write one paragraph connecting the formalism to your agent architecture. this becomes your paper's introduction

cite rightcite van Benthem's "Logical Dynamics" alongside DEL — shows breadth. cite Baltag & Moss for action models specifically

End of Track 2: you can speak ILLC's language. Your agent paper now has a formal semantic foundation — belief states, update operators, and epistemic constraints — derived from theorems, not intuition. This is what makes you different from every other applicant.

proof vault targets — track 2

THM

Completeness for S5

Canonical model construction for epistemic logic · the modal analog of Henkin

month 4

THM

Frame correspondence theorem

T axiom ↔ reflexive frames · 4 axiom ↔ transitive frames · full proof

month 4

THM ★

PAL reduction axiom

[!φ]Kᵢψ ↔ (φ → Kᵢ(φ → [!φ]ψ)) · proof and interpretation

month 6 ★

ESSAY

DEL and your agent — the formal connection

One agent conversation turn formalized as a DEL action model · this is your paper's core section

month 7 ★

why this track exists

The substrate of everything

→ Set theory is the foundational language in which all of mathematics is written. Oxford and Cambridge will assume fluency here. More practically: ordinals and cardinals are what make Löwenheim-Skolem precise, and the axiom of choice is what makes Zorn's lemma work, which you will use in model theory. Start after Phase 2 of Track 1.

PHASE 01 · months 4–5

Enderton — Elements of Set Theory

Ordinals, cardinals, AC — the full foundational picture

primary text ▼

ZFC axioms

The axioms of set theory

Extensionality, pairing, union, power set, infinity, replacement, foundation. These are the axioms from which all of mathematics is built. Know each one and why it is needed.

Ch. 1–2

ordinals

Well-orderings and transfinite induction

Every well-ordered set is isomorphic to a unique ordinal. Transfinite induction and recursion — the generalization of mathematical induction to infinite ordinals. Beautiful and essential.

Ch. 4–5

cardinals

Infinite cardinalities and Cantor's theorem

ℵ₀, ℵ₁, the continuum. Cantor's theorem: |P(X)| > |X| for every set X. The diagonal argument — the same idea as Gödel's proof and Turing's halting problem.

Ch. 6

choice

Axiom of choice and its equivalents

AC ↔ Zorn's lemma ↔ well-ordering theorem. These three are the same theorem in different clothes. Lindenbaum's lemma from Track 1 uses Zorn's lemma — now you see why.

Ch. 7 ★

ZFC axioms — all nine, statement and motivation for each
Ch. 1
Ordinal numbers — definition, well-ordering, transfinite induction
Ch. 4
Cardinal numbers — ℵ₀, ℵ₁, cardinal arithmetic
Ch. 6
Cantor's theorem — |P(X)| > |X| · the diagonal argument in set theory
Ch. 6 ★
Axiom of choice — statement and three equivalent forms
Ch. 7
Zorn's lemma — statement, proof from AC, and one application
Ch. 7 ★
Well-ordering theorem — every set can be well-ordered · proof from AC
Ch. 7

End of Track 3: the foundations are fully closed. You understand what ZFC is, why it is the right foundation, where AC is used silently throughout mathematics, and how infinite cardinalities are measured. Oxford foundations is now reachable.

proof vault targets — track 3

THM

Cantor's theorem

|P(X)| > |X| for every set X · the set-theoretic diagonal argument

month 5

THM ★

AC ↔ Zorn's lemma ↔ well-ordering theorem

Full proof of equivalence across all three forms

month 5 ★

THM

Transfinite induction

The generalization of mathematical induction · proof of principle and one application

month 5

why this track exists

The mathematics of mathematical structures

→ Model theory asks: what can first-order logic say, and what can it not say, about mathematical structures? This is the deep continuation of your compactness and Löwenheim-Skolem work from Track 1. Essential for Barcelona, Paris LMFI, and Manchester. Begin after Track 1 is complete and Track 3 is underway.

PHASE 01 · months 6–8

Marker — Model Theory: An Introduction

Ch. 1–3 · the core of the subject

primary text ▼

elementary equivalence

When two structures satisfy the same sentences

M ≡ N — two structures are elementarily equivalent if they satisfy the same first-order sentences. The rationals and reals are elementarily equivalent as ordered fields. This is wild.

Ch. 1

types

Complete types and type spaces

The type of an element describes every first-order property it has in a model. Type spaces are the geometric objects of model theory. Saturated models realize all types.

Ch. 2

quantifier elimination

When every formula is equivalent to a quantifier-free one

Dense linear orders eliminate quantifiers. Algebraically closed fields eliminate quantifiers. This is model theory's most powerful tool — it shows exactly what a theory can express.

Ch. 3 ★

EF games

Ehrenfeucht-Fraïssé games

A game-theoretic method for proving elementary equivalence — or its failure. Two players, two structures. Duplicator wins iff the structures agree on all sentences of quantifier rank ≤ n.

Ch. 2 ★

Elementary equivalence M ≡ N — definition and examples using compactness
Ch. 1
Elementary embeddings — M ≺ N, Tarski-Vaught test
Ch. 1
Complete types — p(x) a type over M, realizing and omitting types
Ch. 2
Omitting types theorem — when a type can be omitted in a model
Ch. 2
Quantifier elimination — definition and proof for dense linear orders
Ch. 3 ★
Ehrenfeucht-Fraïssé games — definition, winning strategy = elementary equivalence
Ch. 2 ★
ω-categoricity — Ryll-Nardzewski theorem, theories with one countable model
Ch. 2

End of Track 4: you understand what first-order logic can and cannot distinguish between structures. Quantifier elimination, types, and EF games are your tools. Barcelona and Paris LMFI are now reachable. Model theory also deepens everything in your agent paper — the agent's state space is a model.

proof vault targets — track 4

THM

Quantifier elimination for dense linear orders

Every formula over (Q, <) is equivalent to a quantifier-free formula · full proof

month 7

THM ★

EF game theorem

Duplicator has winning strategy in n-round game iff structures agree on rank-n sentences

month 8 ★

THM

Tarski-Vaught test

Criterion for M ≺ N — elementary substructure characterization

month 7

why this track exists

The structure of proofs themselves

→ Proof theory studies proofs as mathematical objects. Gentzen's sequent calculus, cut elimination, and proof normalization are the tools. This track is last because it requires the most mathematical maturity — you need Tracks 1, 2, and 3 solid before it clicks. Do not start before month 8. Essential for Oxford, TU Vienna, and Paris LMFI.

PHASE 01 · months 8–10

Troelstra & Schwichtenberg — Basic Proof Theory

Sequent calculus, cut elimination, normalization

primary text ▼

sequent calculus

Gentzen's LK system

A proof system where the objects are sequents Γ ⊢ Δ — a set of hypotheses entails a set of conclusions. Rules operate on both sides. More symmetric than Hilbert systems. Beautiful.

Ch. 2

cut elimination

Gentzen's Hauptsatz

Every proof in LK can be transformed into a cut-free proof. The cut rule is the sequent-calculus analog of modus ponens. Eliminating it gives you the subformula property — every formula in the proof was in the conclusion.

Ch. 3 ★

natural deduction

Gentzen's NJ and NK systems

Natural deduction is how mathematicians actually reason — introduction and elimination rules for each connective. NJ is intuitionistic. NK is classical. The Curry-Howard correspondence connects NJ to typed lambda calculus.

Ch. 2

normalization

Proof normalization and Curry-Howard

Every natural deduction proof can be normalized — detour eliminations reduce a proof to normal form. Under Curry-Howard, this is beta reduction in the lambda calculus. Proofs are programs.

Ch. 4 ★

Sequent calculus LK — sequents, structural rules, logical rules for all connectives
Ch. 2
Cut rule — statement and why it is dangerous/powerful
Ch. 2
Gentzen's Hauptsatz — cut elimination theorem · full proof
Ch. 3 ★
Subformula property — consequence of cut elimination · every formula in a cut-free proof occurs in the end-sequent
Ch. 3
Natural deduction NJ — introduction and elimination rules, intuitionistic logic
Ch. 2
Proof normalization — normal forms, detour eliminations
Ch. 4
Curry-Howard correspondence — proofs as programs, propositions as types
Ch. 4 ★

How to work through Troelstra & Schwichtenberg

warningthis is the hardest text on this list. do not open it before Track 1 is complete and Track 3 is underway. the notation is dense and the proofs are long

strategyread Buss "Introduction to Proof Theory" (handbook chapter, free online) first — it is shorter and gives you the map before the territory

cut elimspend two full weeks on cut elimination. write the proof yourself before reading theirs. it is the most important result in the book

End of Track 5 — end of the cathedral: you have completeness, incompleteness, modal logic, epistemic update, set-theoretic foundations, model-theoretic tools, and the structure of proofs themselves. You are ready for ILLC. You are ready for Oxford. You built this proof by proof.

proof vault targets — track 5

THM ★

Gentzen's cut elimination theorem

Every LK proof can be transformed into a cut-free proof · full Hauptsatz

month 9 ★

THM

Subformula property

Every formula in a cut-free proof is a subformula of the end-sequent

month 9

ESSAY

Curry-Howard in your own words

Why proofs are programs · intuitionistic logic · the connection to lambda calculus · your synthesis

month 10

proof vault — complete map

Everything that goes in the vault

Every theorem below is a LaTeX document — formal, complete, dated. By month 10, this vault is your application's silent argument. Not a list of books you read. Evidence that you proved things.

THM

Soundness theorem for first-order logic

If Γ ⊢ φ then Γ ⊨ φ · Track 1

month 1

THM

Lindenbaum's lemma

Every consistent set extends to a maximal consistent set · Track 1

month 2

THM ★

Completeness theorem — full Henkin proof

If Γ ⊨ φ then Γ ⊢ φ · the complete proof · Track 1

month 2 ★

THM

Compactness theorem

Γ satisfiable iff every finite subset satisfiable · Track 1

month 3

THM

Downward Löwenheim-Skolem

Every satisfiable theory has a countable model · Track 1

month 3

THM ★

First incompleteness theorem

Full Gödel proof · Track 1

month 4 ★

THM ★

Completeness for S5

Canonical model construction for epistemic logic · Track 2

month 4

THM

Frame correspondence theorem

T ↔ reflexivity · 4 ↔ transitivity · Track 2

month 4

THM ★

AC ↔ Zorn's lemma ↔ well-ordering

Full equivalence proof · Track 3

month 5 ★

THM

Cantor's theorem

|P(X)| > |X| · Track 3

month 5

THM ★

PAL reduction axiom

[!φ]Kᵢψ ↔ (φ → Kᵢ(φ → [!φ]ψ)) · Track 2

month 6 ★

THM ★

Quantifier elimination for dense linear orders

Every formula over (Q, <) equivalent to quantifier-free · Track 4

month 7

THM ★

Ehrenfeucht-Fraïssé game theorem

Duplicator wins n-round game iff elementary equivalence to rank n · Track 4

month 8 ★

THM ★

Gentzen's cut elimination theorem

Every LK proof has a cut-free version · Hauptsatz · Track 5

month 9 ★

ESSAY

DEL and your agent — the formal connection

One agent turn as a DEL event model · your paper's core section · Track 2

month 7 ★

ESSAY

Curry-Howard in your own words

Proofs as programs · Track 5

month 10