Modal logic and intuitionistic logic (Qüestions de lògica II; Official code: 363801)
Lecturer and course coordinator: Joost J. Joosten
The text below and in particular the dates need to be updated.
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 dedication. 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 410 of the Montalegre Building.
The lecture schedule is:
Mondays 11:00 -- 12:00
Tuesdays 11:00 -- 13:00
According to the official UB academic calendar the second semester starts 5--12 of February. (I do not know what it means to have a starting period stretching over more than a week.)
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.
Logic can be described as the art of 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
12/02 through 18/02.
We have spoken about the foundations of mathematics and how constructive mathematics came into existence. Further we have spoken about the characteristics of modal logic. We have seen that the difference between the actual and the future/possible other worlds plays a prominent role in both modal and constructive logic.
19/02 through 25/02.
We have spoken about formula induction and seen some worked-out examples. More in general, we have seen that any inductive definition comes with a corresponding induction principle to prove universal statements. We have given a Hilbert-style proof system for the basic modal logic K and proved some basic properties.
26/02 through 04/03.
We haven studied Hilbert style proofs, substitutions and translations of modal logic into propositional logic. Thus, we finished Chapter 1 and started Chapter 2.
5/03 through 9/03.
We sort of finished Chapter 2: proved the transitivity axiom in GL, proved consistency of GL and of K4, studied GLR, etc.
12/03 through 16/03. We have done some more examples of proofs by induction. Further we have spoken about the difference between classical and constructive logic.
19/03 through 23/03.
Natural deduction for propositional logic both classical and constructive.
02/04 through 06/04. Kripke semantics (the week after Holy Week).
9/04 through 13/04. Ana Borges stood in and did various derivations that were given as homework earlier on.
16/04 through 20/04.
More on Kripke semantics. Examples of non-derivability. Discussed soundness and completeness. Nuria's Proposition.
07/05 through 13/05.
Com bons catalans, hem fet coses . . . .
14/05 through 20/05.
21/05 through 27/05.
Semantics of Constructive logic
28/05 through 03/06.
Translation of IPC in S4 and soundness.
04/06 through 08/06.
Guest lecturer: David Fernández Duque on a proof of faithfulness of the embedding of IPC in S4. On Monday, June 4 we are in Aula 410 from 11-12 and on Tuesday, June 5 we will be in Aula 407 from 11:00 -- 13:00.
FINAL EXAM, TUESDAY, JUNE 12 FROM 11--13 IN AULA 409.
Question and answer