Practicalities
- Instructor: Nick Bezhanishvili email: N.Bezhanishvili[at]uva.nl
- Teaching assistants: Frederik Lauridsen , email: F.M.Lauridsen[at]uva.nl,
Kaibo Xie , email: K.Xie[at]uva.nl and Tim Henke
email: tim.henke[at]gmail.com
- Time and Place: Lectures on Tuesdays 11:00-13:00 (SP 904, C1.112), Tutorials on Thursdays 13:00-15:00 (Groups A and B, SP 904, G5.29 and G3.10)
and 17:00-19:00 (Group C, G3.10).
- EC: 6
- Assessment : There will be a midterm exam on 23 October and also a final exam on 21 December. The final grade consists
40% of the homework grade, 20% of the grade of the midterm exam and 40% of the grade of the final exam.
The homework grade is split into 6 or 7 homework sheets weighing 100 points each.
The homework with the lowest score will be disregarded.
- Midterm exam: The midterm exam will be held on Tuesday, 23 October, 9-12.
- Final exam: The final exam will be held on Thursday, 21 December, 9-12.
- More specific information about homework and grading:
Deadlines for submission are strict; this applies in particular to the condition that homework should be handed in at the beginning of class.
Homework handed in after the deadline will not be taken into consideration.
Unless explicitly specified otherwise, you are allowed to collaborate with your fellow students, on the following conditions:
- you can only work in small groups of at most three people;
- you can discuss the exercises together, but you have to write down the solution individually;
- you must explicitly write on your homework with whom you have been working together.
When writing your solutions to exercises, be succinct. In particular:
- never prove statements that are explicitly mentioned in the lecture notes (unless specifically asked otherwise); simply refer to these results if you use them;
- in the case of a routine argument, you do not need to go into all the technical details;
- in case of proofs by induction on the complexity of formulas, one or two cases will usually suffice.
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,
- general frames,
- propositional dynamic logic
PDL,
- Neighbourhood semantics of modal logic.
- 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 18 September before class.
- Homework 2, due on 2 October before class.
- Homework 3, due on 16 October before class.
- Homework 4, due on 13 November before class.
- Homework 5, due on 27 November before class.
- Homework 6, due on 11 December before class.
Lectures
4 Sep 2018 Tuesday |
Hoorcollege 11-13 SP 904 C1.112 |
| Introduction to modal logic, syntax and semantics of basic modal logic, bisimulations, bisimilarity, bisimulation invariance theorem,
(Sections 1.1-1.3, 2.2)
|
6 Sep 2018 Thursday |
Werkcollege 13-15 Goup A: SP 904 G5.29, Group B: SP 904 G3.10 |
| The first tutorial sheet Tutorial 1
|
11 Sep 2018 Tuesday |
Hoorcollege 11-13 SP 904 G2.10 |
| Hennessy-Milner theorem, disjoint unions, generated submodels and bounded morphisms (Sections 2.1-2.2), validity and frame definability (Sections 1.3-3.1)
|
13 Sep 2018 Thursday |
Werkcollege 13-15 Goup A: SP 904 G5.29, Group B: SP 904 G3.10. 17-19 Group C: SP 904 G3.10
|
| The second tutorial sheet Tutorial 2
|
18 Sep 2018 Tuesday |
Hoorcollege 11-13 SP 904 C1.112 |
| Finite models via filtrations, Filtration Theorem, smallest and largest filtrations, transitive filtrations. (Sections 2.3)
|
20 Sep 2018 Thursday |
<Werkcollege 13-15 Goup A: SP 904 G5.29, Group B: SP 904 G3.10. 17-19 Group C: SP 904 G3.10
|
| The third tutorial sheet Tutorial 3
|
25 Sep 2018 Tuesday |
Hoorcollege 11-13 SP 904 G2.10 |
| The standard translation, van Benthem's Characterization Theorem without proof (Sections 2.4 and 2.6).
Rooted models, tree unravellings and tree model property (Proposition 2.15).
|
27 Sep 2018 Thursday |
<Werkcollege 13-15 Goup A: SP 904 G5.29, Group B: SP 904 G3.10. 17-19 Group C: SP 904 G3.10
|
| The fourth tutorial sheet Tutorial 4
|
2 Oct 2018 Tuesday |
Hoorcollege 11-13 SP 904 C1.112 |
| Frame definability (Secs 3.1-3.2 until 3.10, Prop 3.12, Thm 3.19 the Goldblatt-Thomason Theorem without proof). Automatic first-order correspondence (Sec 3.5 until uniform formulas). Sahlqvist formulas.
|
4 Oct 2018 Thursday |
Werkcollege 13-15 Goup A: SP 904 G5.29, Group B: SP 904 G3.10. 17-19 Group C: SP 904 G3.10
|
| The fifth tutorial sheet Tutorial 5
|
9 Oct 2018 Tuesday |
Hoorcollege 11-13 SP 904 C1.112 |
| Sahlqvist correspondence. The notes on Sahlqvist algorithm (Section 3.6 in the book). |
11 Oct 2018 Thursday |
Werkcollege 13-15 Goup A: SP 904 G5.29, Group B: SP 904 G3.10. 17-19 Group C: SP 904 G3.10
|
| The sixth tutorial sheet Tutorial 6
|
16 Oct 2018 Tuesday |
Hoorcollege 11-13 SP 904 G2.10 |
| Normal modal logics. Hilbert style derivation systems, soundness and completeness, consistent sets
(Sections 1.6 and 4.1 in the modal logic book, see also slides 1-30 in the Modal Logic Notes) |
18 Oct 2018 Thursday |
Werkcollege 13-15 Goup A and B: SP 904 G5.29 17-19 Group C: SP 904 G3.10
|
| The seventh tutorial sheet Tutorial 7
|
Midterm exam: 23 October 2018, 9:00 - 12:00 |
30 Oct 2018 Tuesday |
Hoorcollege 11-13 SP 904 C1.112 |
| Completeness of the basic modal logic K via the canonical model construction (Section 4.2 in the modal logic book, slides 37-49 in the
Modal Logic Notes)
|
1 Nov 2018 Thursday |
Wekcollege 13-15 Goup A: SP 904 G0.18B, Group B: SP 904 G2.02 |
| The eighth tutorial sheet Tutorial 8
|
6 Nov 2018 Tuesday |
Hoorcollege 11-13 SP 904 C1.112 |
| Completeness of normal modal logics via the canonical model construction, canonical logics, Sahlqvist theorem without proof,
the finite model property (Sections 4.2-4.3 in the modal logic book, slides 48-77 in the Modal Logic Notes), Decidability
(Theorems 6.7, 6.13 and 6.15 in Section 6.2).
|
8 Nov 2018 Thursday |
Wekcollege 13-15 Goup A: SP 904 G0.18B, Group B: SP 904 G2.02 |
| The ninth tutorial sheet Tutorial 9
|
13 Nov 2018 Tuesday |
Hoorcollege 11-13 SP 904 C1.112 |
| General frames (Sec 1.4), incomplete modal logics (Sec 4.4), completeness of normal modal logics with respect to general frames (Sec 5.5 until 5.65).
|
15 Nov 2015 Thursday |
Wekcollege 13-15 Goup A: SP 904 G0.18B, Group B: SP 904 G2.02 |
| The tenth tutorial sheet Tutorial 10
|
20 Nov 2018 Tuesday |
Hoorcollege 11-13 SP 904 C1.112 |
| Propositional Dynamic Logic, PDL. Regular frames, soundness of PDL, Fischer-Ladner closure, atoms.
(Section 4.8 until 4.81). |
22 Nov 2018 Thursday |
Wekcollege 13-15 Goups A, B and C: SP 904 G0.18B |
| The eleventh tutorial sheet Tutorial 11
|
27 Nov 2018 Tuesday |
Hoorcollege 11-13 SP 904 C1.112 |
| Completeness of PDL with respect to regular frames (4.81-4.91).
|
<
29 Nov 2018 Thursday |
Wekcollege 13-15 Goups A, B and C: SP 904 G0.18B |
| The twelfth tutorial sheet Tutorial 12
|
4 Dec 2018 Tuesday |
Hoorcollege 11-13 SP 904 C1.112 |
| Motivation for non-normal logics, neighbourhood frames and models, neighbourhood semantics,
two semantics of modal logic on monotone models, monotone bisimulations (Sections 1.3, 1.2.1 and 2.1 until Def 2.9 and without Def 2.5 and Thm 2.6 in Neighborhood Semantics for Modal Logic.)
|
6 Dec 2018 Thursday |
Wekcollege 13-15 Goups A, B and C: SP 904 G0.18B |
| The thirteenth tutorial sheet Tutorial 13
|
11 Dec 2018 Tuesday |
Hoorcollege 11-13 SP 904 C1.112 |
| The landscape of non-normal modal logics, completeness and canonical models (Sections 2.3 and 2.3.1).
|
13 Dec 2018 Thursday |
Wekcollege 13-15 Goups A, B and C: SP 904 G0.18B |
| The fourteenth tutorial sheet Tutorial 14
|
| | |