Introduction to Modal Logic

Autumn 2016

Institute for Logic, Language and Computation

Universiteit van Amsterdam


Exam 2015

Exam 2014




Practicalities

  • Instructors: Nick Bezhanishvili and Sebastian Enqvist , emails: N.Bezhanishvili[at]uva.nl and sebastian.enqvist[at]fil.lu.se

  • Teaching assistants: Frederik Lauridsen , email: F.M.Lauridsen[at]uva.nl ; Ana Lucia Vargas , email: ana.varsa[at]gmail.com

  • Time and Place: Lectures on Tuesdays 15-17h (SP 904, G2.10), Tutorials on Thursdays 9-11 (SP 904, C1.112) and Fridays 9-11 (SP 904, G3.10)

  • EC: 6

  • Assessment : There will be 7 Homework sheets. There will be a midterm exam on 22 October and also a final exam on 22 December. The final grade consists 50% of the homework grade, 10% of the grade of the midterm exam and 40% of the grade of the final exam. The homework grade is split into 6 homework sheets weighing 100 points each.

  • Midterm exam: The midterm exam will be held on Tuesday, 25 October, 9-11 in REC C1.04.


  • Final exam: The final exam will be held on Thursday, 22 December, 9-12 in JWS zaal 1.

Information about the course

  • Objectives:
  • The students should be able to point out when a modal formula is satisfied/valid on a given Kripke model/frame.
  • They should also be able to compute standard translations of modal formulas and first-order correspondents of Sahlqvist formulas.
  • They are expected to produce a completeness proof via the canonical model construction for some basic systems of modal logic.
  • They should also be able to derive finite model property of such systems via the method of filtration.
  • Students should be able to argue about decidability of simple systems of modal logic by combining finite axiomatization and the finite model property of these systems.
  • Students are also expected to solve basic problems involving more complex modal systems such as PDL.

  • Contents: The course covers the basic notions of modal logic:
  • syntax, relational semantics,
  • models and frames,
  • filtrations,
  • bisimulations, van Benthem's bisimulation characterisation theorem,
  • first-order correspondence, Sahlqvist algorithm,
  • model-theoretic and frame-theoretic constructions,
  • soundness and completeness, the finite model property,
  • propositional dynamic logic PDL.

  • Recommended prior knowledge: Knowledge of first order logic (syntax and semantics) and elementary mathematical knowledge and skills.

  • Format: Weekly lectures and tutorial sessions.

  • Study materials: Modal Logic, Blackburn, de Rijke, Venema, Cambridge University Press, 2001.

    • Additional literature

  • Alexander Chagrov and Michael Zakharyaschev: Modal Logic, Oxford University Press, 1997.
  • Johan van Benthem : Modal Logic for Open Minds, 2010.
  • Marcus Kracht: Tools and Techniques in Modal Logic, Elsevier, 1999.
  • Dov M. Gabbay, A. Kurucz, F. Wolter, M. Zakharyaschev: Many-Dimensional Modal Logics: Theory and Applications, Elsevier, 2003.

    • Homeworksheets

  • Homework 1, due on 27 September before class.

  • Homework 2, due on 11 October before class.

  • Homework 3, due on 18 October before class.

  • Homework 4, due on 15 November before class.

  • Homework 5, due on 29 November before class.

  • Homework 6, due on 13 December before Q and A session.

    • Lectures

    <
    6 Sep 2016
    Tuesday    		 Hoorcollege
    15-17
    SP 904 G2.10    		 Slides of the first lecture Lecture 1
    8 Sep 2016
    Thursday    		 Hoorcollege
    9-11
    SP 904 C1.112    		 Slides of the second lecture Lecture 2
    9 Sep 2016
    Friday    		 Wekcollege Group B
    9-11
    		 Cancelled!
    13 Sep 2016
    Tuesday    		 Hoorcollege
    15-17
    SP 904 G2.10    		 Slides of the third lecture Lecture 3
    15 Sep 2016
    Thursday    		 Wekcollege Group A
    9-11
    SP 904 F2.04    		 The first tutorial sheet Tutorial 1
    16 Sep 2016
    Friday    		 Wekcollege Group B
    9-11
    SP 904 G3.10    		 The first tutorial sheet Tutorial 1
    20 Sep 2016
    Tuesday    		 Hoorcollege
    15-17
    SP 904 G2.10    		 Slides of the fourth lecture Lecture 4
    22 Sep 2016
    Thursday    		 Wekcollege Group A
    9-11
    SP 904 G3.02    		 The second tutorial sheet Tutorial 2
    23 Sep 2016
    Friday    		 Wekcollege Group B
    9-11
    SP 904 G3.10    		 The second tutorial sheet Tutorial 2
    27 Sep 2016
    Tuesday    		 Hoorcollege
    15-17
    SP 904 G2.10    		 Cancelled!
    29 Sep 2016
    Thursday    		 Wekcollege Group A
    9-11
    SP 904 B0.201    		 The third tutorial sheet Tutorial 3
    30 Sep 2016
    Friday    		 Wekcollege Group B
    9-11
    SP 904 G3.10    		 The third tutorial sheet Tutorial 3
    4 Oct 2016
    Tuesday    		 Hoorcollege
    15-17
    SP 904 G2.10    		 Standard translation (Sec. 2.4), the van Benthem characterization theorem (without proof), (Sec. 2.4 until ultraproducts), frame definability (Secs 3.1-3.2 until 3.10).
    6 Oct 2016
    Thursday    		 Wekcollege Group A
    9-11
    SP 904 B0.201    		 Discussion of the homework exercises.
    7 Oct 2016
    Friday    		 Wekcollege Group B
    9-11
    SP 904 G3.10    		 Discussion of the homework exercises.
    11 Oct 2016
    Tuesday    		 Hoorcollege
    15-17
    SP 904 G2.10    		 Frame definability and correspondence (Sections 3.1 and 3.2 until Example 3.10). Definable and undefinable properties (Section 3.3 until Corollary 3.16). Automatic First-Order Correspondence (Section 3.5 until uniform formulas).
    13 Oct 2016
    Thursday    		 Wekcollege Group A
    9-11
    SP 904 B0.201    		 The fourth tutorial sheet Tutorial 4
    14 Oct 2016
    Friday    		 Wekcollege Group B
    9-11
    SP 904 G3.10    		 The fourth tutorial sheet Tutorial 4
    18 Oct 2016
    Tuesday    		 Hoorcollege
    15-17
    SP 904 G2.10    		 Sahlqvist theorem and Sahlqvist algorithm (the notes on Sahlqvist algorithm)
    20 Oct 2016
    Thursday    		 Wekcollege Group A
    9-11
    SP 904 B0.201    		 The fifth tutorial sheet Tutorial 5
    21 Oct 2016
    Friday    		 Wekcollege Group B
    9-11
    SP 904 G3.10    		 The fifth tutorial sheet Tutorial 5
    Midterm exam: October 25, 9:00 - 11:00. REC C1.04
    1 Nov 2016
    Tuesday    		 Hoorcollege
    13-15
    SP 904 C1.112    		 Normal modal logics. Hilbert style derivation systems and soundness and completeness (Sections 1.6 and 4.1 in the modal logic book, see also slides 13-22 in the Modal Logic Notes)
    4 Nov Oct 2016
    Friday    		 Wekcollege
    9-11
    SP B0.201    		 The sixth tutorial sheet Tutorial 6 and some partial solutions Solutions 6.
    8 Nov 2016
    Tuesday    		 Hoorcollege
    13-15
    SP 904 C1.112    		 Completeness of K via canonical models (Section 4.2, slides 26-30 and 36-48).
    11 Nov 2016
    Friday    		 Wekcollege
    9-11
    SP B0.201    		 The seventh tutorial sheet Tutorial 7.
    15 Nov 2016
    Tuesday    		 Hoorcollege
    13-15
    SP 904 C1.112    		 Completeness of modal logics via canonical models, canonicity, the finite model property, decidability (Sections 4.2, 4.3 and 6.2, slides 49-77).
    18 Nov 2016
    Friday    		 Wekcollege
    9-11
    SP B0.201    		 The eighth tutorial sheet Tutorial 8.
    22 Nov 2016
    Tuesday    		 Hoorcollege
    13-15
    SP 904 C1.112    		 General frames (Sec 1.4), incomplete logics (Sec 4.4). Propositional Dynamic Logic PDL, regular frames (Example 1.15, Example 1.26, Section 4.8 until Definition 4.79.)
    25 Nov 2016
    Friday    		 Wekcollege
    9-11
    SP B0.201    		 The ninth tutorial sheet Tutorial 9.
    29 Nov 2016
    Tuesday    		 Hoorcollege
    13-15
    SP 904 C1.112    		 Fischer-Ladner closure, atoms, canonical model over Σ, Regular PDL-model over Σ, Existence lemma for basic programs, existence lemma (4.79 - 4.89).
    2 Dec 2016
    Friday    		 Wekcollege
    9-11
    SP B0.201    		 The tenth tutorial sheet Tutorial 10.
    6 Dec 2016
    Tuesday    		 Hoorcollege
    13-15
    SP 904 C1.112    		 Completeness of PDL wrt regular frames (Section 4.8, we didn't prove lemmas 4.87-4.88). Since and Until (Section 7.2 until 7.11). Hybrid logic (Section 7.3 until 7.22, we didn't discuss the satisfaction operator). Neighbourhood semantics (see e.g., Hansen Thesis or Pacuit notes, we only defined the semantics and showed that in this semantics the modal Box does not commute with ∧ and that Box ⊤ is not equivalent to ⊤.)
    9 Dec 2016
    Friday    		 Wekcollege
    9-11
    SP B0.201    		 The eleventh tutorial sheet Tutorial 11.