Semantics and Proof Theory of Modal Logic [3 ETCS, MATH-01/A]

Modal logic is an extension of propositional logic with operators that qualify in what way a statement can be true. For example, a sentence can ‘normally’ be true, or be ‘possibly’ or ‘likely’ true. We give an introduction to modal logic, with a particular emphasis on non-monotonic modal logics—systems that allow conclusions to be withdrawn in light of new information. We will cover key systems such as the logic of neccessity and possibility, but also default logic and probabilistic modal logic. We give semantics to the various logics in terms of possible world models, and – based on the semantics – investigate the mechanics of reasoning in the various different systems. The formal calculi that are of particular interest here are sequent and resolution calculi, as they directly give rise to decision procedures. We establish basic results such as completeness and cut-elimination. We conclude with applications in automated reasoning. and discuss the combination of modal logics and the computational complexity of decision procedures.