Modal logics

This seminar is more like a talk with examples about modal logics. These logics can be used for knowledge representation in multi-agent systems.

Modal logics are an extension of the classical propositional or predicate logic. In modal logic, we do not have only a single universe, but we have a set of so called “possible worlds” $W$. There is also a binary accessibility relation $R \subseteq W \times W$ on the set of the possible worlds, where $R(w, u)$ expresses that world $u$ is accessible from the world $w$. Typically this relation is written in the infix notation as $wRu$. Additionally, we have a function $v$ that for each possible world gives the model of the specific world (truth assignment in propositional logic and structure in predicate logic). Together, the set of possible worlds and the accessibility relation form a frame $\langle W, R \rangle$.

The semantics for connectives and quantifiers is the same as in propositional/predicate logic and is given by the valuation function (and may be different in each possible world). However, in modal logic we additionally define new modalities (unary logical connectives) $\square$ and $\diamond$ and that can be used as unary logical connectives. The formula $\square P$ is true in a world $w$ if and only if it is true in every world $u$ such that $wRu$, and $\diamond P$ is true in a world $w$ if it is true in some $u$ such that $wRu$.

What is the meaning of the new modalities? That actually depends on the particular use case we have for our logic. The common meaning is that $\square P$ says that $P$ is necessarily true (i.e. true in all accessible possible worlds), while $\diamond P$ says that $P$ is potentially true (i.e. true in some accessible possible world).

In classical modal logic, the two modalities are dual as $\forall$ and $\exists$ are in predicate logic. It means that $\square P \equiv \neg \diamond \neg P$ and $\diamond P \equiv \neg \square \neg P$. The former one reads in natural language as “$P$ is necessary if $\neg P$ is not possible” and the later one reads as “$P$ is possible if its negation is not necessary”.

Kripke semantics

Let us now define the semantics of modal logic more formally. This is so called Kripke semantics of possible worlds. Let’s have a frame $\langle W, R \rangle$ and a valuation $v$, we than say that some formula $P$ is true in a world $w$ ($w \vDash P$) if $v(w, P)$, furthermore

• $w \vDash \neg P$ if and only if $w \nvDash P$
• $w \vDash P \to Q$ if and only if $w \nvDash P$ or $w \vDash Q$
• $w \vDash \square P$ if and only if for every $u \in W$, if $wRu$ then $u \vdash P$
• $w \vDash \diamond P$ if and only if for some $u \in W$, if $wRu$ then $u \vdash P$

A formula $P$ is then valid in a model $\langle W, R, v \rangle$ if $w \vdash P$ for all $w \in W$, and it is valid in a frame $\langle W, R \rangle$ if it is valid in $\langle W, R, v \rangle$ for all possible $v$.

The generally defined modal logic above is quite weak, mainly because we have no assumptions about the accessibility relation. In practical applications, we often add additional conditions in order to obtain more useful systems (see below).

Systems of modal logic

Apart from the semantic definition above, we can also define the logic syntactically, by extending propositional (or predicate) logic with additional axioms and rules. Which axioms and rules we add depends on the intended application of the specific system of modal logic.

We definitely need to add the symbols for the two modalities and define them as dual as we did above. Most systems of modal logic (so called normal modal logics) also include the following rule $\bf{N}$ and axiom $\bf{K}$

• $\bf{N}$ (necessitation rule): if $P$ is a theorem, then $\square P$ is also a theorem
• $\bf{K}$ (distribution axiom): $\square(P \to Q) \to (\square P \to \square Q)$

Adding only these two axioms gives us the so called $K$ system (named after Saul Kripke, the author of the semantics of possible worlds). This system is still very weak and does not even prove that if something is necessary, it is also true. However, this can be added as the axiom $\bf{T}$

• $\bf{T}$ (reflexivity axiom): $\square P \to P$

There are also other common axioms that we can find in many systems of modal logic

• $\bf{4}$: $\square P \to \square \square P$
• $\bf{B}$: $P \to \square \diamond P$
• $\bf{D}$: $\square P \to \diamond P$
• $\bf{5}$: $\diamond P \to \square \diamond P$

Adding some of these axioms then creates different systems of modal logic (that can have different applications), for example, the above mentioned system $K$ uses only the $\bf{N}$ and $\bf{K}$ axioms. If we also add $\bf{T}$ we get a system that is commonly called $T$. We get systems called $S4$ and $S5$ by adding $\bf{4}$ or $\bf{5}$, respectively, to $T$. Finally, system $D$ is obtained by adding the axiom $\bf{D}$ to the system $K$.

There is a close correspondence between the axioms and various conditions on the accessibility relation. For example, the $K$ system is equivalent to the general modal logic without any assumptions about the accessibility relation. The $T$ axiom ensures that the accessibility relation is reflexive. The $\bf{4}$ axiom ensures that it is transitive and the $\bf{5}$ axioms ensures the relation is Euclidean (for every $u$, $t$, $w$, if $wRu$ and $wRt$ then $uRt$). The Euclidean property together with reflexivity also implies symmetry and transitivity.

The discussion above about the correspondence between axioms and assumptions about the accessibility relation leads to the observation, that in models of the system $T$ the accessibility relation is reflexive, in models of $S4$ it is reflexive and transitive and in models of $S5$ it is an equivalence.

Multimodal logics

Sometimes it is actually useful to have more than one pair of modalities (see epistemic logic below). If we have a set of $n$ modalities ${\square_1, \dots, \square_n}$, we call the resulting logic $n$-modal. The complementary operators $\diamond_1, \dots, \diamond_n$ are in this case typically defined as $\diamond_i P \equiv \neg \square_i \neg P$. The semantics of multimodal logic is a natural extension of the sematics of the logic described above, however, we now have $n$ accessibility relations $R_1, \dots, R_n$. The $i$-th modality is then evaluated w.r.t. to the $i$-th accessibility relation.

Epistemic modal logic

Epistemic modal logic is one of the types of modal logic that are particularly relevant for multi-agent systems as this type of logic allows us to reason about what agents know. It is a multimodal logic with modalities $K_i$ expressing that agent $i$ knows something. It is also quite common to add additional modalities $E_G$ expressing that everyone in group $G$ knows something (for finite groups of agents this can be defined as $E_G P \equiv \bigwedge K_i P$). In epistemic logic, we typically assume the accessibility relation is an equivalence, and the accessible possible world are sometimes called indistinguishable worlds. These are the worlds, in which the agent may be based on its knowledge. For example, if I do not know whether it is raining outside, I can be in two possible worlds - one in which it is raining outside and another one in which it is not.

Another useful modality is $C_G$ that expresses that something is a common knowledge in the group $G$. Common knowledge is an interesting concept. It means that every agent knows something, but it additionally means that every agent know that every agent knows that thing, and every agent knows that every agent knows that every agent knows that thing and so on to infinity. Common knowledge may have strong implications, as is typically shown by a number of logical induction puzzles. The most well-known of these being the muddy children puzzle.

Distributed knowledge, expressed using the modality $D_G$, is another interesting concept. It is the combined knowledge of a group of agents. Imagine that we have two people, neither of them knows whether it is raining outside, however, one of them knows that their friend wears a read coat only if it is raining and the other just saw the friend in the red coat. Combining these two pieces of information they can deduce that it is raining outside, therefore, this fact is their distributed knowledge.

In epistemic logic, the general axioms described above still hold, but of them have new names.

• $\bf{K}$ (distribution axiom): $(K_i P \land K_i (P \to Q)) \to K_i Q$
• $\bf{N}$ (knowledge generalization rule): $ \vDash P$ then $M \vDash K_i P$ (if $P$ is always true the agent knows $P$ in every possible world $M$)
• $\bf{T}$ (knowledge or truth axiom): $K_i P \to P$
• $\bf{4}$ (positive introspection): $K_i P \to K_i K_i P$
• $\bf{5}$ (negative introspection): $\neg K_i P \to K_i \neg K_i P$

It is easy to check that these axioms directly correspond to the general axioms defined above (specifically, they form the $S5$ system), this also shows, that modal logic can be useful for representing knowledge. If we instead want to represent beliefs (typically denoted with $B_i$ to express that agent $i$ believes something), we may need to remove the knowledge axiom, as sometimes agents may believe something that is not true. We typically replace the axiom with

• $\bf{D}$: $\neg B_i \bot$

Doxastic logic

Doxastic logic is logic about beliefs. It uses a modal operator $B$ that expresses that something is believed to be true. The agents in doxastic logic are called reasoners and there is a huge number of types of reasoners with increasing level of rationality.

For example Type 1 reasoner has full knowledge of propositional logic and eventually believes all tautologies. Their set of beliefs is closed under the modus ponens rule (if they believe $p$ and $p \to q$ they will also believe $q$). These conditions can be written as

• $\vDash p$ then $\vDash B p$
• $\forall p \forall q: B(p \to q) \to (Bp \to Bq)$

Type 1* reasoner is a bit more self aware, as it additionally has the condition

• $\forall p \forall q: B(p \to q) \to B(Bp \to Bq)$

Type 2 reasoner additionally believes that its beliefs are closed under modus ponens

• $\forall p \forall q: B(B p \land B(p \to q)) \to Bq)$

Type 3 reasoner is a normal reasoner of type 2, i.e.

• $\forall p: Bp \to BBp$

Type 4 reasoner is a type 3 reasoner that believes it is normal, i.e.

• $B(\forall p: Bp \to BBp)$

Temporal logic

Temporal logic is another type of multimodal logic. This type allows agents to reason about time. There is a number of different types of temporal logic depending on what they assume about the time. For example, in linear temporal logic (LTL) time is linear i.e. the accessibility relation (that in this case says what worlds are possible in the next time step) is a linear order, in computation tree logic (CTL) the time can be branching with tree-like structure, and it is assumed that one of the branches will be taken in the future. The CTL logic is useful for describing the behavior of computer programs and in formal software verification.

In LTL, we have two modalities - $X$ and $U$. The modality $X$ expresses that something will be true in the next step. The modality $U$ is binary and $A U B$ means that $A$ holds at least until $B$ is true which must happen now or in the future. There are also other operators defined using these fundamental ones

• $G$ means “always”
• $F$ means “sometime in the future”
• $R$ is “release” – $A R B$ means that $A$ must hold until and including the time $B$ becomes true, if $B$ is never true, $A$ must hold forever
• $W$ is “weak release” – $A W B$ means that $A$ must hold at least until $B$, if $B$ is never true, $A$ must hold forever
• $M$ is “strong release” – $A M B$ means that $A$ must hold until and including the time $B$ becomes true, which must happen now or in the future

CTL is the language with branching time in the future. It uses a number of temporal modalities and operators

• $A$ means “true on all future paths”
• $E$ means “there is future path”
• $X$, $G$, $F$, $U$, and $W$ are defined as in LTL

References and Further Reading

If you want to know more about modal logics, I recommend reading the following sources (mostly Wikipedia pages) - these were used to write most of the text here

1. Modal Logic @ Wikipedia
2. Kripke semantics @ Wikipedia
3. Doxastic Logic @ Wikipedia
4. Temporal Logic @ Wikipedia
5. Linear Temporal Logic @ Wikipedia
6. Computation Tree Logic @ Wikipedia
7. Epistemic Logic @ Wikipedia
8. Epistemic Logic @ Stanford Encyclopedia of Philosophy
9. Modal Logic (chapter 5) in Nerode, Anil, and Richard A. Shore. Logic for applications. Springer Science & Business Media, 2012.