Modal logic and intuitionistic logic (Qüestions de lògica II; Official code: 363801, Year 2024--2025)

Organisation

Here is an academic year calendar of the UB.

The second semester for the graduate courses runs from February ??, 2025 -- May ??, 2025.
Lecturer and course coordinator: Joost J. Joosten
Teaching assistant: ???.

This is a course of 6 credits which corresponds to 45 contact hours and the students are supposed to dedicate at least 75 more hours of individual work. Since we do three hours a week, this will correspond to 15 weeks.
Official information regarding the course is published at the course pages of the UB. From there, one can redirect to the courses. The lectures will take place in Aula 406 in the Montalegre Building.

The lecture schedule is as follows:
Mondays 12:00 -- 14:00
Tuesdays 13:00 -- 14:00

We strongly advice students to follow the course in the so-called continua mode. Here we will have take-home exercises, a mid-term exam and a final exam.

Date and location midterm exam: TBA;

Date and location final exam: TBA.

The distribution of points in the final grade is as follows:

Take-home exercises: See teaching plan %

Midterm exam: See teaching plan %

Final exam: See teaching plan %

Students may also decide --even though we stronly would like to discourage this-- to participate in the so-called avaluació única.

Date and location avaluació única exam: June 2, 2025, 12:00 -- 14:00, Aula 406.

Date and location resit exam: June 30, 2025, 12:00 -- 14:00, Aula 406.

As mentioned, the lecturer is Joost J. Joosten and the best way to contact is by sending an email. You can also come around to see if I'm in: the Montalegre building in Room 4045 with phone number +34 934031939.

There will be no lectures on
?;
?
?

Objectives

Logic can be described as the art of valid reasoning. In the first part we will see how one can reason in a logical system that allows for modalities of propositions. These modalities can range from `necessary’ to `known’ . We shall have a special interest in the provability interpretation as well giving rise to a frame-work in which, for example, Gödel’s second incompleteness theorem can be formulated.

Further, we shall see how giving a constructive reading to the connectives gives rise to a different logic: constructive or intuitionistic logic. Naturally this requires a ontological stance very different from platonism/realism underlying classical logic. If time allows we shall see how contstructive logic can be related both to classical and to modal logic.

• To get an understanding how modalities add a subtle and complex dimension to reasoning;
• See a couple of standard modal logics and reason in them;
• Understand the ontological presupposition that underly constructive reasoning;
• Understand the ontological presupposition that underly classical reasoning;
• Understand the fundamental difference and tension between the two.
• Learn formal reasoning systems in Natural Deduction style;
• Learn formal reasoning systems in Gentzen Deduction style;
• Learn and understand proofs by induction
• Study modal semantics;
• Learning how to apply the soundness theorem to obtain non-derivability results;
• Learning how to apply the completenss theorem to obtain provability without actually exhibiting a concrete proof

THE REMAINDER OF THIS PAGE NEEDS UPDATING


Week 1	Week 2
Week 3	Week 4
Week 5	Week 6
Week 7	Week 8
Week 9	Week 10
Week 11	Week 12
Week 13	Week 14

Week 1

(Feb 6 -- 12)
We dwelled on what logic is about, what ontological assumptions are subsumed by classical logic and how this can be challenged and how this is challenged by constructive logic. In the tradition of Brouwer, this is often also known as intuitionistic logic refering the intuition involved in Kant's A priori synthetic knowledge of mathematics. We also discussed how various anomalies plagued foundations of mathematics and logic at the turn of the 19th century.

Week 2

(Feb 13 -- 19) We dealt with syntax of propositional logic and discussed proofs by induction for natural numbers and for formulas. Then we started to do derivations for propositional logic considering just the rules for conjunction and implication. I have written some notes on the theory we dealt with in class. The homework is posted on Overleaf and you got the link through the Campus Virtual. Let me know if you have any complications with that.

Week 3

(Feb 20 -- Feb 26) We continued doing Natural Deduction proofs. We have seen that all rules except RAA are both acceptable both from the BHK perspective and from the classical perspective. Finally, we have seen some proofs with RAA. There is new homework on the Overleaf.

Week 4

(Feb 27 -- March 5) We have done more exercises with Natural Deduction and seen examples of the Curry-Howard Isomorphism. You can consult a first draft of the reader . The password needed to open the pdf will be sent to you by mail through the Campus Virtual. There is some new homework on the Overleaf concerning the Curry-Howard Isomorphism.

Week 5

(Mar 6 -- 12) We spoke about semantics and introduced the notion of Kripke semantics. After mentioning the soundness theorem we could establish some non-derivability results in IPC.

Week 6

(Mar 13 -- 19) We made some further exercises that involved Kripke models. We gave a full proof of monotonicity of the forcing relation. Inductive proofs are (hopefully) getting clearer now.

Week 7

(Mar 20 -- 26)

Examples of Kripke semantics at work.

Week 8

(Mar 27 -- Apr 2) Double negation translation.

Week 9

(Apr 10 -- 16) No class on Monday! Previous week was Easter holiday. On Tuesday, April 11 we will have at the regular time, at the regular place no class but rather the MIDTERM exam. The best way to prepare for the midterm is by making many exercises. There is a new reader of which you will have to study part of Section 3 and Section 6. Updated Reader

Week 10

(Apr 17 -- 23) We started on the modal logic part of this course. In particular, we gave the formal definition of a Kripke model and of truth of a modal formula at a world in a model.

Week 11

(April 24 -- 30) We have seen the definition of logic K and of Logic K4 and have done some basic proofs in the corresponding Hilbert proof systems.

Week 12

(May 1 -- 7) No class on Monday! Tuesday's class was given by Sofia Santiago for which many thanks Sofia! She wrote: We worked on Hilbert style proofs in K. We discussed some schema to simplify this process such as the composition of implication. We proved Lemma 1.4.2 and Exercises 1.6.5 and 1.6.19 and some additional exercises. Finally, the diamond modality was introduced as an abbreviation. Thus, we proved Exercise 1.6.20, which proof relies on the consistency of K (to be proved). Some more extra exercises of Hilbert style proofs were proposed as homework.

Week 13

(May 8 -- 14) We have done more exercises with Hilbert style proofs. Also, we have discussed how to make more exercises on the Overleaf. The idea is that students invent exercises for each other. Then, put your name to the exercises that you invented and they count as homework too. Of course, solving exercises also counts. We proved the soundness of the modal logic K wrt Kripke semantics. As an application, we saw that K4 is a proper extension of K.

Week 14

(May 15 -- 21) We introduced the logics T and S4 and proved soundness wrt their respective Kripke models. Next, we have proven the completeness of propositional logic and then gave a sketch how a completeness proof for K would work

Week 15

(May 22 -- 28) We have finished course in this last week. First, we mentioned the modal completeness for the four modal logics of this course: K, K4, T and S4. We finished by providing a faithful translation from IPC to S4.

Here is the final version of the reader. Please do consult the material that you need from here. Note that there is of course more material.

Week 16

(May 29 -- June 4) Monday was a bank holiday. On Tuesday we did a question hour to revisit all material covered. Also, we gave the skeleton of the second mid-term.

FINAL EXAM: June 6, 12:00 -- 14:00, our usual aula

Question and answer

Question

Answer

A.:

Question

Answer

Question

Answer

Question

Answer

Question

Q.: The meaning of the second item is to list all the normal logics that fulfils the statement? Is this also correct?

Answer

A. No, this is not correct. You should either prove that indeed it holds for any normal modal logic or otherwise find a particular normal modal logic for which the implication fails. Even though the answer is easy, the question is sligthly tricky...