Modal logic and intuitionistic logic (Qüestions de lògica II; Official code: 363801, Year 2021--2022)
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 409 in the Montalegre Building.
The lecture schedule is as follows:
Mondays 11:00 -- 12:00
Tuesdays 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.
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: Friday, June 10, 12:00 -- 14:00, Aula 409;
Date and location resit exam: Wednesday, July 6, 12:00 -- 14:00, Aula 409.
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 14 -- 18)
We started the course. Each student gave a short presentation of him/herself as to background and interests. We then
started reflecting on the nature of logic and what is it subjectmatter repeating the same question in
the realm of mathematics which made sense in the light of Logicism.
From Euclid, Leibniz, Newto, via Frege and Russell we ended straight in the foundational crisis of the turn of the
19th century. We saw how Hilbert's programme to bedrock mathematics lead to the discovery of Gödel's Second Incompleteness Theorems.
This initially negative result actually marked the start of modern mathematical logic where we mentioned pioneers
as Russell (Type Theory), Weill (Predicativism), Turing (Turing progression), Gentzen (Ordinal Analysis) and Brouwer (Intuitionism).
We then started exploring intuitionistic logic under the so called Brouwer-Heyting-Kolmogorov interpretation.
The students are encouraged to perform some literature research (fancy way of saying that they are encouraged to browse the web) to
read for the sake of their interest on the above mentioned subjects.
(Feb 21 -- 25)
We made derivations in natural deduction using implication introduction and elimination and ex falso to get the
constructive implicative fragment of propositional logic. Furthermore we saw how the Brouwer-Heyting-Kolmogorov interpretation
gave rise to lambda terms and the Curry-Howard Isomorphism. Finally we discussed the RAA rule.
(Feb 28 -- Mar4)
We finished the presentation of Natural Deduction for proposicional logic, both classical and constructive. Next,
we presented Kripke semantics (future world semantics) for intuitionistic logic.
Here is a preliminary version of the reader. I propose that you play with
Exercises 3.4.1 -- 3.4.5. Theres is an Overleaf environment to post your answer. (Note that the exercises have a different numbering on Overleaf.)
If you have answered one question, just put your name to it. Others can learn from your answers and Latex code.
(Mar 7 -- 11)
This week has been taught by Moritz Müller for which many thanks. Here is what he wrote on what he has done:
1 Recall natural deduction with some examples. I stressed that it is difficult to find deductions, slogan "it is an art not a technique"
2 introduced definitions and examples for partial orders and trees. I defined trees as posets with linearly ordered predecessor sets and mentioned that this deviates from the usual definition with well-order (I didn't define well-order).
3 I defined Kripke models (K,\le,V) FOR POSETS (K,\le). I mentioned that this deviates from the reader -- see below how I made good for it. I mentioned the slogan "computational thinking" and showed how to read the truth definition as an algorithm and gave the pseudo-code. I made clear that the course does not presume knowledge of computability etc and stayed with informal usage of "algorithm" etc.
4: I proved soundness and stated completeness without proof.
5. I proved that for any poset (K,\le,V) there is a tree (K^tree, \le^tree,V^tree) such that the obvious equivalences hold. K^tree consists of increasing finite sequences from K.
6. I proved the finite model-property and inferred that intuitionistic validity is decidable (again with informal pseudocode)
(Mar 14 -- 18) Monday, Moritz finished his completeness proof and provided a proof of Glivenko's Theorem. On Tuesday, Joost discussed
how to use soundness and completenss in practice. We have seen various applications and practiced both derivations (where strategies are
suggested by considerations using soundness and completenss) and concrete counter models. Please, invent more exercises yourself for your fellow students
and include them in the Overleaf document.
(Mar 21 -- 25)
We had more exposure with Kripke semantics and saw various counter models. In particular,
we proved a lemma that tells us when not phi holds in some world in a Kripke model.
We also proved a lemma that tells us when not not phi holds in some world in a Kripke model.
We saw that three adjecent negations is equivalent in intuitionistic logic to a single negation.
The homework consisted in making counter models and are as always contributed in the large Overleaf document.
(Mar 28 -- Apr 1)
We continued working in Kripke semantics and for this week you are still encouraged to work on countermodels in the overleaf.
We spent quite some time on reflecting how one can prove universal statements. Finally we saw how each inductively defined
domain of discourse comes with its own induction principle.
(Apr 4 -- Apr 8)
We have done various arguments by induction using various induction principles.
For example, we proved by induction on a formula A that [] in a leave x of a Kripke frame a formala A is
forced if and only if A follows classically from V(x)]. For the homework I included some exercises to practice with
inductive reasoning.
Since April 11 -- April 17 is wholy week, and Monday, April 18 is a bank holiday, we will only have one day of class
in Week 9 and we will use that to do the MIDTERM exam: Tuesday, April 19 in the usual aula at the usual time.
I will be there 11:00 sharp so that you can use the full two hours.
(Apr 25 -- 29)
We introduced modal the basic logic K. Apart from a philosophical discussion on modalities and necessity, we
have seen Hilbert style proof systems. You are encouraged to make the corresponding exercises on Overleaf.
(May 2 -- 6)
We have introduced the modal logics K, T, S4, K4 and GL and have done various exercis with
Hilbert style proofs. In particular we have proven that GL contains K4. On Tuesday we also looked at Kripke Semantics
for modal logic and focussed on the differences with intuitionistic relational semantics.
(May 9 -- 13)
We have done more Hilbert style proofs. Then we have seen Kripke Semantics (frames and models). We have proven
soundness and stated without proof completeness of K wrt Kripke semantics. As such we have shown that certain formulas
are not provable in K. You are encouraged to make various exercises about semantics.
(May 16 -- 20)
Planned: frame conditions;
Moritz Müller taught the Monday and Tuesday class (thank you very much!!!).
Here goes his summary:
- I phrased the week’s program by the task: given L=K+(extra axioms), find a frame class F such that sound and complete
- I proved there is at most one choice of F. This proves soundness for all cases below (always explicitly stated).
- I did (T), (B) and (L), left (4) as exercise, and inferred the statements for S4 and S5. I always also gave the „dual“ formulation of the axioms.
- I left the (important) „Substitution Lemma“ as an exercise.
- For (L) I only argued with the very definition of „conversely well-founded“.
- I proved that conv well-founded is not first order
- I gave a philosophical discussion of the McKinsey formula and proved it is not first-order.
- I stated completeness for T,K4,B,S4,S5 without proof.
- I elaborated on the philosophical significance: the Kreisel-argument that completeness theorems nail down informal concepts of „entailment“.
- I stated weak completeness for GL without proof and mentioned that what we called „complete" is often called "strongly complete“.
- I proved GL is not sound and complete for any class of frames, so our task here has no solution.
(May 23 -- 27)
Planned: embedding IPC into S4,
We revisited the completeness and soundness theorems and gave some applications to obtain non-provability results.
Also, we proved that K proves A iff K proves Box A using both soundness and completenss. Finally we saw a translation
of IPC in S4. Next week we shall see that this translation is faithful, thereby ending this course.
All the exercises are now in Overleaf.
(May 30 -- June 3)
We saw how the translation of IPC in S4 works. First we took an IPC tautology and saw that it't translation gave rise
to an S4 tautology. Next we saw an IPC non-tautology and observed that this gave rise to an S4 non-tautology. Moreover,
the S4 countermodel looked very familiar. Rounding up.
FINAL EXAM: Monday, June 13, 9 -- 11, in good old Room 409
THIS DATE HAS CHANGED DUE TO ACCESS TO UNIVERSITY EXAMS IN SITU SO ALL ROOMS ARE RESERVED JUNE 14.
Question and answer
Question
Q:
I think I didn't understand why
falsum -> A can be formalize as the function of identity (lambda x.x).
Answer
A.: The BHK regards justification of A -> B as a constructive uniform map f sending an alleged proof a of A to a proof f(a) of B.
On the basis of BHK, the justification of falsum -> B is that any map will do, for example the identity.
Indeed, it will transform any proof of bot (none) to a proof of B. Universal quantification over an empty domain is trivially true also holds on constructive grounds.
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.