Dynamic epistemic logic
Dynamic epistemic logic (DEL) is a logical framework dealing with knowledge and information change. Typically, DEL focuses on situations involving multiple agents and studies how their knowledge changes when events occur. These events can change factual properties of the actual world (they are called "ontic events"): for example a red card is painted in blue. They can also bring about changes of knowledge without changing factual properties of the world (they are called "epistemic events"): for example a card is revealed publicly (or privately) to be red. Originally, DEL focused on epistemic events. We only present in  this entry some of the basic ideas of the original DEL framework; more details about DEL in general can be found in the references. 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 formula_1 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 formula_2 and formula_3 are often considered to be intuitive principles: if an agent Knows formula_4 then (s)he also Believes formula_4, or if an agent Believes formula_4, then (s)he Knows that (s)he Believes formula_4. 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, formula_8 is a finite set whose elements are called agents and formula_9 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 formula_10 and a distributed knowledge operator formula_11. Formally, the epistemic language formula_12 is defined inductively by the following grammar in BNF: formula_13 where formula_14, formula_15 and formula_16. The basic epistemic language formula_17 is the language formula_18 without the common knowledge and distributed knowledge operators. The formula formula_19 is  an abbreviation for formula_20 (for a given formula_14), formula_22 is an abbreviation for formula_23, formula_24 is an abbreviation for formula_25 and formula_26 an abbreviation for formula_27. 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 formula_28 means that everybody in the group of agents formula_29 knows that formula_28. Formally, this corresponds to the following formula: formula_31 "Common knowledge." Common knowledge of formula_28 means that everybody knows formula_28 but also that everybody knows that everybody knows formula_28, that everybody knows that everybody knows that everybody knows formula_28, and so on "ad infinitum". Formally, this corresponds to the following formula formula_36 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 formula_4: “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 formula_38 and formula_39. Then everybody knowing formula_4 (formally formula_41) is not enough. Indeed, it might still be  possible that the agent formula_38 considers possible that the agent formula_39 does not know formula_4 (formally formula_45). In that case the agent formula_38 will not feel safe to drive on the right because he might consider that the agent formula_39, not knowing formula_4, could drive on the left. To avoid this problem, we could then assume that everybody knows that everybody knows that formula_4 (formally formula_50). This is again not enough to ensure that everybody feels safe to drive on the right. Indeed, it might still be possible that agent formula_38 considers possible that agent formula_39 considers possible that agent  formula_38 does not know formula_4 (formally formula_55). In that case and from formula_38’s point of view, formula_39 considers possible that formula_38, not knowing formula_4, will drive on the left. So from formula_38’s point of view, formula_39 might drive on the left as well (by the same argument as above). So formula_38 will not feel safe to drive on the right. Reasoning by induction, Lewis showed that for any formula_63, formula_64 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 formula_4: formula_66. "Distributed knowledge." Distributed knowledge of formula_28 means that if the agents pulled their knowledge altogether, they would know that formula_28 holds. In other words, the knowledge of formula_28 is "distributed" among the agents. The formula formula_70 reads as ‘it is distributed knowledge among the set of agents formula_71 that formula_28 holds’. Semantics. Epistemic logic is a modal logic. So, what we call an epistemic model formula_73 is just a Kripke model as defined in modal logic. The set formula_74 is a non-empty set whose elements are called "possible worlds" and the "interpretation" formula_75 is  a function specifying which propositional facts (such as ‘Ann has the red card’) are true in each of these worlds. The "accessibility relations" formula_76 are binary relations for each agent formula_77; they are intended to capture the uncertainty of each agent (about the actual world and about the other agents' uncertainty). Intuitively, we have formula_78 when the world formula_79 is compatible with agent formula_39’s information in world formula_81 or, in other words, when agent formula_39 considers that world formula_79 might correspond to the world formula_81 (from this standpoint). We abusively write formula_85 for formula_86 and formula_87 denotes the set  of worlds formula_88. Intuitively, a pointed epistemic model formula_89, where formula_85, represents from an external point of view how the actual world formula_81 is perceived by the agents formula_29. For every epistemic model formula_93, every formula_94 and every formula_95, we define formula_96 inductively by the following truth conditions: where formula_97 is the transitive closure of formula_98: we have that formula_99 if, and only if, there are formula_100 and formula_101 such that formula_102 and for all formula_103, formula_104. 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 formula_71, formula_106 and formula_107 (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 formula_108 represented  below. In this example, formula_109 and formula_110. Each world is labelled by the propositional letters which are true in this world and formula_81 corresponds to the actual world. There is an arrow indexed by agent formula_112 from a possible world formula_113 to a possible world formula_79 when formula_115. Reflexive arrows are omitted, which means that for all formula_116 and all formula_117, we have that formula_118. formula_119 stands for : "formula_71 has the red card<nowiki>"</nowiki> formula_121 stand for: "formula_107 has the blue card<nowiki>"</nowiki> formula_123 stands for: "formula_106 has the green card<nowiki>"</nowiki> and so  on... When accessibility relations are equivalence relations (like in this example) and we have that formula_78, we say that agent formula_39 "cannot distinguish" world formula_81 from world formula_79 (or world formula_81 is indistinguishable from world formula_79 for agent formula_39). So, for example, formula_132 cannot distinguish the actual world formula_81 from the possible world where formula_106 has the blue card (formula_135), formula_107 has the green card (formula_137) and formula_71 still has the red card (formula_119). In particular, the following statements hold: formula_140 'All the agents know the color of their card'. formula_141 'formula_71 knows that formula_106 has either the  blue or the green card and that formula_107 has either the blue or the green card'. formula_145 'Everybody knows that formula_71 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 formula_147 for both knowledge and belief. Hence, depending on the context, formula_148 will either read ‘the agent formula_39 "K"nows that formula_28 holds’ or ‘the agent formula_39 "B"elieves that formula_28 holds’. A crucial difference is that, unlike knowledge, beliefs can be "wrong": the axiom formula_153 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 formula_154: if agent formula_39 knows something, she knows that she knows it. These constraints might affect the nature of the accessibility relations formula_156 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 formula_156. These constraints are matched by particular axioms for the knowledge operator formula_147. Below each property, we give the axiom which "defines" the class of epistemic frames that fulfill this property. (formula_159 stands for formula_148 for any formula_77.) 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, formula_162). 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: formula_163. 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 formula_77, 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 formula_28 (formula_159) and I know that formula_28 implies formula_168 (formula_169 then I know that formula_168 (formula_171). Stronger constraints can be added. The following proof systems for formula_172 are often used in the literature. We define the set of proof systems formula_173. Moreover, for all formula_174, we define the proof system formula_175 by adding the following axiom schemes and rules of inference to those of formula_176. For all formula_177, The relative strength of the proof systems for knowledge is as follows: formula_178 So, all the theorems  of formula_179 are also theorems of formula_180 and formula_181. Many philosophers claim that in the most general cases, the logic of knowledge is formula_179 or formula_183. Typically, in computer science and in many of the theories developed in artificial intelligence, the logic of belief ("doxastic" logic) is taken to be formula_184 and the logic of knowledge ("epistemic" logic) is taken to be formula_181, even if formula_181 is only suitable for situations where the agents do not have mistaken beliefs. formula_187 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 formula_174, the class of formula_176–models or formula_175–models is the class of epistemic models whose accessibility relations satisfy the properties listed above defined by the axioms of formula_176 or formula_175. Then, for all formula_174, formula_176 is sound and strongly complete for formula_172 w.r.t. the class of formula_176–models, and formula_175 is sound and strongly complete for formula_198 w.r.t. the class of formula_175–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 formula_200, 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. Adding Dynamics. Dynamic Epistemic Logic (DEL) is a logical framework for modeling epistemic situations involving several agents, and changes  that occur to these situations as a result of incoming information or more generally incoming action. The methodology of DEL is such that it splits the task of representing the agents’ beliefs and knowledge into three parts: Typically, an informative event can be a public announcement to all the agents of a formula formula_168: this public announcement and correlative update constitute the dynamic part. However, epistemic events can be much more complex than simple public announcement, including hiding information for some of the agents, cheating, lying, bluffing, "etc." This complexity is dealt with when we introduce the notion of event  model. We will first focus on public announcements to get an intuition of the main underlying ideas of DEL. Public Events. In this section, we assume that all events are public. We start by giving a concrete example where DEL can be used, to better understand what is going on. This example is called the muddy children puzzle. Then, we will present a formalization of this puzzle in a logic called Public Announcement Logic (PAL). The muddy children puzzle is one of the most well known puzzles that played a role in the development of DEL. Other significant puzzles include  the sum and product puzzle, the Monty Hall dilemma, the Russian cards problem, the two envelopes problem, Moore's paradox, the hangman paradox, "etc". Muddy Children Example: We have two children, A and B, both dirty. A can see B but not himself, and B can see A but not herself. Let formula_4 be the proposition stating that A is dirty, and formula_203 be the proposition stating that B is dirty. Public announcement logic (PAL): We present the syntax and semantic of Public Announcement Logic (PAL), which combines features of epistemic logic and propositional dynamic logic. We define the language  formula_215 inductively by the following grammar in BNF: formula_216 where formula_77. The language formula_215 is interpreted over epistemic models. The truth conditions for the connectives of the epistemic language are the same as in epistemic logic (see above). The truth condition for the new dynamic action modality formula_219 is defined as follows: where formula_220 with formula_221, formula_222 for all formula_223 and formula_224. The formula formula_219 intuitively means that after a truthful announcement of formula_168, formula_28 holds. A public announcement of a proposition formula_168 changes the current epistemic model like in the figure below. The proof system formula_229 defined below is  sound and strongly complete for formula_215 w.r.t. the class of all pointed epistemic models. The axioms Red 1 - Red 4 are called "reduction axioms" because they allow to reduce any formula of formula_215 to a provably equivalent formula of formula_17 in formula_229. The formula formula_234 is a theorem provable in formula_229. It states that after a public announcement of formula_203, the agent knows that formula_203 holds. PAL is decidable, its model checking problem is solvable in polynomial time and its satisfiability problem is PSPACE-complete. Muddy children puzzle formalized with PAL: Here are some of the statements that hold in  the muddy children puzzle formalized in PAL. formula_238 'In the initial situation, A is dirty and B is dirty'. formula_239 'In the initial situation, A does not know whether he is dirty and B neither'. formula_240 'After the public announcement that at least one of the children A and B is dirty, both of them know that at least one of them is dirty'. However: formula_241 'After the public announcement that at least one of the children A and B is dirty, they still do not know that they are dirty'. Moreover: formula_242 'After the successive public announcements that at  least one of the children A and B is dirty and that they still do not know whether they are dirty, A and B then both know that they are dirty'. In this last statement, we see at work an interesting feature of the update process: a formula is not necessarily true after being announced. That is what we technically call “self-persistence” and this problem arises for epistemic formulas (unlike propositional formulas). One must not confuse the announcement and the update induced by this announcement, which might cancel some of the information encoded in the announcement. Arbitrary Events. In  this section, we assume that events are not necessarily public and we focus on items 2 and 3 above, namely on how to represent events and on how to update an epistemic model with such a representation of events by means of a product update. Event Model. Epistemic models are used to model how agents perceive the actual world. Their perception can also be described in terms of knowledge and beliefs about the world and about the other agents’ beliefs. The insight of the DEL approach is that one can describe how an event is perceived by the agents in  a very similar way. Indeed, the agents’ perception of an event can also be described in terms of knowledge and beliefs. For example, the private announcement of formula_71 to formula_106 that her card is red can also be described in terms of knowledge and beliefs: while formula_71 tells formula_106 that her card is red (event formula_247) formula_107 "believes" that nothing happens (event formula_249). This leads to define the notion of event model whose definition is very similar to that of an epistemic model. A pointed event model formula_250 represents how the actual event represented by formula_247 is perceived by the  agents. Intuitively, formula_252 means that while the possible event represented by formula_247 is occurring, agent formula_39 considers possible that the possible event represented by formula_249 is actually occurring. An event model is a tuple formula_256 where: formula_263 denotes the set formula_264 .We write formula_265 for formula_266, and formula_250 is called a pointed event model (formula_247 often represents the actual event). Card Example: Let us resume the card example and assume that players formula_71 and formula_106 show their card to each other. As it turns out, formula_107 noticed that formula_71 showed her card to formula_106 but did not notice that formula_106  did so to formula_71. Players formula_71 and formula_106 know this. This event is represented below in the event model formula_250. The possible event formula_247 corresponds to the actual event ‘players formula_71 and formula_106 show their and cards respectively to each other’ (with precondition formula_282), formula_249 stands for the event ‘player formula_71 shows her green card’ (with precondition formula_285) and formula_286 stands for the atomic event ‘player formula_71 shows her red card’ (with precondition formula_119). Players formula_71 and formula_106 show their cards to each other, players formula_71 and formula_106 know this and consider it possible, while player formula_107 considers possible that  player formula_71 shows her red card and also considers possible that player formula_71 shows her green card, since he does not know her card. In fact, that is all that player formula_107 considers possible because she did not notice that formula_297 showed her card. Another example of event model is given below. This second example corresponds to the event whereby Player formula_71 shows her red card publicly to everybody. Player formula_71 shows her red card, players formula_71, formula_106 and formula_107 ‘know’ it, players formula_71, formula_106 and formula_107 ‘know’ that each of them ‘knows’ it, "etc." In other words, there is  common knowledge among players formula_71, formula_106 and formula_107 that player formula_71 shows her red card. Product Update. The DEL product update is defined below. This update yields a new pointed epistemic model formula_310 representing how the new situation which was previously represented by formula_89 is perceived by the agents after the occurrence of the event represented by formula_250. Let formula_313 be an epistemic model and let formula_314 be an event model. The product update of formula_93 and formula_316 is the epistemic model formula_317 defined as follows: for all formula_318 and all formula_319, If formula_86 and formula_321 are such that formula_322  then formula_323 denotes the pointed epistemic model formula_324. This definition of the product update is conceptually grounded. Card Example: As a result of the first event described above (Players formula_71 and formula_106 show their cards to each other in front of player formula_107), the agents update their beliefs. We get the situation represented in the pointed epistemic model formula_323 below. In this pointed epistemic model, the following statement holds: formula_329 It states that player formula_71 knows that player formula_106 has the card but player formula_107 'believes' that it is not the case. The result of the second event is represented  below. In this pointed epistemic model, the following statement holds: formula_333. It states that there is common knowledge among formula_106 and formula_107 that they know the true state of the world (namely formula_71 has the red card, formula_106 has the green card and formula_107 has the blue card), but formula_71 does not know it. Based on these three components (epistemic model, event model and product update), Baltag, Moss and Solecki defined a general logical language inspired from the logical language of propositional dynamic logic to reason about information and knowledge change.