Modal logic and intuitionistic logic (Qüestions de lògica II; Official code: 363801, Year 2020--2021)
Organisation
Here is an academic year calendar of the UB.
Lecturer and course coordinator: Joost J. Joosten
The text below shall be updated as we go along in our course.
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.
Also, official dates can be consulted here.
The lectures will take place in the aula 401 in the Montalegre Building. However, during the beginning
we shall be teaching in an online mode from BBCollaborate.
The lecture schedule is already known and falls in the so-called L6 time-slot:
Thursdays 12:00 -- 13:00
Fridays 11:00 -- 13:00
We strongly advice students to follow the course in the so-called avaluació úinca mode. Here we will have take-home exercises, a mid-term exam and a final exam.
Quim Casals Buñuel is the teaching assistant for this course. You can send your weekly homework exercises to Quim by mail.
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: 20 %
Midterm exam: 40 %
Final exam: 40 %
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: Wednesday, June 16, 12:00 -- 14:00, Aula 401;
Date and location resit exam: Tuesday, July 6, 12:00 -- 14:00, Aula 401.
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.
Objectives
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
(Feb 8 -- 12)
We have started an introduction to modal and to constructive logic and will first dwell upon particularities of modal logics.
A reader can be found here. The homework for the first week consists of getting some
version of Latex on your computer and write your first document in it by answering the elementary Exercise 1.6.13. You should send your
answer in generated pdf by mail (precise instructions will follow) before next week Thursday class.
(Feb 15 -- 19)
We have introduced the logic K and made some derivations inside a Hilbert-stye calculus for K. Furthermore, we dwelled upon the proof method
of induction. Every inductively defined set comes with its corresponding induction principle. The homework for this week consists of
1.6.3.
1.6.5.
1.6.15., and
1.6.16.
Quim has been so kind to provide a Latex template for you where you can generate your answerset in.
Here is the template in .tex format. You can compile it locally or in some online service
like Overleaf. When you compile it, the generated pdf will look like this. Thanks a lot Quim!
(Feb 22 -- Mar26)
We have seen many examples of proofs by induction. Be that induction for the natural numbers or induction for formulas or for proofs.
Any inductively defined set comes with its corresponding induction principle. We have defined Logic T and made the trivial observation that
K is included in T. Furthermore we have seen a proof that K is actually consistent using the verum translation into classical propositional calculus.
Homework will be postponed to next week.
(Mar 1 -- 5)
We spent some more time dwelling on inductive definitions. Also, it turned out that the notion and application of Hilbert style proof
was not entirely clear yet so we spent some more time with that too. After making our basis more solid, we proceeded to define the logics
T and K4. We spent quite some time understanding how modalities can be used to describe formalised provability and we defined the logics GLR and GL.
We have proven that GL extends K4. An update of the reader can be found here. This week's homework
consists of 1.6.14, 1.6.15 and 1.6.16. Please be aware that the numberings refer to the new reader excerpt and not to the old one!!!
(Mar 8 -- 12)
Friday's class was given by Quim.
We have introduced the introduction and elimination rules for implication and conjunction along the falsum elimination.
In class we have done proofs 1,2,4 and 5 from exercise 3.4.2. We have given a very brief introduction of disjunction elimination.
No homework this week.
(Mar 15 -- 19)
We have learned more on natural deduction. Furthermore, we have seen how to associate a Natural Deduction system to each Normal Hilbert Logic.
The homework of this week consists of Exercises 3.4.2 Items 1,3,4, 7 and 8 together with Exercise 3.4.3.
(Mar 22 -- 26 )
On Thursday we presented Kripke semantics (a triple so that...) and observed that any theorem of K is true in any world in any Kripke model.
This soundness theorem allows us to prove non-provability results and as an example we have seen that K4 is a proper extension of K.
On Friday, Ana Borges taught. She spent a lot of time on exercise 1.6.15, which was proving something by induction. Ana: ``The induction proof ended up not being the problem, the first problem was that they didn't know how to extend the definition (given for propositional letters) to formulas. Also, our first interpretation of the exercise was wrong, and we found a counter-example together. Then they suggested different interpretations or ways that the exercise could be changed to make it true and we finished with an interpretation we were happy with and that we used to prove the exercise. (The goal is to show something "for every formula", but we originally assumed it was for every modal formula, when actually it only holds for every propositional formula.)
Then I talked a bit about how if you don't use the principle of explosion nor the RAA you get minimal logic, and then we proved p \/ ~p together. ''
The homework to be handed in before our class on Thursday, April 8 consists of Exercise 3.4.5, Exercise 4.5.2, Exercise 4.5.4, and Exercise 4.5.5. Enjoy Easter!
(Mar 29 -- Apr 2)
Easter. No lectures.
(Apr 5 -- 9)
We zoomed in on Kripke semantics and addressed various doubts. As an example, we saw that K does not prove Box Box p --> Box p.
We observed that any world with no successors makes true Box falsum. We spoke on soundness its contraposition, on incompleteness, the finite model
property and decidability. Once we realised that we have completeness and soundness for modal logics, we realised that we
need a method to decided whether or not a modal model is a model of a modal logic or not. We have seen the frame-conditions for K4 and T giving us
a sufficient condition for validity on a model and a necessary and sufficient condition for validity on a frame. The homework for this week
consists of 4.5.13 (here you may use the properties of completeness and soundness as given) and 5.4.3.1.
(Apr 12 -- 16) We dwelled upon soundness and completenss and how they can be used in Exercise 4.5.13. We created, for
the purpose of practicing, some more countermodels. We spoke on frames and announced (without proofs) that the logics that we
are interested in are all frame-complete (K, K4, T). The homework for this week consists of Exercise 5.4.3 Items 2, 3, and 4.
(Apr 19 -- 23)
Friday in Saint George so there are no lectures. On Thursday we have spoken more on frames and on modal completeness and applications.
Next we moved to an informal treatment of semantics for constructive proposicional logic.
We spoke on the philosophical fundaments of constructive logic. The exercises consist of 3.4.4. You should say for each proof
if it is constructive or not.
(Apr 26 -- 30)
On Thursday we looked at Kripke semantics for intuitionistic logic. The Friday lecture consisted on focussing on exercises and
address various questions from the students and this session is provided by Quim. Here is the new reader.
The homework for this week consists of Exercise 7.4.2. Item 2. Apart from giving the countermodel, you should briefly explain
why it is a countermodel.
(May 3 -- 7)
We have seen more examples of Krikpe models for intuitionistic logic and dwelled on the differences between modal and intuitionistic Krikpe semantics.
Also did we make a start on a first so-called double negation translation of classical logic into intuitionistic logic.
The homework for this week consists of Exercise 7.4.2, Items 7 and 8.
(May 10 -- May 14) We focussed on the double negation translation. Homework for this week consists of Exercise 7.4.3.
(May 17 -- May 21) We introduced the logic S4 and mentioned completeness w.r.t. finite, rooted, reflexive and transitive frames.
Furthermore, we agreed upon a grading protocol and the students received a mail about this via the mail service
of the campus virtual.
We finished Chapters 7 and 8 of the reader. The last homework exercise exists of Exercise 8.4.2.
FINAL EXAM
The final exam consists of a collection of additional exercises and is due for Friday, June 17 (aoe).
Please be aware that the exercise numbers refer to the NEW VERSION OF THE READER.
Here goes the selection of exercises:
Exercise 1.6.20.1;
Exercise 2.4.3;
Exercise 3.4.8, Items 1, 2 and 3;
Exercise 4.5.4, Items 1, 2, 3 and 4;
Exercise 5.4.8.1;
Exercise 7.4.2, Items 5 and 6;
Exercise 8.4.3.
Question and answer
Question
Q:
In Elementos de lógica formal, Jansana et al. inductively define Form (for classical propositional logic) in the following way:
Toda letra proposicional de L es una fórmula.
Si A es una fórmula, ~A es una fórmula.
Si A y B son fórmulas, entonces (A ^ B), (A v B), (A -> B) y (A <-> B) son fórmulas.
This is different from the way in which we defined Form. Our definition didn't include (A <-> B), and it did include (unlike Jansana's) \bot and \top. I guess that we don't really need to include (A <-> B) since it is equivalent to (A -> B) ^ (B -> A). Moreover, adding \top and \bot is not a complication, since we could "obtain" (I'm not sure if it is the correct way to phrase it) \bot with any CPC contradiction, such as e.g. p ^ ~p (something similar applies to \top, which could be easily "obtained" with any CPC tautology, such as e.g. p -> p). Is this right?
On the other hand, which is the "standard" inductive definition of Form? Jansana's or ours? Which reasons are there in favour of picking any of those, or is it a matter of preference?
Answer
A.: Over classical logic various connectives can be interderived as we know. So, indeed it does not really matter which set you take as
long as the set is, what is called, truth-functionally complete. Likewise, as you observe, the logical constants can be dispensed with
since, for example, top has exactly the same behaviour as (p --> p).
So then, what is the standard definition? The answer is, there is none. Which definition you choose depends on your purposes.
For example, if you wish to prove things about formulas, then it would be nice if there were very few generators in your
inductively defined set. That means, few connectives. If your aim is succinct formulas to describe/define then it would be better to have
many connectives.
Moreover, if you do intuitionistic logic, there is no interderivability anymore. Disjunction cannot be expressed in terms of the others as we shall see.
Question
Q:
Can we do a ternary / trinary inference in natural deduction with {1) phi implies psi, 2) phi, 3) not psi | FALSUM}? Or we have to do it step by step {1, 2 | psi} and then {psi, not psi | FALSUM}?
Answer
A. The answer depends on the system of ND you are working with. The idea with formal logic is that you can only apply those rules which
are explicitly allowed. And other rules which are not stated in your system NOT. So, in the reader, the rule is not given so it is NOT allowed.
And indeed, you would have to go in two steps as you suggest.
Of course, if you wish to use the rule in your research, you can define your own ND system where it is included. However, then you will need
to reprove all your meta-theorems (soundness, completenss, Deduction Theorem, etc.) over again or prove some lemma that these theorems
are not affected by your extension.
Question
Q: I am finding some difficulties on Ex. 3.4.3 Item 2.
Up to the moment, I have found two incomplete derivations:
First: With the Open assumption ( not phi ), I can derive the desired formula.
Second: With the Open assumption ( psi ), I can derive the desired formula.
I am trying to obtain either a derivation with the open assumption ( phi ) or a derivation with the open assumption ( not psi ), then apply Disjunction Elimination. Mi first question is: Is this a good strategy? Which one is easier? The point is I am finding both hard to find.
Answer
A. Remember that this exercise concerns constructive logic. In that sense the strategy of disjunction elemination is a very bad idea.
In constructive logic, proving a disjunction is tantamount to proving one of the disjuncts as we shall see. It is good if you realise that bot
is just like any other propositional letter except that we can apply the ex-falso to it. I hope this helps.
Question
Q. My second question is if we can use (p or not p) as an open assumption when applying Disjunction Elimination. If I could use RAA, I would just prove it, and follow the proof. Since we are in constructive logic I think we can't prove (p or not p).
Answer
A. Indeed, the excluded middle --(p or not p)-- is not valid in constructive logic, so you cannot use it. But even if you were reasoning in
classical ND, you cannot use the assumption outright. I mean, of course you can use the assumption but then it will be exactly that, an assumption
and if it is not discarded it will remain the status of open assumption. What you can do in classical logic is, repeat the proof of
p or not p, and then from there reason further.
Question
Q: Let S be a substitution of the form S : PropLetter -> Form_\Box. Let phi be a formula in Form_\Box. Does it make sense
to consider S(phi), since phi is a formula not just a propositional letter?
Answer
A: The way we define substitutions tries to capture the intuition that we have when thinking about "substituting things", namely, removing the "variables" from an expression and put something else instead. Our intuition says that a substitution should respect the "general form" of the expression, therefore we can assume that a substitution will respect the formula's structure and only act on propositional letters (the "variables").
For example, given S we can define S' : Form_\Box -> Form_\Box as
S' (falsum) = falsum
S' (p) = S(p)
S' (phi -> psi) = S'(phi) -> S'(psi)
... etc
Question
Q: After reading Chapter 4, I noticed that it is possible to create a simple model with a world that forces both φ and □¬φ (for example, the model M =⟨{x,y},{< x,y >},{φ→{x}}⟩) is such that x forces both φ and □¬φ).
Either
(1) The semantic definition of □ϕ (□ϕ is true on x when ϕ is true in all worlds accessible from x) is flawed,
(2) R always contains the identity of M (every world is accessible from itself),
(3) It is acceptable that a world forces both φ and □¬φ.
Which one is true?
Answer
A. Definitely the third is the right answer.
Other than just giving the answer let me write some additional observations that may be helpful.
First of all, I wish to observe that a valuation maps propositional variables to subsets of the domain.
If you speak of ϕ, then you suggest that this is a general formula. However, ϕ may happen to be a tautology in which case we cannot tweak
its truth value as we wish. Therefore, you better had written p instead of ϕ.
Furthermore, there is an easier model to make simultaneously φ and □¬φ true at some world x. Namely, take φ to be the propositional variable p.
Your new domain consists of a single world x with no successors at all (in particular x cannot see itself). Moreover we define p to be true at x
by setting V(p):= { x }. Since x has no successors at all, □A holds at x for any formula A, and in particular x forces □¬p.
Question
Q. Sometimes I have seen the notation
M=〈{x,y,z},{< x,y >,< y,z >},{< p,{y}>}〉
What to make of that?
Answer
A. This is standard notation. A Kripke model is a triple and triples or pairs or in general n-tuples are denoted using the sharp
angled brackets < > where the different elements of the tuple are separated by commas. Sets are denoted using the accolades { }
where the different elements of the tuple are separated by commas.
So, indeed, M=〈{x,y,z},{< x,y >,< y,z >},{< p,{y}>}〉is a tuple with three elements (which are called triples). The first is the domain which is the
{x,y,z}, the second {< x,y >,< y,z >} is the relation which is a set of pairs (the elements that are related to each other) and the third
{< p,{y}>} is a set with just one element which is a pair. Note that a set of pairs where each left element occurs only once is what we call a function.
So, indeed, the third element
{< p,{y}>} encodes a valuation that maps a propositional variable to a subset of our domain. Note, that to be really precise we should include for all
proposicional variables a value. For example by stating {< q,{ }>} for q other than p. Thus, any q will be mapped to the empty set.
Thus, any q other than p is true nowhere. And p is only true at y. We tend to omit the {< q,{ }>} for q other than p and only state
positive information. That is, where a proposicional variable is true with the tacit understanding that the other variables map to the empty set via V.
Question
Q: How do we interpret the "either one" expression on exercise 4.5.13? [Reader2] Should I choose one logic among K, T or K4 and then prove the statement? Or instead, should I consider L to be any of them, and so prove the statement for the three of them?
Answer
A. The latter. The statement holds for all three logics.
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...
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.