Modal Logic 2020/2021 (official course code 569070)
Organisation
Here is an academic year calendar of the UB.
The lectures will take place (tentative)
Wednesdays: 11:00 -- 13:00;
Fridays: 9:00 -- 10:00.
Calle Montalegre 6 in Aula 410. However, due to Covid-19 regulations we will be starting with online teaching only, hoping that we may resort
to regular teaching shortly.
The start date is Wednesday, February 10. Official schedule information can be found here
We observe that our current schedule is slightly different from the original and official one (official is Wednesday from 11:30 -- 12:30 and Fridays 9-11).
We decided on this change between all participants.
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. Esperanza Buitrago will be teaching assistant. The best way to contact me is by sending me an e-mail. You can also come around to see if I am in at the Montalegre building in Room 4045 with phone number +34 934037984.
We will have a final exam near the end of the semester. An eventual resit could be held after that.
The literature will consist of among others a reader to be distributed among the participants.
The modal logic course constitutes for 5 European credits and as such comprises 42 contact hours, so that makes 14 weeks, 3 hours each.
As mentioned, You can find the complete schedule here.
Likewise there is an official page with the course description.
(Feb 8 -- 12)
We have started our course and dealt with Chapter 1 of the linked document.
The homework of this week consists of Exercises 1.6.12, 1.6.16 and 1.6.17. Please hand it in before the next class on Wednesday by sending your
solution in pdf to Esperanza.
(Feb 15 -- 19)
We have finished Chapter 1 and started Chapter 2 introducing new logics (T and K4). We spend much time seeing that the 4-axiom scheme makes
sense in the provability logic interpretation and handwaived a proof of provable Sigma-1 soundness in PA.
For details you can check Chapter 3 of Boolos's The Logic of Provability.
The homework for this week consists of Exercise 2.4.11 to be handed in before the next lecture on Wednesday in pdf form in a mail to Esperanza.
(Feb 22 -- Mar26)
We finished Chapter 2 and made a quick start on Section 3: natural deduction for modal logics. No homework this week :-)
(Mar 1 -- 5)
We finished the proof that each Hilbert style proof system for a modal logic whose only rules are Modus Ponens and Necessitation is equivalent
to its corresponding natural deduction style proof system. Then we saw some examples of proofs in natural deduction, both in the regular ND system
and also in the modal setting. We then moved on to possible world semantics and proved soundness of the modal logic K. In particular we
have shown that T strictly extends K and so does K4. The homework for this week consists of Exercises 2.4.13, Exercise 3.4.2 Items 1, 4, 7 and 8.
You may wish to install a Latex package for typesetting proofs. I can recommend the one by Samuel Buss.
(Mar 8 -- 12)
We have done more with Kripke semantics. Some more on proofs in natural deduction. Also, we discussed why and how to move to local consequence.
No extra homework this week.
(Mar 15 -- 19)
We defined the canonical model corresponding to a normal Hilbert logic. Proved the deduction theorem for local consequence and some more good properties.
The homework for this week consists of Exercises 4.5.10 and 4.5.12.
(Mar 22 -- 26 )
On Wednesday we have defined frame validity. We have seen how the canonical model for T satisfies the frame condition. We have computed
the frame condition for K4. We have seen a model that is not reflexive yet satisfies all of T. On Friday we have given and proven the frame
condition for GL. Moreover, we have seen that T and K are canonical logics. We have announced that GL is not canonical.
The homework for over Easter consists of Exercise 5.4.3, 5.4.6, 5.4.9, 5.4.10, and 5.4.11.
(Mar 29 -- Apr 2)
Easter. No lectures.
(Apr 5 -- 9)
We have seen that GL is not canonical and that in general we do not have compactness of modal logics wrt to their class of frames.
We have observed that every normal Hilbert logic with the finite model property is decidable. We have given the proof that GL is
complete wrt finite, irreflexive and transitive models. We dwelled upon the following notions: canonicity, frame completeness and general completeness.
We have shown that second order logic is incomplete (leaving some details as an exercise). The homework for this week consists of Exercise 9.4.1 from the
updated reader.
(Apr 12 -- 16) This week, we addessed some missing definitions from the reader, like local derivability for an arbitrary normal modal logic.
Then we proved that the logic KH is frame incomplete. We spoke about the first-order translation of modal logic. The homework for this week consists of 4.5.13
and the following. Consider Creswell's model as exhibited in Boolos's book The Logic of Provability, Chapter 11.
We alter the model by making 0* irreflexive, that is 0* can no longer see itself. Can we still prove the results?
Briefly comment on the important steps. If a part of the argument breaks down and no longer works, point out where exactly.
(Apr 19 -- 23)
Wew spoke on the second order transaltion of modal logic. We have seen how modal frames define normal modal logics and that they are closed under arbitrary intersections.
Next we started with Bisimulations and saw that bisimilar points are modally equivalent. Thus, we have finished (almost all content of) Chapter 6 and the beginning
of Chapter 7 till Lemma 7.1.2. The homework of this week consists of Exercise 6.3.3.
(Apr 26 -- 30)
We have spoken more on Bisimulations and modal equivalence and the difference. We introduced n-bisimulations
presented the method of unraveling making it up to Lemma 7.3.2. The homework of this week consists of Exercise 7.5.1.
(May 3 -- 7)
After Joost settled some doubts on Wednesday, this week was taught by Ana Borges. She spoke on quantified modal logic and as such of
Hughes & Cresswell (1996), A New Introduction to Modal Logic,
we have covered Chapter 13 Sections "Modal LPC", "Semantics for modal LPC", and "Systems of modal predicate logic"; and the first section of Chapter 15: "Validity without the Barcan Formula".
The homework is: show that QK proves
♢ ∀ x φ → ∀ x ♢ φ
(May 10 -- May 14)
Ana continued her lecture series on quantified modal logics.
She started on Section "Canonical models without BF" of Chapter 15 of Hughes & Cresswell (1996), A New Introduction to Modal Logic,
circling back to Chapter 6 and Section "Canonical models for Modal LPC" of Chapter 14 for some
of the definitions and lemmas.
Here is the homework for this week:
Let Φ := ∀ x ♢ φ → ♢ ∀ x φ
For each of the logics QK, QK4, and QT, show either that Φ is provable, or provide a counter-model.
(May 17 -- May 21)
Ana finished her presentation on Quantified modal logic. In particular, she finished the completeness proof of GS w.r.t. inclusive models.
AFter this we treated with the metod of filtration. In particular we saw that filtration will yield differentiated models.
We fixed the boundaries of possible accessibility relations for the filtration and showed that any relation between
the boundaries will preserve truth values of modal formulas. We finished the most relevant content of Chapter 8.
The homework for this week consists of Exercise 8.5.8.
The final exam is agreed by students and lecturer to be in take-home format due to Covid-19.
It consists of the following selection of the updated reader:
Exercise 2.4.14
Exercise 7.5.6
Exercise 8.5.1
Exercise 8.5.12
Exercise 10.4.3
The resit will be TBA and will be rather similar in concept to the previous exam.
Question and answer
Question
Q. I have been trying to solve Exercise 4.5.10 My idea is to define formulas \phi_n such that if \phi_n is true in a world m, then if forces the structure of a binary tree of height n with root m.
I do not know if this approach is promising or not. If It is, I am facing three problems
1) How can I express the ‘preservation property’, i.e., if a propositional variable (except from p0) is true in a world n of the tree, then it is also true everywhere else above n?
2) While it is quite simple to force the split is the first step (the formula \neg p0 \wedge\Diamond(p0\wedge p1) \wedge\Diamond(p0\wedge \neg p1) works) it is no so simple to produce new branches in successive words.
3) I have made some progress in 1) and 2), but in general, when defining the formula \phi_{n+1}, I tend to use the formula \phi_{n} at least twice as part of the definition. This ends up in a exponential growth of the length of the formulas.
Answer
Your idea of forcing a binary splitting at each level is promising indeed. I like the way you isolate the technical problems you encounter.
This is a very good way of starting to organize your ideas and a first step of finding a good strategy to your solution.
At (1) I can indeed say: since the exercise does not consider transitivity you will have to repeat all your requirements for each level of successors.
So, if you want Property A. at all n future levels you will have to say Box A /\ Box Box A /\ ... Box^n A. That is not too elegant but grows linearly in the depth.
At (2) you may need to consider fresh variables. Also, you should be sure that your model cannot `'reuse'` worlds. So, that it cannot look back to
some earlier world. At (3) I can only say that you should carefully count and keep track of the number of copies. Enjoy working on it.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.