fbpx
Wikipedia

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.[1] Independently, Gerbrandy and Groeneveld[2] proposed a system dealing moreover with private announcement and that was inspired by the work of Veltman.[3] Another system was proposed by van Ditmarsch whose main inspiration was the Cluedo game.[4] But the most influential and original system was the system proposed by Baltag, Moss and Solecki.[5][6] 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.[7]

Epistemic Logic edit

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   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.[8] The formal work, based on modal logic, that inaugurated contemporary research into epistemic logic dates back only to 1962 and is due to Hintikka.[9] It then sparked in the 1960s discussions about the principles of knowledge and belief and many axioms for these notions were proposed and discussed.[10] For example, the interaction axioms   and   are often considered to be intuitive principles: if an agent Knows   then (s)he also Believes  , or if an agent Believes  , then (s)he Knows that (s)he Believes  . More recently, these kinds of philosophical theories were taken up by researchers in economics,[11] artificial intelligence and theoretical computer science[12] 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 edit

In the sequel,   is a finite set whose elements are called agents and   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   and a distributed knowledge operator  . Formally, the epistemic language   is defined inductively by the following grammar in BNF:

 

where  ,   and  . The basic epistemic language   is the language   without the common knowledge and distributed knowledge operators. The formula   is an abbreviation for   (for a given  ),   is an abbreviation for  ,   is an abbreviation for   and   an abbreviation for  .

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.[13] It was then applied to distributed systems[12] and to game theory,[14] 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   means that everybody in the group of agents   knows that  . Formally, this corresponds to the following formula:

 

Common knowledge.

Common knowledge of   means that everybody knows   but also that everybody knows that everybody knows  , that everybody knows that everybody knows that everybody knows  , and so on ad infinitum. Formally, this corresponds to the following formula

 

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  : “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   and  . Then everybody knowing   (formally  ) is not enough. Indeed, it might still be possible that the agent   considers possible that the agent   does not know   (formally  ). In that case the agent   will not feel safe to drive on the right because he might consider that the agent  , not knowing  , could drive on the left. To avoid this problem, we could then assume that everybody knows that everybody knows that   (formally  ). This is again not enough to ensure that everybody feels safe to drive on the right. Indeed, it might still be possible that agent   considers possible that agent   considers possible that agent   does not know   (formally  ). In that case and from  ’s point of view,   considers possible that  , not knowing  , will drive on the left. So from  ’s point of view,   might drive on the left as well (by the same argument as above). So   will not feel safe to drive on the right. Reasoning by induction, Lewis showed that for any  ,   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  :  .

Distributed knowledge.

Distributed knowledge of   means that if the agents pulled their knowledge altogether, they would know that   holds. In other words, the knowledge of   is distributed among the agents. The formula   reads as ‘it is distributed knowledge among the set of agents   that   holds’.

Semantics edit

Epistemic logic is a modal logic. So, what we call an epistemic model   is just a Kripke model as defined in modal logic. The set   is a non-empty set whose elements are called possible worlds and the interpretation   is a function specifying which propositional facts (such as ‘Ann has the red card’) are true in each of these worlds. The accessibility relations   are binary relations for each agent  ; they are intended to capture the uncertainty of each agent (about the actual world and about the other agents' uncertainty). Intuitively, we have   when the world   is compatible with agent  ’s information in world   or, in other words, when agent   considers that world   might correspond to the world   (from this standpoint). We abusively write   for   and   denotes the set of worlds  .

Intuitively, a pointed epistemic model  , where  , represents from an external point of view how the actual world   is perceived by the agents  .

For every epistemic model  , every   and every  , we define   inductively by the following truth conditions:

  iff  
  iff  
  iff  
  iff  
  iff  
  iff  

where   is the transitive closure of  : we have that   if, and only if, there are   and   such that   and for all  ,  .

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  ,   and   (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   represented below. In this example,   and  . Each world is labelled by the propositional letters which are true in this world and   corresponds to the actual world. There is an arrow indexed by agent   from a possible world   to a possible world   when  . Reflexive arrows are omitted, which means that for all   and all  , we have that  .

 
Card Example: pointed epistemic model  

  stands for : "  has the red card''

  stand for: "  has the blue card''

  stands for: "  has the green card''

and so on...

When accessibility relations are equivalence relations (like in this example) and we have that  , we say that agent   cannot distinguish world   from world   (or world   is indistinguishable from world   for agent  ). So, for example,   cannot distinguish the actual world   from the possible world where   has the blue card ( ),   has the green card ( ) and   still has the red card ( ).

In particular, the following statements hold:

 

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

 

'  knows that   has either the blue or the green card and that   has either the blue or the green card'.

 

'Everybody knows that   has either the red, green or blue card and this is even common knowledge among all agents'.

Knowledge versus Belief edit

We use the same notation   for both knowledge and belief. Hence, depending on the context,   will either read ‘the agent   Knows that   holds’ or ‘the agent   Believes that   holds’. A crucial difference is that, unlike knowledge, beliefs can be wrong: the axiom   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  : if agent   knows something, she knows that she knows it. These constraints might affect the nature of the accessibility relations   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  . These constraints are matched by particular axioms for the knowledge operator  . Below each property, we give the axiom which defines[15] the class of epistemic frames that fulfill this property. (  stands for   for any  .)

Properties of accessibility relations and corresponding axioms
serial  
D  
transitive  
4  
Euclidicity  
5  
reflexive  
T  
symmetric  
B  
confluent  
.2  
weakly connected  
.3  
semi-Euclidean  
.3.2  
R1  
.4  

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.[16] 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.[17] 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,  ). 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:  . The other intricate axioms .2, .3, .3.2 and .4 have been introduced by epistemic logicians such as Lenzen and Kutchera in the 1970s[10][18] 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.[19]

Axiomatization edit

The Hilbert proof system K for the basic modal logic is defined by the following axioms and inference rules: for all  ,

Proof system   for  
Prop All axioms and inference rules of propositional logic
K  
Nec If   then  

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   ( ) and I know that   implies   (  then I know that   ( ). Stronger constraints can be added. The following proof systems for   are often used in the literature.

Common proof systems for  
KD45 = K+D+4+5 S4.2 = S4+.2 S4.3.2 = S4+.3.2 S5 = S4+5
S4 = K+T+4 S4.3 = S4+.3 S4.4 = S4+.4 Br = K+T+B

We define the set of proof systems  .

Moreover, for all  , we define the proof system   by adding the following axiom schemes and rules of inference to those of  . For all  ,

Dis  
Mix  
Ind  

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

 

So, all the theorems of   are also theorems of   and  . Many philosophers claim that in the most general cases, the logic of knowledge is   or  .[18][20] Typically, in computer science and in many of the theories developed in artificial intelligence, the logic of belief (doxastic logic) is taken to be   and the logic of knowledge (epistemic logic) is taken to be  , even if   is only suitable for situations where the agents do not have mistaken beliefs.[17]   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.[21]

For all  , the class of  –models or  –models is the class of epistemic models whose accessibility relations satisfy the properties listed above defined by the axioms of   or  . Then, for all  ,   is sound and strongly complete for   w.r.t. the class of  –models, and   is sound and strongly complete for   w.r.t. the class of  –models.

Decidability and Complexity edit

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  , 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.[22][23]

Complexity of the satisfiability problem
Logic     with common knowledge
K, S4 PSPACE PSPACE EXPTIME
KD45 NP PSPACE EXPTIME
S5 NP PSPACE EXPTIME

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

Adding Dynamics edit

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:

  1. One represents their beliefs about an initial situation thanks to an epistemic model;
  2. One represents their beliefs about an event taking place in this situation thanks to an event model;
  3. One represents the way the agents update their beliefs about the situation after (or during) the occurrence of the event thanks to a product update.

Typically, an informative event can be a public announcement to all the agents of a formula  : 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 edit

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.[24]

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   be the proposition stating that A is dirty, and   be the proposition stating that B is dirty.

  1. We represent the initial situation by the pointed epistemic model   represented below, where relations between worlds are equivalence relations. States   intuitively represent possible worlds, a proposition (for example  ) satisfiable at one of these worlds intuitively means that in the corresponding possible world, the intuitive interpretation of   (A is dirty) is true. The links between worlds labelled by agents (A or B) intuitively express a notion of indistinguishability for the agent at stake between two possible worlds. For example, the link between   and   labelled by A intuitively means that A can not distinguish the possible world   from   and vice versa. Indeed, A cannot see himself, so he cannot distinguish between a world where he is dirty and one where he is not dirty. However, he can distinguish between worlds where B is dirty or not because he can see B. With this intuitive interpretation we are brought to assume that our relations between worlds are equivalence relations.
     
    Initial situation: pointed epistemic model  
  2. Now, suppose that their father comes and announces that at least one is dirty (formally,  ). Then we update the model and this yields the pointed epistemic model represented below. What we actually do is suppressing the worlds where the content of the announcement is not fulfilled. In our case this is the world where   and   are true. This suppression is what we call the update. We then get the model depicted below. As a result of the announcement, both A and B do know that at least one of them is dirty. We can read this from the epistemic model.
     
    Updated epistemic model after the first announcement  
  3. Now suppose there is a second (and final) announcement that says that neither knows they are dirty (an announcement can express facts about the situation as well as epistemic facts about the knowledge held by the agents). We then update similarly the model by suppressing the worlds which do not satisfy the content of the announcement, or equivalently by keeping the worlds which do satisfy the announcement. This update process thus yields the pointed epistemic model represented below. By interpreting this model, we get that A and B both know that they are dirty, which seems to contradict the content of the announcement. However, if we assume that A and B are both perfect reasoners and that this is common knowledge among them, then this inference makes perfect sense.
 
Updated epistemic model after the second announcement

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.[25]

We define the language   inductively by the following grammar in BNF:

 

where  .

The language   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   is defined as follows:

  iff  

where   with

 ,

  for all   and

 .

The formula   intuitively means that after a truthful announcement of  ,   holds. A public announcement of a proposition   changes the current epistemic model like in the figure below.

 
Eliminate all worlds which currently do not satisfy  

The proof system   defined below is sound and strongly complete for   w.r.t. the class of all pointed epistemic models.

  The Axioms and the rules of inference of the proof system  (see above)
Red 1  
Red 2  
Red 3  
Red 4  

The axioms Red 1 - Red 4 are called reduction axioms because they allow to reduce any formula of   to a provably equivalent formula of   in  . The formula   is a theorem provable in  . It states that after a public announcement of  , the agent knows that   holds.

PAL is decidable, its model checking problem is solvable in polynomial time and its satisfiability problem is PSPACE-complete.[26]

Muddy children puzzle formalized with PAL:

Here are some of the statements that hold in the muddy children puzzle formalized in PAL.

 

'In the initial situation, A is dirty and B is dirty'.

 

'In the initial situation, A does not know whether he is dirty and B neither'.

 

'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:

 

'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:

 

'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.[27]

Arbitrary Events edit

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 edit

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   to   that her card is red can also be described in terms of knowledge and beliefs: while   tells   that her card is red (event  )   believes that nothing happens (event  ). This leads to define the notion of event model whose definition is very similar to that of an epistemic model.

A pointed event model   represents how the actual event represented by   is perceived by the agents. Intuitively,   means that while the possible event represented by   is occurring, agent   considers possible that the possible event represented by   is actually occurring.

An event model is a tuple   where:

  •   is a non-empty set of possible events,
  •   is a binary relation called an accessibility relation on  , for each  ,
  •   is a function called the precondition function assigning to each possible event a formula of  .

  denotes the set   .We write   for  , and   is called a pointed event model (  often represents the actual event).

Card Example:

Let us resume the card example and assume that players   and   show their card to each other. As it turns out,   noticed that   showed her card to   but did not notice that   did so to  . Players   and   know this. This event is represented below in the event model  .

The possible event   corresponds to the actual event ‘players   and   show their and cards respectively to each other’ (with precondition  ),   stands for the event ‘player   shows her green card’ (with precondition  ) and   stands for the atomic event ‘player   shows her red card’ (with precondition  ). Players   and   show their cards to each other, players   and   know this and consider it possible, while player   considers possible that player   shows her red card and also considers possible that player   shows her green card, since he does not know her card. In fact, that is all that player   considers possible because she did not notice that   showed her card.

 
Pointed event model  : Players A and B show their cards to each other in front of player C

Another example of event model is given below. This second example corresponds to the event whereby Player   shows her red card publicly to everybody. Player   shows her red card, players  ,   and   ‘know’ it, players  ,   and   ‘know’ that each of them ‘knows’ it, etc. In other words, there is common knowledge among players  ,   and   that player   shows her red card.

 
Pointed event model  

Product Update edit

The DEL product update is defined below.[5] This update yields a new pointed epistemic model   representing how the new situation which was previously represented by   is perceived by the agents after the occurrence of the event represented by  .

Let   be an epistemic model and let   be an event model. The product update of   and   is the epistemic model   defined as follows: for all   and all  ,

  =  
  =  
  =  

If   and   are such that   then   denotes the pointed epistemic model  . This definition of the product update is conceptually grounded.[6]

Card Example:

As a result of the first event described above (Players   and   show their cards to each other in front of player  ), the agents update their beliefs. We get the situation represented in the pointed epistemic model   below. In this pointed epistemic model, the following statement holds:   It states that player   knows that player   has the card but player   'believes' that it is not the case.

 
Updated pointed epistemic model  

The result of the second event is represented below. In this pointed epistemic model, the following statement holds:  . It states that there is common knowledge among   and   that they know the true state of the world (namely   has the red card,   has the green card and   has the blue card), but   does not know it.

 
Updated pointed epistemic model  

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[25] to reason about information and knowledge change.[5][6]

See also edit

Notes edit

  1. ^ Plaza, Jan (2007-07-26). "Logics of public communications". Synthese. 158 (2): 165–179. doi:10.1007/s11229-007-9168-7. ISSN 0039-7857. S2CID 41619205.
  2. ^ Gerbrandy, Jelle; Groeneveld, Willem (1997-04-01). "Reasoning about Information Change". Journal of Logic, Language and Information. 6 (2): 147–169. doi:10.1023/A:1008222603071. ISSN 0925-8531. S2CID 
dynamic, epistemic, logic, logical, framework, dealing, with, knowledge, information, change, typically, focuses, situations, involving, multiple, agents, studies, their, knowledge, changes, when, events, occur, these, events, change, factual, properties, actu. 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 1 Independently Gerbrandy and Groeneveld 2 proposed a system dealing moreover with private announcement and that was inspired by the work of Veltman 3 Another system was proposed by van Ditmarsch whose main inspiration was the Cluedo game 4 But the most influential and original system was the system proposed by Baltag Moss and Solecki 5 6 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 7 Contents 1 Epistemic Logic 1 1 Syntax 1 2 Semantics 1 3 Knowledge versus Belief 1 4 Axiomatization 1 5 Decidability and Complexity 2 Adding Dynamics 2 1 Public Events 2 2 Arbitrary Events 2 2 1 Event Model 2 2 2 Product Update 3 See also 4 Notes 5 References 6 External linksEpistemic Logic editEpistemic 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 ϵpisthmh displaystyle epsilon pi iota sigma tau eta mu eta nbsp 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 8 The formal work based on modal logic that inaugurated contemporary research into epistemic logic dates back only to 1962 and is due to Hintikka 9 It then sparked in the 1960s discussions about the principles of knowledge and belief and many axioms for these notions were proposed and discussed 10 For example the interaction axioms Kp Bp displaystyle Kp rightarrow Bp nbsp and Bp KBp displaystyle Bp rightarrow KBp nbsp are often considered to be intuitive principles if an agent Knows p displaystyle p nbsp then s he also Believes p displaystyle p nbsp or if an agent Believes p displaystyle p nbsp then s he Knows that s he Believes p displaystyle p nbsp More recently these kinds of philosophical theories were taken up by researchers in economics 11 artificial intelligence and theoretical computer science 12 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 edit In the sequel AGTS 1 n displaystyle AGTS 1 ldots n nbsp is a finite set whose elements are called agents and PROP displaystyle PROP nbsp 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 CA displaystyle C A nbsp and a distributed knowledge operator DA displaystyle D A nbsp Formally the epistemic language LELC displaystyle mathcal L textsf EL C nbsp is defined inductively by the following grammar in BNF LELC ϕ p ϕ ϕ ϕ Kjϕ CAϕ DAϕ displaystyle mathcal L textsf EL C phi p mid neg phi mid phi land phi mid K j phi mid C A phi mid D A phi nbsp where p PROP displaystyle p in PROP nbsp j AGTS displaystyle j in AGTS nbsp and A AGTS displaystyle A subseteq AGTS nbsp The basic epistemic language LEL displaystyle mathcal L EL nbsp is the language LELC displaystyle mathcal L EL C nbsp without the common knowledge and distributed knowledge operators The formula displaystyle bot nbsp is an abbreviation for p p displaystyle neg p land p nbsp for a given p PROP displaystyle p in PROP nbsp Kj ϕ displaystyle langle K j rangle phi nbsp is an abbreviation for Kj ϕ displaystyle neg K j neg phi nbsp EAϕ displaystyle E A phi nbsp is an abbreviation for j AKjϕ displaystyle bigwedge limits j in A K j phi nbsp and Cϕ displaystyle C phi nbsp an abbreviation for CAGTSϕ displaystyle C AGTS phi nbsp 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 13 It was then applied to distributed systems 12 and to game theory 14 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 phi nbsp means that everybody in the group of agents AGTS displaystyle AGTS nbsp knows that ϕ displaystyle phi nbsp Formally this corresponds to the following formula Eϕ j AGTSKjϕ displaystyle E phi underset j in AGTS bigwedge K j phi nbsp Common knowledge Common knowledge of ϕ displaystyle phi nbsp means that everybody knows ϕ displaystyle phi nbsp but also that everybody knows that everybody knows ϕ displaystyle phi nbsp that everybody knows that everybody knows that everybody knows ϕ displaystyle phi nbsp and so on ad infinitum Formally this corresponds to the following formulaCϕ Eϕ EEϕ EEEϕ displaystyle C phi E phi land EE phi land EEE phi land ldots nbsp 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 p displaystyle p nbsp 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 i displaystyle i nbsp and j displaystyle j nbsp Then everybody knowing p displaystyle p nbsp formally Ep displaystyle Ep nbsp is not enough Indeed it might still be possible that the agent i displaystyle i nbsp considers possible that the agent j displaystyle j nbsp does not know p displaystyle p nbsp formally KiKjp displaystyle neg K i K j p nbsp In that case the agent i displaystyle i nbsp will not feel safe to drive on the right because he might consider that the agent j displaystyle j nbsp not knowing p displaystyle p nbsp could drive on the left To avoid this problem we could then assume that everybody knows that everybody knows that p displaystyle p nbsp formally EEp displaystyle EEp nbsp This is again not enough to ensure that everybody feels safe to drive on the right Indeed it might still be possible that agent i displaystyle i nbsp considers possible that agent j displaystyle j nbsp considers possible that agent i displaystyle i nbsp does not know p displaystyle p nbsp formally KiKjKip displaystyle neg K i K j K i p nbsp In that case and from i displaystyle i nbsp s point of view j displaystyle j nbsp considers possible that i displaystyle i nbsp not knowing p displaystyle p nbsp will drive on the left So from i displaystyle i nbsp s point of view j displaystyle j nbsp might drive on the left as well by the same argument as above So i displaystyle i nbsp will not feel safe to drive on the right Reasoning by induction Lewis showed that for any k N displaystyle k in mathbb N nbsp Ep E1p Ekp displaystyle Ep land E 1 p land ldots land E k p nbsp 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 p displaystyle p nbsp Cp displaystyle Cp nbsp Distributed knowledge Distributed knowledge of ϕ displaystyle phi nbsp means that if the agents pulled their knowledge altogether they would know that ϕ displaystyle phi nbsp holds In other words the knowledge of ϕ displaystyle phi nbsp is distributed among the agents The formula DAϕ displaystyle D A phi nbsp reads as it is distributed knowledge among the set of agents A displaystyle A nbsp that ϕ displaystyle phi nbsp holds Semantics edit Epistemic logic is a modal logic So what we call an epistemic model M W R1 Rn I displaystyle mathcal M W R 1 ldots R n I nbsp is just a Kripke model as defined in modal logic The set W displaystyle W nbsp is a non empty set whose elements are called possible worlds and the interpretation I W 2PROP displaystyle I W rightarrow 2 PROP nbsp is a function specifying which propositional facts such as Ann has the red card are true in each of these worlds The accessibility relations Rj W W displaystyle R j subseteq W times W nbsp are binary relations for each agent j AGTS displaystyle j in AGTS nbsp they are intended to capture the uncertainty of each agent about the actual world and about the other agents uncertainty Intuitively we have w v Rj displaystyle w v in R j nbsp when the world v displaystyle v nbsp is compatible with agent j displaystyle j nbsp s information in world w displaystyle w nbsp or in other words when agent j displaystyle j nbsp considers that world v displaystyle v nbsp might correspond to the world w displaystyle w nbsp from this standpoint We abusively write w M displaystyle w in mathcal M nbsp for w W displaystyle w in W nbsp and Rj w displaystyle R j w nbsp denotes the set of worlds v W w v Rj displaystyle v in W w v in R j nbsp Intuitively a pointed epistemic model M w displaystyle mathcal M w nbsp where w M displaystyle w in mathcal M nbsp represents from an external point of view how the actual world w displaystyle w nbsp is perceived by the agents AGTS displaystyle AGTS nbsp For every epistemic model M displaystyle mathcal M nbsp every w M displaystyle w in mathcal M nbsp and every ϕ LEL displaystyle phi in mathcal L textsf EL nbsp we define M w ϕ displaystyle mathcal M w models phi nbsp inductively by the following truth conditions M w p displaystyle mathcal M w models p nbsp iff p I w displaystyle p in I w nbsp M w ϕ displaystyle mathcal M w models neg phi nbsp iff it is not the case that M w ϕ displaystyle textrm it is not the case that mathcal M w models phi nbsp M w ϕ ps displaystyle mathcal M w models phi land psi nbsp iff M w ϕ and M w ps displaystyle mathcal M w models phi textrm and mathcal M w models psi nbsp M w Kjϕ displaystyle mathcal M w models K j phi nbsp iff for all v Rj w M v ϕ textstyle textrm for all v in R j w mathcal M v models phi nbsp M w CAϕ displaystyle mathcal M w models C A phi nbsp iff for all v j ARj w M v ϕ displaystyle textrm for all v in left underset j in A bigcup R j right w mathcal M v models phi nbsp M w DAϕ displaystyle mathcal M w models D A phi nbsp iff for all v j ARj w M v ϕ displaystyle textrm for all v in underset j in A bigcap R j w mathcal M v models phi nbsp where j ARj displaystyle left underset j in A bigcup R j right nbsp is the transitive closure of j ARj displaystyle underset j in A bigcup R j nbsp we have that v j ARj w displaystyle v in left underset j in A bigcup R j right w nbsp if and only if there are w0 wm M displaystyle w 0 ldots w m in mathcal M nbsp and j1 jm A displaystyle j 1 ldots j m in A nbsp such that w0 w wm v displaystyle w 0 w w m v nbsp and for all i 1 m displaystyle i in 1 ldots m nbsp wi 1Rjiwi displaystyle w i 1 R j i w i nbsp 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 A displaystyle A nbsp B displaystyle B nbsp and C displaystyle C nbsp 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 M w displaystyle mathcal M w nbsp represented below In this example AGTS A B C displaystyle AGTS A B C nbsp and PROP A B C B C A C A B displaystyle PROP color red A color green B color blue C color red B color green C color blue A color red C color green A color blue B nbsp Each world is labelled by the propositional letters which are true in this world and w displaystyle w nbsp corresponds to the actual world There is an arrow indexed by agent j A B C displaystyle j in A B C nbsp from a possible world u displaystyle u nbsp to a possible world v displaystyle v nbsp when u v Rj displaystyle u v in R j nbsp Reflexive arrows are omitted which means that for all j A B C displaystyle j in A B C nbsp and all v M displaystyle v in mathcal M nbsp we have that v v Rj displaystyle v v in R j nbsp nbsp Card Example pointed epistemic model M w displaystyle mathcal M w nbsp A displaystyle color red A nbsp stands for A displaystyle A nbsp has the red card C displaystyle color blue C nbsp stand for C displaystyle C nbsp has the blue card B displaystyle color green B nbsp stands for B displaystyle B nbsp has the green card and so on When accessibility relations are equivalence relations like in this example and we have that w v Rj displaystyle w v in R j nbsp we say that agent j displaystyle j nbsp cannot distinguish world w displaystyle w nbsp from world v displaystyle v nbsp or world w displaystyle w nbsp is indistinguishable from world v displaystyle v nbsp for agent j displaystyle j nbsp So for example A textstyle A nbsp cannot distinguish the actual world w displaystyle w nbsp from the possible world where B displaystyle B nbsp has the blue card B displaystyle color blue B nbsp C displaystyle C nbsp has the green card C displaystyle color green C nbsp and A displaystyle A nbsp still has the red card A displaystyle color red A nbsp In particular the following statements hold M w A KAA C KCC B KBB displaystyle mathcal M w models color red A land K A color red A land color blue C land K C color blue C land color green B land K B color green B nbsp All the agents know the color of their card M w KA B B KA C C displaystyle mathcal M w models K A color blue B vee color green B land K A color blue C vee color green C nbsp A displaystyle A nbsp knows that B displaystyle B nbsp has either the blue or the green card and that C displaystyle C nbsp has either the blue or the green card M w E A A A C A A A displaystyle mathcal M w models E color red A vee color blue A vee color green A land C color red A vee color blue A vee color green A nbsp Everybody knows that A displaystyle A nbsp has either the red green or blue card and this is even common knowledge among all agents Knowledge versus Belief edit We use the same notation Kj displaystyle K j nbsp for both knowledge and belief Hence depending on the context Kjϕ displaystyle K j phi nbsp will either read the agent j displaystyle j nbsp Knows that ϕ displaystyle phi nbsp holds or the agent j displaystyle j nbsp Believes that ϕ displaystyle phi nbsp holds A crucial difference is that unlike knowledge beliefs can be wrong the axiom Kjϕ ϕ displaystyle K j phi rightarrow phi nbsp 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 Kjϕ KjKjϕ displaystyle K j phi rightarrow K j K j phi nbsp if agent j displaystyle j nbsp knows something she knows that she knows it These constraints might affect the nature of the accessibility relations Rj displaystyle R j nbsp 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 Rj displaystyle R j nbsp These constraints are matched by particular axioms for the knowledge operator Kj displaystyle K j nbsp Below each property we give the axiom which defines 15 the class of epistemic frames that fulfill this property Kϕ displaystyle K phi nbsp stands for Kjϕ displaystyle K j phi nbsp for any j AGTS displaystyle j in AGTS nbsp Properties of accessibility relations and corresponding axioms serial R w displaystyle R w neq emptyset nbsp D Kϕ K ϕ displaystyle K phi rightarrow langle K rangle phi nbsp transitive If w R w and w R w then w R w displaystyle textrm If w in R w textrm and w in R w textrm then w in R w nbsp 4 Kϕ KKϕ displaystyle K phi rightarrow KK phi nbsp Euclidicity If w R w and w R w then w R w displaystyle textrm If w in R w textrm and w in R w textrm then w in R w nbsp 5 Kϕ K Kϕ displaystyle neg K phi rightarrow K neg K phi nbsp reflexive w R w displaystyle w in R w nbsp T Kϕ ϕ displaystyle K phi rightarrow phi nbsp symmetric If w R w then w R w displaystyle textrm If w in R w textrm then w in R w nbsp B ϕ K K ϕ displaystyle phi rightarrow K neg K neg phi nbsp confluent If w R w and w R w then there is v such that v R w and v R w displaystyle textrm If w in R w textrm and w in R w textrm then there is v textrm such that v in R w textrm and v in R w nbsp 2 K Kϕ K K ϕ displaystyle langle K rangle K phi rightarrow K langle K rangle phi nbsp weakly connected If w R w and w R w then w w or w R w or w R w displaystyle textrm If w in R w textrm and w in R w textrm then w w textrm or w in R w textrm or w in R w nbsp 3 K ϕ K ps K ϕ ps K ps K ϕ K ϕ K ps displaystyle langle K rangle phi land langle K rangle psi rightarrow langle K rangle phi land psi vee langle K rangle psi land langle K rangle phi vee langle K rangle phi land langle K rangle psi nbsp semi Euclidean If w R w and w R w and w R w then w R w displaystyle textrm If w in R w textrm and w notin R w textrm and w in R w textrm then w in R w nbsp 3 2 K ϕ K Kps K K ϕ ps displaystyle langle K rangle phi land langle K rangle K psi rightarrow K langle K rangle phi vee psi nbsp R1 If w R w and w w and w R w then w R w displaystyle textrm If w in R w textrm and w neq w textrm and w in R w textrm then w in R w nbsp 4 ϕ K Kϕ Kϕ displaystyle phi land langle K rangle K phi rightarrow K phi nbsp 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 16 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 17 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 ϕ K Kϕ displaystyle neg neg phi land neg K neg K phi nbsp 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 B displaystyle neg B bot nbsp The other intricate axioms 2 3 3 2 and 4 have been introduced by epistemic logicians such as Lenzen and Kutchera in the 1970s 10 18 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 19 Axiomatization edit The Hilbert proof system K for the basic modal logic is defined by the following axioms and inference rules for all j AGTS displaystyle j in AGTS nbsp Proof system K displaystyle textsf K nbsp for LEL displaystyle mathcal L EL nbsp Prop All axioms and inference rules of propositional logicK Kj ϕ ps Kjϕ Kjps displaystyle K j phi rightarrow psi rightarrow K j phi rightarrow K j psi nbsp Nec If ϕ displaystyle phi nbsp then Kjϕ displaystyle K j phi nbsp 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 phi nbsp Kϕ displaystyle K phi nbsp and I know that ϕ displaystyle phi nbsp implies ps displaystyle psi nbsp K ϕ ps displaystyle K phi rightarrow psi nbsp then I know that ps displaystyle psi nbsp Kps displaystyle K psi nbsp Stronger constraints can be added The following proof systems for LEL displaystyle mathcal L textsf EL nbsp are often used in the literature Common proof systems for LEL displaystyle mathcal L EL nbsp KD45 K D 4 5 S4 2 S4 2 S4 3 2 S4 3 2 S5 S4 5S4 K T 4 S4 3 S4 3 S4 4 S4 4 Br K T BWe define the set of proof systems LEL K KD45 S4 S4 2 S4 3 S4 3 2 S4 4 S5 displaystyle mathbb L textsf EL textsf K textsf KD45 textsf S4 textsf S4 2 textsf S4 3 textsf S4 3 2 textsf S4 4 textsf S5 nbsp Moreover for all H LEL displaystyle mathcal H in mathbb L textsf EL nbsp we define the proof system HC displaystyle mathcal H textsf C nbsp by adding the following axiom schemes and rules of inference to those of H displaystyle mathcal H nbsp For all A AGTS displaystyle A subseteq AGTS nbsp Dis Kjϕ DAϕ displaystyle K j phi rightarrow D A phi nbsp Mix CAϕ EA ϕ CAϕ displaystyle C A phi rightarrow E A phi land C A phi nbsp Ind if ϕ EA ps ϕ then ϕ CAps displaystyle textrm if phi rightarrow E A psi land phi textrm then phi rightarrow C A psi nbsp The relative strength of the proof systems for knowledge is as follows S4 S4 2 S4 3 S4 3 2 S4 4 S5 displaystyle textsf S4 subset textsf S4 2 subset textsf S4 3 subset textsf S4 3 2 subset textsf S4 4 subset textsf S5 nbsp So all the theorems of S4 2 displaystyle textsf S4 2 nbsp are also theorems of S4 3 S4 3 2 S4 4 displaystyle textsf S4 3 textsf S4 3 2 textsf S4 4 nbsp and S5 displaystyle textsf S5 nbsp Many philosophers claim that in the most general cases the logic of knowledge is S4 2 displaystyle textsf S4 2 nbsp or S4 3 displaystyle textsf S4 3 nbsp 18 20 Typically in computer science and in many of the theories developed in artificial intelligence the logic of belief doxastic logic is taken to be KD45 displaystyle textsf KD45 nbsp and the logic of knowledge epistemic logic is taken to be S5 displaystyle textsf S5 nbsp even if S5 displaystyle textsf S5 nbsp is only suitable for situations where the agents do not have mistaken beliefs 17 Br displaystyle textsf Br nbsp 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 21 For all H LEL displaystyle mathcal H in mathbb L textsf EL nbsp the class of H displaystyle mathcal H nbsp models or HC displaystyle mathcal H textsf C nbsp models is the class of epistemic models whose accessibility relations satisfy the properties listed above defined by the axioms of H displaystyle mathcal H nbsp or HC displaystyle mathcal H textsf C nbsp Then for all H LEL displaystyle mathcal H in mathbb L textsf EL nbsp H displaystyle mathcal H nbsp is sound and strongly complete for LEL displaystyle mathcal L textsf EL nbsp w r t the class of H displaystyle mathcal H nbsp models and HC displaystyle mathcal H textsf C nbsp is sound and strongly complete for LELC displaystyle mathcal L textsf EL textsf C nbsp w r t the class of HC displaystyle mathcal H textsf C nbsp models Decidability and Complexity edit 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 n 2 displaystyle n geq 2 nbsp 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 22 23 Complexity of the satisfiability problem Logic n 1 displaystyle n 1 nbsp n 2 displaystyle n geq 2 nbsp with common knowledgeK S4 PSPACE PSPACE EXPTIMEKD45 NP PSPACE EXPTIMES5 NP PSPACE EXPTIMEThe computational complexity of the model checking problem is in P in all cases Adding Dynamics editDynamic 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 One represents their beliefs about an initial situation thanks to an epistemic model One represents their beliefs about an event taking place in this situation thanks to an event model One represents the way the agents update their beliefs about the situation after or during the occurrence of the event thanks to a product update Typically an informative event can be a public announcement to all the agents of a formula ps displaystyle psi nbsp 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 edit 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 24 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 p displaystyle p nbsp be the proposition stating that A is dirty and q displaystyle q nbsp be the proposition stating that B is dirty We represent the initial situation by the pointed epistemic model N s displaystyle mathcal N s nbsp represented below where relations between worlds are equivalence relations States s t u v displaystyle s t u v nbsp intuitively represent possible worlds a proposition for example p displaystyle p nbsp satisfiable at one of these worlds intuitively means that in the corresponding possible world the intuitive interpretation of p displaystyle p nbsp A is dirty is true The links between worlds labelled by agents A or B intuitively express a notion of indistinguishability for the agent at stake between two possible worlds For example the link between s displaystyle s nbsp and t displaystyle t nbsp labelled by A intuitively means that A can not distinguish the possible world s displaystyle s nbsp from t displaystyle t nbsp and vice versa Indeed A cannot see himself so he cannot distinguish between a world where he is dirty and one where he is not dirty However he can distinguish between worlds where B is dirty or not because he can see B With this intuitive interpretation we are brought to assume that our relations between worlds are equivalence relations nbsp Initial situation pointed epistemic model N s displaystyle mathcal N s nbsp Now suppose that their father comes and announces that at least one is dirty formally p q displaystyle p vee q nbsp Then we update the model and this yields the pointed epistemic model represented below What we actually do is suppressing the worlds where the content of the announcement is not fulfilled In our case this is the world where p displaystyle neg p nbsp and q displaystyle neg q nbsp are true This suppression is what we call the update We then get the model depicted below As a result of the announcement both A and B do know that at least one of them is dirty We can read this from the epistemic model nbsp Updated epistemic model after the first announcement p q displaystyle p vee q nbsp Now suppose there is a second and final announcement that says that neither knows they are dirty an announcement can express facts about the situation as well as epistemic facts about the knowledge held by the agents We then update similarly the model by suppressing the worlds which do not satisfy the content of the announcement or equivalently by keeping the worlds which do satisfy the announcement This update process thus yields the pointed epistemic model represented below By interpreting this model we get that A and B both know that they are dirty which seems to contradict the content of the announcement However if we assume that A and B are both perfect reasoners and that this is common knowledge among them then this inference makes perfect sense nbsp Updated epistemic model after the second announcementPublic announcement logic PAL We present the syntax and semantic of Public Announcement Logic PAL which combines features of epistemic logic and propositional dynamic logic 25 We define the language LPAL displaystyle mathcal L PAL nbsp inductively by the following grammar in BNF LPAL ϕ p ϕ ϕ ϕ Kjϕ ϕ ϕ displaystyle mathcal L PAL phi p mid neg phi mid phi land phi mid K j phi mid phi phi nbsp where j AGTS displaystyle j in AGTS nbsp The language LPAL displaystyle mathcal L PAL nbsp 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 ps ϕ displaystyle psi phi nbsp is defined as follows M w ps ϕ displaystyle mathcal M w models psi phi nbsp iff if M w ps then Mps w ϕ displaystyle mbox if mathcal M w models psi mbox then mathcal M psi w models phi nbsp where Mps Wps R1ps Rnps Ips displaystyle mathcal M psi W psi R 1 psi ldots R n psi I psi nbsp withWps w W M w ps displaystyle W psi w in W mathcal M w models psi nbsp Rjps Rj Wps Wps displaystyle R j psi R j cap W psi times W psi nbsp for all j 1 n displaystyle j in 1 ldots n nbsp andIps w I w for all w Wps displaystyle I psi w I w textrm for all w in W psi nbsp The formula ps ϕ displaystyle psi phi nbsp intuitively means that after a truthful announcement of ps displaystyle psi nbsp ϕ displaystyle phi nbsp holds A public announcement of a proposition ps displaystyle psi nbsp changes the current epistemic model like in the figure below nbsp Eliminate all worlds which currently do not satisfy ps displaystyle psi nbsp The proof system HPAL displaystyle mathcal H PAL nbsp defined below is sound and strongly complete for LPAL displaystyle mathcal L PAL nbsp w r t the class of all pointed epistemic models K displaystyle textsf K nbsp The Axioms and the rules of inference of the proof system K displaystyle textsf K nbsp see above Red 1 ps p ps p displaystyle psi p leftrightarrow psi rightarrow p nbsp Red 2 ps ϕ ps ps ϕ displaystyle psi neg phi leftrightarrow psi rightarrow neg psi phi nbsp Red 3 ps ϕ x ps ϕ ps x displaystyle psi phi land chi leftrightarrow psi phi land psi chi nbsp Red 4 ps Kiϕ ps Ki ps ps ϕ displaystyle psi K i phi leftrightarrow left psi rightarrow K i psi rightarrow psi phi right nbsp The axioms Red 1 Red 4 are called reduction axioms because they allow to reduce any formula of LPAL displaystyle mathcal L PAL nbsp to a provably equivalent formula of LEL displaystyle mathcal L EL nbsp in HPAL displaystyle mathcal H PAL nbsp The formula q Kq displaystyle q Kq nbsp is a theorem provable in HPAL displaystyle mathcal H PAL nbsp It states that after a public announcement of q displaystyle q nbsp the agent knows that q displaystyle q nbsp holds PAL is decidable its model checking problem is solvable in polynomial time and its satisfiability problem is PSPACE complete 26 Muddy children puzzle formalized with PAL Here are some of the statements that hold in the muddy children puzzle formalized in PAL N s p q displaystyle mathcal N s models p land q nbsp In the initial situation A is dirty and B is dirty N s KAp KA p KBq KB q displaystyle mathcal N s models neg K A p land neg K A neg p land neg K B q land neg K B neg q nbsp In the initial situation A does not know whether he is dirty and B neither N s p q KA p q KB p q displaystyle mathcal N s models p vee q K A p vee q land K B p vee q nbsp 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 N s p q KAp KA p KBq KB q displaystyle mathcal N s models p vee q neg K A p land neg K A neg p land neg K B q land neg K B neg q nbsp 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 N s p q KAp KA p KBq KB q KAp KBq displaystyle mathcal N s models p vee q neg K A p land neg K A neg p land neg K B q land neg K B neg q K A p land K B q nbsp 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 27 Arbitrary Events edit 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 edit 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 A displaystyle A nbsp to B displaystyle B nbsp that her card is red can also be described in terms of knowledge and beliefs while A displaystyle A nbsp tells B displaystyle B nbsp that her card is red event e displaystyle e nbsp C displaystyle C nbsp believes that nothing happens event f displaystyle f nbsp This leads to define the notion of event model whose definition is very similar to that of an epistemic model A pointed event model E e displaystyle mathcal E e nbsp represents how the actual event represented by e displaystyle e nbsp is perceived by the agents Intuitively f Rj e displaystyle f in R j e nbsp means that while the possible event represented by e displaystyle e nbsp is occurring agent j displaystyle j nbsp considers possible that the possible event represented by f displaystyle f nbsp is actually occurring An event model is a tuple E Wa R1a Rma Ia displaystyle mathcal E W alpha R 1 alpha ldots R m alpha I alpha nbsp where Wa displaystyle W alpha nbsp is a non empty set of possible events Rja Wa Wa displaystyle R j alpha subseteq W alpha times W alpha nbsp is a binary relation called an accessibility relation on Wa displaystyle W alpha nbsp for each j AGTS displaystyle j in AGTS nbsp Ia Wa LEL displaystyle I alpha W alpha rightarrow mathcal L textsf EL nbsp is a function called the precondition function assigning to each possible event a formula of LEL displaystyle mathcal L textsf EL nbsp Rja e displaystyle R j alpha e nbsp denotes the set f Wa e f Rja displaystyle f in W alpha e f in R j alpha nbsp We write e E displaystyle e in mathcal E nbsp for e Wa displaystyle e in W alpha nbsp and E e displaystyle mathcal E e nbsp is called a pointed event model e displaystyle e nbsp often represents the actual event Card Example Let us resume the card example and assume that players A displaystyle A nbsp and B displaystyle B nbsp show their card to each other As it turns out C displaystyle C nbsp noticed that A displaystyle A nbsp showed her card to B displaystyle B nbsp but did not notice that B displaystyle B nbsp did so to A displaystyle A nbsp Players A displaystyle A nbsp and B displaystyle B nbsp know this This event is represented below in the event model E e displaystyle mathcal E e nbsp The possible event e displaystyle e nbsp corresponds to the actual event players A displaystyle A nbsp and B displaystyle B nbsp show their and cards respectively to each other with precondition A B displaystyle color red A land color green B nbsp f displaystyle f nbsp stands for the event player A displaystyle A nbsp shows her green card with precondition A displaystyle color green A nbsp and g displaystyle g nbsp stands for the atomic event player A displaystyle A nbsp shows her red card with precondition A displaystyle color red A nbsp Players A displaystyle A nbsp and B displaystyle B nbsp show their cards to each other players A displaystyle A nbsp and B displaystyle B nbsp know this and consider it possible while player C displaystyle C nbsp considers possible that player A displaystyle A nbsp shows her red card and also considers possible that player A displaystyle A nbsp shows her green card since he does not know her card In fact that is all that player C displaystyle C nbsp considers possible because she did not notice that B displaystyle B nbsp showed her card nbsp Pointed event model E e displaystyle mathcal E e nbsp Players A and B show their cards to each other in front of player CAnother example of event model is given below This second example corresponds to the event whereby Player A displaystyle A nbsp shows her red card publicly to everybody Player A displaystyle A nbsp shows her red card players A displaystyle A nbsp B displaystyle B nbsp and C displaystyle C nbsp know it players A displaystyle A nbsp B displaystyle B nbsp and C displaystyle C nbsp know that each of them knows it etc In other words there is common knowledge among players A displaystyle A nbsp B displaystyle B nbsp and C displaystyle C nbsp that player A displaystyle A nbsp shows her red card nbsp Pointed event model F e displaystyle mathcal F e nbsp Product Update edit The DEL product update is defined below 5 This update yields a new pointed epistemic model M w E e displaystyle mathcal M w otimes mathcal E e nbsp representing how the new situation which was previously represented by M w displaystyle mathcal M w nbsp is perceived by the agents after the occurrence of the event represented by E e displaystyle mathcal E e nbsp Let M W R1 Rn I displaystyle mathcal M W R 1 ldots R n I nbsp be an epistemic model and let E Wa R1a Rna Ia displaystyle mathcal E W alpha R 1 alpha ldots R n alpha I alpha nbsp be an event model The product update of M displaystyle mathcal M nbsp and E displaystyle mathcal E nbsp is the epistemic model M E W R1 Rn I displaystyle mathcal M otimes mathcal mathcal E W otimes R 1 otimes ldots R n otimes I otimes nbsp defined as follows for all v W displaystyle v in W nbsp and all f Wa displaystyle f in W alpha nbsp W displaystyle W otimes nbsp v f W Wa M v Ia f displaystyle v f in W times W alpha mathcal M v models I alpha f nbsp Rj v f displaystyle R j otimes v f nbsp u g W u Rj v and g Rja f displaystyle u g in W otimes u in R j v textrm and g in R j alpha f nbsp I v f displaystyle I otimes v f nbsp I v displaystyle I v nbsp If w W displaystyle w in W nbsp and e Wa displaystyle e in W alpha nbsp are such that M w Ia e displaystyle mathcal M w models I alpha e nbsp then M w E e displaystyle mathcal M w otimes mathcal E e nbsp denotes the pointed epistemic model M E w e displaystyle mathcal M otimes mathcal E w e nbsp This definition of the product update is conceptually grounded 6 Card Example As a result of the first event described above Players A displaystyle A nbsp and B displaystyle B nbsp show their cards to each other in front of player C displaystyle C nbsp the agents update their beliefs We get the situation represented in the pointed epistemic model M w E e displaystyle mathcal M w otimes mathcal E e nbsp below In this pointed epistemic model the following statement holds M w E e B KAB KC KAB displaystyle mathcal M w otimes mathcal E e models color green B land K A color green B land K C neg K A color green B nbsp It states that player A displaystyle A nbsp knows that player B displaystyle B nbsp has the card but player C displaystyle C nbsp believes that it is not the case nbsp Updated pointed epistemic model M w E e displaystyle mathcal M w otimes mathcal E e nbsp The result of the second event is represented below In this pointed epistemic model the following statement holds M w F e C B C A B C KA B C displaystyle mathcal M w otimes mathcal F e models C B C color red A land color green B land color blue C land neg K A color green B land color blue C nbsp It states that there is common knowledge among B displaystyle B nbsp and C displaystyle C nbsp that they know the true state of the world namely A displaystyle A nbsp has the red card B displaystyle B nbsp has the green card and C displaystyle C nbsp has the blue card but A displaystyle A nbsp does not know it nbsp Updated pointed epistemic model M w F e displaystyle mathcal M w otimes mathcal F e nbsp 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 25 to reason about information and knowledge change 5 6 See also edit nbsp Philosophy portalEpistemic logic Epistemology Logic in computer science Modal logicNotes edit Plaza Jan 2007 07 26 Logics of public communications Synthese 158 2 165 179 doi 10 1007 s11229 007 9168 7 ISSN 0039 7857 S2CID 41619205 Gerbrandy Jelle Groeneveld Willem 1997 04 01 Reasoning about Information Change Journal of Logic Language and Information 6 2 147 169 doi 10 1023 A 1008222603071 ISSN 0925 8531 S2CID a, wikipedia, wiki, book, books, library,

article

, read, download, free, free download, mp3, video, mp4, 3gp, jpg, jpeg, gif, png, picture, music, song, movie, book, game, games.