Dynamic Epistemic Logic This article tells the story of the rise of dynamic epistemic logic, which began with epistemic logic, the logic of knowledge, in the 1960s. Then, in the late 1980s, came dynamic epistemic logic, the logic of change of knowledge. Much of it was motivated by puzzles and paradoxes. The number … Continue reading Dynamic Epistemic Logic →.

Dynamic Epistemic Logic This article tells the story of the rise of dynamic epistemic logic, which began with epistemic logic, the logic of knowledge, in the 1960s. Then, in the late 1980s, came dynamic epistemic logic, the logic of change of knowledge. Much of it was motivated by puzzles and paradoxes. The number … Continue reading Dynamic Epistemic Logic →.

In ‘belief revision’ a theory\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\cal K}$$\end{document} is revised with a formula φ resulting in a revised theory \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\cal K}\ast\varphi$$\end{document}. Typically, \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\neg\varphi$$\end{document} is in \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\cal K}$$\end{document}, one has to give up belief in \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\neg\varphi$$\end{document} by a process (...) of retraction, and φ is in \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\cal K}\ast\varphi$$\end{document}. We propose to model belief revision in a dynamic epistemic logic. In this setting, we typically have an information state (pointed Kripke model) for the theory \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\cal K}$$\end{document} wherein the agent believes the negation of the revision formula, i.e., wherein \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$B\neg\varphi$$\end{document} is true. The revision with φ is a program *φ that transforms this information state into a new information state. The transformation is described by a dynamic modal operator [*φ], that is interpreted as a binary relation [ [*φ] ] between information states. The next information state is computed from the current information state and the belief revision formula. If the revision is successful, the agent believes φ in the resulting state, i.e., Bφ is then true. To make this work, as information states we propose ‘doxastic epistemic models’ that represent both knowledge and degrees of belief. These are multi-modal and multi-agent Kripke models. They are constructed from preference relations for agents, and they satisfy various characterizable multi-agent frame properties. Iterated, revocable, and higher-order belief revision are all quite natural in this setting. We present, for an example, five different ways of such dynamic belief revision. One can also see that as a non-deterministic epistemic action with two alternatives, where one is preferred over the other, and there is a natural generalization to general epistemic actions with preferences. (shrink)

In an information state where various agents have both factual knowledge and knowledge about each other, announcements can be made that change the state of information. Such informative announcements can have the curious property that they become false because they are announced. The most typical example of that is ‘fact p is true and you don’t know that’, after which you know that p, which entails the negation of the announcement formula. The announcement of such a formula in a given (...) information state is called an unsuccessful update. A successful formula is a formula that always becomes common knowledge after being announced. Analysis of information systems and ‘philosophical puzzles’ reveals a growing number of dynamic phenomena that can be described or explained by unsuccessful updates. This increases our understanding of such philosophical problems. We also investigate the syntactic characterization of the successful formulas. (shrink)

Dynamic Epistemic Logic is the logic of knowledge change. This book provides various logics to support such formal specifications, including proof systems. Concrete examples and epistemic puzzles enliven the exposition. The book also offers exercises with answers. It is suitable for graduate courses in logic. Many examples, exercises, and thorough completeness proofs and expressivity results are included. A companion web page offers slides for lecturers and exams for further practice.

Dynamic epistemic logic describes the possible information-changing actions available to individual agents, and their knowledge pre-and post conditions. For example, public announcement logic describes actions in the form of public, truthful announcements. However, little research so far has considered describing and analysing rational choice between such actions, i.e., predicting what rational self-interested agents actually will or should do. Since the outcome of information exchange ultimately depends on the actions chosen by all the agents in the system, and assuming that agents (...) have preferences over such outcomes, this is a game theoretic scenario. This is, in our opinion, an interesting general research direction, combining logic and game theory in the study of rational information exchange. In this article we take some first steps in this direction: we consider the case where available actions are public announcements, and where each agent has a (typically epistemic) goal formula that she would like to become true. What will each agent announce? The truth of the goal formula also depends on the announcements made by other agents. We analyse such public announcement games. (shrink)

In ‘belief revision’ a theory is revised with a formula φ resulting in a revised theory . Typically, is in , one has to give up belief in by a process of retraction, and φ is in . We propose to model belief revision in a dynamic epistemic logic. In this setting, we typically have an information state (pointed Kripke model) for the theory wherein the agent believes the negation of the revision formula, i.e., wherein is true. The revision with (...) φ is a program *φ that transforms this information state into a new information state. The transformation is described by a dynamic modal operator [*φ], that is interpreted as a binary relation [ [*φ] ] between information states. The next information state is computed from the current information state and the belief revision formula. If the revision is successful, the agent believes φ in the resulting state, i.e., Bφ is then true. To make this work, as information states we propose ‘doxastic epistemic models’ that represent both knowledge and degrees of belief. These are multi-modal and multi-agent Kripke models. They are constructed from preference relations for agents, and they satisfy various characterizable multi-agent frame properties. Iterated, revocable, and higher-order belief revision are all quite natural in this setting. We present, for an example, five different ways of such dynamic belief revision. One can also see that as a non-deterministic epistemic action with two alternatives, where one is preferred over the other, and there is a natural generalization to general epistemic actions with preferences. (shrink)

Editors van Ditmarsch, Hendriks and Verbrugge of this special issue of topiCS on lying describe some recent trends in research on lying from a multidisciplinary perspective, including logic, philosophy, linguistics, psychology, cognitive science, behavioral economics, and artificial intelligence. Furthermore, they outline the seven contributions to this special issue.

In an information state where various agents have both factual knowledge and knowledge about each other, announcements can be made that change the state of information. Such informative announcements can have the curious property that they become false because they are announced. The most typical example of that is 'fact p is true and you don't know that', after which you know that p, which entails the negation of the announcement formula. The announcement of such a formula in a given (...) information state is called an unsuccessful update. A successful formula is a formula that always becomes common knowledge after being announced. Analysis of information systems and 'philosophical puzzles' reveals a growing number of dynamic phenomena that can be described or explained by unsuccessful updates. This increases our understanding of such philosophical problems. We also investigate the syntactic characterization of the successful formulas. (shrink)

We model the forgetting of propositional variables in a modal logical context where agents become ignorant and are aware of each others’ or their own resulting ignorance. The resulting logic is sound and complete. It can be compared to variable-forgetting as abstraction from information, wherein agents become unaware of certain variables: by employing elementary results for bisimulation, it follows that beliefs not involving the forgotten atom(s) remain true.

We propose a dynamic logic of lying, wherein a ‘lie that $$\varphi $$ ’ is an action in the sense of dynamic modal logic, that is interpreted as a state transformer relative to the formula $$\varphi $$. The states that are being transformed are pointed Kripke models encoding the uncertainty of agents about their beliefs. Lies can be about factual propositions but also about modal formulas, such as the beliefs of other agents or the belief consequences of the lies of (...) other agents. We distinguish two speaker perspectives: an outside observer who is lying to an agent that is modelled in the system, and an agent who is lying to another agent, and where both are modelled in the system. We distinguish three addressee perspectives: the credulous agent who believes everything that it is told, the skeptical agent who only believes what it is told if that is consistent with its current beliefs, and the belief revising agent who believes everything that it is told by consistently revising its current, possibly conflicting, beliefs. The logics have complete axiomatizations, which can most elegantly be shown by way of their embedding in what is known as action model logic or in the extension of that logic to belief revision. (shrink)

We model three examples of beliefs that agents may have about other agents' beliefs, and provide motivation for this conceptualization from the theory of mind literature. We assume a modal logical framework for modelling degrees of belief by partially ordered preference relations. In this setting, we describe that agents believe that other agents do not distinguish among their beliefs ('no preferences'), that agents believe that the beliefs of other agents are in part as their own ('my preferences'), and the special (...) case that agents believe that the beliefs of other agents are exactly as their own ('preference refinement'). This multi-agent belief interaction is frame characterizable. We provide examples for introspective agents. We investigate which of these forms of belief interaction are preserved under three common forms of belief revision. (shrink)

We model the forgetting of propositional variables in a modal logical context where agents become ignorant and are aware of each others’ or their own resulting ignorance. The resulting logic is sound and complete. It can be compared to variable-forgetting as abstraction from information, wherein agents become unaware of certain variables: by employing elementary results for bisimulation, it follows that beliefs not involving the forgotten atom(s) remain true.

Suppose we have a stack of cards that is divided over some players. For certain distributions of cards it is possible to communicate your hand of cards to another player by public announcements, without yet another player learning any of your cards. A solution to this problem consists of some sequence of announcements and is called an exchange. It is called a direct exchange if it consists of (the minimum of) two announcements only. The announcements in an exchange have a (...) special form: they are safe communications, an interesting new form of update. Certain unsafe communications turn out to be unsuccessful updates. A communication is a public announcement that is known to be true. Each communication may be about a set of alternative card deals only, and even about a set of alternatives to the communicating player's own hand only. We list the direct exchanges for a deal of seven cards where the two players holding three cards communicate their hands to each other. Our work may be applicable to the design of cryptographic protocols. (shrink)

Take your average publication on the dynamics of knowledge. In one of its first paragraphs you will probably encounter a phrase like “a logic of public announcements was first proposed by Plaza in 1989 (Plaza 1989).” Tracking down this publication seems easy, because googling its title ‘Logics of Public Communications’ takes you straight to Jan Plaza’s website where it is online available in the author’s own version, including, on that page, very helpful and full bibliographic references to the proceedings in (...) which it originally appeared. Those proceedings are then somewhat harder to find. In fact, I have never seen them. Unfortunately, for the research community, Plaza’s work has never been followed up by a journal version. I am very grateful to the editor Wiebe van der Hoek of the journal ‘Knowledge, Rationality, and Action’ to correct this omission.Plaza’s work is reprinted as such, without an update encompassing more than fifteen additional years of research in this area. This commentary aims to provide some background to bridge that gap. (shrink)

Pit is a multi-player card game that simulates the commodities trading market, and where actions consist of bidding and of swapping cards. We present a formal description of the knowledge and change of knowledge in that game. The description is in a standard language for dynamic epistemics expanded with assignment. Assignment is necessary to describe that cards change hands. The formal description is a prerequisite to model Pit in game theory. The main contribution of this paper should be seen as (...) the rigorous formalization of all knowledge in Pit. (shrink)

This book focuses on the game-theoretical semantics and epistemic logic of Jaakko Hintikka. Hintikka was a prodigious and esteemed philosopher and logician, and his death in August 2015 was a huge loss to the philosophical community. This book, whose chapters have been in preparation for several years, is dedicated to the work of Jaako Hintikka, and to his memory. This edited volume consists of 23 contributions from leading logicians and philosophers, who discuss themes that span across the entire range of (...) Hintikka’s career. Semantic Representationalism, Logical Dialogues, Knowledge and Epistemic logic are among some of the topics covered in this book's chapters. The book should appeal to students, scholars and teachers who wish to explore the philosophy of Jaako Hintikka. (shrink)

We propose a dynamic logic of lying, wherein a ‘lie that $\varphi $ ’ (where $\varphi $ is a formula in the logic) is an action in the sense of dynamic modal logic, that is interpreted as a state transformer relative to the formula $\varphi $ . The states that are being transformed are pointed Kripke models encoding the uncertainty of agents about their beliefs. Lies can be about factual propositions but also about modal formulas, such as the beliefs of (...) other agents or the belief consequences of the lies of other agents. We distinguish two speaker perspectives: (Obs) an outside observer who is lying to an agent that is modelled in the system, and (Ag) an agent who is lying to another agent, and where both are modelled in the system. We distinguish three addressee perspectives: (Cred) the credulous agent who believes everything that it is told (even at the price of inconsistency), (Skep) the skeptical agent who only believes what it is told if that is consistent with its current beliefs, and (Rev) the belief revising agent who believes everything that it is told by consistently revising its current, possibly conflicting, beliefs. The logics have complete axiomatizations, which can most elegantly be shown by way of their embedding in what is known as action model logic or in the extension of that logic to belief revision. (shrink)

When agents know a protocol, this leads them to have expectations about future observations. Agents can update their knowledge by matching their actual observations with the expected ones. They eliminate states where they do not match. In this paper, we study how agents perceive protocols that are not commonly known, and propose a semantics-driven logical framework to reason about knowledge in such scenarios. In particular, we introduce the notion of epistemic expectation models and a propositional dynamic logic-style epistemic logic for (...) reasoning about knowledge via matching agentsÊ expectations to their observations. It is shown how epistemic expectation models can be obtained from epistemic protocols. Furthermore, a characterization is presented of the effective equivalence of epistemic protocols. We introduce a new logic that incorporates updates of protocols and that can model reasoning about knowledge and observations. Finally, the framework is extended to incorporate fact-changing actions, and a worked-out example is given. © 2013 Elsevier B.V. (shrink)

Hans van Ditmarsch and Barteld Kooi (2008). Semantic results for ontic and epistemic change. In: G. Bonanno, W. van der Hoek and M. Wooldridge (editors). Logic and the Foundations of Game and Decision Theory (LOFT 7). Texts in Logic and Games 3, pp. 87-117, Amsterdam University Press, Amsterdam.

To describe simultaneous knowledge updates for different subgroups we propose anepistemic language with dynamic operators for actions. The language is interpreted onequivalence states (S5 states). The actions are interpreted as state transformers. Two crucial action constructors are learning and local choice. Learning isthe dynamic equivalent of common knowledge. Local choice aids in constraining theinterpretation of an action to a functional interpretation (state transformer).Bisimilarity is preserved under execution of actions. The language is applied todescribe various actions in card games.

We propose a multi-agent logic of knowledge, public announcements and arbitrary announcements, interpreted on topological spaces in the style of subset space semantics. The arbitrary announcement modality functions similarly to the effort modality in subset space logics, however, it comes with intuitive and semantic differences. We provide axiomatizations for three logics based on this setting, with S5 knowledge modality, and demonstrate their completeness. We moreover consider the weaker axiomatizations of three logics with S4 type of knowledge and prove soundness and (...) completeness results for these systems. (shrink)

We propose a separation logic where resources are histories (sequences) of epistemic actions so that resource update means concatenation of histories and resource decomposition means splitting of histories. This separation logic, called AMHSL, allows us to reason about the past: does what is true now depend on what was true in the past, before certain actions were executed? We show that the multiplicative connectives can be eliminated from a logical language with also epistemic and action model modalities, if the horizon (...) of epistemic actions is bounded. (shrink)

In this work we define contingency logic with arbitrary announcement. In contingency logic, the primitive modality contingency formalises that a proposition may be true but also may be false, so that if it is non-contingent then it is necessarily true or necessarily false. To this logic one can add dynamic operators to describe change of contingency. Our logic has operators for public announcement and operators for arbitrary public announcement, as in the dynamic epistemic logic called arbitrary public announcement logic. However, (...) our language primitive is the more suitable notion of public announcement whether, instead of the public announcement that. We compare the expressive power of our logic and its various fragments to related dynamic epistemic logics. We further present an axiomatisation and show its completeness by adapting a method to demonstrate completeness of arbitrary public announcement logic. Various extensions are also shown to be complete with respect to the corresponding frame classes. (shrink)

We model three examples of beliefs that agents may have about other agents’ beliefs, and provide motivation for this conceptualization from the theory of mind literature. We assume a modal logical framework for modelling degrees of belief by partially ordered preference relations. In this setting, we describe that agents believe that other agents do not distinguish among their beliefs (‘no preferences’), that agents believe that the beliefs of other agents are in part as their own (‘my preferences’), and the special (...) case that agents believe that the beliefs of other agents are exactly as their own (‘preference refinement’). This multi-agent belief interaction is frame characterizable. We provide examples for introspective agents. We investigate which of these forms of belief interaction are preserved under three common forms of belief revision. (shrink)

Fitch showed that not every true proposition can be known in due time; in other words, that not every proposition is knowable. Moore showed that certain propositions cannot be consistently believed. A more recent dynamic phrasing of Moore-sentences is that not all propositions are known after their announcement, i.e., not every proposition is successful. Fitch's and Moore's results are related, as they equally apply to standard notions of knowledge and belief (S 5 and KD45, respectively). If we interpret ‘successful’ as (...) ‘known after its announcement’ and ‘knowable’ as ‘known after some announcement’, successful implies knowable. Knowable does not imply successful: there is a proposition ϕ that is not known after its announcement but there is another announcement after which ϕ is known. We show that all propositions are knowable in the more general sense that for each proposition, it can become known or its negation can become known. We can get to know whether it is true: ◊(Kϕ ∨ K¬ϕ). This result comes at a price. We cannot get to know whether the proposition was true. This restricts the philosophical relevance of interpreting ‘knowable’ as ‘known after an announcement’. (shrink)

Arbitrary public announcement logic ) reasons about how the knowledge of a set of agents changes after true public announcements and after arbitrary announcements of true epistemic formulas. We consider a variant of arbitrary public announcement logic called positive arbitrary public announcement logic ), which restricts arbitrary public announcements to announcement of positive formulas. Positive formulas prohibit statements about the ignorance of agents. The positive formulas correspond to the universal fragment in first-order logic. As two successive announcements of positive formulas (...) need not correspond to the announcement of a positive formula, \ is rather different from \. We show that \ is more expressive than public announcement logic \, and that \ is incomparable with \. We also provide a sound and complete infinitary axiomatisation. (shrink)

Editors van Ditmarsch, Hendriks and Verbrugge of this special issue of topiCS on lying describe some recent trends in research on lying from a multidisciplinary perspective, including logic, philosophy, linguistics, psychology, cognitive science, behavioral economics, and artificial intelligence. Furthermore, they outline the seven contributions to this special issue.

The original publication of the article is missing the funding information.

We look at lying as an act of communication, where (i) the proposition that is communicated is not true, (ii) the utterer of the lie knows that what she communicates is not true, and (iii) the utterer of the lie intends the lie to be taken as truth. Rather than dwell on the moral issues, we provide a sketch of what goes on logically when a lie is communicated. We present a complete logic of manipulative updating, to analyse the effects (...) of lying in public discourse. Next, we turn to the study of lying in games. First, a game-theoretical analysis is used to explain how the possibility of lying makes such games interesting, and how lying is put to use in optimal strategies for playing the game. Finally, we give a matching logical analysis. Our running example of lying in games in liar’s dice. (shrink)

We examine various logics that combine knowledge, awareness, and change of awareness. An agent can become aware of propositional propositions but also of other agents or of herself. The dual operation to becoming aware, forgetting, can also be modelled. Our proposals are based on a novel notion of structural similarity that we call awareness bisimulation, the obvious notion of modal similarity for structures encoding knowledge and awareness.

We introduce a class of neighbourhood frames for graded modal logic embedding Kripke frames into neighbourhood frames. This class of neighbourhood frames is shown to be first-order definable but not modally definable. We also obtain a new definition of graded bisimulation with respect to Kripke frames by modifying the definition of monotonic bisimulation.

In this work, we present a multi-agent logic of knowledge and change of knowledge interpreted on topological structures. Our dynamics are of the so-called semi-private character where a group G of agents is informed of some piece of information \, while all the other agents observe that group G is informed, but are uncertain whether the information provided is \ or \. This article follows up on our prior work where the dynamics were public events. We provide a complete axiomatization (...) of our logic, and give two detailed examples of situations with agents learning information through semi-private announcements. (shrink)

A proposition is noncontingent, if it is necessarily true or it is necessarily false. In an epistemic context, ‘a proposition is noncontingent’ means that you know whether the proposition is true. In this paper, we study contingency logic with the noncontingency operator? but without the necessity operator 2. This logic is not a normal modal logic, because?→ is not valid. Contingency logic cannot define many usual frame properties, and its expressive power is weaker than that of basic modal logic over (...) classes of models without reflexivity. These features make axiomatizing contingency logics nontrivial, especially for the axiomatization over symmetric frames. In this paper, we axiomatize contingency logics over various frame classes using a novel method other than the methods provided in the literature, based on the ‘almost-definability’ schema AD proposed in our previous work. We also present extensions of contingency logic with dynamic operators. Finally, we compare our work to the related work in the fields of contingency logic and ignorance logic, where the two research communities have similar results but are apparently unaware of each other’s work. One goal of our paper is to bridge this gap. (shrink)

This is a case-study in knowledge representation and dynamic epistemic protocol verification. We analyze the ‘one hundred prisoners and a lightbulb’ puzzle. In this puzzle it is relevant what the agents know, how their knowledge changes due to observations, and how they affect the state of the world by changing facts, i.e., by their actions. These actions depend on the history of previous actions and observations. Part of its interest is that all actions are local, i.e. not publicly observable, and (...) part of the problem is therefore how to disseminate local results to other agents, and make them global. The various solutions to the puzzle are presented as protocols. The paper consists of three parts. First, we present different versions of the puzzle, and their solutions. This includes a probabilistic version, and a version assuming synchronicity. The latter is very informative for the prisoners, and allows different protocols. Then, we model the puzzle in an epistemic logic incorporating dynamic operators for the effects of information changing events. Such events include both informative actions, where agents become more informed about the non-changing state of the world, and factual changes, wherein the world and the facts describing it change themselves as well. Finally, we verify the basic protocol to solve the problem. Novel contributions in this paper are: Firstly, Protocol 2 and Protocol 4. Secondly, the modelling in dynamic epistemic logic in its entirety — we do not know of a case study that combines factual and informational dynamics in a setting of non-public events, or of a similar proposal to handle asynchronous behaviour in a dynamic epistemic logic. Thirdly, our method to verify dynamic epistemic protocols by reasoning over possibly infinite execution sequences of these protocols. A precursor of the present paper, entitled ‘One hundred prisoners and a lightbulb – logic and computation’, was presented at KR 2010, Toronto. The differences with the present contribution are as follows: the former contains a section with computational results, whereas the focus of the present paper is the verification of one of the presented protocols in the former. (shrink)