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.

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 |

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.

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!

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!

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.

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?

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.

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.

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.

S' (falsum) = falsum

S' (p) = S(p)

S' (phi -> psi) = S'(phi) -> S'(psi)

... etc

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?

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.

M=〈{x,y,z},{< x,y >,< y,z >},{< p,{y}>}〉

What to make of that?