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

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 8 -- 12)

Week 2

(Feb 15 -- 19)

Week 3

(Feb 22 -- Mar26)

Week 4

(Mar 1 -- 5)

Week 5

(Mar 8 -- 12)

Week 6

(Mar 15 -- 19)

Week 7

(Mar 22 -- 26 )

Week 8

Week 9

Week 10

Week 11

(Apr 19 -- 23)

Week 12

(Apr 26 -- 30)

Week 13

(May 3 -- 7)

Week 14

Week 15




FINAL EXAM

TBA.

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.