Proof Theory of Modal Logic
Oliver Roy & Norbert Gratzl
Logic & Computation
Week One - 11.00-12.30 - Level: I
This course is about proof theory for modal logic. We will cover sequents and hypersequents, labeled calculi, and display logic. The focus will be on normal modal logics. If time permits we will look at multi-modal systems, non-normal modalities, and hybrid languages.
The course aims at giving a unified perspective on the various proof- theoretic methods that are available for modal logic. At the end of the course the students should have mastered the key proof-theoretic toolbox. They should also understand when and why each of its constituent comes handy, and what kind of trade-offs are involved in choosing one over the other.
The course will be example-driven. The different proof-theoretic meth- ods will be introduced through modal logics that are of independent interest for students of ESSLLI: basic modal logic K, and epistemic logic (S5), stan- dard deontic logic (KD).
The course should be of interest for students in philosophy, computer science and linguistic. It will be mostly self-contained. Previous knowledge of the modal or proof-theoretical concepts is an asset but is not required. Basic acquaintance with propositional and first-order logic will be assumed.