Logic and Modeling, Period 5, 2020

In Spring 2020 I taught Logic and Modeling, a second-year undergraduate course in theoretical computer science, at the VU. Due to COVID-19, the course was entirely online. Lectures were pre-recorded in 10 minute video clips. For each lecture, I hosted a live Q&A session via video meeting. Exercise classes were also held live by the course teaching assistants, Geoffrey Frankhuizen and Katrin Obendrauf.

For archival purposes, I have collected here the lectures and the recordings of live sessions.


The official (pre-COVID) syllabus is available here.

Briefly, Logic and Modeling is an introduction to different logical languages as tools for specification and verification. The course covers syntax, semantics, and derivations in propositional and first order logic; syntax and Kripke semantics of modal logic; metatheorems of the different logics, including soundness, completeness, and (un)decidability; and the structure of informal mathematical proofs.

The pen-and-paper presentations of propositional and first order logic are supplemented by the use of Lean, a tool that can check logical proofs automatically. Lean and similar systems are used “in the wild” for software verification, giving the course a practical component.

The first nine lectures, through propositional logic, follow the text Logic and Proof, which I have written with Jeremy Avigad and Floris van Doorn. The remaining lectures, on modal logic and metatheorems, follow Huth and Ryan’s Logic in Computer Science.

Archived Canvas pages

Course materials were distributed over Canvas. I have archived a few relevant pages here for public consumption.


Unfortunately the Kaltura interface makes it somewhat inconvenient to publicize these videos. I have collected the videos for each lecture on one single page. Some mobile platforms do not display them with full features: you should be able to choose between seeing my screen, my face, or either embedded in the other.

Exercise Classes

My wonderful TAs recorded their live exercise sessions.

Q&A Sessions

At each scheduled lecture time, I hosted a live Q&A session.