Teaching

Second-year course on mathematical logic for computer scientists, organised around one question: how can we be sure? The course runs from propositional logic to Gödel's theorems and on to the design of logics for particular problems. These notes accompany the lectures and contain the full mathematics, the exercises and the story that connects the weeks.

A five-day introductory course on proof-theoretic semantics (P-tS): an inferentialist alternative to the model-theoretic tradition, on which the meaning of a logical expression is constituted by the rules governing its use in proof rather than by reference to truth conditions in a model. The course was designed for graduate students, young researchers, and other non-specialists with a working knowledge of logic, and does not presuppose prior exposure to P-tS.

Across five lectures, the course develops the subject from first principles: proof theory and the shift from denotational to inferential semantics; Prawitz's theory of proof-theoretic validity; Sandqvist's base-extension semantics for classical and intuitionistic logic, and its connections to resolution calculi and logic programming; base-extension semantics for classical logic set against Kripke's model-theoretic semantics, and its extension to modal logic; and its extension to substructural logics, illustrated through intuitionistic multiplicative linear logic and inferentialist resource semantics.