Dynamic epistemic logic

Due to the nature of its object of study and its abstract approach, DEL is related and has applications to numerous research areas, such as computer science (artificial intelligence), philosophy (formal epistemology), economics (game theory) and cognitive science. In computer science, DEL is for example very much related to multi-agent systems, which are systems where multiple intelligent agents interact and exchange information.

As a combination of dynamic logic and epistemic logic, dynamic epistemic logic is a young field of research. It really started in 1989 with Plaza's logic of public announcement. Independently, Gerbrandy and Groeneveld proposed a system dealing moreover with private announcement and that was inspired by the work of Veltman. Another system was proposed by van Ditmarsch whose main inspiration was the Cluedo game. But the most influential and original system was the system proposed by Baltag, Moss and Solecki. This system can deal with all the types of situations studied in the works above and its underlying methodology is conceptually grounded. We will present in this entry some of its basic ideas.

Formally, DEL extends ordinary epistemic logic by the inclusion of event models to describe actions, and a product update operator that defines how epistemic models are updated as the consequence of executing actions described through event models. Epistemic logic will first be recalled. Then, actions and events will enter into the picture and we will introduce the DEL framework.

Epistemic Logic

Epistemic logic is a modal logic dealing with the notions of knowledge and belief. As a logic, it is concerned with understanding the process of reasoning about knowledge and belief: which principles relating the notions of knowledge and belief are intuitively plausible? Like epistemology, it stems from the Greek word ${\displaystyle ϵ\pi \iota \sigma \tau \eta \mu \eta }$ or ‘episteme’ meaning knowledge. Epistemology is nevertheless more concerned with analyzing the very nature and scope of knowledge, addressing questions such as “What is the definition of knowledge?” or “How is knowledge acquired?”. In fact, epistemic logic grew out of epistemology in the Middle Ages thanks to the efforts of Burley and Ockham. The formal work, based on modal logic, that inaugurated contemporary research into epistemic logic dates back only to 1962 and is due to Hintikka. It then sparked in the 1960s discussions about the principles of knowledge and belief and many axioms for these notions were proposed and discussed. For example, the interaction axioms ${\displaystyle Kp\to Bp}$ and ${\displaystyle Bp\to KBp}$ are often considered to be intuitive principles: if an agent Knows ${\displaystyle p}$ then (s)he also Believes ${\displaystyle p}$, or if an agent Believes ${\displaystyle p}$, then (s)he Knows that (s)he Believes ${\displaystyle p}$. More recently, these kinds of philosophical theories were taken up by researchers in economics, artificial intelligence and theoretical computer science where reasoning about knowledge is a central topic. Due to the new setting in which epistemic logic was used, new perspectives and new features such as computability issues were then added to the research agenda of epistemic logic.

Syntax

In the sequel, ${\displaystyle AGTS=\{1,\dots ,n\}}$ is a finite set whose elements are called agents and ${\displaystyle PROP}$ is a set of propositional letters.

The epistemic language is an extension of the basic multi-modal language of modal logic with a common knowledge operator ${\displaystyle C_A}$ and a distributed knowledge operator ${\displaystyle D_A}$. Formally, the epistemic language ${\displaystyle {\mathcal{L}}_{\mathsf{\text{EL}}}^C}$ is defined inductively by the following grammar in BNF:

${\displaystyle {\mathcal{L}}_{\mathsf{\text{EL}}}^C:\varphi ::=p\mid \mathrm{\neg }\varphi \mid (\varphi \wedge \varphi )\mid K_j\varphi \mid C_A\varphi \mid D_A\varphi }$

where ${\displaystyle p\in PROP}$, ${\displaystyle j\in AGTS}$ and ${\displaystyle A\subseteq AGTS}$. The basic epistemic language ${\displaystyle {\mathcal{L}}_{EL}}$ is the language ${\displaystyle {\mathcal{L}}_{EL}^C}$ without the common knowledge and distributed knowledge operators. The formula ${\displaystyle \mathrm{\perp }}$ is an abbreviation for ${\displaystyle \mathrm{\neg }p\wedge p}$ (for a given ${\displaystyle p\in PROP}$), ${\displaystyle ⟨K_j⟩\varphi }$ is an abbreviation for ${\displaystyle \mathrm{\neg }{K}_j\mathrm{\neg }\varphi }$, ${\displaystyle E_A\varphi }$ is an abbreviation for ${\displaystyle \underset{j\in A}{\bigwedge }{K}_j\varphi }$ and ${\displaystyle C\varphi }$ an abbreviation for ${\displaystyle C_{AGTS}\varphi }$.

Group notions: general, common and distributed knowledge.

In a multi-agent setting there are three important epistemic concepts: general knowledge, distributed knowledge and common knowledge. The notion of common knowledge was first studied by Lewis in the context of conventions. It was then applied to distributed systems and to game theory, where it allows to express that the rationality of the players, the rules of the game and the set of players are commonly known.

General knowledge.

General knowledge of ${\displaystyle \varphi }$ means that everybody in the group of agents ${\displaystyle AGTS}$ knows that ${\displaystyle \varphi }$. Formally, this corresponds to the following formula:

${\displaystyle E\varphi :=\underset{j\in AGTS}{\bigwedge }{K}_j\varphi .}$

Common knowledge.

Common knowledge of ${\displaystyle \varphi }$ means that everybody knows ${\displaystyle \varphi }$ but also that everybody knows that everybody knows ${\displaystyle \varphi }$, that everybody knows that everybody knows that everybody knows ${\displaystyle \varphi }$, and so on ad infinitum. Formally, this corresponds to the following formula

${\displaystyle C\varphi :=E\varphi \wedge EE\varphi \wedge EEE\varphi \wedge \dots }$

As we do not allow infinite conjunction the notion of common knowledge will have to be introduced as a primitive in our language.

Before defining the language with this new operator, we are going to give an example introduced by Lewis that illustrates the difference between the notions of general knowledge and common knowledge. Lewis wanted to know what kind of knowledge is needed so that the statement ${\displaystyle p}$: “every driver must drive on the right” be a convention among a group of agents. In other words, he wanted to know what kind of knowledge is needed so that everybody feels safe to drive on the right. Suppose there are only two agents ${\displaystyle i}$ and ${\displaystyle j}$. Then everybody knowing ${\displaystyle p}$ (formally ${\displaystyle Ep}$) is not enough. Indeed, it might still be possible that the agent ${\displaystyle i}$ considers possible that the agent ${\displaystyle j}$ does not know ${\displaystyle p}$ (formally ${\displaystyle \mathrm{\neg }{K}_i{K}_{j}p}$). In that case the agent ${\displaystyle i}$ will not feel safe to drive on the right because he might consider that the agent ${\displaystyle j}$, not knowing ${\displaystyle p}$, could drive on the left. To avoid this problem, we could then assume that everybody knows that everybody knows that ${\displaystyle p}$ (formally ${\displaystyle EEp}$). This is again not enough to ensure that everybody feels safe to drive on the right. Indeed, it might still be possible that agent ${\displaystyle i}$ considers possible that agent ${\displaystyle j}$ considers possible that agent ${\displaystyle i}$ does not know ${\displaystyle p}$ (formally ${\displaystyle \mathrm{\neg }{K}_i{K}_j{K}_{i}p}$). In that case and from ${\displaystyle i}$’s point of view, ${\displaystyle j}$ considers possible that ${\displaystyle i}$, not knowing ${\displaystyle p}$, will drive on the left. So from ${\displaystyle i}$’s point of view, ${\displaystyle j}$ might drive on the left as well (by the same argument as above). So ${\displaystyle i}$ will not feel safe to drive on the right. Reasoning by induction, Lewis showed that for any ${\displaystyle k\in \mathbb{N}}$, ${\displaystyle Ep\wedge E^{1}p\wedge \dots \wedge E^{k}p}$ is not enough for the drivers to feel safe to drive on the right. In fact what we need is an infinite conjunction. In other words, we need common knowledge of ${\displaystyle p}$: ${\displaystyle Cp}$.

Distributed knowledge.

Distributed knowledge of ${\displaystyle \varphi }$ means that if the agents pulled their knowledge altogether, they would know that ${\displaystyle \varphi }$ holds. In other words, the knowledge of ${\displaystyle \varphi }$ is distributed among the agents. The formula ${\displaystyle D_A\varphi }$ reads as ‘it is distributed knowledge among the set of agents ${\displaystyle A}$ that ${\displaystyle \varphi }$ holds’.

Semantics

Epistemic logic is a modal logic. So, what we call an epistemic model ${\displaystyle \mathcal{M}=(W,R_1,\dots ,R_n,I)}$ is just a Kripke model as defined in modal logic. The set ${\displaystyle W}$ is a non-empty set whose elements are called possible worlds and the interpretation ${\displaystyle I:W\to 2^{PROP}}$ is a function specifying which propositional facts (such as ‘Ann has the red card’) are true in each of these worlds. The accessibility relations ${\displaystyle R_j\subseteq W\times W}$ are binary relations for each agent ${\displaystyle j\in AGTS}$; they are intended to capture the uncertainty of each agent (about the actual world and about the other agents' uncertainty). Intuitively, we have ${\displaystyle (w,v)\in R_j}$ when the world ${\displaystyle v}$ is compatible with agent ${\displaystyle j}$’s information in world ${\displaystyle w}$ or, in other words, when agent ${\displaystyle j}$ considers that world ${\displaystyle v}$ might correspond to the world ${\displaystyle w}$ (from this standpoint). We abusively write ${\displaystyle w\in \mathcal{M}}$ for ${\displaystyle w\in W}$ and ${\displaystyle R_j(w)}$ denotes the set of worlds ${\displaystyle \{v\in W;(w,v)\in R_j\}}$.

Intuitively, a pointed epistemic model ${\displaystyle (\mathcal{M},w)}$, where ${\displaystyle w\in \mathcal{M}}$, represents from an external point of view how the actual world ${\displaystyle w}$ is perceived by the agents ${\displaystyle AGTS}$.

For every epistemic model ${\displaystyle \mathcal{M}}$, every ${\displaystyle w\in \mathcal{M}}$ and every ${\displaystyle \varphi \in {\mathcal{L}}_{\mathsf{\text{EL}}}}$, we define ${\displaystyle \mathcal{M},w\models \varphi }$ inductively by the following truth conditions:

where ${\displaystyle {\left(\bigcup _{j\in A}{R}_j\right)}^{+}}$ is the transitive closure of ${\displaystyle \bigcup _{j\in A}{R}_j}$: we have that ${\displaystyle v\in {\left(\bigcup _{j\in A}{R}_j\right)}^{+}(w)}$ if, and only if, there are ${\displaystyle w_0,\dots ,w_m\in \mathcal{M}}$ and ${\displaystyle j_1,\dots ,j_m\in A}$ such that ${\displaystyle w_0=w,w_m=v}$ and for all ${\displaystyle i\in \{1,\dots ,m\}}$, ${\displaystyle w_{i-1}{R}_{j_i}{w}_i}$.

Despite the fact that the notion of common belief has to be introduced as a primitive in the language, we can notice that the definition of epistemic models does not have to be modified in order to give truth value to the common knowledge and distributed knowledge operators.

Card Example:

Players ${\displaystyle A}$, ${\displaystyle B}$ and ${\displaystyle C}$ (standing for Ann, Bob and Claire) play a card game with three cards: a red one, a green one and a blue one. Each of them has a single card but they do not know the cards of the other players. Ann has the red card, Bob has the green card and Claire has the blue card. This example is depicted in the pointed epistemic model ${\displaystyle (\mathcal{M},w)}$ represented below. In this example, ${\displaystyle AGTS:=\{A,B,C\}}$ and ${\displaystyle PROP:=\{A,B,C,B,C,A,C,A,B\}}$. Each world is labelled by the propositional letters which are true in this world and ${\displaystyle w}$ corresponds to the actual world. There is an arrow indexed by agent ${\displaystyle j\in \{A,B,C\}}$ from a possible world ${\displaystyle u}$ to a possible world ${\displaystyle v}$ when ${\displaystyle (u,v)\in R_j}$. Reflexive arrows are omitted, which means that for all ${\displaystyle j\in \{A,B,C\}}$ and all ${\displaystyle v\in \mathcal{M}}$, we have that ${\displaystyle (v,v)\in R_j}$.

${\displaystyle A}$ stands for : "${\displaystyle A}$ has the red card''

${\displaystyle C}$ stand for: "${\displaystyle C}$ has the blue card''

${\displaystyle B}$ stands for: "${\displaystyle B}$ has the green card''

and so on...

When accessibility relations are equivalence relations (like in this example) and we have that ${\displaystyle (w,v)\in R_j}$, we say that agent ${\displaystyle j}$ cannot distinguish world ${\displaystyle w}$ from world ${\displaystyle v}$ (or world ${\displaystyle w}$ is indistinguishable from world ${\displaystyle v}$ for agent ${\displaystyle j}$). So, for example, $A$ cannot distinguish the actual world ${\displaystyle w}$ from the possible world where ${\displaystyle B}$ has the blue card (${\displaystyle B}$), ${\displaystyle C}$ has the green card (${\displaystyle C}$) and ${\displaystyle A}$ still has the red card (${\displaystyle A}$).

In particular, the following statements hold:

${\displaystyle \mathcal{M},w\models (A\wedge K_{A}A)\wedge (C\wedge K_{C}C)\wedge (B\wedge K_{B}B)}$

'All the agents know the color of their card'.

${\displaystyle \mathcal{M},w\models K_A(B\vee B)\wedge K_A(C\vee C)}$

'${\displaystyle A}$ knows that ${\displaystyle B}$ has either the blue or the green card and that ${\displaystyle C}$ has either the blue or the green card'.

${\displaystyle \mathcal{M},w\models E(A\vee A\vee A)\wedge C(A\vee A\vee A)}$

'Everybody knows that ${\displaystyle A}$ has either the red, green or blue card and this is even common knowledge among all agents'.

Knowledge versus Belief

We use the same notation ${\displaystyle K_j}$ for both knowledge and belief. Hence, depending on the context, ${\displaystyle K_j\varphi }$ will either read ‘the agent ${\displaystyle j}$ Knows that ${\displaystyle \varphi }$ holds’ or ‘the agent ${\displaystyle j}$ Believes that ${\displaystyle \varphi }$ holds’. A crucial difference is that, unlike knowledge, beliefs can be wrong: the axiom ${\displaystyle K_j\varphi \to \varphi }$ holds only for knowledge, but not necessarily for belief. This axiom called axiom T (for Truth) states that if the agent knows a proposition, then this proposition is true. It is often considered to be the hallmark of knowledge and it has not been subjected to any serious attack ever since its introduction in the Theaetetus by Plato.

The notion of knowledge might comply to some other constraints (or axioms) such as ${\displaystyle K_j\varphi \to K_j{K}_j\varphi }$: if agent ${\displaystyle j}$ knows something, she knows that she knows it. These constraints might affect the nature of the accessibility relations ${\displaystyle R_j}$ which may then comply to some extra properties. So, we are now going to define some particular classes of epistemic models that all add some extra constraints on the accessibility relations ${\displaystyle R_j}$. These constraints are matched by particular axioms for the knowledge operator ${\displaystyle K_j}$. Below each property, we give the axiom which defines the class of epistemic frames that fulfill this property. (${\displaystyle K\varphi }$ stands for ${\displaystyle K_j\varphi }$ for any ${\displaystyle j\in AGTS}$.)

We discuss the axioms above. Axiom 4 states that if the agent knows a proposition, then she knows that she knows it (this axiom is also known as the “KK-principle”or “KK-thesis”). In epistemology, axiom 4 tends to be accepted by internalists, but not by externalists. Axiom 4 is nevertheless widely accepted by computer scientists (but also by many philosophers, including Plato, Aristotle, Saint Augustine, Spinoza and Schopenhauer, as Hintikka recalls ). A more controversial axiom for the logic of knowledge is axiom 5 for Euclidicity: this axiom states that if the agent does not know a proposition, then she knows that she does not know it. Most philosophers (including Hintikka) have attacked this axiom, since numerous examples from everyday life seem to invalidate it. In general, axiom 5 is invalidated when the agent has mistaken beliefs, which can be due for example to misperceptions, lies or other forms of deception. Axiom B states that it cannot be the case that the agent considers it possible that she knows a false proposition (that is, ${\displaystyle \mathrm{\neg }(\mathrm{\neg }\varphi \wedge \mathrm{\neg }K\mathrm{\neg }K\varphi )}$). If we assume that axioms T and 4 are valid, then axiom B falls prey to the same attack as the one for axiom 5 since this axiom is derivable. Axiom D states that the agent's beliefs are consistent. In combination with axiom K (where the knowledge operator is replaced by a belief operator), axiom D is in fact equivalent to a simpler axiom D' which conveys, maybe more explicitly, the fact that the agent's beliefs cannot be inconsistent: ${\displaystyle \mathrm{\neg }B\mathrm{\perp }}$. The other intricate axioms .2, .3, .3.2 and .4 have been introduced by epistemic logicians such as Lenzen and Kutchera in the 1970s and presented for some of them as key axioms of epistemic logic. They can be characterized in terms of intuitive interaction axioms relating knowledge and beliefs.

Axiomatization

The Hilbert proof system K for the basic modal logic is defined by the following axioms and inference rules: for all ${\displaystyle j\in AGTS}$,

The axioms of an epistemic logic obviously display the way the agents reason. For example, the axiom K together with the rule of inference Nec entail that if I know ${\displaystyle \varphi }$ (${\displaystyle K\varphi }$) and I know that ${\displaystyle \varphi }$ implies ${\displaystyle \psi }$ (${\displaystyle K(\varphi \to \psi ))}$ then I know that ${\displaystyle \psi }$ (${\displaystyle K\psi }$). Stronger constraints can be added. The following proof systems for ${\displaystyle {\mathcal{L}}_{\mathsf{\text{EL}}}}$ are often used in the literature.

We define the set of proof systems ${\displaystyle {\mathbb{L}}_{\mathsf{\text{EL}}}:=\{\mathsf{\text{K}},\mathsf{\text{KD45}},\mathsf{\text{S4}},\mathsf{\text{S4.2}},\mathsf{\text{S4.3}},\mathsf{\text{S4.3.2}},\mathsf{\text{S4.4}},\mathsf{\text{S5}}\}}$.

Moreover, for all ${\displaystyle \mathcal{H}\in {\mathbb{L}}_{\mathsf{\text{EL}}}}$, we define the proof system ${\displaystyle {\mathcal{H}}^{\mathsf{\text{C}}}}$ by adding the following axiom schemes and rules of inference to those of ${\displaystyle \mathcal{H}}$. For all ${\displaystyle A\subseteq AGTS}$,

The relative strength of the proof systems for knowledge is as follows:

${\displaystyle \mathsf{\text{S4}}\subset \mathsf{\text{S4.2}}\subset \mathsf{\text{S4.3}}\subset \mathsf{\text{S4.3.2}}\subset \mathsf{\text{S4.4}}\subset \mathsf{\text{S5}}.}$

So, all the theorems of ${\displaystyle \mathsf{\text{S4.2}}}$ are also theorems of ${\displaystyle \mathsf{\text{S4.3}},\mathsf{\text{S4.3.2}},\mathsf{\text{S4.4}}}$ and ${\displaystyle \mathsf{\text{S5}}}$. Many philosophers claim that in the most general cases, the logic of knowledge is ${\displaystyle \mathsf{\text{S4.2}}}$ or ${\displaystyle \mathsf{\text{S4.3}}}$. Typically, in computer science and in many of the theories developed in artificial intelligence, the logic of belief (doxastic logic) is taken to be ${\displaystyle \mathsf{\text{KD45}}}$ and the logic of knowledge (epistemic logic) is taken to be ${\displaystyle \mathsf{\text{S5}}}$, even if ${\displaystyle \mathsf{\text{S5}}}$ is only suitable for situations where the agents do not have mistaken beliefs. ${\displaystyle \mathsf{\text{Br}}}$ has been propounded by Floridi as the logic of the notion of 'being informed’ which mainly differs from the logic of knowledge by the absence of introspection for the agents.

For all ${\displaystyle \mathcal{H}\in {\mathbb{L}}_{\mathsf{\text{EL}}}}$, the class of ${\displaystyle \mathcal{H}}$–models or ${\displaystyle {\mathcal{H}}^{\mathsf{\text{C}}}}$–models is the class of epistemic models whose accessibility relations satisfy the properties listed above defined by the axioms of ${\displaystyle \mathcal{H}}$ or ${\displaystyle {\mathcal{H}}^{\mathsf{\text{C}}}}$. Then, for all ${\displaystyle \mathcal{H}\in {\mathbb{L}}_{\mathsf{\text{EL}}}}$, ${\displaystyle \mathcal{H}}$ is sound and strongly complete for ${\displaystyle {\mathcal{L}}_{\mathsf{\text{EL}}}}$ w.r.t. the class of ${\displaystyle \mathcal{H}}$–models, and ${\displaystyle {\mathcal{H}}^{\mathsf{\text{C}}}}$ is sound and strongly complete for ${\displaystyle {\mathcal{L}}_{\mathsf{\text{EL}}}^{\mathsf{\text{C}}}}$ w.r.t. the class of ${\displaystyle {\mathcal{H}}^{\mathsf{\text{C}}}}$–models.

Decidability and Complexity

The satisfiability problem for all the logics introduced is decidable. We list below the computational complexity of the satisfiability problem for each of them. Note that it becomes linear in time if there are only finitely many propositional letters in the language. For ${\displaystyle n\ge 2}$, if we restrict to finite nesting, then the satisfiability problem is NP-complete for all the modal logics considered. If we then further restrict the language to having only finitely many primitive propositions, the complexity goes down to linear in time in all cases.

The computational complexity of the model checking problem is in P in all cases.