MLoM Introduction to Modal Logic

Autumn 2010, ILLC, Universiteit van Amsterdam.

News

Course plan

The current plan for the course. First period until the autumn break: train you in basic concepts and basic theory. Second period: special topics, probably on agency (knowledge, belief, action, information dynamics, and games). We will take you to the border of current ILLC research in some of these cases.

Your feedback is always appreciated: either to u.grandi(at)uva.nl, or johan(at)science.uva.nl. In particular, if you have some new thoughts on the material, or topics that are inspired by it.

Course Log

Dynamic Logic

Week 13:

General Revision

Final Homework .

Dear All, We did a very general tour today of what the course has been about. We looked at some ways in which basic theoretical themes (Part I) returned in the bunch of logics for agency (Part II), which together bundle up quite a bit of the separate topics that have traditionally formed the area of 'philosophical logic'. Examples: language extensions (and matching notions of bisimulation), lifting completeness proofs to non-routine areas like conditional logic or propositional dynamic logic. New theoretical themes were briefly considered as well, with two favourites from recent decades: complexity of logic combinations (depending on how we put components together), and modal fixed-point logics for recursive definitions. For a further look at modal logic as done at ILLC right now, look at the 5 dissertations defended this year by Cedric Degremont, Gaelle Fontaine, Amelie Gheerbrant, Nina Gierasimczuk, and Jonathan Zvesper. Also relevant are those of Lena Kurzen and Fernando Velazquez next year.

For the moment, I wish you good luck with homework and papers.

Johan van Benthem

Week 12:

Games

Exercises set 12.

We started with the definition of finite games in extensive form, giving some examples, among which modal evaluation games (on finite models). Evaluation games are a specific type of extensive games, namely those with only two players (verifier and falsifier) whose preferences are fully "incompatible": if verifier wins then falsifier loses, and vice-versa. For this class of games (two-player zero-sum) we have seen how the set of winning positions for each agent, can be recursively defined as the least fix-point of a modal formula. As the root of the game will belong to the winning positions of only one of the two players, this proves that such games are determined (Zermelo's theorem). The inductive construction of the winning positions corresponds to running a back-ward induction algorithm on the game tree.

In the second hour we illustrated the notion of backward induction on non zero-sum games too, where players' preferences are taken to be total preorders. We have looked at the centipede game as an example. The backward induction algorithm produces two sub-relations on the tree. One, is the actual backward induction path, i.e., the solution of the game, the other one is the relation consisting of all links representing "rational" choices according to the algorithm, i.e., the backward induction strategy profile. It turns out that this latter relation, which we called "best", can be characterized by a modal formula (with Kleene star) in terms of a frame correspondence result. Finally we have sketched how the first relation, the backward induction path, can be obtained as the result of iterated announcements of a property of rationality saying, roughly: "the current point has not been reached via any strictly dominated choice".

Modal logic and games is an extremely lively research area at the moment, witness international conferences such as: - LOFT: http://www.econ.ucdavis.edu/faculty/bonanno/loft.html - TARK: http://www.tark.org/

Week 11:

Logic of information and information change

Exercises set 11.

We have reviewed the landscape of logics for information and information change that we have introduced in the last weeks, classifying them as static/dynamic logics of hard/soft information. We have focused in particular on the epistemic doxastic models for the static representation of beliefs. We have reviewed the definitions of the different operators (safe belief, belief and conditional belief) emphasizing how they behave in the presence of different conditions over the plausibility relations. We have briefly pointed at some features of the definition of conditional belief in terms of safe belief, and at some technical issues concerning the axiomatization of the strict part of the plausibility relation.

In the second hour we have focus on dynamics, reviewing briefly public announcements and discussing extensively radical upgrade. We have shown how radical upgrade can be defined as an operation of relation change, applied on the plausibility relation, which makes use of PDL constructors without Kleene star. We have seen how such definition allows a natural computation of the reduction axiom for safe belief under radical upgrade. This method is generalizable to any relation change operation whenever defined by PDL constructors without Kleene star.

Week 10:

Open problems in PAL (by Wes Holliday).

Exercises set 10.

*Wes Holliday* (wesholliday@stanford.edu) started off with some open problems around Public Announcement Logic. The Stanford Dynamics Group has recently given syntactic characterizations of the learnable formulas, and also of the schematic PAL-validities, both for the single-agent case. The given references tell you about their results and proofs. Feel free to solve the multi-agent versions!

We then reviewed the material on beliefs. Doxastic logic started with a special accessibility relation for belief, contained in the epistemic accessibility relation. But we preferred *plausibility orders* on epistemic ranges, since these are concrete, and also naturally model conditional beliefs. Our assumption was that these orders are uniform on a range, a more general semantics would make them world-dependent. (Such ternary relations are the typical style of similarity models for conditional logic.)

Our dynamic logics identified important actions, described formally in terms of model change, which then enrich the language to a dynamic-epistemic one via action modalities, for which we wrote reduction axioms. The latter give, you might say, *relative completeness* w.r.t. the complete base logic that we started with for knowledge or belief. Actually, things are a bit more tricky: reduction axioms sometimes suggest enriching the base language, as with the axiom for [!P]B phi, which needed conditional belief. Similar things with the reduction axiom for common knowledge.

Let us now take soft update up(P) as our running example. We need reductions axioms for [up(P)]B phi, plus, when you see what is used, [up(P)]B^{psi} phi for conditional belief. But there is also still the combination [up(P)]Kphi. Since plausibility change does not affect the epistemic relations, the latter is just an operator commutation: [up(P)]K phi <--> K[up(P)] phi. While this looks simple, we did see that it really expresses something strong. E.g., the commutation law K[a] phi <--> [a]K phi is not valid for all our actions and knowledge about their effects.

Then one of these cases where technical and philosophical developments occurred in parallel. Belief and conditional belief can be *defined in terms of the base modality* over plausibility orderings. (Precise formulas in your homework.) So we can translate our belief logic into modal S4. This brings immediate benefits, like axiomatizability and even decidability. What it does not tell us what a complete proof system looks like, since a 'modal base proof' might contain auxiliary intermediate formulas that are not doxastic. E.g., completeness proofs for conditional logic can be hard. (Similar point in predicate logic: you have learnt completeness for the usual axiomatization that deals with single quantifiers. This does not automatically tell you what a separate complete logic would be for a language of two-quantifier combinations. Some very interesting work is taking place on that right now.) The parallel philosophical discovery: in addition to knowledge and belief, there are other relevant attitudes, such as safe belief, intermediate between knowledge and belief, whose motivation is dynamic: it is robust against receiving new true information.

Then we made our transition to program structure. Muddy Children, the pet of dynamic-epistemic logicians, actually shows all major program operations in its scenario: sequential composition (;), guarded choice (IF THEN ELSE), and guarded iteration (WHILE DO) - and if you wish, even parallel action: 'speaking simultaneously'.

Logic of action arose from logic of programs, since the 1960s. A program, or action in general, may be viewed semantically as a set of transitions between states of a computer, or the world. Then 'Hoare correctness assertions' about basic programs a are essentially modal formulas phi --> [a] psi. So the base logic of action is multi-modal K. But Propositional Dynamic Logic then adds complex action structure, using a mathematically more elegant version of the above repertoire to create programs pi from atomic actions a by the operations ; , U (choice), and arbitrary finite iteration * - plus test actions ?P on formulas P. For more details, see the book chapter on Dynamic Logic, and the explanations that will be given by the assistants.

This language has both formulas: expressions for properties of states, and programs: expressions for actions. It is still modal, because all its formulas are invariant for bisimulation. It is also still modal in that validity is decidable, and there is a perspicuous set of axioms reducing out program operations. The only operation that does not reduce out really is iteration: the reason is that here is where *recursion* enters the logical language, we really want valid 'fixed-point equations' for *. (Finding PDL proofs for even simple validities is a nice game!)

Some of you worried: how does this relate to dynamic epistemic logic, where action was *model change*? What we do in PDL is step up the abstraction level: atomic actions are arbitrary transition relations between arbitrary states. What the logic analyses is just the behaviour of such arbitrary actions, giving us a 'core logic' of computation and general action. (Thus huge abstraction beyond programs in specific computer languages was a brilliant move.)

Now you can see PAL as a special case: 'states' are epistemic models, 'atomic actions' are announcement updates. (Please do not read the following if you feel dizzy already:) Now what happens when we *combine PDL and PAL*, looking at complex iterative 'conversational programs' such as "keep saying nice things to this person until he releases the money"? Two simple logics put together: so a simple result? The answer is NO: the logic of PAL plus complex programs is undecidable, and even unaxiomatizable. The reason: there is so much mathematical richness to the concrete 'update universe' that its extended logical theory is very complex indeed. (If you still find this strange, try to think of analogous phenomena in general logic.)

Final issue: why is there no *dynamic predicate logic*, given that the original program examples start from atomic instructions like 'x := t' : 'set the value of variable x equal to the value of t'? The reason: if we combine propositional PDL with predicate logic, we can define the natural numbers up to isomorphism: the logical complexity becomes that of True Arithmetic. (Still, I sometimes wonder whether there is no more general semantics for quantified PDL that would remain reasonable.)

Coming Weeks: Johan van Benthem will do one small and one large Review of the course, Davide Grossi will tell you about two more topics: preference logic, and then games, where knowledge, belief, preference, and action come together, as we already discussed last week.

Final Projects: in addition to the topics you have already chosen, you can also do 'site visits' with some of our Ph.D. students with modal logic dissertations right now, e.g., on learning theory, modal logic and games, or dynamics of inference and awareness. Davide's own work on, e.g., argumentation is also very relevant.

Week 9:

Belief, conditionals and revision

Exercises set 9.

This week started with a general perspective on what is happening in this part of the course. While 'Philosophical Logic' has consisted of a large family of logics for separate notions, such as knowledge, action, conditionality, or obligation, these all come together in one natural setting when we consider *agency*, as done in computer science or game theory. We saw how analyzing even the simplest little game with two moves leads you to think of a mixture of: action, knowledge, belief, preference, and counterfactuals.

Then we looked at the resulting research program, developed in a number of chapters. We need states of agents with the relevant attitudes: knowledge, belief, preference, etc. (In computer science, the well-known 'BDI framework' says that we also need 'intentions'.) Then we need to study the acts of change for these, often information- driven: public announcements, questions, and others (say, commands). This gives a picture of single *state changes*, the heart of the dynamic logics that we are presenting, as analyzed in their 'reduction axioms'. With this building block, two major further steps arise. The first is *temporal perspective*: many consecutive update steps form larger discourses, learning protocols, procedures of inquiry. These have logical structure of their own, often studied in 'temporal logics'. The second extension is from lonely individuals to socially inter- acting individuals, to the creation of *groups* as bona fide agents.

We could see all this coming in our simple motivating example of a question and an answer. Knowledge about facts and about others, state change leading to change in truth values: Questioner did not know the answer before, but afterwards, she does, and the group achieves common knowledge. But also, questions usually suggest a larger purpose: they are only part of a longer temporal scenario.

How to implement this technically? We first identify a best available logic in the literature, and then 'dynamify' it by adding an explicit account of its underlying dynamic actions. Example: start with *epistemic logic* EL as account of agents' semantic information. This is a concrete version of our earlier abstract modal logics. The logic (if we take equivalence relations, the simplest version) will be modal S5 for each agent. Now we add actions of *public announcement* (totally reliable public information, say words from an Authority, or making a reliable public observation). We define the informational effects abstractly as model change, and then write a dynamic epistemic logic that can talk about these changes explicitly. It is axiomatized mainly by finding the key reduction axioms for knowledge after announcement: [!P]Kphi <--> (P -->K(P-->[!P]phi)). Note the recursion here.

Digression: reinterpretation. This is far from Hintikka's original interpretation of the grand purpose of EL as analyzing Knowledge. We switched to semantic information, much more down to earth. But this is often the key to scientific success of a theory: do not let yourself be tied down by what the inventor wanted with it. You want a guide to take you to the highest mountain peaks, but you don't want her to tell you how to appreciate the scenery. (We *can* return to epistemology later, and many people are doing that right now, but then with the new tools of dynamic analysis.)

Digression: interpunction. PAL really makes the exclamation mark ! a logical operator, just like &, v, ¬. Likewise, dynamic logics of questions make the question mark ? a logical operator. The idea that interpunction is a major intellectual achievement close to logic, growing slowly over millennia of writing language, is appealing. (I first learnt it in a book by Ray Jennings, a Canadian logician.)

PAL is deceptivey simple. It actually raises quite tricky technical problems, where one needs to 'think mathematical logic'. Wesley Holliday from Stanford will give us a cameo performance next week, telling you about recent develpment on two fronts: the 'schematic validities' of PAL (closed under substitution) and the syntax of 'self-refuting and self-fulfilling announcements'.

The above two extensions. PAL supports *social* group knowledge, but finding the right reduction axioms for common knowledge has taken some thinking. See the textbook, and Umberto's tutorial. PAL also fits with temporal perspective. The puzzle of the Muddy Children illustrates *temporal* scenarios where interesting things happen 'in the limit': e.g., knowledge arises in the limit of truly announcing your ignorance. (repetitions of true !P can eventually lead to truth of the negation ¬P: so-called 'self-refuting' scenarios.) (BTW, Muddy Children also involves all basic operations of *programs*, a pointer to the dynamic logic of next week.)

Then we went to *beliefs*. I first waxed exstatic over the positive value of having beliefs in addition to knowledge, as the driver of all practical action. (I may have been too critical of Socrates, who wanted us to replace beliefs by knowledge - whereas I said that jumping to beliefs is the more creative ability, so we should try to acquire more beliefs!) This is also the sense of 'learning by trial and error' that Popper has emphasized, which is basic to formal learning theory: we constantly conjecture things that can then be falsified by new evidence, and replaced by new hypotheses. While knowledge update is associated with acts like inference and observation, we now crucially also have another cognitive, and I would say, logical ability that keeps beliefs attuned to the evidence: acts of *belief revision*. (This was studied deeply by logicians like Peter Gaerdenfors.) BTW, Nina Gierasimczuk will defend her Ph.D. thesis linking dynamic-epistemic logic and learning theory this December.

We follow the same methodology as before. First we find a substantial static logic of belief, which we did by enriching epistemic models with *plausibility orderings* on agents' semantic ranges. We talked about the complete static logic of belief as truth in the most plausible worlds in a range. Then we did dynamics of hard information: how do beliefs change under public announcement? The key reduction axiom [!P]Bphi <--> (P --> B ^{P}[!P]phi) then required extension of the static language with *conditional beliefs* (dynamics can influence statics), and we need a reduction axiom for conditional beliefs as well - which we can give. This setting already contained non-trivial scenarios, such as 'cheating with the truth': true information can give an agent false beliefs. In line with this new epistemic notions come up, such as *safe belief* that cannot be shaken by true information. (Actually, this is a simple base modality.)

But then we made a major step. Most information is soft, as we saw in the example of the Beijing Gate in 1911. Soft information Up(P) does not eliminate ¬P-worlds from the current model, but it *upgrades* the P-worlds. These now come on top in the plausibility order, the ¬P- worlds lie below, but within the zones, the old order reigns. Again we can write complete dynamic logics DDL for this, with reduction axioms for [up(P)B^{phi}psi for up(P) and many other forms of upgrade. But soft updates are more complex than public announcement. We are now looking at *general model transformations* whose effects can be tricky. For instance, repeated soft updates can result in cycles where you keep oscillating between the same plausibility patterns. Thus, the temporal limit behaviour is somewhat exciting, which again connects up with results in formal learning theory. Also, if the mathematicians among you want an open problem: I know of no good reduction axiom for *common group belief*.

OK, that was quite a lot. I wish you good luck in digesting it. If you have problems, do talk to Umberto, Davide, or me. I am also happy to do another review session at some stage.

Something about the student comments (I hope I remember all):

* "The picture for the research program of agency *itself* looks like a modal model, with actions of information change between epistemic models." This is just right! I call this The Supermodel, and its theory is very interesting. For instance, if we restrict the available announcements in PAL, we get 'protocol versions' of dynamic-epistemic logics, whose logic changes from PAL (see the 2009 Stanford dissertation of Tomohiro Hoshi for this).

* "What is the source of the plausibility ordering?" This is a central issue everywhere: how do we choose our models? In simple epistemic scenarios, like card games, the choice of epistemic accessibility often seems very natural, but it can also be much more controversial. Compare the well- known difficulty in probability theory of how to choose your 'prior', the initial probability distribution of a scenario. I cannot explain the choice of the initial plausibility order for you: some good taste, and good luck, may be needed. But after that, the dynamic upgrade view does tell you how that ordering gets changed systematically by new triggering events as we proceeed. This is already much more information about it then you would get in traditional philosophical logics.

* "Soft upgrades have tricky effects: the order in which you state them matters." This is absolutely correct. One typical hall-mark of a dynamic approach is *order-sensitivity*. Think about it, this is true of conversation, and any action. Being able to deal with it is a typical cognitive skill. And actually, order of updates matters even in PAL, as the book explains. But the logic gets it all straight. In particular, [!P][!Q]phi is not in general equivalent to [!Q][!P]phi.

* "Is this philosophy, mathematics, computer science?" I would say it is *logic*. But very diferent aspects of logic play a role. Philosophical logicians often are first, proposing crucial new ideas such as common knowledge. Then mathematical logicians come and do the analysis much more neatly, discovering hidden depths. Then one can take these technical results back to philosophy, and see if they have some new broader insights to suggest. and so on: this is a very productive historical cycle! And in all this, you benefit a lot from an open mind for related developments in other fields: linguistics, computer science, economics, wherever.

PS1 The physics on the blackboard when we started: I said that the picture of the circles was relevant. It is. If you have a connected plausibility order for belief, one good graphic way of picturing it is in concentric circles of lower to greater plausibility. Many people find that helpful, though abstract orders are fine, too. But actually, there is a bit more. The simple equation on the board was about 'kinetic' and 'potential' energy (recall the formulas 1/2mv^{2} and mgh that I erased). This has been an issue on my mind for a while. In physics, 'kinematics' just describes the observable movements of bodies, whereas 'dynamics' describes the forces that cause the kinematics. Can it be that our dynamic logics like PAL, DDL are just 'mental kinematics'? In that case, what is the True Dynamics? I now think that the latter comes from intentions and preferences, and generally, the interplay of information, evaluation and intention. Then assumptions of 'rationality' as in game theory might play a very similar role as the 'bridge laws' of physics connecting forces and movement.

PS 2 Has there ever been a single act of 100% reliable hard information in human history? One candidate would be a pronouncement by the Pope when made 'ex cathedra'. According to catholic dogma, these statements are infallible: http://en.wikipedia.org/wiki/Papal_infallibility. Just think of what this might do for famous open scientific problems!

Week 8:

Epistemic logic and update

Exercises set 8.

This first week after the autumn break, we started a sequence of chapters on agency. *Epistemic logic* is a concrete interpretation of modal logic where links between worlds encode agent's *semantic information*, the current set of options for what might be the actual world. Fewer options, more information. Originally designed for applications to epistemology, this is now mainly used in multi-agent scenarios of communication. We saw how for the case of questions and answers. The logic for each agent is S5, interaction axioms for different K-i K-j would only hold under special contsraints on the relations for the agents (computable via frame correspondences). One such special case: epistemic models for matrix games (see Friday session), where the relations satisfy a natural confluence property. New direction: groups as informational agents, *common knowledge*, not definable in the old modal base language, not first-order, special axioms having to do with induction and fixed-points ('reflexive equilibrium'). Still modal: EL + common knowledge is invariant for bisimulation. (Even streamlines the model theory: each finite model is definable up to bisimulation in the language EL-C.) Common knowledge in lots of disciplines since 1960s. Next, information comes with change: *update by public announcement*, totally reliable public 'hard information'. !P eliminates the worlds that currently do not satisfy P. Truth value change may occur for epistemic formulas, since the model changes. Now put these actions inside the logical language with appropriate syntax. Semantics of the system PAL looks at the changed model after an update: M, s |=[!P]phi iff if M, s |= P, then M|P, s |= phi. *Completely axiomatizable* via recursion axioms stating basic properties of the update process, and allowing us to compute what new knowledge an agent will have in terms of (conditional) knowledge that she had before. Further features [we did not get to these in class]: still bisimulation-invariant, reduction axiom for common knowledge a bit tricky (needs extension of static base language EL-C to 'conditional common knowledge'), further operations for complex conversation: e.g., in Muddy Children puzzle, find consecutive assertions, simultaneous assertions, conditional choice between assertions, repeated assertions (WHILE DO loops). General systems of this sort also deal with *private information* where not all agents make the same public observation. *Dyamic-epistemic logic DEL*.

Week 7:

General Review: Wednesday 13-15. Friday 9-11 exercise session.

Exercises set 7.
Week 6: Extended Languages. Exercises set 6.

I have introduced and defined the standard translation ST from formulae of the basic modal language (ML), to formulae of the language of first-order logic (FOL). The standard translation of a modal formula is equivalent to the formula itself, as we can see from the "Switch Lemma", which I have formulated for both the cases of truth in a pointed model, and truth in a pointed frame (second order notion!). Essentially, what the the standard translation does, is to make explicit the sort of quantification patterns hiding behind modal boxes and diamonds. The set of all FOL formulae which are the result of the application of ST to some ML formula defines what is called the Modal Fragment (MF). So MF is included in FOL, and this allows us to import meta-logical results from FOL to ML, such as Compactness, Loewenheim-Skolem (although we have seen earlier that ML does better thanks to the finite model property!), and Craig's Interpolation (with the important caveat that the interpolant need not be modal!). I have also given examples of FOL formulae which cannot be expressed via ML formulae (using an argument via bisimulation), which shows us that the MF is not only included, but strictly included in FOL. The question then arises of whether the class of FOL formulae which are equivalent to some modal formula (i.e., equivalent to the standard translation of some modal formula) can be characterized. The question is answered affirmatively by the Modal Invariance Theorem (Van Benthem Characterization Theorem) which characterizes such set as the set of FOL formulae which are invariant for bisimulation. I have given a sketch of the proof trying to show you the general lines of the argument. In the second hour we have looked at enrichments in expressivity of the basic modal language. The aim behind this is to gain the ability to distinguish models that are indistinguishable from the point of view of the basic modal language (more granularity in the language!). So, in order to express FOL properties such as "the accessibility relation is not empty" I have introduced the universal modality. We have seen its semantics, its notion of bisimulation (total bisimulation), its standard translation and its axiomatics (with a sketch of how to get things right in the canonical relation once we try to prove completeness). I have shown how certain FOL formulae now become expressible. Along the same line I have then introduced the difference modality, which allows for even more expressivity (we can now distinguish between irreflexive and reflexive models for instance). Also for this modality we have briefly looked at its characteristic type of bisimulation and its axiomatics. Then, with a final giant leap I have sketched the full language of hybrid logic (whose fragment without binders, I have shown, was already expressible by means of the difference modality). In the end I have observed how the increase in expressivity determines an increase in complexity (the satisfiability for ML with universal or difference modality is more complex than in the basic ML) up to even losing decidability, like in the case of hybrid logic with binders.

Week 5: Correspondence Theory. Exercises set 5. Solution of Exercise 2 by Haitao.

This week we did correspondences between modal axioms and special properties of the accessibility relation, one of the typical features of modal logic. You should practice a number of cases to get the feel for it, then delve into the proof of the Sahlqvist theorem to see *why* this nice connection works in so many (though not all) cases. There is ongoing mathematical theory here (e.g., among the non-first-order cases, Lob's Axiom is better-behaved than the McKinsey Axiom in a precise sense), but that, though exciting, is a bit beyond the cope of this course.

PS Something left over from earlier weeks. "Not every infinite model has a bisimulation with a finite one." Several of you sent solutions (the assistants will give you bonus points for such initiatives). One easy solution: in a language with infinitely many proposition letters, give some root world infinitely many definably different successors. More interesting answers: finitely many proposition letters. I got two solutions based on decimal expansions of real numbers (only the rational numbers among them have finitely recurring periodic patterns of digits, encoded by proposition letters). There was also a solution on the natural numbers with successor, setting V(p) equal to the powers of 2. Then all numbers get a unique modal definition, and therefore, no contraction to a finite model is possible (since the latter can distinguish only finitely many worlds). My own solution: take the infinite hedgehog with ever larger finite branches from the root, used earlier in the proof that modal equivalence does not imply bisimilarity. Assume that this model has a bisimulation at the root connecting it to a finite model of n worlds. Then looking at the hedgehog's quill of length n+1 gives a contradiction, since the finite model would need to have a cycle, and the back-and-forth clause then runs afoul of the end of the quill.

Week 4: Chapter 5 of the book. Exercises set 4.

We have looked at the problem of describing the set of valid formulae of modal logic by means of a finite set of axiom schemata and inference rules (but note that, although there are only finitely many schemata, they have countably many instances!), that is, what we called an axiomatization (or Hilbert calculus). We have discussed the axiom system K and given examples of both a derivable rule of inference, and a provable formula, i.e., a theorem. This has illustrated how the key to formal proof often resides in the choice of suitable instances of propositional and modal axioms or of (already proven) theorems. In the second part of the lecture we went through the proof of adequacy of system K in some details. We have seen that soundness is rather easy to prove as it amounts to proving that axioms are valid (in the case of the distributivity axiom we saw that already last week by means of its tableaux) and that inference rules preserve validity. The case of completeness is more difficult and interesting as it shows that the very general notion of truth in every model (validity), implies the very concrete---and apparently unrelated one---of the existence of a proof in the Hilbert calculus K. We have proven this implication by its contrapositive, showing that any K-consistent formula has a model, therefore reducing it to a model existence problem. Here is how we proceeded. We tackled the model existence problem by constructing one, which we called the canonical model (Henkin construction, borrowed from Henkin's proof of completeness of FOL). This is built out of the set of all maximal consistent sets (MCSs) of modal formulae. Thanks to the Lindenbaum Lemma we could then be sure that any K-consistent formula is contained in some of these MCSs. We then defined the canonical relation between two MCSs by requiring that the second MCS is included in the set of formulae that occur in the scope of the diamond in the first MCS. The Existence lemma shows that this definition is the right one since it shows that a diamond formula occurs in a MCS iff there is a second MCS which contains the formula and is related to the first one. We have seen that theorems and rules of K play an essential role in proving such lemma. The Truth Lemma completes the proof by allowing us to reason as follows: if a formula is K-consistent then it is contained in some MCS in the canonical model (Lindenbaum Lemma). But then the formula is true at that same MCS in the canonical model (Truth Lemma), and hence it has a model.

Week 3: Chapter 4 of the book. Exercises set 3.

We defined modal validity, and looked at some simple valid and non-valid principles. Non-validity can be shown in counter-examples: (hopefully simple) models (M, s) where the non-valid formula is false. This search can be made systematic in so-called 'semantic tableaux', a method invented by Evert Beth in Amsterdam 1955. Tableaux are sound and complete for testing validity, with 'closed tableaux' establishing validity, and open tableaus yielding counter-examples that can be read off directly. Tableaux have the following further features: they show that non-valid formulas have counter-models of a size effectively computable from the length of the input formula (the 'effective finite model property'), while closed tableaux correspond to formal proofs. Tableaux are a very nice general method that also works for first-order logic and other systems, while they also lend themselves nicely to programming and automation. I had hoped to also analyze the computational complexity of modal validity testing and related tasks, but had no time for this: you can read it yourself in the textbook. Occasionally, questions come up in class, such as wether each infinite model in a language with just atoms 'True', 'False' (no proposition letters) has a bisimulation with a finite model. The answer is "No": do try an answer. In fact, any further thoughts are welcome -- but you can ask all more routine questions to the assistant(s).
Week 2: Chapter 3 of the book. Exercises set 2.
Here are the solutions of the exercises in Chapter 3 of the book.
Typos in Tutorial 2: in Ex8* the second occurrence of $\phi$ is $\psi$.
Exercise 5 is wrong, but can easily be fixed. Can you modify M' so that it works?

This second week, we have looked at the expressive power of the modal language, via the matching structural notion of bisimulation between models. We have seen some uses of this notion, while we also saw that modal formulas are invariant for bisimulation. We then looked into the 'fine- structure' of all this via bisimulation games, where modal formulas correspond to winning strategies for Spoilers, while bisimulations are winning strategies for Duplicators. There is a lot more model theory to all this in the research literature, but the door now stands open for you. Finally, we noted that this invariance perspective is quite general (even though somewhat underappreciated in some areas of 'formal semantics'). If you understand it for modal logic, you have also learnt something about first-order logic and other systems, about the mathematical approach to natural structure levels via 'invariance transformations', and indeed, about the emergence of language in general.

Week 1: Chapter 2 of the book. Exercises set 1.
Here you can find a small guide on how to make proofs.

This first week, we have done an ultra-brief introduction to the notion of modality. Please read Chapter 1 of the book for some further background. After that, we plunged right into the basic modal logic with its language, semantics, and a few remarks on validity and on evaluation games.

Staff

Dates & location

Course material

We will make use of the book Modal Logic for Open Minds by Johan van Benthem. For an extended monography, you can consult the Handbook of Modal Logic. For more recent developments, look at the series of conferences on Advances in Modal Logic (the last of which took place in Moscow).

Grading

Grading will be based on: