Modal Logic (Official code 569070)


The lectures will take place
Wednesdays: 16:00 -- 17:30;
Fridays: 9:00 -- 10:30.
In Aula 411 of Calle Montalegre 6. The start date is Wednesday, September 18.

The final grade is determined by
(A) Homework questions (this may include a mid-term exam); (60 %)
(B) Final Exam; (40 %).

All materials and assignments will also be placed on this page.
Joost J. Joosten is the lecturer of this course. The best way to contact me is by sending us a mail. You can also come around to see if I am in at the Montalegre building in Room 1095 with phone number +34 934031939.

The teaching assistant for this course is Eduardo Hermo Reyes. He shall be grading the exercises and is available for helping on theory and exercises outside class-hours. Also, he shall present some worked-out exercise sets. The best way to contact Eduardo is by sending a mail to the address that starts with "ehermo" followed by an underscore, that is a symbol "_", the goes "reyes" that an at symbol, and then the reversal of "liamtoh" and then the dot and then the reversal of "moc".

The literature will consist of among others, a reader written by Ramon Jansana with minor additions and corrections by J. J. Joosten and F. Bou Moliner. Please send me an email to request the password needed to open this document. I shall also write notes myself. Moreover, we shall work with Boolos's book, The Logic of Provability and likely some research paper.

The academic teaching-evaluation period of the the master for the first semester is from 12 September to 31 January. Our course comprises 42 contact hours, so 14 weeks.
Week 1 | | Week 5 | | Week 9 | | Week 13
Week 2 | | Week 6 | | Week 10| | Week 14
Week 3 | | Week 7 | | Week 11
Week 4 | | Week 8 | | Week 12

Week 1

(Sept 16 -- 20)
On Wednesday we had an introduction where we saw what the scope, advantages and disadvantages of modal logics are/can be. Then we gave some formal definitions, most notably of the logic K given in Hilbert style formulation. We saw a derivation in K and a non-derivation.

On Friday we have introduced the logics K4 and GL and have seen that the 4 axiom is derivable in GL.

The homework for the first week is short and easy: give a fully formal proof in K of []A --> []([](A /\ []A) --> A /\ []A). Preferably, you type this in Latex and hand it in to Eduardo before or at our next class on next Wednesday. Alternatively, you can write it on a plain sheet of paper and hand it in to Eduardo. Here are answers as given by Cory Knapp to the first exercise set. Note that, by invoking the lemma, it is no longer a fully formal proof. Personally I like to separate formulas by commas as to make clear that it is a list. The right-hand column with explanations, together with the line numbering makes reading very nice and easy.

Week 2

(Sept 23 -- 27)On Wednesday, we have proved consistency of GL, K and K4 and have seen that Loeb's rule and Loeb's axiom are equivalent over K4. An easy proof showed that GL plus reflection is inconsistent. We saw how K4 proves reflection for Loeb's axiom, and we have proven a very restricted form of reflection in K. Further we discussed normal modal logics and how Hilbert style calculi for them can be transformed in a natural deduction style calculus with restricted rules. Here are the notes for this week that I have written. Password available upon request. (Equal to the password to the other document.)

Week 3

(Sept 30 -- Oct 4) We have spoken on modal semantics and proved a basic soundness theorem. Next we considered a frame correspondence for K4. On Friday, we revisited the Completeness Theorem for classical propositional logic and discussed how parts of this could be used to provide a completeness proof for modal logic. We motived and defined the canonical model and proved some basic properties. The homework, due for next Wednesday, consists of Exercise 2.5.1 and filling in the proof of Lemma 2.2.3 in the new version of the reader.

Week 4

(Oct 7 -- 11 ) We have proven all the missing details of the completeness proofs (local and global). Note that the latest version of the reader now contains concise notation to deal with our two semantic notions (local and global) given a modal logic L. The homework consists of Exercises and (solving also and/or yields a bonus) and is due for Wednesday October 16.

Week 5

(Oct 14 -- 18 ) We spoken in more detail about frame validity and shown that each class of frames defines a nml. We have given frame-correspondence results for various logics. In particular we have seen a proof of the frame correspondence for GL based on Transfinite induction. (We also saw the elementary proofs.) We mentioned that it is undecidable whether or not a given logic has a first-order frame condition. We have seen that two consequence relations that are naturally associated with frame validity do not in general have all nice properties that we are used to. In particular we have seen hat local frame validity for GL is not compact. We introduced the notion of a logic being canonical and proved that all canonical logics are frame-complete. Here is the latest version of the reader. The homework consists of Exercise 2.6.6 and providing a proof of Lemma 2.3.7 and is due for next Wednesday.

Week 6

(Oct 21 -- 25 ) There will be an extra lecture on Thursday, October 24 from 18:00--19:30 in Aula 412.

Week 7

(Oct 28 -- Nov 1 ) We all work on the Midterm Exam. Friday November 1 is a bank holiday and the Wednesday was shifted to previous week. Friday, November 1 is a bank-holiday (all saints) on which the university closes.

Week 8

(Nov 4 -- Nov 8) On Wednesday we picked up the pieces after the midterm exam. We saw two ways of obtaining a differentiated model given an arbitrary model. Next we have proven that a finite differentiated model of a logic gives rise to a frame of that logic proving all the necessary lemmas leading up to that.

Week 9

(Nov 11 -- Nov 15) We studied the method of filtration in more detail and proved finite model property for T, K and K4. We have seen how finite model property implies decidability under some very reasonable additional conditions. We have discussed the first-order and second-order translations of modal logic. Here is the latest version of the reader. The homework for this week consists of filling out the details of Lemma 3.16 and 3.17 of the Jansana reader. The homework is due for next week Wednesday.

Week 10

(Nov 18 -- Nov 22) From here on we will start to read

Beklemishev, L.D. (2010): Kripke semantics for provability logic GLP. Annals of Pure and Applied Logic, v. 161, No. 6, 2010, p. 737-744. DOI: 10.1016/j.apal.2009.06.011.

The material will be presented in large by students who take the course for credits.

Week 11

(Nov 25 -- Nov 29)

Week 12

(Dec 2 -- Dec 6) Friday, December 6 is a Spanish bank holiday (Constitution's day) on which apparently also Catalan research institutes and universities are closed. The Wednesday lecture has been moved to Tuesday, December 3 from 17:00--18:30 in Aula 404.

Week 13

(Dec 9 -- Dec 13)

Week 14

(Dec 16 -- Dec 20)

Final Exam

Wednesday January 15
Aula 408 (Philosophy building).

Question and answer


Q I'm a bit confused as to why the following model isn't a counterexample to Exercise 2.5.2 for both K and K4: Take M={w}, with R empty and V(p) empty for some variable p (so p is false at w)---the evaluation of V on other variables makes no difference. Then it seems that is a model for which []p holds in all worlds, but p does not. In fact, p fails at all worlds.


A. A counter example will go very much along the lines that you are trying out now. But note, that the exercise speaks of PROVABILITY in L rather than valid in one particular model of L. Of course, we know by the completeness theorem that this is equivalent to being true at all models, but certain you cannot restrict your attention just to any odd model.


Q But it also seems that is a model of K4. Perhaps I'm wrong on this? We have all tautologies at w, all distribution axioms at w, all for any formula phi, []phi and [][]phi must hold in w, so 4 is validated and necessitation is "admissible" in our model.


A. Most certainly this is also a model of K4. We actually proved a frame correspondence for the 4 axiom although I have not yet included this in the notes.


Q Unrelated, in Definition 1.4.3, the word "logic" appears twice in a row before K4 and T. It seems like it could be intentional an intentional way to introduce "logic K4", but it definitely looks like a typo.


A. Great! Thanks! The first typo in the very preliminary draft of our book communicated to me by a student. Congratulations. I remember that when I was a student (and in the old days of course all was still a lot better) students were eager to report errors in readers and especially books under production :-) Your contributions are much appreciated and those contributing most will be duly acknowledged.