Paper deep dive
Belief Contraction in Dynamic Epistemic Logic
Gaia Belardinelli, Snow Zhang
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 97%
Last extracted: 7/5/2026, 8:05:12 AM
Summary
The paper addresses the limitations of standard Dynamic Epistemic Logic (DEL) and plausibility-based models in representing belief contraction, specifically regarding hedged public announcements. The authors demonstrate that plausibility-based approaches cannot model agents who violate positive introspection or respond to announcements that a proposition might be false. To solve this, they introduce a new mechanism for belief contraction defined directly on standard Kripke models without constraints on the doxastic accessibility relation. This leads to the definition of Hedged Public Announcement Logic (HPAL), which is shown to be sound and complete via reduction axioms. Furthermore, the authors propose a more general dynamic logic, GDEL, which extends standard DEL to accommodate contractions from private or semi-private announcements.
Entities (6)
Relation Signals (3)
Plausibility Model → isatypeof → Kripke Model
confidence 100% · A plausibility model is a Kripke model (W, ⊯, V)
Dynamic Epistemic Logic → isextendedby → GDEL
confidence 100% · We also define a more general dynamic logic GDEL that is an extension of standard DEL
Hedged Public Announcement Logic → isatypeof → Dynamic Epistemic Logic
confidence 90% · We define a sound and complete logic for this contraction modality, which we call hedged public announcement logic (HPAL)
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Dynamic epistemic logic represents belief change via model transformations induced by epistemic events. Its standard formulation (Baltag, Moss, Solecki, 1998) provides a natural account of belief expansion through the elimination of possibilities, but it cannot model belief contraction about factual propositions. A classic response enriches Kripke models with plausibility orderings, representing contraction as an update that promotes certain possibilities over others. We show that this approach has expressive limitations. In particular, the approach cannot model belief that violates positive introspection and contraction dynamics in response to a hedged public announcement that phi might be false. Motivated by these considerations, we introduce a mechanism for belief contraction defined directly on standard Kripke models, without any constraints on the doxastic accessibility relation. We show that it satisfies some of the standard properties of belief contraction but not others, study the conditions under which contraction may be unsuccessful, and provide a sound and complete axiomatization of the logic via reduction axioms. We also define a more general dynamic logic that is an extension of standard DEL and accommodates belief contractions due to events such as private or semi-private announcements, and provide a complete and sound axiomatization of the general logic.
Tags
Links
- Source: https://arxiv.org/abs/2606.31861v1
- Canonical: https://arxiv.org/abs/2606.31861v1
Trouble viewing inline? Open PDF directly →
Full Text
67,357 characters extracted from source content.
Expand or collapse full text
M. Bílková, M. Gattinger, I. van der Giessen, M. Girlando, Y. Wang (Eds.): Advances in Modal Logic 2026 (AiML 2026) EPTCS 447, 2026, p. 137–157, doi:10.4204/EPTCS.447.8 © G. Belardinelli & S. Zhang This work is licensed under the Creative Commons Attribution License. Belief Contraction in Dynamic Epistemic Logic Gaia Belardinelli Department of Philosophy Stanford University Stanford, USA gaiabel@stanford.edu Snow Zhang Department of Philosophy University of California, Berkeley Berkeley, USA snowzhang@berkeley.edu Dynamic epistemic logic (DEL) represents belief change via model transformations induced by epis- temic events. Its standard formulation (Baltag, Moss, Solecki, 1998) provides a natural account of belief expansion through the elimination of possibilities, but it cannot model belief contraction about factual propositions. A classic response enriches Kripke models with plausibility orderings, repre- senting contraction as an update that promotes certain possibilities over others. We show that this approach has expressive limitations. In particular, the approach cannot model belief that violates positive introspection and contraction dynamics in response to ahedgedpublic announcement thatφ mightbe false. Motivated by these considerations, we introduce a mechanism for belief contraction defined directly on standard Kripke models, without any constraints on the doxastic accessibility re- lation. We show that it satisfies some of the standard properties of belief contraction but not others, study the conditions under which contraction may be unsuccessful, and provide a sound and complete axiomatization of the logic via reduction axioms. We also define a more general dynamic logic that is an extension of standardDELand accommodates belief contractions due to events such as private or semi-private announcements, and provide a complete and sound axiomatization of the general logic. 1 Introduction Dynamic epistemic logic (DEL) is a family of logics that model multi-agent belief change by incorporat- ing information revealed by epistemic events—such as public or private announcements—into agents’ epistemic states. In standardDEL[6], this incorporation proceeds byeliminatingall possibilities that are incompatible with the disclosed information. As a result, standardDELcan’t straightforwardly model announcements that make agents reconsider possibilities they previously ruled out as impossible, as re- quired for belief contraction. A popular solution is to distinguish “hard” from “soft” updates; while hard updates involveeliminatingpossibilities, soft updates involvepromotingpossibilities in terms of their comparativeplausibility[12, 8]. Then, belief contraction about a factual propositionpconsists in coming to judge that a¬p-possibility is at least as plausible as the most plausiblep-possibility, thereby losing the belief thatpholds. While the plausibility-based approach can model belief contraction [8, 23], it has certain expres- sive limitations. First, since plausibility orderings are transitive, the framework validates positive in- trospection for beliefs (axiom4), and so can’t model agents who are mistaken about their own beliefs. Second, the approach can’t accommodate belief contractions due tohedged public announcements— announcements thatp might be false. Intuitively, such an announcement could cause an agent who initially believespto suspend judgment onpwithout gaining any new (factual) beliefs. We show that there is a precise sense in which such dynamicscan’tbe modeled in the plausibility framework. These limitations motivate the search for a new model of belief contraction. We offer such a model in this paper. We introduce a dynamic operation of belief contraction on standard, multi-agent Kripke 138Belief Contraction in Dynamic Epistemic Logic models of beliefs, with no assumptions on the doxastic accessibility relations. Roughly, a hedged an- nouncement thatφmight be falsetriggers a contraction onφ, which involves adding¬φ-possibilities to an agent’s belief set if she believesφ, and doing nothing otherwise. We define a sound and complete logic for this contraction modality, which we callhedged public announcement logic (HPAL), and prove that this update satisfies a number of natural properties of belief contraction. We then define a more general dynamic logicGDELthat conservatively extends standardDELto also accommodate belief contractions due to events such as private or semi-private announcements. We show that it containsHPALand that its updates are always a simulation of a refinement of an initial Kripke model. Finally, we provide a complete and sound axiomatization of the general logic. Related literature.The logicGDELcan be viewed as a natural extension of standardDEL. As contrac- tion is a form of information-loss, our model is also related to logics offorgettingand simulation modal logic [18, 19, 22], as well as to the fragment of graph modifier logic that adds edges to Kripke models [5]. Our theory however contrasts with the theory of belief contraction as studied in AGM [1]; our contraction operator does not satisfy many of the AGM postulates. This is to be expected, as dynamic contraction involves transformations that could change the truth-values of epistemic formulas, which is not consid- ered in AGM. Philosophically, the problem of belief contraction due to hedged public announcement is related to the problem of evaluating indicative conditionals that have modal antecedents, which remains an open problem [32, 27, 10]. The proofs of main theorems can be found in the Appendix. 2 StandardDELframework We begin by reviewing the basics ofDELand fix notations. 1 LetAtbe a countable set of atomic formulas andAgbe a finite set of agents. LetLbe thedoxastic languagegenerated fromAtby the following grammar:φ : =⊤|p|¬φ|φ∧φ|B a φ, wherep∈Atanda∈Ag. We write⊥for¬⊤and e B a φfor ¬B a ¬φ. Aliteralis an atomic formulapor its negation¬p. Let V φ∈S φ=⊤ifSis empty. We adopt the standard semantics of epistemic logic, where a Kripke model is a tripleM= (W,R,V) withW̸=/0 a set of worlds,R a ⊆(W×W)an accessibility relation defined for alla∈Ag, andV:At→ ℘(W)is a valuation function. We use notationR a (w) =v∈W:(w,v)∈R a to representthe set of possible worlds compatible with agent a’s belief at w. The satisfaction relation between a Kripke modelM= (W,R,V)with worldw∈Wand a formula φ∈Lis defined as standard, where in particular the semantics of the belief modality is given by: M,w⊨B a φiffM,v⊨φfor allv∈R a (w). A formulaφisvalid in a modelM(notation:M⊨φ), if for all worldswinM,M,w⊨φ. A formula φisvalid in a class of modelsL(notation:⊨ L φ), if for all modelsMinL,φis valid inM. Astandard event modelis a tripleE= (E,Q,pre)whereE̸=/0 is a finite set of events,Q a ⊆(E×E) is an accessibility relation between events, for alla∈Ag, andpre:E→La precondition function. 2 We use notationQ a (e) =f∈E:(e,f)∈Q a for the set of events that are considered possible byaate. For a Kripke modelM= (W,R,V)and a standard event modelE= (E,Q,pre), thestandard product updateofMwithEis the Kripke modelM⊗E= (W E ,R E ,V E )whereW E =(w,e)∈W×E:w⊨ 1 For presentation purposes, in this section we only introduce the basic doxastic language without dynamic modalities. We introduce the full language ofDELin the last section, where we also use it. For an introduction toDEL, see [7]. 2 In the most general form ofDEL, the precondition function assigns to each event a formula from the dynamic language (i.e.Lextended with dynamic formulas). We keep it simple here and consider this generalDELform in the last section. G. Belardinelli & S. Zhang139 pre(e),R E a (w,e) =(v,f)∈W E :v∈R a (w)andf∈Q a (e), andV E (p) =(w,e)∈W E :w∈V(p), for allp∈At. Informally, a world(w,e)representsthe state of affairs at w after e occurs. We call these event models and product updatesstandardto distinguish them from the framework introduced later. It is well known that standardDELhas undesirable consequences when agents are presented with information that contradicts their beliefs [12, 26]. For a concrete illustration: Example 2.1.Alice believes that she locked her office door before she left. She runs into Bob, who tells her thather office door was open. Alice trusts Bob and revises her beliefs accordingly. Letpdenote the proposition “Alice’s office door is open”. Figure 1 illustrates that, if we model Alice’s belief revision using a standard product update, then she will end up having inconsistent beliefs. ¬p w p v a a M p e a E p (v,e) M⊗E Figure 1:Left: The Kripke modelM= (W,R,V)representing Alice’s initial belief state. An edge from a worldvto a worldwmeansw∈R a (v). We haveM⊨B a ¬p∧¬B a p.Middle: The standard event model E= (E,Q,pre)representing Bob’s announcement. The eventecontains its own preconditionpre(e) =p. The loop onemeanse∈Q a (e).Right: The Kripke modelM⊗E= (W E ,R E ,V E )representing Alice’s belief state after the update, whereR E a ((v,e)) =/0 and so e.g.M⊗E⊨B a p∧B a ¬p. 3 Plausibility models The “standard diagnosis” of the problem of modeling belief contraction in standardDELis that we need a richer view of beliefs [12]. In particular, we need a framework where an agent believes not just any proposition entailed by her information, but those that are true at the ‘best’ or ‘most plausible’ possibilities compatible with her information [8, 12]. I believe that I am not dreaming. It is notimpossible that I am, but those possibilities are lessplausiblethan those in which I am awake. Similarly, one interpretation of Alice’s initial doxastic situation is that she believes that her office is closed, not because she has completely ruled out the possibility that it is open, but only that she judges that possibility to be relatively implausible. And it is this relative plausibility judgment that gets revised by Bob’s testimony. This idea is formalized by modeling belief in terms of plausibility orderings over possible worlds. Formally, aplausibility order on a set Sis a connected, reflexive and transitive relation⊴⊆S×Ssuch that every non-empty subsetS ′ ⊆Shas at least one⊴-minimal element, i.e.Min ⊴ (S ′ ) =w∈S ′ :∀v∈ S ′ ,w⊴v̸=/0. 3 Aplausibility modelis a Kripke model(W,⪯,V)with⪯ a a plausibility order onW, for all agentsa∈Ag. We write≺ a for its asymmetric component, i.e.w≺ a vifw⪯ a vandv̸⪯ a w. The semantics ofLover plausibility models is standard for propositional formulas, but belief is interpreted differently from above, capturing that the agent believes what is the case at the most plausible worlds: M,w⊨B a φiffM,v⊨φfor allv∈Min ⪯ a (W). Aplausibility event modelis an event modelE= (E,≤,pre)with≤ a a plausibility order onEfor all a∈Ag. We write< a for its asymmetric component. As in standardDEL, event models update plausibility models via product update. Theplausibility-updateofM= (W,⪯,V)withEis the plausibility model M∗E= (W E ,⪯ E ,V E )whereW E andV E are defined as in standard product updates and⪯ E is given 3 Note that we assume the plausibility order to beconnected. This is more restrictive than usual [8], but it is justified here as our framework only models belief and omits knowledge. 140Belief Contraction in Dynamic Epistemic Logic by(w,e)⪯ E a (v,f)iffe< a f,ore≡ a fandw⪯ a v. Figure 2 shows how to model Example 2.1 via a plausibility update. Alice’s change of mind is captured as asoftupdate where no world is ruled out as impossible, but their relative plausibility is switched. ¬p w p v a M p e ¬p f a E ¬p (w,f) p (v,e) a M∗E Figure 2:Left: The plausibility modelM= (W,⪯,V)representing Alice’s initial belief state. An edge fromvtowmeansw⪯ a v. We haveM⊨B a ¬p∧¬B a p.Middle: The plausibility event model E= (E,≤,pre)capturing a soft update thatpholds. An edge fromftoemeanse≤ a f.Right: The plausibility modelM∗Erepresenting Alice’s belief state after updating, withM∗E⊨B a p∧¬B a ¬p. 3.1 Limitations of plausibility models One limitation of the plausibility model of beliefs is that it validates axiom4:B a φ→B a B a φ. For this reason, it cannot model agents who are mistaken about their own beliefs. Such cases, however, seem possible: an employer might profess that they believe in gender equality while consistently favoring one gender group in hiring. One way of describing this employer is that they in fact believe that candidates from one gender group are more qualified, even though they (falsely) believe that they don’t believe that. Another limitation of the approach, mentioned above, concerns belief contraction that does not in- volve adopting any new factual beliefs. A variant of Example 2.1 illustrates what we have in mind: Example 3.1.As before, Alice believes that she locked the door to her office before she left. She runs into Bob, who tells her thather office door might be open. Given Bob’s testimony, Alice comes to suspend judgment on whether she locked the door to her office before she left. Letpdenote the propositionAlice’s office door is open. Alice’s belief states before and after the update can be modeled byMandNin Figure 3, respectively. ¬p w p v a a M ¬p w p v a a N Figure 3:Left: The plausibility modelM= (W,⪯,V)representing Alice’s initial belief state, where M⊨B a ¬p∧¬B a p. Conventions for edges are as in Fig. 2.Right: The plausibility modelN= (W,⪯ N ,V)representing Alice’s belief state after updating on Bob’s testimony, whereN⊨¬B a p∧¬B a ¬p. However, it turns out that this updatecannotbe modeled as a plausibility update. More precisely, let K≡K ′ denote modal equivalence between two modelsKandK ′ with respect toL. 4 Then: Theorem 3.2.There is no plausibility event modelEsuch thatM∗E≡N. Proof.LetM= (W,⪯,V)andN= (W,⪯ N ,V)be as depicted in Figure 3. Suppose towards a con- tradiction that there is a plausibility event modelE=E,≤,presuch thatM∗E= (W E ,⪯ E ,V E )is a plausibility model that is modally equivalent toN. We claim that, for any(v,f)∈W E , there exists a(v,f ′ )̸= (v,f)such that(v,f ′ )≺ E a (v,f). It follows then thatM∗Econtains an infinite descending 4 Recall that two Kripke (or plausibility) modelsK= (W,R,V)andK ′ = (W ′ ,R ′ ,V ′ )aremodally equivalentwith respect toLif for every formulaφ∈Land every statew∈W, there exists a statew ′ ∈W ′ such thatK,w⊨φiffK ′ ,w ′ ⊨φ, and conversely, for everyw ′ ∈W ′ there exists a statew∈Wwith the same property. G. Belardinelli & S. Zhang141 chain, which contradicts the assumption that it is a plausibility model. Let(v,f)∈W E . By assumption, (M∗E,(v,f))is modally equivalent to(N,v). Since(N,v)⊨¬B a p, we have(M∗E,(v,f))⊨¬B a p. So there exists(w,e)∈W E such that(w,e)⪯ E a (v,f). For this(w,e), it must be that(M∗E,(w,e))is modally equivalent to(N,w)(since it can’t be modally equivalent to(N,v)). SinceN,w⊨ e B a p, there exists(v,f ′ )∈W E such that(v,f ′ )⪯ E a (w,e). Moreover, sincev̸⪯ a w, we must havef ′ < a e≤ a f. So f ′ < a fand therefore(v,f ′ )≺ E a (v,f). Note that if two models are not modally equivalent with respect toL, then they are not modally equiva- lent with respect to any extension ofL. So it follows from Theorem 3.2 that there is no plausibility event modelEsuch thatM∗Eis modally equivalent toNwith respect toLenriched with, e.g. modalities for conditional beliefs, safe beliefs or dynamic modalities. Relatedly, since modal equivalence is gener- ally assumed to be a necessary condition for an adequate notion of bisimilarity, it also follows that there is no plausibility event modelEsuch thatM∗Eis bisimilar toNwith respect to any adequate notion of bisimilarity (see e.g. [16, 2, 3] for different notions of bisimilarity for plausibility structures). 4 A new model for belief contraction Theorem 3.2 shows that plausibility updates can’t weaken an agent’s belief in a way that makes her consider the two worlds equiplausible. We now introduce a framework for belief contraction that can achieve that. In general, belief contraction can be caused by many different kinds of epistemic events. In this section, we focus on a simple case of belief contraction due tohedged public announcements, like Bob’s testimony that Alice’s doormightbe open. 5 Formally, we represent the effects of such announce- ments by the dynamic modality “[÷φ]ψ”. Intuitively, it says thatψis the case after the hedged public announcement thatφmight be false. Let thecontraction languageL ÷ be the language generated by the grammar ofLextended with the following clauses for the dynamic modality and a universal modality: φ : = [÷φ]φ|∀φ. We define∃φ : =¬∀¬φ. A standard (non-hedged) public announcement thatφis falseis modeled as eliminating all theφ- possibilities fro5m all agents’ doxastic spaces [29]. A natural thought, then, is that a hedged public announcement thatφmight be falseshould add all the¬φ-possibilities to all agents’ doxastic spaces. However, this is not quite right. Adding all such possibilities to all agents’ doxastic spaces may force those who already consider¬φpossible to update their beliefs and start considering additional¬φ- possibilities, thereby losing more beliefs than is warranted by the announcement. This suggests that, unlike standard public announcements, the epistemic effects of a hedged announcement thatφmight be false depend on the agents’ initial beliefs, and in particular on whether they believeφprior to the announcement. For this section, we assume that this is the only relevant difference: if an agent already considers¬φpossible, then the announcementφmight be falsehas no effects on her beliefs; if the agent believesφ, then the announcement leads her to consider all¬φ-worlds as possible. Definition 4.1(Contraction onφ).Given a Kripke modelM= (W,R,V)and a formulaφ∈L ÷ . Let M ÷φ = (W,R ÷φ ,V)be defined by, for alla∈Agand allw∈W: R ÷φ a (w) = ( R a (w)∪v∈W:M,v⊨¬φifM,w⊨B a φ R a (w)otherwise 5 The namehedged public announcementreflects the public and non-committal (“hedged”) character of the announcement, which opens up possibilities rather than restricting them—much like epistemic modals in so-called “hedged assertions” [13]. 142Belief Contraction in Dynamic Epistemic Logic CallM ÷φ the model obtained fromMby contracting onφ. Note that it is always the case thatR a (w)⊆ R ÷φ a (w). This means that a hedged public announcement alwaysextendsthe initial Kripke model. The semantics ofL ÷ is given by the semantics ofLover Kripke models extended with these clauses: M,w⊨[÷φ]ψiffM ÷φ ,w⊨ψ; M,w⊨∀φifffor allv∈W,M,v⊨φ. Consider again Example 3.1. In the present framework, the effect of Bob’s announcement thatAlice’s office door might be opencan be modeled by contracting on the propositionAlice’s office door is closed (¬p), which amounts to adding worldvto Alice’s set of doxastic possibilities atwandv. See Figure 4. ¬p w p v a a M ¬p w p v a a a M ÷¬p Figure 4:Left: The Kripke modelM(same as Figure 1), representing Alice’s initial belief state.Right: The Kripke modelM ÷¬p representing Alice’s belief state after updating on Bob’s hedged announcement, obtained by contracting on¬p. We haveM ÷¬p ⊨¬B a ¬p∧¬B a p, so Alice lost a belief in¬p. One natural question is what is the logic of the contraction update as defined above. The next theorem shows that such logic is given by the system presented in Table 1. CLall classical propositional tautologies ∀K∀(φ→ψ)→(∀φ→∀ψ) ∀T∀φ→φ ∀5¬∀φ→∀¬∀φ ∀B∀φ→B a φ BKB a (φ→ψ)→(B a φ→B a ψ) A1[÷φ]p↔p A2[÷φ]¬ψ↔¬[÷φ]ψ A3[÷φ](ψ∧χ)↔[÷φ]ψ∧[÷φ]χ A4[÷φ]∀ψ↔∀[÷φ]ψ A5[÷φ]B a ψ↔(B a [÷φ]ψ∧(B a φ→∀(¬φ→[÷φ]ψ))) MPFromφandφ→ψ, inferψ REFromφ↔ψ, inferχ[φ/p]↔χ[ψ/p] NECNecessitation rules for all modalities 6 Table 1:The Theory ofHedged Public Announcement Logic (HPAL) Theorem 4.2.The dynamic logic of contraction updates is completely axiomatized byHPAL. Proof sketch.Soundness follows by straightforward validity arguments. For completeness, given the reduction axioms, every formula with dynamic modalities is provably equivalent inHPALto a formula without. So the completeness ofHPALfollows from the completeness of the basic doxastic logic with the universal modality [14, Theorem 7.2]. Besides axioms and rules of inference of the basic modal logicKwith the universal modality (which is an S5 modality), the theory contains inference rules and reduction axioms for the contraction modality that 6 Notice that necessitation for the belief modality is redundant, as it is derivable from∀B and∀-necessitation. G. Belardinelli & S. Zhang143 parallel the reduction axioms in Public Announcement Logic (PAL) [29, 20, 31]. Axiom A5 is specific to our logic of contraction. It says that after contraction onφ(viz. a hedged announcement thatφmight be false), an agent believesψiff she doesn’t believeφprior to the announcement and she believes that ψholds after the announcement, or she believesφprior to the announcement and at any¬φ-worlds,ψ holds after the announcement. 5 Preservation and Moorean formulas A well-known phenomenon in public announcement logic is that some formulas become false after they are announced. As a result, the formula is not believed after the announcement. InPAL, formulas that become false or are not believed after an announcement are both calledunsuccessful formulas. Let[!φ] be the dynamic modality “after the announcement ofφ” inPAL. 7 There are thus two closely related notions ofsuccessinPAL: (i) what is announced is true after its announcement ([!φ]φis valid); (i) what is announced is believed after its announcement ([!φ]B a φis valid for alla∈Ag). For clarity, we will say φispreserved inPALif it satisfies (i);φissuccessful inPALif it satisfies (i). It is well-known that, in PAL, any formula that satisfies (i) also satisfies (i), though the converse does not hold. 8 In this section, we focus on developing a notion of preservation forHPALthat is analogous to (i) forPAL. A natural starting point is to say thatφispreservedif it is true after the hedged announcement thatφ might be true, viz.[÷¬φ]φis valid. But this isn’t quite right: while a public announcement thatφistrue eliminatesall¬φ-possibilities, a hedged public announcement thatφmightbe true doesn’t eliminate any possibilities, and so any possibility whereφis false before the announcement remains in the model (though they may satisfyφin the new model after the announcement). This observation suggests the following alternative definition of preservation for hedged public announcements (letLbe a class of models that validates logicL): Definition 5.1(Preservation).φispreserved(in the logicL) if⊨ L φ→[÷¬φ]φ Not all formulas inL ÷ are preserved inHPAL. Consider Example 3.1 again. Suppose Bob tells Alice instead thatshe might have a false belief that her office door is closed, viz. it might be true thatp∧B a ¬p. Figure 5 shows that this hedged announcement is not preserved. ¬p w p v a a M ¬p w p v a a a M ÷¬(p∧B a ¬p) Figure 5: Alice’s belief update as a contraction on¬(p∧B a ¬p). The formulap∧B a ¬pis true atvbefore the update (on the left) but false atvafter the update (on the right). Hence,p∧B a ¬pis not preserved. More generally, sayφisself-refuting(in the logicL) if⊨ L φ→[÷¬φ]¬φ. Clearly,φis not preserved if it is self-refuting. The above example is a special case of the following result: 7 InPAL, the formula[!φ]ψintuitively saysψis true after eliminating all¬φ-possibilities from the model; see [20, Chapter 4] and references therein for more onPAL. 8 The proof that (i) implies (i) is analogous to the “only if”-direction of [20, Proposition 4.32], though here the modality is belief rather than knowledge, and in particular it does not necessarily satisfy the T-axiom, which is the reason why the other direction does not hold in general. For example, supposeAg=a, letφ : =p∧B a ¬p∧¬B a ⊥, and consider a Kripke model and a worldwin it where suchφis true. Then, after the public announcement ofφ, which eliminates all possibilities whereφ is not true and so also all worlds that were accessible foraatw,awill have inconsistent beliefs atwand believe (trivially) that φis true. Hence,[!φ]B a φis valid. On the other hand,[!φ]φis invalid and in particular[!φ]¬B a ⊥is invalid. 144Belief Contraction in Dynamic Epistemic Logic Proposition 5.2.The formulas p∧∃B a ¬p and p∧B a ¬p are self-refuting inHPAL. 9 Proof.Letφ : =p∧∃B a ¬p. SupposeM,w⊨p∧∃B a ¬p. ThenM⊨∃B a ¬pand soM ÷¬φ =M ÷¬p . ThusM ÷¬φ ⊨∀ e B a pand soM ÷¬φ ,w⊨¬φ. Similarly, letψ : =p∧B a ¬p. SupposeM,w⊨ψ. Since B a ¬p⊨B a ¬ψ,M,w⊨B a ¬ψ. Sow∈R ÷¬ψ a (w). SinceM,w⊨p,M ÷¬ψ ,w⊨ e B a p. Given that e B a p⊨ ¬ψ,M ÷¬ψ ,w⊨¬ψ. So which formulas are preserved? Recall that a formulaφisexistentialif it is built only from literals, ∧,∨and e B a ;φisuniversalif it is built only from literals,∧,∨andB a . It’s well-known that universal formulas remain true after being (standardly) publicly announced, in any normal modal logic [20]. Their dual—existential formulas—are always preserved by hedged public announcements: Theorem 5.3.Ifφ∈L ÷ is equivalent inHPALto an existential formula, then it is preserved inHPAL. Proof.Supposeφis equivalent inHPALto an existential formula. Thenφis preserved under model extension [4]. SinceM ÷¬φ extendsM, ifM,w⊨φ, thenM ÷¬φ ,w⊨φ, i.e.M,w⊨φ→[÷¬φ]φ. One upshot of Theorem 5.3 is that, while the “strong” Moorean sentencep∧B a ¬pis never preserved, the “weak” Moorean sentencep∧¬B a p, which is equivalent to an existential formula, is preserved. So being logically equivalent to an existential formula is sufficient for being preserved. But it is not necessary. In particular, the non-existential formulap∧B a p(agentahas a true belief thatp) is preserved. Proposition 5.4.The formula p∧B a p is preserved inHPAL. Proof.LetM= (W,R,V)be a Kripke model withM,w⊨p∧B a p. AsR ÷¬(p∧B a p) a (w)⊆R a (w)∪v∈ W:M,v⊨p∧B a p⊆v∈W:M,v⊨pandpis preserved, thenM ÷¬(p∧B a p) ,w⊨p∧B a p. It would be nice to have a complete characterization of the set of preserved formulas, which we leave as an open question. But there is a partial result. Let’s considerknowledgeinstead ofbelieffor a moment, and restrict our attention to single-agent models. The standard logic for knowledge isS5, and extending HPALwithS5axioms implies that all formulas inLare preserved. Theorem 5.5.Suppose|Ag|=1. Then every formula inLis preserved inHPALextended withS5. Proof sketch.InS5, ifM,w⊨φwithφ∈L, then every world in the equivalence class ofwsatisfies e B a φ and so contracting on¬φdoes not change relations inside those classes. Then,(M,w)and(M ÷¬φ ,w) are bisimilar, and sinceLis bisimulation-invariant,φis preserved. Note that modelMin Figure 5 validatesKD45, so the preservation result doesn’t hold in these settings. 10 6 AGM-style contraction principles In the AGM literature, belief contraction is modeled as a static operation on the set of formulas, repre- senting the agent’s belief base, and is characterized by a set of axioms. As [9] points out, many of those axioms do not naturally hold in the dynamic setting where belief contraction induces model transforma- tions. In this section, we give an overview of which of the AGM axioms hold/fail for our contraction operator. Following [30], we render AGM statements that express that the agent believesχafter con- tracting byφ, by the formula[÷φ]B a χ. The modal version of the AGM axioms for contraction can then be expressed by the following formulas, whereφ,ψ,χ∈L ÷ : 9 Note that the Moorean sentencep∧B a ¬pis unsatisfiable inS5, whilep∧∃B a ¬pis satisfiable even if belief is factive. 10 As an anonymous referee pointed out, the result does not generalize to the multi-agent setting. G. Belardinelli & S. Zhang145 •Closure.[÷φ](B a (ψ→χ)→(B a ψ→B a χ)). •Success.∃¬φ→[÷φ]¬B a φ. •Inclusion.[÷φ]B a ψ→B a ψ. •Vacuity.¬B a φ→(χ↔[÷φ]χ). •Extensionality. If⊨φ↔ψthen⊨[÷φ]χ↔[÷ψ]χ. •Conjunctive Inclusion.[÷(φ∧ψ)]¬B a φ→([÷(φ∧ψ)]B a χ→[÷φ]B a χ). •Conjunctive Overlap.([÷φ]B a χ∧[÷ψ]B a χ)→[÷(φ∧ψ)]B a χ. •Consistency.¬B a ⊥→[÷φ]¬B a ⊥. From the list above we omitted the axiom calledRecovery(expansion byφafter contraction byφ restores the agent’s original beliefs), as it involves an expansion operation which we do not focus on. 11 We added to this list a natural property calledConsistency, which is discussed in [30, 26]. Some of these properties are valid inHPAL. In particular,ClosureandExtensionalityhold un- restrictedly in our semantic framework.Consistencyalso holds, as the contraction operation never removes edges. For the other properties, the situation is more mixed, as the next two subsections show. 6.1 Success Recall thatφis successful inPALif it is believed after it is announced:[!φ]B a φis valid for alla∈Ag. A natural analogue of this notion in our contraction settings is thatφisnot believedafter a hedged announcement that it might be false, viz.[÷φ]¬B a φfor alla∈Ag. The only caveat concerns the case whereφis valid in the model. In that case, since there are no¬φ-possibilities, contracting onφleaves the model unchanged and so may leave agents’ beliefs inφunchanged. 12 This illustrates whySuccessis given by the conditional∃¬φ→[÷φ]¬B a φ. Say that a formulaφissuccessfulif it satisfies this property. As with preservation, not all formulas are successful. For instance, the hedged announcement that p∧B a ¬pmight be true in Figure 5 is unsuccessful: after updating on Bob’s announcement that she might have a false belief that¬p, by contracting on¬(p∧B a ¬p), Alice will come to believe that she believes neitherpnor¬p, and so she will believe that she doesn’t have a false belief thatp(i.e.M ÷¬(p∧B a ¬p) ⊨ B a ¬(p∧B a ¬p)). InPAL, if a formula remains true after being announced, then it is believed after the announcement [20, Proposition 4.32]. A similar result holds forHPAL. Proposition 6.1.InHPAL, if¬φ∈L ÷ is preserved, thenφis successful. Proof.LetM= (W,R,V)and supposeM,w⊨∃¬φ. Assume that¬φis preserved. We show that M,w⊨[÷φ]¬B a φ. There are two cases. First, suppose thatM,w⊨¬B a φ. Then, there isv∈R a (w) = R ÷φ a (w)such thatM,v⊨¬φ. As¬φis preserved,M,v⊨[÷φ]¬φand soM,w⊨[÷φ]¬B a φ. Second, supposeM,w⊨B a φ. SinceM,w⊨∃¬φ, there is av∈WwithM,v⊨¬φandv∈R ÷φ a (w). By preservation of¬φ,M,v⊨[÷φ]¬φand soM,w⊨[÷φ]¬B a φ. Given that existential formulas are preserved (Theorem 5.3), we then obtain the following corollary, which gives a sufficient condition for a formula to be successful: 11 Notice, however, thatRecoverydoes not hold in general in this framework: while the contraction operator[÷φ]can informally be viewed as a dual of the public announcement operator[!φ], it is not a formal dual, in the sense that contraction byφfollowed by expansion byφdoes not in general recover the original model (whether we model expansion by world- or arrow-eliminations). We explore this issue in a longer version of the paper. 12 This mirrors the AGM constraint that beliefs in validities cannot be given up [1, 25]. 146Belief Contraction in Dynamic Epistemic Logic Corollary 6.2.Ifφ∈L ÷ is equivalent inHPALto a universal formula, thenφis successful inHPAL. Proof.Ifφis equivalent to a universal formula,¬φis equivalent to an existential formula. By Theo- rem 5.3 existential formulas are preserved, and by Prop. 6.1 if¬φis preserved, thenφis successful. 6.2 Other properties The previous section showed thatSuccessis not valid inHPAL. However, by Corollary 6.2, all universal formulas are successful and in particular all propositional formulas are successful. The same holds for Inclusion,Conjunctive InclusionandConjunctive Overlap. These postulates fail for reasons similar to the failure ofSuccess. For instance, in Figure 4, after Bob’s hedged announcement, Alice comes to believe that she doesn’t believep—a belief that she didn’t have before, which is a failure ofInclusion (M,w⊨¬B a ¬B a ¬p∧[÷¬p]B a ¬B a ¬p). This is to be expected: on the dynamic approach, the truths of doxastic formulas can be influenced by hedged announcements. However, all three postulates hold if the believed formula is propositional. LetKbe the class of all Kripke models. Proposition 6.3.The following are valid inHPAL, whereχandλare propositional andφ,ψ∈L ÷ : 1.Propositional Inclusion.[÷φ]B a χ→B a χ. 2.Propositional Conjunctive Inclusion.[÷λ∧ψ]¬B a λ→([÷λ∧ψ]B a χ→[÷λ]B a χ). 3.Propositional Conjunctive Overlap.([÷φ]B a χ∧[÷ψ]B a χ)→[÷φ∧ψ]B a χ. Proof sketch.Propositional Inclusionfollows fromR a (w)⊆R ÷φ a (w)and from propositional truth being unaffected by contraction.Propositional Conjunctive InclusionandOverlapfollow because contract- ing on a conjunction introduces no alternatives beyond those required to give up one of its conjuncts. Finally, whileVacuityis also among the properties that do not hold unrestrictedly, the following strong version holds: •Strong Vacuity. V a∈Ag ∀¬B a φ→(χ↔[÷φ]χ). This principle strengthens the standardVacuityprinciple listed above by requiring thatno agentbelieves the contracted formulaat any world in the model. Such restrictions reflect the multi-agent and public nature of our contraction operation. They are not required in classic AGM theory, where beliefs are propositional, nor in dynamic doxastic logic, which is single-agent [1, 30]. Proposition 6.4.Strong Vacuityis a theorem ofHPAL. Proof.Letφ,χ∈L ÷ and consider a Kripke modelM= (W,R,V)and a worldwin it. Assume that M,w⊨∀¬B a φ, for alla∈Ag, i.e.,M,u⊨¬B a φfor allu∈Wanda∈Ag. ThenR a (u) =R ÷φ a (u)for all worldsuand all agentsa, i.e.,M=M ÷φ and soM,w⊨χiffM ÷φ ,w⊨χ, that is,M,w⊨χiff M,w⊨[÷φ]χ. 7 GeneralizedDEL In this section, we introduce a generalized DEL framework that can model belief contraction resulting from different kinds of announcements, like hedged private announcements. Let theDELlanguageL DEL be the language generated by the grammar of the doxastic languageL extended with the following clausesφ::= [E,e]φ|∀φ, whereEis a generalized event model (introduced below) andeis an event in it. The formula[E,e]φreads “after(E,e)happens,φis the case”. G. Belardinelli & S. Zhang147 Definition 7.1(Generalized event model).Ageneralized event modelis a tupleE= (E,Q,Q + ,pre) whereEandQ a are defined as in standard event models,Q + a ⊆E×Eis an accessibility relation between events defined for all agentsa∈Ag, andpre:E→L DEL is a precondition function. A generalized event model is a standard event model extended with additional accessibility relations Q + a , for each agenta∈Ag, and in which preconditions can be formulas of the dynamic languageL DEL . As before, we use notationQ + a (e) =f∈E:(e,f)∈Q + a . Intuitively, bothQ a (e)andQ + a (e)represent events that are accessible, and thus considered possible, by agentaat evente. The difference, which will become formally clear with the product update definition below, is thatQ + a (e)contains alternatives that areintroduced by event e as possible for agent a(irrespective ofa’s prior beliefs), whileQ a (e)is the standard accessibility relation containing possibilities that are notruled out for agent a by event e. The distinction is illustrated by the event modelEin Figure 6, which is the event model correspond- ing to Example 3.1. Intuitively,frepresents the eventBob tells Alice her office door might be open and it is actually closed, andhrepresents the eventBob tells Alice her office door might be open and it is actually open. For Alice, Bob’s announcement doesn’t rule out eitherforh, but it introduceshas possible. Formally, this meansQ a (f) =Q a (h) =f,h, whileQ + a (f) =Q + a (h) =h. ¬p w p v a M ¬p f p h a+a+ E ¬p (w,f) p (v,h) a a a M⊗E Figure 6:Left: The Kripke modelMrepresenting Alice’s initial belief states.Middle: The generalized event modelE= (E,Q,Q + ,pre)representing Bob’s announcement to Alice thatpmight hold. An edge from an eventfto an eventhlabeled by+ameans thath∈Q + a (f). We omit theQ-edges sinceQ a (e) =E for alle∈E.Right: The Kripke modelM⊗E= (W E ,R E ,V E )representing Alice’s belief states after Bob’s announcement to Alice. Given this interpretation, the product update is then defined as the following: Definition 7.2(Generalized product update).Given a Kripke modelM= (W,R,V)and a generalized event modelE= (E,Q,Q + ,pre), their product updateM⊗Eis defined asM⊗E= (W E ,R E ,V E ) whereW E andV E are defined as in standard product updates (cf. Section 2) andR E is given by: (v,f)∈R E a (w,e)iff eitherf∈Q + a (e),orv∈R a (w)andf∈Q a (e). This product update behaves like a standard product update in eliminating possibilities (cf. Section 2), but additionally allows to expand the set of accessible worlds by adding all worlds(v,f)wherefis a newly considered possibility. In particular, the first disjunct allows agents to start considering worlds paired with events inQ + a , regardless of the original accessibility relation. The semantics of the dynamic modality is standard [20]: M,w⊨[E,e]φiffifM,w⊨pre(e)thenM⊗E,(w,e)⊨φ. The following definition shows that generalizedDELcan express contraction as induced by hedged public announcements. Definition 7.3(Event model for contraction onφ).Letφ∈L DEL . Anevent model for contraction onφ is a generalized event modelE(÷φ) = (E,Q,Q + ,pre)where 1.E=φ∧ V a∈A ¬B a φ∧ V a∈Ag B a φ:A⊆Ag∪¬φ∧ V a∈A ¬B a φ∧ V a∈Ag B a φ:A⊆Ag. 148Belief Contraction in Dynamic Epistemic Logic 2. For alla∈Agande∈E,Q a (e) =EandQ + a (e) = ( f∈E:pre(f)⊨¬φifpre(e)⊨B a φ; /0otherwise. 3. For alle∈E,pre(e) =e. Event modelE(÷φ)contains events for all possible configurations of the truth value ofφand which agents believeφ. The relationQ a is universal, capturing that the announcement reveals nothing about which event occurred. The relationQ + a captures contraction: agents who believedφcome to consider ¬φ-events possible, while the others are unaffected. Proposition 7.4.For any Kripke modelMand formulaφ∈L,M ÷φ is isomorphic toM⊗E(÷φ). Proof sketch.Both updates preserve all worlds ofM, so there is an isomorphism between the updated models: asR a (w)⊆R ÷φ a (w)andQ a (e) =Efor alla∈Ag,e∈E, all relations inMare preserved by both updates. Also, the only relations added in both cases are fromB a φ-worlds to¬φ-worlds. Next we consider an example involving hedged private announcement: Example 7.5.Alice just told Clark that she locked her office door before she left. Later, while Clark is evidently distracted, Bob privately tells Alice that her office door might actually be open. Alice comes to suspend judgment on whether she locked the door, while Clark does not notice this exchange, continuing to believe that Alice’s office door is closed and that Alice believes that. We model Bob’s private announcement using the generalized event modelEas described below: ¬p w p v a,ca,c M ⊤ e ¬p f p h c c a,c a a a+ a a+ E ¬p (w,f) p (v,h) ¬p (w,e) p (v,e) a,c a,c a c c a a M⊗E Figure 7:Left: The Kripke modelMrepresenting Alice and Clark’s initial belief states. We have M⊨B a ¬p∧B c ¬p∧B c B a ¬p.Middle: The generalized event modelE= (E,Q,Q + ,pre)representing Bob’s private announcement to Alice thatpmight hold. An edge from an eventfto an eventhlabeled by+ameans thath∈Q + a (f). If an edge’s label does not contain+, then the edge is aQ-relation, e.g. e∈Q c (f).Right: The Kripke modelM⊗E= (W E ,R E ,V E )representing Alice and Clark’s belief states after Bob’s private announcement to Alice. We now look into what is the logic of generalized updates. First, we define the composition of two generalized event models and then show that it is equivalent to the sequential updates of the two. Definition 7.6(Composition).Given two generalized event modelsE= (E E ,Q E ,Q +E ,pre E )andF= (E F ,Q F ,Q +F ,pre F ), then their composition isE◦F= (E,Q,Q + ,pre)where •E=E E ×E F ; •(e ′ ,f ′ )∈Q a ((e,f))iffe ′ ∈Q E a (e)andf ′ ∈Q F a (f); •(e ′ ,f ′ )∈Q + a ((e,f))ifff ′ ∈Q +F a (f), orf ′ ∈Q F a (f)ande ′ ∈Q +E a (e); •pre((e,f)) =pre E (e)∧[E,e]pre F (f). G. Belardinelli & S. Zhang149 CLall classical propositional tautologies ∀K∀(φ→ψ)→(∀φ→∀ψ) ∀T∀φ→φ ∀5¬∀φ→∀¬∀φ ∀B∀φ→B a φ BKB a (φ→ψ)→(B a φ→B a ψ) A1[E,e]p↔(pre(e)→p) A2[E,e]¬φ↔(pre(e)→¬[E,e]φ) A3[E,e](φ∧ψ)↔([E,e]φ∧[E,e]ψ) A4[E,e]∀φ↔(pre(e)→ V f∈E ∀[E,f]φ) A5[E,e]B a φ↔(pre(e)→( V f∈Q + a (e) ∀[E,f]φ∧ V f∈Q a (e) B a [E,f]φ)) A6[E,e][F,f]φ↔[E◦F,(e,f)]φ MP and necessitation rules for all modalities Table 2:The TheoryGDEL The following shows that this is given by the system presented in Table 2. 13 Theorem 7.7.The dynamic logic of generalized updates is completely axiomatized byGDEL. Proof sketch.The proof strategy is analogous to that used for Theorem 4.2, using the composition axiom A6 instead of the inference rule RE. The theoryGDELcontains the static axioms ofHPAL, together with the inference rules for all modalities. Additionally, it contains reduction axioms for event models analogous to those of standardDEL. Axiom A5 captures the effect of generalized updates on belief via the relationsQ a andQ + a . The next theorem shows that generalized updates always produce a model that is a simulation of a refinement of the initial model (refinement and simulation are defined standardly [14], but see Appendix). As noted in [15, 18], refinements decrease uncertainty by eliminating possibilities, while simulations capture increases in uncertainty by adding possibilities. Generalized updates thus can be seen as updates where agents may rule out possibilities while starting to consider new ones, as in belief revision. Theorem 7.8.For any Kripke modelMand generalized event modelE,M⊗Eis a simulation of a refinement ofM. Proof sketch.The idea is to split a generalized update into two steps. First ignore theQ + a edges and obtain a standardDELupdate, which gives a refinement of the initial model [15]. The full generalized update then only adds edges to this model, so it is a simulation of that refinement. Before concluding this section, we discuss one limitation of the contraction operation as defined in Section 4, and how the generalized product update helps to overcome it. Example 7.9.Alice and Clark walk down the hallway. Alice believes that she closed her office door (¬p) and that there will be a department meeting in the afternoon (q). Clark, however, is uncertain about both questions, though he believes that Alice believes the truth no matter what it is, and so does Alice. They then encounter Bob, who tells them that Alice’s office door might be open. 13 Note that, unlike the axiomatization ofHPAL, the axiomatization ofGDELincludes a composition axiom (A6) but without RE as a valid rule of inference. We conjecture that we can omit A6 and include RE as a valid inference rule, though we leave the verification of this conjecture to future work. 150Belief Contraction in Dynamic Epistemic Logic Intuitively, given Bob’s announcement, Clark will come to think that, if Alice initially believes that her office door is closed, then she’l come to suspend judgment about whether her office door is open, but she will remain confident about whether there will be a department meeting in the afternoon. So Alice’s and Clark’s beliefs should be modeled byNin Figure 8. pq u p¬q z ¬pq w ¬p¬q v a,ca,c a,ca,c c c c c M pq u p¬q z ¬pq w ¬p¬q v a,ca,c a,ca,c a a c c c c N Figure 8:Left: The Kripke modelMrepresenting Alice and Clark’s initial belief states. We have M⊨B c (B a p∨B a ¬p)∧B c (B a q∨B a ¬q).Right: The Kripke modelNrepresenting Alice and Clark’s belief states after Bob’s hedged announcement, whereN,w⊨¬B c (B a p∨B a ¬p)∧B c (B a q∨B a ¬q). Proposition 7.10.There is no formulaφ∈L ÷ such thatM ÷φ ≡N. Proof.Suppose towards a contradiction thatM ÷φ ≡Nfor someφ∈L ÷ . Since every world inM satisfies a distinct set of propositional formulas and contraction preserves propositional valuation, it follows that for allx∈W,(M ÷φ ,x)≡(N,x). Sinceu̸∈R a (w)butu∈R ÷φ a (w), we haveM,w⊨B a φ andM,u⊨¬φ. Similarly,M,v⊨B a φandM,z⊨¬φ. By the definition of contraction,x∈W:M,x⊨ ¬φ⊆R ÷φ a (w). Soz∈R ÷φ a (w). SoM ÷φ ,w⊨¬B a q. SinceN,w⊨B a q, this contradicts the assumption that(M ÷φ ,w)and(N,w)are modally equivalent. One way of addressing this problem within theHPALframework is to restrict the set of worlds that Alice starts considering to a subset ofp-possibilities, e.g. those that are compatible with her back- ground knowledge or “entrenched” beliefs. We can also model these dynamics usingGDEL. Consider E= (E,Q,Q + ,pre)depicted as in Figure 9, which captures three aspects of the update: (i) Bob’s an- nouncement doesn’t eliminate any possibilities (so theQ-relations are universal); (i) if Alice believes p, then Bob’s announcement doesn’t make her consider new possibilities (Q + a (e) =Q + a (g) =/0) (i) if Alice believes¬p, then Bob’s announcement makes her considerppossible without revising her beliefs aboutq(Q + a (f) =eandQ + a (h) =g). It’s not hard to check thatM⊗E=N. pq e ¬pq f p¬q g ¬p¬q h a+a+ Figure 9: The generalized event modelE= (E,Q,Q + ,pre)representing Bob’s announcement to Alice and Clark. As before, we omit theQ-edges, sinceQ i (x) =Efor all eventsx∈Eand agentsi∈a,c. Each event’s precondition is given by the conjunction of the literals listed inside the event. So for example eventehas preconditionp∧q. G. Belardinelli & S. Zhang151 8 Conclusion and future work In this paper, we introduced a logic for belief contraction due to hedged public announcements, and then a generalizedDELtheory for belief expansion and contraction. There are many questions left open for future work, such as: the full characterization of successful formulas forHPAL, the interaction between contraction and expansion operators, properties of a revision operator defined in terms of their combinations via the Levi identity [25], and the iterative properties ofGDEL. Of special importance are the closure properties ofGDEL. While updates with standard event models and plausibility event models preserve natural properties of accessibility relations, such as transitivity and Euclideanness, this is not true of generalized product updates, even if both theQ- and theQ + -relations in the generalized event model are equivalence relations. This has the undesirable consequence that an agent who had full introspection of her own beliefs prior to the update may have higher-order uncertainties about her own beliefs after the update. While it is possible to enforce preservation of introspection in our framework, it is an open question for which class of generalized event models this can be guaranteed. In addition to the above questions, we also plan to investigate how our model compares with al- ternative models of belief contraction [28, 24] as well as other models of information loss, such as forgetting and awareness growth [17, 11], and the dynamic approach to interpreting conditionals with modal antecedents. In particular, one may ask how expressive our generalized updates are with respect to plausibility updates. In one sense, we can transform any distinguished Kripke modelK= (W,R,V) into any Kripke modelK ′ = (W ′ ,R ′ ,V ′ )withW=W ′ andV=V ′ by adding the edges inK ′ without keeping any edges inK. 14 To this extent, our framework can emulate the belief dynamics that can be modeled in the plausibility framework, though we’l leave a detailed comparison to future works. Acknowledgments We would like to acknowledge Hans van Ditmarsch for suggesting the paper’s title and for very helpful comments on the paper, in particular for noticing that the axiomatization ofHPALwas missing replace- ment of equivalents. Gaia would also like to acknowledge Thomas Bolander for very helpful initial discussions on this work and contraction in DEL. We also thank three anonymous reviewers for very helpful comments. Gaia Belardinelli is funded by Independent Research Fund Denmark (grant no. 4255- 00020B). A Proofs Throughout, bylogical equivalencewe mean provable inK. We letJφK=w∈W:M,w⊨φ, and JφK ÷ψ =w∈W ÷ψ :M ÷ψ ,w⊨φ. Definition A.1(Bisimulation, refinement, simulation).LetM= (W,R,V)andM ′ = (W ′ ,R ′ ,V ′ )be two Kripke models. AbisimulationbetweenMandM ′ is a non-empty relationZ⊆W×W ′ such that for all(w,w ′ )∈Zanda∈Ag: (Atom):w∈V(p)iffw ′ ∈V ′ (p), for allp∈At; 14 Recall thatK= (W,R,V)isdistinguishedif for every worldwthere is a unique formulaφsuch thatM,w⊨φ. The simulation strategy is similar to the strategy used in [21] to show that inDELwith postconditions, one can transform any Kripke model in any other Kripke model. The strategy there is also to get rid of the structure of the initial Kripke model and then reconstruct it by means of carefully devised event models with postconditions. 152Belief Contraction in Dynamic Epistemic Logic (Forth): Ifv∈R a (w)then there existsv ′ ∈W ′ such thatv ′ ∈R ′ a (w ′ )and(v,v ′ )∈Z; (Back): Ifv ′ ∈R ′ a (w ′ )then there existsv∈Wsuch thatv∈R a (w)and(v,v ′ )∈Z; When a bisimulation exists between two models, we say that they arebisimilar. A relation that satisfies Atom and Back is arefinement. When a refinement exists betweenMandM ′ , we say thatM ′ is a refinementofM. A relation that satisfies Atom and Forth is asimulation. When a simulation exists betweenMandM ′ , we say thatM ′ is asimulationofM. Proof of Theorem 4.2.For soundness, the only non-trivial axiom is A5, namely[÷φ]B a ψ↔(B a [÷φ]ψ∧ (B a φ→∀(¬φ→[÷φ]ψ))). SupposeM,w⊨[÷φ]B a ψ. We claim thatM,w⊨B a [÷φ]ψ. Letv∈ R a (w). Thenv∈R ÷φ a (w). By assumption,M ÷φ ,w⊨B a ψ. SoM ÷φ ,v⊨ψ. ThusM,v⊨[÷φ]ψ. So M,w⊨B a [÷φ]ψ. Next, we claim that, ifM,w⊨B a φandM,w⊨[÷φ]B a ψ, then for everyv∈W, M,v⊨¬φ→[÷φ]ψ. Letv∈W. SupposeM,v⊨¬φ. SinceM,w⊨B a φ,v∈R ÷φ (w). SinceM,w⊨ [÷φ]B a ψ,M ÷φ ,v⊨ψ. SoM,v⊨[÷φ]ψ. Conversely, supposeM,w⊨B a [÷φ]ψ∧(B a φ→∀(¬φ→[÷φ]ψ)). There are two cases, either M,w⊨¬B a φorM,w⊨B a φ. SupposeM,w⊨¬B a φ. Letv∈R ÷φ (w). Thenv∈R a (w). Since M,w⊨B a [÷φ]ψ, we haveM,v⊨[÷φ]ψ. SoM ÷φ ,v⊨ψ. ThusM,w⊨[÷φ]B a ψ. Now suppose M,w⊨B a φ. SoM,w⊨∀(¬φ→[÷φ]ψ). Letv∈R ÷φ (w). Eitherv∈R a (w)orM,v⊨¬φ. In the first case, by the assumption thatM,w⊨B a [÷φ]ψ, we haveM ÷φ ,v⊨ψ. In the second case, since M,w⊨∀(¬φ→[÷φ]ψ), we haveM,v⊨[÷φ]ψor equivalentlyM ÷φ ,v⊨ψ. SoM,w⊨[÷φ]B a ψ. We now show that RE is validity preserving. Suppose⊨φ↔ψ. We proceed by induction on the complexity of the environmentχ. Ifχis a propositional variablep∈At, thenχ[φ/p] =φand χ[ψ/p] =ψ. So⊨χ[φ/p]↔χ[ψ/p]by assumption. The cases of negation and conjunction follow from propositional logic. Suppose⊨χ[φ/p]↔χ[ψ/p]. Then M,w⊨B a χ[φ/p]ifffor allv∈R a (w)M,v⊨χ[φ/p] ifffor allv∈R a (w)M,v⊨χ[ψ/p] iffM,w⊨B a χ[ψ/p] A similar argument shows that⊨∀χ[φ/p]↔∀χ[ψ/p]. Letλ∈L ÷ . Then M,w⊨[÷λ]χ[φ/p]iffM ÷λ ,w⊨χ[φ/p] iffM ÷λ ,w⊨χ[ψ/p] iffM,w⊨[÷λ]χ[ψ/p] Lastly, for any Kripke modelM= (W,R,V), we claim thatM ÷χ[φ/p] =M ÷χ[ψ/p] . It suffices to show thatR ÷χ[φ/p] a (w) =R ÷χ[ψ/p] a (w)for allw∈Wanda∈Ag. SupposeM,w⊨¬B a χ[φ/p]. Then by the inductive hypothesis,M,w⊨¬B a χ[ψ/p]and soR ÷χ[φ/p] a (w) =R a (w) =R ÷χ[ψ/p] a (w). Suppose M,w⊨B a χ[φ/p]. Then by IH,M,w⊨B a χ[ψ/p]and R ÷χ[φ/p] a (w) =R a (w)∪v∈W:M,v⊨¬χ[φ/p] =R a (w)∪v∈W:M,v⊨¬χ[ψ/p] =R ÷χ[ψ/p] a (w) SoM ÷χ[φ/p] =M ÷χ[ψ/p] . Thus, for any Kripke modelMand worldw, G. Belardinelli & S. Zhang153 M,w⊨[÷χ[φ/p]]λiffM ÷χ[φ/p] ,w⊨λ iffM ÷χ[ψ/p] ,w⊨λ iffM,w⊨[÷χ[ψ/p]]λ Given the reduction axioms, every formula with dynamic modalities is provably equivalent inHPAL to a formula without dynamic modalities. So the completeness ofHPALfollows from the completeness of the basic doxastic logic with universal modalities.□ Proof of Theorem 5.5.SupposeAg=a. Letφ∈L. LetM= (W,R,V)be a Kripke model that validatesS5. SupposeM,w⊨φ. SinceR a is an equivalence relation, for allv∈R a (w),M,v⊨ e B a φ. ThenR a (v) =R ÷¬φ a (v)for allv∈R a (w). ConsiderZ=(v,v):v∈R a (w). We claim thatZis a bisimulation between(M,w)and(M ÷¬φ ,w). Clearly the two worlds satisfy the same proposition atoms. Let(v,v)∈Z. Thenv∈R a (w). Supposeu∈R a (v). SinceR a is an equivalence relation, we haveu∈R a (w)and so(u,u)∈Z. Moreover, sinceR a (v) =R a (w) =R ÷¬φ a (w) =R ÷¬φ a (v), we haveu∈ R ÷¬φ a (v). Similarly, supposeu∈R ÷¬φ a (v). Thenu∈R ÷¬φ a (w) =R a (w) =R a (v). SoZis a bisimulation between(M,w)and(M ÷¬φ ,w). Thus,M ÷¬φ ,w⊨φ.□ Proof of Proposition 6.3. Letφ,ψ,χ,λ∈L ÷ withχ,λpropositional and consider a Kripke model M= (W,R,V)and a worldwin it. Notationally, letM ÷φ = (W ÷φ ,R ÷φ ,V ÷φ ),JψK=w∈W:M,w⊨ ψandJψK ÷φ =w∈W:M ÷φ ,w⊨ψ. 1.Propositional Inclusion: Assume thatM,w⊨[÷φ]B a χ. ThenM ÷φ ,w⊨B a χ. SoR ÷φ a (w)⊆ JχK ÷φ . By definition of contractionR a (w)⊆R ÷φ a (w)⊆JχK ÷φ . Asχis propositional,JχK= JχK ÷φ . Hence,M,w⊨B a χ. 2.Propositional Conjunctive Inclusion: SupposeM,w⊨[÷λ∧ψ]¬B a λandM,w⊨[÷λ∧ψ]B a χ. There are two cases: eitherM,w⊨¬B a (λ∧ψ)orM,w⊨B a (λ∧ψ). Suppose the first. Then R ÷λ∧ψ a (w) =R a (w). SinceM,w⊨[÷λ∧ψ]¬B a λ, there existsv∈R ÷λ∧ψ a (w)withM ÷λ∧ψ ,v⊨ ¬λ. Asλis propositional, thenM,v⊨¬λ, and sinceR ÷λ∧ψ a (w) =R a (w)thenM,w⊨¬B a λ. So R ÷λ a (w) =R a (w). Hence,R ÷λ∧ψ a (w) =R ÷λ a (w). SoM,w⊨[÷λ∧ψ]B a χimpliesR ÷λ a (w) = R ÷λ∧ψ a (w)⊆JχK ÷λ∧ψ =JχK ÷λ , where the last identity holds asχis propositional. Hence, M,w⊨[÷λ]B a χ. Now suppose the second case holds. ThenM,w⊨B a λ, and soR ÷λ a (w) = R a (w)∪J¬λK⊆R a (w)∪J¬λ∨¬ψK=R ÷(λ∧ψ) a (w). As by assumptionM,w⊨[÷λ∧ψ]B a χ, thenR ÷(λ∧ψ) a (w)⊆JχK ÷(λ∧ψ) =JχK ÷λ . Hence,R ÷λ a (w)⊆JχK ÷λ and soM,w⊨[÷λ]B a χ. 3.Propositional Conjunctive Overlap. Suppose thatM,w⊨[÷φ]B a χ∧[÷ψ]B a χ. ThenR ÷φ a (w)⊆ JχK ÷φ andR ÷ψ a (w)⊆JχK ÷ψ . Asχis propositional,JχK ÷φ =JχK ÷ψ =JχK ÷φ∧ψ , and so(R ÷φ a (w)∪ R ÷ψ a (w))⊆JχK ÷φ∧ψ . Two cases: eitherM,w⊨B a (φ∧ψ)or not. If the first, thenM,w⊨B a φ andM,w⊨B a ψ. SoR ÷φ a (w) =R a (w)∪J¬φKandR ÷ψ a (w) =R a (w)∪J¬ψKandR ÷φ∧ψ a (w) = R a (w)∪J¬φ∨¬ψK=R a (w)∪J¬φK∪J¬ψK. Then,R ÷φ∧ψ a (w) =R ÷φ a (w)∪R ÷ψ a (w), and so R ÷φ∧ψ a (w)⊆JχK ÷φ∧ψ . Hence,M,w⊨[÷φ∧ψ]B a χ. Suppose instead thatM,w⊨¬B a (φ∧ψ). Then,R ÷φ∧ψ a (w) =R a (w), and since by initial assumptionR ÷φ a (w)⊆JχK ÷φ∧ψ and by definition of contractionR a (w)⊆R ÷φ a (w), thenR a (w)⊆JχK ÷φ∧ψ . Hence,M,w⊨[÷φ∧ψ]B a χ.□ Proof of Proposition 7.4. LetM= (W,R,V)be a Kripke model. Notationally, we letE(÷φ) = (E,Q,Q + ,pre),M⊗E(÷φ) = (W E(÷φ) ,R E(÷φ) ,V E(÷φ) )andM ÷φ = (W ÷φ ,R ÷φ ,V ÷φ ). The func- tionh:W E(÷φ) →W ÷φ , defined byh((w,e)) =w, for allw∈W, is a bijection: first, notice that, by 154Belief Contraction in Dynamic Epistemic Logic definition ofE(÷φ), for each worldw∈Wthere is exactly one evente∈Esuch thatM,w⊨pre(e), and so(w,e)∈W E(÷φ) iffw∈W. Then notice that, by definition of÷φ-update,W ÷φ =W, and so (w,e)∈W E(÷φ) iffw∈W ÷φ . We now show thathpreserves atomic valuations and accessibility rela- tions. The atomic valuations are clearly preserved, asV E(÷φ) (p) =V(p) =V ÷φ (p)for allp∈At. For the accessibility relations, leta∈Agand(w,e)∈W E(÷φ) . We want to show that(v,f)∈R E(÷φ) a (w,e)iff v∈R ÷φ a (w). We consider two cases: eitherM,w̸⊨B a φ, orM,w⊨B a φ. SupposeM,w̸⊨B a φ. Then E(÷φ)is such thatQ a (e) =EandQ + a (e) =/0, andM ÷φ is such thatR a (w) =R ÷φ a (w). So we have that (v,f)∈R E(÷φ) a (w,e)iff (by definition of generalized product update)v∈R a (w)iff (by definition of÷φ- update)v∈R ÷φ a (w), as we wanted to show. Suppose insteadM,w⊨B a φ. Assume(v,f)∈R E(÷φ) a (w,e). Then eitherv∈R a (w)andf∈Q a (e), orf∈Q + a (e). Ifv∈R a (w), thenv∈R ÷φ a (w), as desired. If instead f∈Q + a (e), thenM,v⊨¬φand sov∈R ÷φ a (w), as desired. For the other direction, assumev∈R ÷φ a (w). Then eitherv∈R a (w)orM,v⊨¬φ. Ifv∈R a (w), then sinceQ a (e) =E,(v,f)∈R E(÷φ) a (w,e). If in- steadM,v⊨¬φ, then by(v,f)∈W E(÷φ) ,pre(f)⊨¬φby definition ofE(÷φ). SinceM,w⊨B a φthen Q + a (e) =g∈E:pre(g)⊨¬φ, and so(v,f)∈R E(÷φ) a (w,e). Hence in all cases we have the desired.□ Proof of Theorem 7.7. It is straightforward that the inference rules preserve validity. We check the soundness of A4 and A5. The soundness of the other axioms is immediate. LetM= (W,R,V)be a Kripke model, letE= (E,Q,Q + ,pre)be a generalized event model, and letM⊗E= (W E ,R E ,V E ). • A4: Note that, ifM,w̸⊨pre(e), then the biconditional holds automatically at(M,w). Suppose M,w⊨pre(e)andM,w⊨[E,e]∀φ. ThenM⊗E,(w,e)⊨∀φ, i.e. for all(v,f)∈W E ,M⊗ E,(v,f)⊨φ. In other words, for allf∈Eandv∈Wsuch thatM,v⊨pre(f),M,v⊨[E,f]φ. So M,w⊨ V f∈E ∀[E,f]φ. Conversely, supposeM,w⊨pre(e)butM,w⊨¬[E,e]∀φ, i.e.M⊗E,(w,e)̸⊨∀φ. So there is(v,f)∈W E such thatM⊗E,(v,f)̸⊨φ. It follows thatM,v⊨¬[E,f]φand soM,w⊨ ¬ V f∈E ∀[E,f]φ. • A5: SupposeM,w⊨[E,e]B a φ∧pre(e). Letf∈Q + a (e). Then for anyv∈W, ifM,v⊨pre(f), we have(v,f)∈R E a ((w,e))and so by assumptionM E ,(v,f)⊨φ. ThusM,w⊨ V f∈Q + a (e) ∀[E,f]φ. Letf∈Q a (e)andv∈R a (w). Then(v,f)∈R E a ((w,e))and soM E ,(v,f)⊨φ. ThusM,v⊨[E,f]φ. SoM,w⊨ V f∈Q a (e) B a [E,f]φ. Conversely, supposeM,w⊨pre(e)→ V f∈Q + a (e) ∀[E,f]φ∧ V f∈Q a (e) B a [E,f]φand let(v,f)∈ R E a ((w,e)). Eitherf∈Q + a (e)orf∈Q a (e)andv∈R a (w). In the first case, sinceM,w⊨∀[E,f]φ, we haveM,v⊨[E,f]φ. In the second case, sinceM,w⊨B a [E,f]φ, we haveM,v⊨[E,f]φ. So either way,M E ,(v,f)⊨φand soM E ,(w,e)⊨B a φ. • A6: The proof mainly requires showing that there exists an isomorphism between(M⊗E)⊗ F= (W EF ,R EF ,V EF )andM⊗(E◦F) = (W E◦F ,R E◦F ,V E◦F ). By invariance of truth under isomorphism, this will imply the desired. We use notationM⊗E= (W E ,R E ,V E ), andE= (E E ,Q E ,Q +E ,pre E )andF= (E F ,Q F ,Q +F ,pre F ). To show the existence of the isomorphism, leth:W EF →W E◦F be defined byh((w,e),f) = (w,(e,f)). Clearly,his a bijection:((w,e),f)∈W EF iffM,w|=pre E (e)andM⊗E,(w,e)|= pre F (f),iffM,w|=pre E (e)∧[E,e]pre F (f),iff(w,(e,f))∈W E◦F . It also preserves valua- tions, since for every atomp∈At,((w,e),f)∈V EF (p)iffw∈V(p)iff(w,(e,f))∈V E◦F (p). Finally,hpreserves accessibility relations. Let((w ′ ,e ′ ),f ′ )∈R EF a (((w,e),f)). We want to show that(w ′ ,(e ′ ,f ′ ))∈R E◦F a ((w,(e,f))). Let((w ′ ,e ′ ),f ′ )∈R EF a (((w,e),f)). Two cases: eitherf ′ ∈ G. Belardinelli & S. Zhang155 Q +F a (f)or(w ′ ,e ′ )∈R E a ((w,e))andf ′ ∈Q F a (f). Iff ′ ∈Q +F a (f)then(e ′ ,f ′ )∈Q +E◦F a (e,f)and so(w ′ ,(e ′ ,f ′ ))∈R E◦F a ((w,(e,f))). If(w ′ ,e ′ )∈R E a ((w,e))andf ′ ∈Q F a (f), then again two cases, eithere ′ ∈Q +E a (e), orw ′ ∈R a (w)ande ′ ∈Q E a (e). Ife ′ ∈Q +E a (e)then byf ′ ∈Q F a (f)and defini- tion of composition,(e ′ ,f ′ )∈Q +E◦F a ((e,f)), which implies(w ′ ,(e ′ ,f ′ ))∈R E◦F a ((w,(e,f))). If w ′ ∈R a (w)ande ′ ∈Q E a (e), then byf ′ ∈Q F a (f)and definition of composition we have(e ′ ,f ′ )∈ Q E◦F a ((e,f)), and so(w ′ ,(e ′ ,f ′ ))∈R E◦F a ((w,(e,f))). Hence, in all cases the desired holds. The other direction (that is, if(w ′ ,(e ′ ,f ′ ))∈R E◦F a ((w,(e,f)))then((w ′ ,e ′ ),f ′ )∈R EF a ((w,e),f)) fol- lows by a similar straightforward application of the definition of composition and generalized product update. Thus,his an isomorphism. By invariance of truth under isomorphisms, for every((w,e),f)∈ W EF and everyφ∈L DEL , we have((M⊗E)⊗F,((w,e),f))⊨φiff(M⊗(E◦F),(w,(e,f)))⊨ φ. It remains only to connect this with the truth conditions for the dynamic modalities. Letw∈W. IfM,w̸⊨pre E (e), then both[E,e][F,f]φand[E◦F,(e,f)]φare true atwvacuously, since pre E◦F (e,f) =pre E (e)∧[E,e]pre F (f). IfM,w⊨pre E (e)butM⊗E,(w,e)̸⊨pre F (f), then again[E,e][F,f]φis true atwvacuously, and so is[E◦F,(e,f)]φ, sinceM,w̸⊨pre E◦F (e,f). Finally, ifM,w⊨pre E (e)andM⊗E,(w,e)⊨pre F (f), then both product points((w,e),f)and (w,(e,f))exist, and the desired equivalence follows from the isomorphism above. Hence, in all cases,M,w⊨[E,e][F,f]φiffM,w⊨[E◦F,(e,f)]φ. SinceMandwwere arbitrary, the equiv- alence is valid. Completeness ofGDELfollows from the completeness ofKwith the universal modality by standard reduction arguments.□ Proof of Theorem 7.8. LetM= (W,R,V)be a Kripke model andE= (E,Q,Q + ,pre)be a generalized event model. Notationally, letM⊗E= (W E ,R E ,V E ). Our proof strategy is to define a submodel of M⊗Ethat serves as the intermediate refinement step, and then show thatM⊗Eis a simulation of that model. Let(W E − ,R E − ,V E − )be a Kripke model such thatW E − =W E ,R E − a (w,e) =(v,f)∈W E :v∈ R a (w),f∈Q a (e), for alla∈Ag, andV E − =V E . This is a submodel ofM⊗E, only missing the edges between worlds that theQ + relation added. It is then clear that we recover the fullR E by taking the union ofR E − with the set containing those edges, that isR E a (w,e) =R E − a (w,e)∪(v,f)∈W E :f∈Q + a (e), for alla∈Agand(w,e)∈W E . Now,(W E − ,R E − ,V E )is a standardDELupdate, and it is a well known result that it is a refinement ofM[15]. We now show thatM⊗Eis a simulation ofM⊗E − , from which we can conclude thatM⊗Eis a simulation of a refinement ofM. LetZ⊆W E − ×W E be such that((w,e),(w,e))∈Z. AsR E only adds edges toR E − without removing any, it clearly holds that if (v,f)∈R E − a (w,e), then(v,f)∈R E a (w,e), and since((v,f),(v,f))∈ZthenZis a simulation.□ References [1] Carlos E. Alchourrón, Peter Gärdenfors & David Makinson (1985):On the Logic of Theory Change: Partial Meet Contraction and Revision Functions.The Journal of Symbolic Logic50(2), p. 510–530, doi:10.2307/2274239. [2] Mikkel Birkegaard Andersen, Thomas Bolander, Hans van Ditmarsch & Martin Holm Jensen (2013):Bisimulation for single-agent plausibility models. In:Australasian Joint Conference on Artificial Intelligence, Springer, p. 277–288, doi:10.1007/978-3-319-03680-9_30. 156Belief Contraction in Dynamic Epistemic Logic [3] Mikkel Birkegaard Andersen, Thomas Bolander, Hans van Ditmarsch & Martin Holm Jensen (2017):Bisimulation and expressivity for conditional belief, degrees of belief, and safe belief.Syn- these194(7), p. 2447–2487, doi:10.1007/s11229-016-1060-x. [4] Hajnal Andréka, István Németi & Johan Van Benthem (1998):Modal languages and bounded fragments of predicate logic.Journal of philosophical logic27(3), p. 217–274, doi:10.1023/A:1004275029985. [5] Guillaume Aucher, Philippe Balbiani, Luis Fariñas del Cerro & Andreas Herzig (2009):Global and Local Graph Modifiers.Electronic Notes in Theoretical Computer Science231, p. 293–307, doi:10.1016/j.entcs.2009.02.042. Proceedings of the 5th Workshop on Methods for Modalities (M4M5 2007). [6] Alexandru Baltag, Lawrence S. Moss & Slawomir Solecki (1998):The Logic of Public Announce- ments and Common Knowledge and Private Suspicions. In Itzhak Gilboa, editor:Proceedings of the 7th Conference on Theoretical Aspects of Rationality and Knowledge (TARK-98), Morgan Kaufmann, p. 43–56. [7] Alexandru Baltag & Bryan Renne (2016):Dynamic Epistemic Logic. In Edward N. Zalta, editor: The Stanford Encyclopedia of Philosophy, Winter 2016 edition, Metaphysics Research Lab, Stan- ford University. Available athttps://plato.stanford.edu/archives/win2016/entries/ dynamic-epistemic/. [8] Alexandru Baltag & Sonja Smets (2008):A Qualitative Theory of Dynamic Interactive Belief Re- vision. In Giacomo Bonanno, Wiebe van der Hoek & Michael Wooldridge, editors:Logic and the Foundations of Game and Decision Theory (LOFT7),Texts in Logic and Games3, Amsterdam University Press, p. 13–60. Available athttps://w.jstor.org/stable/j.ctt46mz4h.4. [9] Johan van Benthem (2007):Dynamic logic for belief revision.Journal of applied non-classical logics17(2), p. 129–155, doi:10.3166/jancl.17.129-155. [10] Johan van Benthem (2023):The Logic of Conditionals on Outback Trails.Logic Journal of the IGPL31(6), p. 1135–1152, doi:10.1093/jigpal/jzac064. [11] Johan van Benthem & Fernando R. Velázquez-Quesada (2010):The dynamics of awareness.Syn- these177, p. 5–27, doi:10.1007/s11229-010-9764-9. [12] Johan van Benthem and (2007):Dynamic logic for belief revision.Journal of Applied Non- Classical Logics17(2), p. 129–155, doi:10.3166/jancl.17.129-155. [13] Matthew A. Benton & Peter Van Elswyk (2020):Hedged Assertion.In Sanford Gold- berg, editor:The Oxford Handbook of Assertion, Oxford University Press, p. 245–263, doi:10.1093/oxfordhb/9780190675233.013.11. [14] Patrick Blackburn, Maarten de Rijke & Yde Venema (2001):Modal Logic.Cambridge Tracts in Theoretical Computer Science53, Cambridge University Press, Cambridge, UK, doi:10.1017/CBO9781107050884. [15] Laura Bozzelli, Hans van Ditmarsch, Tim French, James Hales & Sophie Pinchinat (2014):Refine- ment modal logic.Information and Computation239, p. 303–339, doi:10.1016/j.ic.2014.07.013. [16] Lorenz Demey (2011):Some remarks on the model theory of epistemic plausibility models.Journal of Applied Non-Classical Logics21(3-4), p. 375–395, doi:10.3166/jancl.21.375-395. G. Belardinelli & S. Zhang157 [17] Hans van Ditmarsch & Tim French (2009):Awareness and forgetting of facts and agents. In: 2009 IEEE/WIC/ACM International Joint Conference on Web Intelligence and Intelligent Agent Technology, 3, IEEE, p. 478–483, doi:10.1109/WI-IAT.2009.330. [18] Hans van Ditmarsch, Tim French, Rustam Galimullin & Louwe B. Kuijer (2025):Modal Logic for Simulation, Refinement, and Mutual Ignorance.Electronic Proceedings in Theoretical Computer Science437, p. 379–398, doi:10.4204/eptcs.437.30. [19] Hans van Ditmarsch, Andreas Herzig, Jérôme Lang & Pierre Marquis (2009):Introspective forget- ting.Synthese169(2), p. 405–423, doi:10.1007/s11229-009-9554-4. [20] Hans van Ditmarsch, Wiebe van der Hoek & Barteld Kooi (2008):Dynamic epistemic logic. Springer, doi:10.1007/978-1-4020-5839-4. [21] Hans van Ditmarsch & Barteld Kooi (2008):Semantic Results for Ontic and Epistemic Change. In Giacomo Bonanno, Wiebe van der Hoek & Michael Wooldridge, editors:Logic and the Foundation of Game and Decision Theory (LOFT 7), p. 87–117. Available athttps://w.jstor.org/ stable/j.ctt46mz4h.6. [22] David Fernández–Duque, Ángel Nepomuceno–Fernández, Enrique Sarrión–Morrillo, Fernando Soler–Toscano & Fernando R. Velázquez–Quesada (2015):Forgetting complex propositions.Logic Journal of the IGPL23(6), p. 942–965, doi:10.1093/jigpal/jzv049. [23] Virginie Fiutek (2013):Playing with Knowledge and Belief. Ph.D. thesis, University of Amsterdam, Institute for Logic, Language, and Computation. Available athttps://eprints.illc.uva.nl/ id/eprint/2120. [24] Patrick Girard, Jeremy Seligman & Fenrong Liu (2012):General Dynamic Dynamic Logic. In Thomas Bolander, Torben Braüner, Silvio Ghilardi & Lawrence Moss, editors:Advances in Modal Logic 9, College Publications, p. 239–260, doi:10.1093/oso/9780198538592.003.0004. [25] Sven Ove Hansson (2022):Logic of Belief Revision.In Edward N. Zalta, editor:The Stanford Encyclopedia of Philosophy, Spring 2022 edition, Metaphysics Research Lab, Stan- ford University. Available athttps://plato.stanford.edu/archives/spr2022/entries/ logic-belief-revision/. [26] Andreas Herzig (2017):Dynamic Epistemic Logics:Promises, Problems, Shortcom- ings, and Perspectives.Journal of Applied Non-Classical Logics27(3-4), p. 328–341, doi:10.1080/11663081.2017.1416036. [27] Wesley H. Holliday & Thomas F. Icard I (2017):Indicative conditionals and dynamic epistemic logic.arXiv preprint arXiv:1707.08752, doi:10.48550/arXiv.1707.08752. [28] Hannes Leitgeb & Krister Segerberg (2007):Dynamic doxastic logic: why, how, and where to? Synthese155(2), p. 167–190, doi:10.1007/s11229-006-9143-8. [29] Jan Plaza (2007):Logics of public communications.Synthese158(2), p. 165–179, doi:10.1007/s11229-007-9168-7. [30] Krister Segerberg (1999):Two Traditions in the Logic of Belief: Bringing them Together, p. 135– 147. Springer Netherlands, Dordrecht, doi:10.1007/978-94-011-4574-9_8. [31] Yanjing Wang & Qinxiang Cao (2013):On axiomatizations of public announcement logic.Syn- these190(Suppl 1), p. 103–134, doi:10.1007/s11229-012-0233-5. [32] Seth Yalcin (2007):Epistemic modals.Mind116(464), p. 983–1026, doi:10.1093/mind/fzm983.