In the literature, different axiomatizations of Public Announcement Logic (PAL) have been proposed. Most of these axiomatizations share a “core set” of the so-called “reduction axioms”. In this paper, by designing non-standard Kripke semantics for the language of PAL, we show that the proof system based on this core set of axioms does not completely axiomatize PAL without additional axioms and rules. In fact, many of the intuitive axioms and rules we took for granted could not be derived from the (...) core set. Moreover, we also propose and advocate an alternative yet meaningful axiomatization of PAL without the reduction axioms. The completeness is proved directly by a detour method using the canonical model where announcements are treated as merely labels for modalities as in normal modal logics. This new axiomatization and its completeness proof may sharpen our understanding of PAL and can be adapted to other dynamic epistemic logics. (shrink)

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)

Multi-modal versions of propositional logics S5 or S4—commonly accepted as logics of knowledge—are capable of describing static states of knowledge but they do not reflect how the knowledge changes after communications among agents. In the present paper (part of broader research on logics of knowledge and communications) we define extensions of the logic S5 which can deal with public communications. The logics have natural semantics. We prove some completeness, decidability and interpretability results and formulate a general method that solves certain (...) kind of problems involving public communications—among them well known puzzles of Muddy Children and Mr. Sum & Mr. Product. As the paper gives a formal logical treatment of the operation of restriction of the universe of a Kripke model, it contributes also to investigations of semantics for modal logics. (shrink)

We propose a general framework for dynamic epistemic logics. It consists of a generic language for DELs and a class of structures, called model transition systems, that describe model transformations in a static way. An MTS can be viewed as a two-layered Kripke model and consequently inherits standard concepts such as bisimulation and bounded morphism from the ordinary Kripke models. In the second half of this article we add the global operator to the language, which enables us to define the (...) notions of a canonical MTS and canonicity of a DEL formula for a property of MTSs. Using these notions, we clarify correspondences between axioms of DELs and properties of MTSs. (shrink)

A variety of logical frameworks have been developed to study rational agents interacting over time. This paper takes a closer look at one particular interface, between two systems that both address the dynamics of knowledge and information flow. The first is Epistemic Temporal Logic (ETL) which uses linear or branching time models with added epistemic structure induced by agents’ different capabilities for observing events. The second framework is Dynamic Epistemic Logic (DEL) that describes interactive processes in terms of epistemic event (...) models which may occur inside modalities of the language. This paper systematically and rigorously relates the DEL framework with the ETL framework. The precise relationship between DEL and ETL is explored via a new representation theorem characterizing the largest class of ETL models corresponding to DEL protocols in terms of notions of Perfect Recall, No Miracles, and Bisimulation Invariance. We then focus on new issues of completeness. One contribution is an axiomatization for the dynamic logic of public announcements constrained by protocols, which has been an open problem for some years, as it does not fit the usual ‘reduction axiom’ format of DEL. Finally, we provide a number of examples that show how DEL suggests an interesting fine-structure inside ETL. (shrink)

This paper adds evidence structure to standard models of belief, in the form of families of sets of worlds. We show how these more fine-grained models support natural actions of “evidence management”, ranging from update with external new information to internal rearrangement. We show how this perspective leads to new richer languages for existing neighborhood semantics for modal logic. Our main results are relative completeness theorems for the resulting dynamic logic of evidence.

Many logical systems today describe intelligent interacting agents over time. Frameworks include Interpreted Systems (IS, Fagin et al. [8]), Epistemic-Temporal Logic (ETL, Parikh & Ramanujam [22]), STIT (Belnap et al. [5]), Process Algebra and Game Semantics (Abramsky [1]). This variety is an asset, as different modeling tools can be fine-tuned to specific applications. But it may also be an obstacle, when barriers between paradigms and schools go up. This paper takes a closer look at one particular interface, between two systems (...) that both address the dynamics of knowledge and information flow in multi-agent systems. One is IS/ETL (IS and ETL are, from a technical point of view, the same up to model transformations, cf. [20]), which uses linear or branching time models with added epistemic structure induced by agents’ different capabilities for observing events. These models provide a Grand Stage where histories of some process unfold constrained by a protocol, and a matching epistemic-temporal language describes what happens. The other framework is Dynamic Epistemic Logic (DEL, [10, 4, 34]) that describes interactive processes in terms of epistemic event models which may occur inside modalities of the language. Temporal evolution is then computed from some initial epistemic model through a process of successive ‘product updates’. It has long been unclear how to best compare IS/ETL and DEL. Various aspects have been investigated in [10, 30, 32], but in this paper, we study the interface in a more systematic way. Often, DEL and ETL are presented as alternative ways of adding dynamics to multi-agent epistemic models. In this paper, we rather focus on how merging the two different modeling choices leads to interesting new questions. Our leading interest here will be a view of informational processes as evolving over time. To see what we mean, consider the simplest version of DEL, viz. the logic of public announcements PAL ([23]) which adds a very specific type of communicative 1 action to epistemic models: a public announcement.. (shrink)

We show how belief revision can be treated systematically in the format of dynamicepistemic logic, when operators of conditional belief are added. The core engine consists of definable update rules for changing plausibility relations between worlds, which have been proposed independently in the dynamic-epistemic literature on preference change. Our analysis yields two new types of modal result. First, we obtain complete logics for concrete mechanisms of belief revision, based on compositional reduction axioms. Next, we show how various abstract postulates for (...) belief revision can be analyzed by standard modal frame correspondences for model-changing operations. (shrink)

Statements not only update our current knowledge, but also have other dynamic effects. In particular, suggestions or commands ?upgrade' our preferences by changing the current order among worlds. We present a complete logic of knowledge update plus preference upgrade that works with dynamic-epistemic-style reduction axioms. This system can model changing obligations, conflicting commands, or ?regret'. We then show how to derive reduction axioms from arbitrary definable relation changes. This style of analysis also has a product update version with preferences between (...) actions, as well as worlds. Some illustrations are presented involving defaults and obligations. We conclude that our dynamic framework is viable, while admitting a further extension to more numerical ?utility update'. (shrink)

In this paper, we present several extensions of epistemic logic with update operators modelling public information change. Next to the well-known public announcement operators, we also study public substitution operators. We prove many of the results regarding expressivity and completeness using so-called reduction axioms. We develop a general method for using reduction axioms and apply it to the logics at hand.

van Bentham et al. (Merging frameworks for interaction: DEL and ETL, 2007) provides a framework for generating the models of Epistemic Temporal Logic ( ETL : Fagin et al., Reasoning about knowledge, 1995; Parikh and Ramanujam, Journal of Logic, Language, and Information, 2003) from the models of Dynamic Epistemic Logic ( DEL : Baltag et al., in: Gilboa (ed.) Tark 1998, 1998; Gerbrandy, Bisimulations on Planet Kripke, 1999). We consider the logic TDEL on the merged semantic framework, and its extension (...) with the labeled past-operator “ P ϵ ” (“The event ϵ has happened before which. . .”). To axiomatize the extension, we introduce a method for transforming a given model into a normal form in a suitable sense. These logics suggest further applications of DEL in the theory of agency, the theory of learning, etc. (shrink)

A variety of logical frameworks have been developed to study rational agents interacting over time. This paper takes a closer look at one particular interface, between two systems that both address the dynamics of knowledge and information flow. The first is Epistemic Temporal Logic (ETL) which uses linear or branching time models with added epistemic structure induced by agents’ different capabilities for observing events. The second framework is Dynamic Epistemic Logic (DEL) that describes interactive processes in terms of epistemic event (...) models which may occur inside modalities of the language. This paper systematically and rigorously relates the DEL framework with the ETL framework. The precise relationship between DEL and ETL is explored via a new representation theorem characterizing the largest class of ETL models corresponding to DEL protocols in terms of notions of Perfect Recall , No Miracles , and Bisimulation Invariance . We then focus on new issues of completeness . One contribution is an axiomatization for the dynamic logic of public announcements constrained by protocols, which has been an open problem for some years, as it does not fit the usual ‘reduction axiom’ format of DEL. Finally, we provide a number of examples that show how DEL suggests an interesting fine-structure inside ETL. (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.

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.

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 →.

This paper adds evidence structure to standard models of belief, in the form of families of sets of worlds. We show how these more fine-grained models support natural actions of “evidence management”, ranging from update with external new information to internal rearrangement. We show how this perspective leads to new richer languages for existing neighborhood semantics for modal logic. Our main results are relative completeness theorems for the resulting dynamic logic of evidence.

This paper adds temporal logic to public announcement logic (PAL) and dynamic epistemic logic (DEL). By adding a previous-time operator to PAL, we express in the language statements concerning the muddy children puzzle and sum and product. We also express a true statement that an agent’s beliefs about another agent’s knowledge flipped twice, and use a sound proof system to prove this statement. Adding a next-time operator to PAL, we provide formulas that express that belief revision does not take place (...) in PAL. We also discuss relationships between announcements and the new knowledge agents thus acquire; such relationships are related to learning and to Fitch’s paradox. We also show how inverse programs and hybrid logic each can be used to help determine whether or not an arbitrary structure represents the play of a game. We then add a past-time operator to DEL, and discuss the importance of adding yet another component to the language in order to prove completeness. (shrink)

This modern, advanced textbook reviews modal logic, a field which caught the attention of computer scientists in the late 1970's.

This paper provides a sound and complete proof system for a language that adds to Dynamic Epistemic Logic a discrete previous-time operator as well as single symbol formulas that partially reveal the most recent event that occurred. The completeness theorem is by filtration followed by model unraveling and other model transformations. Decidability follows from the completeness proof. The degree to which it is important to include the additional single symbol formulas is addressed in a discussion about the difficulties of the (...) completeness for a language that only adds the previous-time operator to DEL. Discussion is also given regarding the completeness for a language obtained by removing common knowledge operators from. (shrink)