A bird’s eye view of modal logic I. Syntax and semantics

(the pdf version of this entry)
It is strange to start this blog with a text on modal logic. Historically, the language of model theory has been the language of first-order logic (although recently there are efforts to go beyond first-order context), and this choice turned out to be so good that all the other logics that use other languages has become known under the name of “non-classical logics”. Among those non-classical logics modal logics is probably the simplest and the most general class of logics.

Indeed, the least that you expect from a logic is to be able to express boolean connectives: “and”, “or”, “not” and such. Modal logics add very little to those: they add one or several so-called modalities, so you can say “it is necessary that ” or “it is possible that ” in those logics (written as and , pronounced “box p” and “diamond p”). While this “syntactic” presentation of modal logics might not seem particularly enlightening, I still hope that I convinced you that we are dealing with very simple logics. I am saying “logics” here because there is a lot of space left for customization (the choice of modalities and their interpretation).

In fact, it was syntax that motivated the creators of modal logics (such as Lewis and Langford). First modal logics were studied only in proof-theoretic terms and were used to model in a formal way different philosophical notions like necessity, obligation or belief. In 1960s Saul Kripke proposed a semantics that gave a start to the development
of the field of modal logics as we know it today.

Here is the formal definition of the Kripke semantics. A frame is a set endowed with a binary relation . A model is a frame together with a valuation function that sends propositional letters to subsets of . The formulas of the basic modal language are given by the grammar

(where p is one of propositional letters) and are evaluated at points of a model. The satisfiability relation (denoted ) is a
ternary relation between models, points (they are also called states or possible worlds) of models and formulas. It is defined as follows:

iff
iff not

iff and

iff there exists such that and

(one says “ is satisfied at the state in the model ”). Other boolean connectives then can be defined in terms of and , and is defined as an abbreviation of (some authors take box to be the base modality and define diamond in terms of it). There are all kinds of generalizations that you can bring into this definition: you can consider several diamonds (then you need to have several relations in your frame, each of them interprets the corresponding diamond). It is possible to have n-ary modalities too (then you have (n+1)-ary relations to interpret them in the frame).

For example, consider a frame where sends the only propositional letter $p$ to the set of even numbers. Then, clearly, is satisfied at any natural number, while is not satisfied anywhere.

Contrary to first-order logic where one distinguishes sentences and formulas with free variables, in modal logic all formulas have the same status. On the other hand there are several degrees of “being valid”:
- one says that a formula is globally true in a model if is satisfied at every point of the model;
- one says that a formula is valid on a frame if it is globally true in every model based on that frame.
There are other notions like “valid on a frame at a point”, but what I want to emphasize here is that in the field of modal logics it is common to quantify over valuations, which implicitly brings universal monadic second-order quantification to the language. Consider for example a formula . If one says “ is valid on a class of frames ” it is equivalent to saying that the following formula (of monadic second-order logic) is valid on :

“Valid on a frame” corresponds to at the beginning of the formula and quantifies over all possible sets a valuation can send to. Notice also that once we strip those two quantifiers off we end up with a first-order formula in one free variable. You might have already figured out looking at the definition of Kripke semantics that any modal formula can be translated into such a first-order formula. The box and the diamond correspond to restricted quantification of the form and . Thus, on one hand modal logic is less expressive than first-order logic when we are talking about models because of the restricted quantification, but it is more powerful when we talk about frames. The bounds of expressivity of modal logics can be illustrated by the following examples.

We say that a modal formula defines a class of frames when a frame is in iff is valid on . Thus, the formula above defines the class of frames where the relation is the graph of a partial function.

1) The Löb formula defines the class of frames whose relation is transitive and its converse is well-founded. We leave it to you to verify that this formula is valid on this class of frames. Let us show that if is valid on a frame then this frame is transitive and converse well-founded (that is, there is no infinite sequence such that for all ). Suppose for the sake of contradiction that the frame is transitive and not converse well-founded (again, we leave the case when the frame is not transitive to the reader). Let be the set of all points $w$ in the frame such that an infinite chain starts at . Define the valuation

Then the formula is valid in the model because the chains that are subsets of are infinite and there are no points in them that would have no successors and hence would satisfy . Next, since is valid, is valid too. But on the other hand, any point of does not satisfy . A contradiction.

So, we have seen that a modal formula defines a property of graphs (frames) of being transitive and conversely well-founded. But a simple compactness argument shows that well-foundedness is not first-order
definable.

2) Completeness (every node is linked to every node) of a graph is a first-order property. However, it is not definable using any modal formula and here’s why. It is easy to show by induction on formula structure that satisfiability (and hence, frame validity) of modal formulas is preserved under taking disjoint unions of graphs. Indeed, the only interesting clause in the semantics definition — the diamond — is defined locally, in terms of point’s immediate successors. If a modal formula defined completeness, then we could take two complete graphs which would validate it and infer that their disjoint union (which is not complete) also validates — a contradiction.

Thus, modal logics are not good at defining non-local properties, but on the other hand they can sometimes be more expressive than first-order logic. The interplay of different types of quantification in the definition of relational semantics for modal logic has been a source of a lot of research.

Now consider the set of modal formulas, that are valid on all frames. It is clear, that it contains all the propositional
tautologies. Next, it is also clear that is is closed under application of modus ponens and substitution of propositional letters by arbitrary formulas. The novelty is that it is also closed under “necessitation”: if is valid on all frames, then is also valid. Next, the following axioms clearly belong to this set:

In fact, any set of of modal formulas that are valid on a class of frames has aforementioned properties. We might want to forget about the class of frames that gives rise to the set of formulas. If we only require that a set of formulas contains all the propositional tautologies and the two axioms above, is closed under modus ponens, substitution and necessitation, we call such a set of formulas a normal modal logic (or simply logic). The normal modal logic generated by a set of axioms is the smallest normal modal logic that contains . A logic is said to be finitely axiomatizable if it is generated by a finite set of formulas.

For those of you who find this terminology misleading, try to think of a first-order theory (of a structure) and keep in mind that logic is essentially the same thing. The term comes from the early days of modal logic, when the formal systems under consideration were called “logic of necessity”, “logic of knowledge”, “logic of obligation” and were defined axiomatically. Later, with the advent of Kripke semantics, it turned out that they can be regarded as sets of
formulas valid on classes of frames that satisfy certain conditions.

Now time has come to talk about the purpose and the subject of modal logic. I would like to draw a parallel with model theory here. In model theory, one tries to understand what the category of definable sets of a model is. Even if theories occur in model theory, they are usually complete, so their models are all elementary equivalent and their definable sets behave the same way in any model. In modal logic, the accent is rather shifted to the syntactic side. The object mostly
often under consideration is a normal modal logic, and one tries to understand its structure by proving completeness with respect to some nice class of frames or, even better, by providing a (preferably fast) algorithm that decides whether a formula belongs to the logic.

There are also various meta-logical properties that one might be curious to check (interpolation, Beth definability), but usually, once computational complexity bounds of the decision problem have been established, the logic is believed to no longer be an unknown territory. So, classes of frames have the same status as models in model theory, and normal modal logics are like categories of definable sets.

There were several attempts in 1970s to establish some general results that would allow given a finite axiomatisation of a logic to determine its complexity and find a decision procedure. This problem in its full generality is undecidable, but there are some results that apply in restricted cases.

But how the choice of the language and its semantics makes modal logic different from first-order logic?

First, the restricted quantification is the reason why many modal logics are decidable (as opposed to first-order logic) and often of low computational complexity, which is appealing for computer scientists. This comes at a price of reduced expressivity which is still sufficient for many applications. A lot of flavours of modal logics have been invented, and their expressivity and complexity were investigated. After all, modal logics can be seen as yet another specification language.

Second, the notion of validity on frames makes the modal semantics behave in a strange way giving rise to the phenomenon of incompleteness. The syntactic side of first-order logic can be formalized in many different ways: Hilbert-style axiomatics, natural deduction or Gentzen sequent calculus. A good property of all those formal systems is their extensibility. Suppose, you want to deal with all the formulas valid on partial orders. You can write down a formula that defines a class of structures that are partial orders. Then it suffices to add to the list of axioms in our proof system and magically the system will be able to prove all partial order validities. Unfortunately, this is not the case for modal logics. There are examples of normal modal logics (namely, the normal modal logic generated by Löb formula) that are consistent and yet do not coincide with the set of validities of any class of frames whatsoever. Completeness of modal logics does not come for free and proving it can be sometimes quite tricky.

Just these two aspects underlie a vast majority of research on modal logic. In the subsequent posts I will speak more about them, I will also try to give a brief overview of several particular topics in the field of modal logics that I find interesting.