1 Introduction↩︎

Dynamic epistemic logic (DEL) is a family of logics that model multi-agent belief change by incorporating information revealed by epistemic events—such as public or private announcements—into agents’ epistemic states. In standard DEL [@baltag1998logic], this incorporation proceeds by eliminating all possibilities that are incompatible with the disclosed information. As a result, standard DEL can’t straightforwardly model announcements that make agents reconsider possibilities they previously ruled out as impossible, as required for belief contraction. A popular solution is to distinguish “hard” from “soft” updates; while hard updates involve eliminating possibilities, soft updates involve promoting possibilities in terms of their comparative plausibility [@benthem2007dynamic; @baltag2008qualitative]. Then, belief contraction about a factual proposition \(p\) consists in coming to judge that a \(\neg p\)-possibility is at least as plausible as the most plausible \(p\)-possibility, thereby losing the belief that \(p\) holds.

While the plausibility-based approach can model belief contraction [@baltag2008qualitative; @fiutek2013], it has certain expressive limitations. First, since plausibility orderings are transitive, the framework validates positive introspection for beliefs (axiom 4), and so can’t model agents who are mistaken about their own beliefs. Second, the approach can’t accommodate belief contractions due to hedged public announcements—announcements that \(p\) might be false. Intuitively, such an announcement could cause an agent who initially believes \(p\) to suspend judgment on \(p\) without gaining any new (factual) beliefs. We show that there is a precise sense in which such dynamics can’t be 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 models of beliefs, with no assumptions on the doxastic accessibility relations. Roughly, a hedged announcement that \(\varphi\) might be false triggers a contraction on \(\varphi\), which involves adding \(\neg\varphi\)-possibilities to an agent’s belief set if she believes \(\varphi\), and doing nothing otherwise. We define a sound and complete logic for this contraction modality, which we call hedged 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 logic GDEL that conservatively extends standard DEL to also accommodate belief contractions due to events such as private or semi-private announcements. We show that it contains HPAL and 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 logic GDEL can be viewed as a natural extension of standard DEL. As contraction is a form of information-loss, our model is also related to logics of forgetting and simulation modal logic [@ditmarsch2025simulation; @ditmarsch2009introspective; @fernandez-duque2015forgetting], as well as to the fragment of graph modifier logic that adds edges to Kripke models [@aucher2009global]. Our theory however contrasts with the theory of belief contraction as studied in AGM [@alchurron1985logic]; 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 considered 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 [@yalcin2007epistemic; @holliday2017indicative; @vanBenthem2023-VANTLO-47].

The proofs of main theorems can be found in the Appendix.

2 Standard DEL framework↩︎

We begin by reviewing the basics of DEL and fix notations.¹ Let \(At\) be a countable set of atomic formulas and \(Ag\) be a finite set of agents. Let \(\mathcal{L}\) be the doxastic language generated from \(At\) by the following grammar: \(\varphi\mathrel{\vcenter{:}}= \top\mid p\mid\neg\varphi\mid\varphi\wedge\varphi\mid B_a\varphi\), where \(p\in At\) and \(a\in Ag\). We write \(\bot\) for \(\neg\top\) and \(\widetilde{B}_a\varphi\) for \(\neg B_a\neg\varphi\). A literal is an atomic formula \(p\) or its negation \(\neg p\). Let \(\bigwedge_{\varphi\in S}\varphi=\top\) if \(S\) is empty.

We adopt the standard semantics of epistemic logic, where a Kripke model is a triple \(\mathcal{M}=(W, R, V)\) with \(W\not=\emptyset\) a set of worlds, \(R_a\subseteq(W\times W)\) an accessibility relation defined for all \(a\in Ag\), and \(V: At\rightarrow\wp(W)\) is a valuation function. We use notation \(R_a(w)=\{v\in W\colon (w,v)\in R_a\}\) to represent the set of possible worlds compatible with agent \(a\)’s belief at \(w\).

The satisfaction relation between a Kripke model \(\mathcal{M}=(W,R,V)\) with world \(w\in W\) and a formula \(\varphi\in\mathcal{L}\) is defined as standard, where in particular the semantics of the belief modality is given by:

A formula \(\varphi\) is valid in a model \(\mathcal{M}\) (notation: \(\mathcal{M}\vDash \varphi\)), if for all worlds \(w\) in \(\mathcal{M}\), \(\mathcal{M},w\vDash \varphi\). A formula \(\varphi\) is valid in a class of models \(\mathfrak{L}\) (notation: \(\vDash_\mathfrak{L} \varphi\)), if for all models \(\mathcal{M}\) in \(\mathfrak{L}\), \(\varphi\) is valid in \(\mathcal{M}\).

A standard event model is a triple \(\mathcal{E}=(E, Q, pre)\) where \(E\not=\emptyset\) is a finite set of events, \(Q_a\subseteq(E\times E)\) is an accessibility relation between events, for all \(a\in Ag\), and \(pre: E\rightarrow\mathcal{L}\) a precondition function.² We use notation \(Q_a(e)=\{f\in E\colon (e,f)\in Q_a\}\) for the set of events that are considered possible by \(a\) at \(e\).

For a Kripke model \(\mathcal{M}=(W, R, V)\) and a standard event model \(\mathcal{E}=(E, Q, pre)\), the standard product update of \(\mathcal{M}\) with \(\mathcal{E}\) is the Kripke model \(\mathcal{M} \otimes \mathcal{E} = (W^\mathcal{E},R^\mathcal{E},V^\mathcal{E})\) where \(W^\mathcal{E}=\{(w,e)\in W\times E\colon w\vDash pre(e)\}\), \(R^\mathcal{E}_a(w,e)=\{(v,f)\in W^\mathcal{E}\colon v\in R_a (w)\text{ and } f\in Q_a(e)\}\), and \(V^\mathcal{E}(p)=\{(w,e)\in W^\mathcal{E}\colon w\in V(p)\}\), for all \(p\in At\). Informally, a world \((w,e)\) represents the state of affairs at \(w\) after \(e\) occurs. We call these event models and product updates standard to distinguish them from the framework introduced later.

It is well known that standard DEL has undesirable consequences when agents are presented with information that contradicts their beliefs [@benthem2007dynamic; @herzig2017dynamic]. For a concrete illustration:

Let \(p\) denote 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.

3 Plausibility models↩︎

The “standard diagnosis” of the problem of modeling belief contraction in standard DEL is that we need a richer view of beliefs [@benthem2007dynamic]. 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 [@baltag2008qualitative; @benthem2007dynamic]. I believe that I am not dreaming. It is not impossible that I am, but those possibilities are less plausible than 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, a plausibility order on a set \(S\) is a connected, reflexive and transitive relation \(\trianglelefteq\subseteq S\times S\) such that every non-empty subset \(S'\subseteq S\) has at least one \(\trianglelefteq\)-minimal element, i.e. \(Min_\trianglelefteq (S')=\{w\in S': \forall v\in S', w\trianglelefteq v\}\neq\emptyset\). ³ A plausibility model is a Kripke model \((W,\preceq, V)\) with \(\preceq_a\) a plausibility order on \(W\), for all agents \(a\in Ag\). We write \(\prec_a\) for its asymmetric component, i.e. \(w\prec_a v\) if \(w\preceq_a v\) and \(v\not\preceq_a w\). The semantics of \(\mathcal{L}\) over 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: \[\mathcal{M}, w\vDash B_a \varphi \text{ iff } \mathcal{M}, v\vDash\varphi \text{ for all } v\in Min_{\preceq_a}(W).\] A plausibility event model is an event model \(\mathcal{E}=(E, \leq, pre)\) with \(\leq_a\) a plausibility order on \(E\) for all \(a\in Ag\). We write \(<_a\) for its asymmetric component. As in standard DEL, event models update plausibility models via product update. The plausibility-update of \(\mathcal{M}=(W, \preceq, V)\) with \(\mathcal{E}\) is the plausibility model \(\mathcal{M}\ast\mathcal{E}=(W^\mathcal{E},\preceq^\mathcal{E},V^\mathcal{E})\) where \(W^\mathcal{E}\) and \(V^\mathcal{E}\) are defined as in standard product updates and \(\preceq^\mathcal{E}\) is given by \((w,e)\preceq_a^\mathcal{E}(v,f) \text{ iff } e<_af, \text{ or } e\equiv_a f \text{ and }w\preceq_a v\). Figure 2 shows how to model Example 1 via a plausibility update. Alice’s change of mind is captured as a soft update where no world is ruled out as impossible, but their relative plausibility is switched.

3.1 Limitations of plausibility models↩︎

One limitation of the plausibility model of beliefs is that it validates axiom 4: \(B_a\varphi\rightarrow B_aB_a\varphi\). 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 involve adopting any new factual beliefs. A variant of Example 1 illustrates what we have in mind:

Let \(p\) denote the proposition Alice’s office door is open. Alice’s belief states before and after the update can be modeled by \(\mathcal{M}\) and \(\mathcal{N}\) in Figure 3, respectively.

However, it turns out that this update cannot be modeled as a plausibility update. More precisely, let \(\mathcal{K} \equiv \mathcal{K}'\) denote modal equivalence between two models \(\mathcal{K}\) and \(\mathcal{K}'\) with respect to \(\mathcal{L}\).⁴ Then:

Note that if two models are not modally equivalent with respect to \(\mathcal{L}\), then they are not modally equivalent with respect to any extension of \(\mathcal{L}\). So it follows from 1 that there is no plausibility event model \(\mathcal{E}\) such that \(\mathcal{M}\ast\mathcal{E}\) is modally equivalent to \(\mathcal{N}\) with respect to \(\mathcal{L}\) enriched with, e.g. modalities for conditional beliefs, safe beliefs or dynamic modalities. Relatedly, since modal equivalence is generally assumed to be a necessary condition for an adequate notion of bisimilarity, it also follows that there is no plausibility event model \(\mathcal{E}\) such that \(\mathcal{M}\ast \mathcal{E}\) is bisimilar to \(\mathcal{N}\) with respect to any adequate notion of bisimilarity (see e.g. [@demey2011remarks; @andersen2013bisimulation; @andersen2017bisimulation] for different notions of bisimilarity for plausibility structures).

4 A new model for belief contraction↩︎

1 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 to hedged public announcements, like Bob’s testimony that Alice’s door might be open.⁵ Formally, we represent the effects of such announcements by the dynamic modality “\([\div\varphi]\psi\)”. Intuitively, it says that \(\psi\) is the case after the hedged public announcement that \(\varphi\) might be false. Let the contraction language \(\mathcal{L}^\div\) be the language generated by the grammar of \(\mathcal{L}\) extended with the following clauses for the dynamic modality and a universal modality: \(\varphi\mathrel{\vcenter{:}}= [\div\varphi]\varphi\mid \forall \varphi\). We define \(\exists \varphi\mathrel{\vcenter{:}}= \neg\forall\neg\varphi\).

A standard (non-hedged) public announcement that \(\varphi\) is false is modeled as eliminating all the \(\varphi\)-possibilities fro5m all agents’ doxastic spaces [@plaza2007logics]. A natural thought, then, is that a hedged public announcement that \(\varphi\) might be false should add all the \(\neg\varphi\)-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 \(\neg\varphi\) possible to update their beliefs and start considering additional \(\neg\varphi\)-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 \(\varphi\) might be false depend on the agents’ initial beliefs, and in particular on whether they believe \(\varphi\) prior to the announcement. For this section, we assume that this is the only relevant difference: if an agent already considers \(\neg\varphi\) possible, then the announcement \(\varphi\) might be false has no effects on her beliefs; if the agent believes \(\varphi\), then the announcement leads her to consider all \(\neg\varphi\)-worlds as possible.

Call \(\mathcal{M}^{\div\varphi}\) the model obtained from \(\mathcal{M}\) by contracting on \(\varphi\). Note that it is always the case that \(R_a(w)\subseteq R_a^{\div\varphi}(w)\). This means that a hedged public announcement always extends the initial Kripke model. The semantics of \(\mathcal{L}^\div\) is given by the semantics of \(\mathcal{L}\) over Kripke models extended with these clauses:

Consider again Example 2. In the present framework, the effect of Bob’s announcement that Alice’s office door might be open can be modeled by contracting on the proposition Alice’s office door is closed (\(\neg p\)), which amounts to adding world \(v\) to Alice’s set of doxastic possibilities at \(w\) and \(v\). See Figure 4.

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

Besides axioms and rules of inference of the basic modal logic K with the universal modality (which is an S5 modality), the theory contains inference rules and reduction axioms for the contraction modality that parallel the reduction axioms in Public Announcement Logic (PAL) [@plaza2007logics; @van2008dynamic; @wang2013axiomatizations]. Axiom A5 is specific to our logic of contraction. It says that after contraction on \(\varphi\) (viz. a hedged announcement that \(\varphi\) might be false), an agent believes \(\psi\) iff she doesn’t believe \(\varphi\) prior to the announcement and she believes that \(\psi\) holds after the announcement, or she believes \(\varphi\) prior to the announcement and at any \(\neg\varphi\)-worlds, \(\psi\) 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. In PAL, formulas that become false or are not believed after an announcement are both called unsuccessful formulas. Let \([!\varphi]\) be the dynamic modality “after the announcement of \(\varphi\)” in PAL.⁶ There are thus two closely related notions of success in PAL: (i) what is announced is true after its announcement (\([!\varphi]\varphi\) is valid); (ii) what is announced is believed after its announcement (\([!\varphi]B_a\varphi\) is valid for all \(a\in Ag\)). For clarity, we will say \(\varphi\) is preserved in PAL if it satisfies (i); \(\varphi\) is successful in PAL if it satisfies (ii). It is well-known that, in PAL, any formula that satisfies (i) also satisfies (ii), though the converse does not hold.⁷ In this section, we focus on developing a notion of preservation for HPAL that is analogous to (i) for PAL.

A natural starting point is to say that \(\varphi\) is preserved if it is true after the hedged announcement that \(\varphi\) might be true, viz. \([\div\neg\varphi]\varphi\) is valid. But this isn’t quite right: while a public announcement that \(\varphi\) is true eliminates all \(\neg\varphi\)-possibilities, a hedged public announcement that \(\varphi\) might be true doesn’t eliminate any possibilities, and so any possibility where \(\varphi\) is false before the announcement remains in the model (though they may satisfy \(\varphi\) in the new model after the announcement). This observation suggests the following alternative definition of preservation for hedged public announcements (let \(\mathfrak{L}\) be a class of models that validates logic L):

Not all formulas in \(\mathcal{L}^\div\) are preserved in HPAL. Consider Example 2 again. Suppose Bob tells Alice instead that she might have a false belief that her office door is closed, viz. it might be true that \(p\wedge B_a\neg p\). Figure 5 shows that this hedged announcement is not preserved.

More generally, say \(\varphi\) is self-refuting (in the logic L) if \(\vDash_\mathfrak{L} \varphi\rightarrow [\div\neg\varphi]\neg\varphi\). Clearly, \(\varphi\) is not preserved if it is self-refuting. The above example is a special case of the following result:

So which formulas are preserved? Recall that a formula \(\varphi\) is existential if it is built only from literals, \(\wedge\), \(\vee\) and \(\widetilde{B}_a\); \(\varphi\) is universal if it is built only from literals, \(\wedge\), \(\vee\) and \(B_a\). It’s well-known that universal formulas remain true after being (standardly) publicly announced, in any normal modal logic [@van2008dynamic]. Their dual—existential formulas—are always preserved by hedged public announcements:

One upshot of Theorem 3 is that, while the “strong” Moorean sentence \(p\wedge B_a\neg p\) is never preserved, the “weak” Moorean sentence \(p\wedge\neg B_ap\), 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 formula \(p\wedge B_ap\) (agent \(a\) has a true belief that \(p\)) is preserved.

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 consider knowledge instead of belief for a moment, and restrict our attention to single-agent models. The standard logic for knowledge is S5, and extending HPAL with S5 axioms implies that all formulas in \(\mathcal{L}\) are preserved.

Note that model \(\mathcal{M}\) in Figure 5 validates KD45, so the preservation result doesn’t hold in these settings.⁹

6 AGM-style contraction principles↩︎

In the AGM literature, belief contraction is modeled as a static operation on the set of formulas, representing the agent’s belief base, and is characterized by a set of axioms. As [@van2007dynamic] points out, many of those axioms do not naturally hold in the dynamic setting where belief contraction induces model transformations. In this section, we give an overview of which of the AGM axioms hold/fail for our contraction operator. Following [@segerberg1999two], we render AGM statements that express that the agent believes \(\chi\) after contracting by \(\varphi\), by the formula \([\div\varphi]B_a\chi\). The modal version of the AGM axioms for contraction can then be expressed by the following formulas, where \(\varphi,\psi,\chi\in\mathcal{L}^{\div}\):

• Closure. \([\div\varphi](B_a(\psi\rightarrow\chi)\rightarrow(B_a\psi\rightarrow B_a\chi))\).

• Success. \(\exists\neg \varphi\rightarrow [\div\varphi]\neg B_a\varphi\).

• Inclusion. \([\div\varphi]B_a\psi \rightarrow B_a\psi\).

• Vacuity. \(\neg B_a\varphi \rightarrow (\chi\leftrightarrow [\div\varphi]\chi)\).

• Extensionality. If \(\vDash \varphi \leftrightarrow \psi\) then \(\vDash [\div\varphi]\chi\leftrightarrow [\div\psi]\chi\).

• Conjunctive Inclusion. \([\div (\varphi\wedge\psi)]\neg B_a\varphi\rightarrow([\div (\varphi\wedge\psi)] B_a\chi \rightarrow[\div \varphi] B_a\chi)\).

• Conjunctive Overlap. \(([\div \varphi] B_a\chi \wedge [\div \psi] B_a\chi)\rightarrow [\div (\varphi\wedge \psi)] B_a\chi\).

• Consistency. \(\neg B_a\bot\rightarrow[\div\varphi] \neg B_a\bot\).

From the list above we omitted the axiom called Recovery (expansion by \(\varphi\) after contraction by \(\varphi\) restores the agent’s original beliefs), as it involves an expansion operation which we do not focus on.¹⁰ We added to this list a natural property called Consistency, which is discussed in [@segerberg1999two; @herzig2017dynamic].

Some of these properties are valid in HPAL. In particular, Closure and Extensionality hold unrestrictedly in our semantic framework. Consistency also 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 \(\varphi\) is successful in PAL if it is believed after it is announced: \([!\varphi]B_a\varphi\) is valid for all \(a\in Ag\). A natural analogue of this notion in our contraction settings is that \(\varphi\) is not believed after a hedged announcement that it might be false, viz. \([\div\varphi]\neg B_a\varphi\) for all \(a\in Ag\). The only caveat concerns the case where \(\varphi\) is valid in the model. In that case, since there are no \(\neg\varphi\)-possibilities, contracting on \(\varphi\) leaves the model unchanged and so may leave agents’ beliefs in \(\varphi\) unchanged.¹¹ This illustrates why Success is given by the conditional \(\exists\neg \varphi\rightarrow [\div\varphi]\neg B_a\varphi\). Say that a formula \(\varphi\) is successful if it satisfies this property.

As with preservation, not all formulas are successful. For instance, the hedged announcement that \(p\wedge B_a\neg p\) might be true in Figure 5 is unsuccessful: after updating on Bob’s announcement that she might have a false belief that \(\neg p\), by contracting on \(\neg (p\wedge B_a\neg p)\), Alice will come to believe that she believes neither \(p\) nor \(\neg p\), and so she will believe that she doesn’t have a false belief that \(p\) (i.e. \(\mathcal{M}^{\div\neg (p\wedge B_a\neg p)}\vDash B_a\neg (p\wedge B_a\neg p)\)). In PAL, if a formula remains true after being announced, then it is believed after the announcement [@van2008dynamic]. A similar result holds for HPAL.

Given that existential formulas are preserved (Theorem 3), we then obtain the following corollary, which gives a sufficient condition for a formula to be successful:

6.2 Other properties↩︎

The previous section showed that Success is not valid in HPAL. However, by Corollary 1, all universal formulas are successful and in particular all propositional formulas are successful. The same holds for Inclusion, Conjunctive Inclusion and Conjunctive Overlap. These postulates fail for reasons similar to the failure of Success. For instance, in Figure 4, after Bob’s hedged announcement, Alice comes to believe that she doesn’t believe \(p\)—a belief that she didn’t have before, which is a failure of Inclusion (\(\mathcal{M}, w\vDash \neg B_a\neg B_a\neg p\wedge [\div\neg p]B_a\neg B_a\neg 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. Let \(\mathfrak{K}\) be the class of all Kripke models.

Finally, while Vacuity is also among the properties that do not hold unrestrictedly, the following strong version holds:

• Strong Vacuity. \(\bigwedge_{a\in Ag}\forall\neg B_a\varphi \rightarrow (\chi\leftrightarrow [\div\varphi]\chi)\).

This principle strengthens the standard Vacuity principle listed above by requiring that no agent believes the contracted formula at 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 [@alchurron1985logic; @segerberg1999two].

7 Generalized DEL↩︎

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 the DEL language \(\mathcal{L}_{DEL}\) be the language generated by the grammar of the doxastic language \(\mathcal{L}\) extended with the following clauses \(\varphi::=[\mathcal{E},e]\varphi\mid \forall \varphi\), where \(\mathcal{E}\) is a generalized event model (introduced below) and \(e\) is an event in it. The formula \([\mathcal{E},e]\varphi\) reads “after \((\mathcal{E},e)\) happens, \(\varphi\) is the case”.

A generalized event model is a standard event model extended with additional accessibility relations \(Q^+_a\), for each agent \(a\in Ag\), and in which preconditions can be formulas of the dynamic language \(\mathcal{L}_{DEL}\). As before, we use notation \(Q_a^+(e)=\{f\in E\colon (e,f)\in Q^+_a\}\). Intuitively, both \(Q_a(e)\) and \(Q^+_a(e)\) represent events that are accessible, and thus considered possible, by agent \(a\) at event \(e\). The difference, which will become formally clear with the product update definition below, is that \(Q^+_a(e)\) contains alternatives that are introduced by event \(e\) as possible for agent \(a\) (irrespective of \(a\)’s prior beliefs), while \(Q_a(e)\) is the standard accessibility relation containing possibilities that are not ruled out for agent \(a\) by event \(e\).

The distinction is illustrated by the event model \(\mathcal{E}\) in Figure 6, which is the event model corresponding to Example 2. Intuitively, \(f\) represents the event Bob tells Alice her office door might be open and it is actually closed, and \(h\) represents the event Bob tells Alice her office door might be open and it is actually open. For Alice, Bob’s announcement doesn’t rule out either \(f\) or \(h\), but it introduces \(h\) as possible. Formally, this means \(Q_a(f)=Q_a(h)=\{f,h\}\), while \(Q_a^+(f)=Q_a^+(h)=\{h\}\).

Given this interpretation, the product update is then defined as the following:

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)\) where \(f\) is a newly considered possibility. In particular, the first disjunct allows agents to start considering worlds paired with events in \(Q_a^+\), regardless of the original accessibility relation.

The semantics of the dynamic modality is standard [@van2008dynamic]:

The following definition shows that generalized DEL can express contraction as induced by hedged public announcements.

Event model \(\mathcal{E}(\div\varphi)\) contains events for all possible configurations of the truth value of \(\varphi\) and which agents believe \(\varphi\). The relation \(Q_a\) is universal, capturing that the announcement reveals nothing about which event occurred. The relation \(Q_a^+\) captures contraction: agents who believed \(\varphi\) come to consider \(\neg\varphi\)-events possible, while the others are unaffected.

Next we consider an example involving hedged private announcement:

We model Bob’s private announcement using the generalized event model \(\mathcal{E}\) as described below:

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.

The following shows that this is given by the system presented in Table 5.¹²

The theory GDEL contains the static axioms of HPAL, together with the inference rules for all modalities. Additionally, it contains reduction axioms for event models analogous to those of standard DEL. Axiom A5 captures the effect of generalized updates on belief via the relations \(Q_a\) and \(Q_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 [@bluebook], but see Appendix). As noted in [@bozzelli2014refinement; @ditmarsch2025simulation], 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.

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.

Intuitively, given Bob’s announcement, Clark will come to think that, if Alice initially believes that her office door is closed, then she’ll 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 by \(\mathcal{N}\) in 8.

One way of addressing this problem within the HPAL framework is to restrict the set of worlds that Alice starts considering to a subset of \(p\)-possibilities, e.g. those that are compatible with her background knowledge or “entrenched” beliefs. We can also model these dynamics using GDEL. Consider \(\mathcal{E}=(E, Q, Q^+, pre)\) depicted as in Figure 9, which captures three aspects of the update: (i) Bob’s announcement doesn’t eliminate any possibilities (so the \(Q\)-relations are universal); (ii) if Alice believes \(p\), then Bob’s announcement doesn’t make her consider new possibilities (\(Q_a^+(e)=Q_a^+(g)=\emptyset\)) (iii) if Alice believes \(\neg p\), then Bob’s announcement makes her consider \(p\) possible without revising her beliefs about \(q\) (\(Q_a^+(f)=\{e\}\) and \(Q_a^+(h)=\{g\}\)). It’s not hard to check that \(\mathcal{M}\otimes\mathcal{E}=\mathcal{N}\).

8 Conclusion and future work↩︎

In this paper, we introduced a logic for belief contraction due to hedged public announcements, and then a generalized DEL theory for belief expansion and contraction. There are many questions left open for future work, such as: the full characterization of successful formulas for HPAL, the interaction between contraction and expansion operators, properties of a revision operator defined in terms of their combinations via the Levi identity [@sep-logic-belief-revision], and the iterative properties of GDEL. Of special importance are the closure properties of GDEL. 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 the \(Q\)- and the \(Q^+\)-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 alternative models of belief contraction [@leitgeb2007dynamic; @girard2012general] as well as other models of information loss, such as forgetting and awareness growth [@ditmarsch2009awareness; @benthem2010awareness], 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 model \(\mathcal{K}=(W, R, V)\) into any Kripke model \(\mathcal{K'}=(W', R', V')\) with \(W=W'\) and \(V=V'\) by adding the edges in \(\mathcal{K'}\) without keeping any edges in \(\mathcal{K}\).¹³ To this extent, our framework can emulate the belief dynamics that can be modeled in the plausibility framework, though we’ll 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 of HPAL was missing replacement 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).

9 Proofs↩︎

Throughout, by logical equivalence we mean provable in \(\mathbf{K}\). We let \(\llbracket\varphi\rrbracket=\{w\in W\colon\mathcal{M},w\vDash \varphi\}\), and \(\llbracket\varphi\rrbracket^{\div\psi}=\{w\in W^{\div\psi}\colon\mathcal{M}^{\div\psi},w\vDash \varphi\}\).

Proof of Theorem 4.2. For soundness, the only non-trivial axiom is A5, namely \([\div\varphi]B_a\psi\leftrightarrow (B_a[\div\varphi]\psi\wedge (B_a\varphi\rightarrow \forall (\neg\varphi\rightarrow[\div\varphi]\psi)))\). Suppose \(\mathcal{M}, w\vDash [\div\varphi] B_a\psi\). We claim that \(\mathcal{M}, w\vDash B_a[\div\varphi]\psi\). Let \(v\in R_a(w)\). Then \(v\in R_a^{\div\varphi}(w)\). By assumption, \(\mathcal{M}^{\div\varphi},w\vDash B_a\psi\). So \(\mathcal{M}^{\div\varphi}, v\vDash \psi\). Thus \(\mathcal{M}, v\vDash [\div\varphi]\psi\). So \(\mathcal{M}, w\vDash B_a[\div\varphi]\psi\). Next, we claim that, if \(\mathcal{M}, w\vDash B_a\varphi\) and \(\mathcal{M}, w\vDash[\div\varphi]B_a\psi\), then for every \(v\in W\), \(\mathcal{M}, v\vDash \neg\varphi\rightarrow [\div\varphi]\psi\). Let \(v\in W\). Suppose \(\mathcal{M}, v\vDash \neg\varphi\). Since \(\mathcal{M}, w\vDash B_a\varphi\), \(v\in R^{\div\varphi}(w)\). Since \(\mathcal{M}, w\vDash [\div\varphi]B_a\psi\), \(\mathcal{M}^{\div\varphi}, v\vDash \psi\). So \(\mathcal{M}, v\vDash [\div\varphi]\psi\).

Conversely, suppose \(\mathcal{M}, w\vDash B_a[\div\varphi]\psi\wedge (B_a\varphi\rightarrow \forall (\neg\varphi\rightarrow [\div\varphi]\psi))\). There are two cases, either \(\mathcal{M}, w\vDash \neg B_a\varphi\) or \(\mathcal{M}, w\vDash B_a\varphi\). Suppose \(\mathcal{M}, w\vDash \neg B_a\varphi\). Let \(v\in R^{\div\varphi}(w)\). Then \(v\in R_a(w)\). Since \(\mathcal{M}, w\vDash B_a[\div\varphi]\psi\), we have \(\mathcal{M}, v\vDash [\div\varphi]\psi\). So \(\mathcal{M}^{\div\varphi}, v\vDash \psi\). Thus \(\mathcal{M}, w\vDash [\div\varphi]B_a\psi\). Now suppose \(\mathcal{M}, w\vDash B_a\varphi\). So \(\mathcal{M}, w\vDash \forall (\neg\varphi\rightarrow [\div\varphi]\psi)\). Let \(v\in R^{\div\varphi}(w)\). Either \(v\in R_a(w)\) or \(\mathcal{M}, v\vDash \neg\varphi\). In the first case, by the assumption that \(\mathcal{M}, w\vDash B_a[\div\varphi]\psi\), we have \(\mathcal{M}^{\div\varphi}, v\vDash \psi\). In the second case, since \(\mathcal{M}, w\vDash \forall (\neg\varphi\rightarrow [\div\varphi]\psi)\), we have \(\mathcal{M}, v\vDash [\div\varphi]\psi\) or equivalently \(\mathcal{M}^{\div\varphi},v\vDash\psi\). So \(\mathcal{M}, w\vDash [\div\varphi]B_a\psi\).

We now show that RE is validity preserving. Suppose \(\vDash\varphi\leftrightarrow\psi\). We proceed by induction on the complexity of the environment \(\chi\). If \(\chi\) is a propositional variable \(p\in At\), then \(\chi[\varphi/p]=\varphi\) and \(\chi[\psi/p]=\psi\). So \(\vDash\chi[\varphi/p]\leftrightarrow \chi[\psi/p]\) by assumption. The cases of negation and conjunction follow from propositional logic. Suppose \(\vDash \chi[\varphi/p]\leftrightarrow\chi[\psi/p]\). Then

A similar argument shows that \(\vDash \forall\chi[\varphi/p]\leftrightarrow\forall \chi[\psi/p]\). Let \(\lambda\in\mathcal{L}^{\div}\). Then

Lastly, for any Kripke model \(\mathcal{M}=(W, R, V)\), we claim that \(\mathcal{M}^{\div\chi[\varphi/p]}=\mathcal{M}^{\div\chi[\psi/p]}\). It suffices to show that \(R_a^{\div\chi[\varphi/p]}(w)=R_a^{\div\chi[\psi/p]}(w)\) for all \(w\in W\) and \(a\in Ag\). Suppose \(\mathcal{M}, w\vDash \neg B_a\chi[\varphi/p]\). Then by the inductive hypothesis, \(\mathcal{M}, w\vDash \neg B_a\chi[\psi/p]\) and so \(R_a^{\div\chi[\varphi/p]}(w)=R_a(w)=R_a^{\div\chi[\psi/p]}(w)\). Suppose \(\mathcal{M}, w\vDash B_a\chi[\varphi/p]\). Then by IH, \(\mathcal{M}, w\vDash B_a\chi[\psi/p]\) and

So \(\mathcal{M}^{\div\chi[\varphi/p]}=\mathcal{M}^{\div\chi[\psi/p]}\). Thus, for any Kripke model \(\mathcal{M}\) and world \(w\),

Given the reduction axioms, every formula with dynamic modalities is provably equivalent in HPAL to a formula without dynamic modalities. So the completeness of HPAL follows from the completeness of the basic doxastic logic with universal modalities. \(\Box\)

Proof of Theorem 5.5. Suppose \(Ag=\{a\}\). Let \(\varphi\in\mathcal{L}\). Let \(\mathcal{M}=(W, R, V)\) be a Kripke model that validates S5. Suppose \(\mathcal{M}, w\vDash \varphi\). Since \(R_a\) is an equivalence relation, for all \(v\in R_a(w)\), \(\mathcal{M}, v\vDash \widetilde{B}_a\varphi\). Then \(R_a(v)=R_a^{\div\neg\varphi}(v)\) for all \(v\in R_a(w)\). Consider \(Z=\{(v,v): v\in R_a(w)\}\). We claim that \(Z\) is a bisimulation between \((\mathcal{M}, w)\) and \((\mathcal{M}^{\div\neg\varphi}, w)\). Clearly the two worlds satisfy the same proposition atoms. Let \((v,v)\in Z\). Then \(v\in R_a(w)\). Suppose \(u\in R_a(v)\). Since \(R_a\) is an equivalence relation, we have \(u\in R_a(w)\) and so \((u,u)\in Z\). Moreover, since \(R_a(v)=R_a(w)=R_a^{\div\neg\varphi}(w)=R_a^{\div\neg\varphi}(v)\), we have \(u\in R_a^{\div\neg\varphi}(v)\). Similarly, suppose \(u\in R_a^{\div\neg\varphi}(v)\). Then \(u\in R_a^{\div\neg\varphi}(w)=R_a(w)=R_a(v)\). So \(Z\) is a bisimulation between \((\mathcal{M}, w)\) and \((\mathcal{M}^{\div\neg\varphi}, w)\). Thus, \(\mathcal{M}^{\div\neg\varphi}, w\vDash \varphi\). \(\Box\)

Proof of Proposition 6.3. Let \(\varphi,\psi,\chi, \lambda\in\mathcal{L}^\div\) with \(\chi, \lambda\) propositional and consider a Kripke model \(\mathcal{M}=(W,R,V)\) and a world \(w\) in it. Notationally, let \(\mathcal{M}^{\div\varphi}=(W^{\div\varphi},R^{\div\varphi},V^{\div\varphi})\), \(\llbracket\psi\rrbracket =\{w\in W: \mathcal{M}, w\vDash\psi\}\) and \(\llbracket \psi \rrbracket^{\div\varphi}=\{w\in W: \mathcal{M}^{\div\varphi}, w\vDash \psi\}\).

1. Propositional Inclusion: Assume that \(\mathcal{M},w\vDash [\div\varphi]B_a\chi\). Then \(\mathcal{M}^{\div\varphi},w\vDash B_a\chi\). So \(R_a^{\div\varphi}(w)\subseteq \llbracket \chi \rrbracket^{\div\varphi}\). By definition of contraction \(R_a(w)\subseteq R_a^{\div\varphi}(w)\subseteq \llbracket \chi \rrbracket^{\div\varphi}\). As \(\chi\) is propositional, \(\llbracket \chi \rrbracket=\llbracket \chi \rrbracket^{\div\varphi}\). Hence, \(\mathcal{M},w\vDash B_a\chi\).

2. Propositional Conjunctive Inclusion: Suppose \(\mathcal{M},w\vDash [\div \lambda\wedge\psi]\neg B_a\lambda\) and \(\mathcal{M},w\vDash[\div\lambda\wedge\psi] B_a\chi\). There are two cases: either \(\mathcal{M},w\vDash\neg B_a(\lambda\wedge \psi)\) or \(\mathcal{M},w\vDash B_a(\lambda\wedge \psi)\). Suppose the first. Then \(R_a^{\div\lambda\wedge\psi}(w)=R_a(w)\). Since \(\mathcal{M},w\vDash[\div\lambda\wedge\psi]\neg B_a\lambda\), there exists \(v\in R_a^{\div\lambda\wedge\psi}(w)\) with \(\mathcal{M}^{\div\lambda\wedge\psi},v\vDash \neg \lambda\). As \(\lambda\) is propositional, then \(\mathcal{M},v\vDash \neg \lambda\), and since \(R_a^{\div\lambda\wedge\psi}(w)=R_a(w)\) then \(\mathcal{M},w\vDash \neg B_a\lambda\). So \(R_a^{\div \lambda}(w)=R_a(w)\). Hence, \(R_a^{\div\lambda\wedge\psi}(w)=R_a^{\div \lambda}(w)\). So \(\mathcal{M},w\vDash [\div\lambda\wedge\psi] B_a\chi\) implies \(R_a^{\div \lambda}(w)=R_a^{\div\lambda\wedge\psi}(w)\subseteq \llbracket\chi\rrbracket^{\div\lambda\wedge\psi}=\llbracket\chi\rrbracket^{\div \lambda}\), where the last identity holds as \(\chi\) is propositional. Hence, \(\mathcal{M},w\vDash [\div \lambda] B_a\chi\). Now suppose the second case holds. Then \(\mathcal{M},w\vDash B_a\lambda\), and so \(R^{\div\lambda}_a(w)=R_a(w)\cup\llbracket\neg\lambda\rrbracket \subseteq R_a(w)\cup \llbracket\neg\lambda\vee\neg\psi\rrbracket =R_a^{\div(\lambda\wedge \psi)}(w)\). As by assumption \(\mathcal{M},w\vDash[\div\lambda\wedge\psi] B_a\chi\), then \(R_a^{\div(\lambda\wedge \psi)}(w)\subseteq \llbracket \chi\rrbracket^{\div(\lambda\wedge \psi)}=\llbracket \chi\rrbracket^{\div\lambda}\). Hence, \(R^{\div\lambda}_a(w)\subseteq\llbracket \chi\rrbracket^{\div\lambda}\) and so \(\mathcal{M},w\vDash[\div \lambda] B_a\chi\).

3. Propositional Conjunctive Overlap. Suppose that \(\mathcal{M},w\vDash [\div \varphi] B_a\chi \wedge [\div \psi] B_a\chi\). Then \(R_a^{\div\varphi}(w)\subseteq \llbracket\chi \rrbracket^{\div\varphi}\) and \(R_a^{\div\psi}(w)\subseteq \llbracket\chi \rrbracket^{\div\psi}\). As \(\chi\) is propositional, \(\llbracket\chi \rrbracket^{\div\varphi}=\llbracket\chi \rrbracket^{\div\psi}=\llbracket\chi \rrbracket^{\div\varphi\wedge\psi}\), and so \((R_a^{\div\varphi}(w)\cup R_a^{\div\psi}(w))\subseteq \llbracket\chi \rrbracket^{\div\varphi\wedge\psi}\). Two cases: either \(\mathcal{M},w\vDash B_a(\varphi\wedge\psi)\) or not. If the first, then \(\mathcal{M},w\vDash B_a\varphi\) and \(\mathcal{M},w\vDash B_a\psi\). So \(R_a^{\div\varphi}(w)=R_a(w)\cup \llbracket\neg\varphi\rrbracket\) and \(R_a^{\div\psi}(w)= R_a(w)\cup \llbracket\neg\psi\rrbracket\) and \(R_a^{\div\varphi\wedge\psi}(w)= R_a(w)\cup \llbracket\neg\varphi\vee\neg\psi\rrbracket=R_a(w)\cup \llbracket\neg\varphi\rrbracket\cup\llbracket\neg\psi\rrbracket\). Then, \(R_a^{\div\varphi\wedge\psi}(w)= R_a^{\div\varphi}(w)\cup R_a^{\div\psi}(w)\), and so \(R_a^{\div\varphi\wedge\psi}(w)\subseteq \llbracket\chi \rrbracket^{\div\varphi\wedge\psi}\). Hence, \(\mathcal{M},w\vDash [\div \varphi\wedge \psi] B_a\chi\). Suppose instead that \(\mathcal{M},w\vDash \neg B_a(\varphi\wedge\psi)\). Then, \(R_a^{\div\varphi\wedge\psi}(w)= R_a(w)\), and since by initial assumption \(R_a^{\div\varphi}(w)\subseteq \llbracket\chi \rrbracket^{\div\varphi\wedge\psi}\) and by definition of contraction \(R_a(w)\subseteq R_a^{\div\varphi}(w)\), then \(R_a(w)\subseteq\llbracket\chi \rrbracket^{\div\varphi\wedge\psi}\). Hence, \(\mathcal{M},w\vDash [\div \varphi\wedge \psi] B_a\chi\).\(\Box\)

Proof of Proposition 7.4. Let \(\mathcal{M}=(W,R,V)\) be a Kripke model. Notationally, we let \(\mathcal{E}(\div\varphi)=(E,Q,Q^+,pre)\), \(\mathcal{M}\otimes \mathcal{E}(\div\varphi)=(W^{\mathcal{E}(\div\varphi)},R^{\mathcal{E}(\div\varphi)},V^{\mathcal{E}(\div\varphi)})\) and \(\mathcal{M}^{\div\varphi}=(W^{\div\varphi},R^{\div\varphi},V^{\div\varphi})\). The function \(h\colon W^{\mathcal{E}(\div\varphi)}\rightarrow W^{\div\varphi}\), defined by \(h((w,e))=w\), for all \(w\in W\), is a bijection: first, notice that, by definition of \(\mathcal{E}(\div\varphi)\), for each world \(w\in W\) there is exactly one event \(e\in E\) such that \(\mathcal{M},w\vDash pre(e)\), and so \((w,e)\in W^{\mathcal{E}(\div\varphi)}\) iff \(w\in W\). Then notice that, by definition of \(\div\varphi\)-update, \(W^{\div\varphi}=W\), and so \((w,e)\in W^{\mathcal{E}(\div\varphi)}\) iff \(w\in W^{\div\varphi}\). We now show that \(h\) preserves atomic valuations and accessibility relations. The atomic valuations are clearly preserved, as \(V^{\mathcal{E}(\div\varphi)}(p)=V(p)=V^{\div\varphi}(p)\) for all \(p\in At\). For the accessibility relations, let \(a\in Ag\) and \((w,e)\in W^{\mathcal{E}(\div\varphi)}\). We want to show that \((v,f)\in R_a^{\mathcal{E}(\div\varphi)}(w,e)\) iff \(v\in R^{\div\varphi}_a(w)\). We consider two cases: either \(\mathcal{M},w\not\vDash B_a\varphi\), or \(\mathcal{M},w\vDash B_a\varphi\). Suppose \(\mathcal{M},w\not\vDash B_a\varphi\). Then \(\mathcal{E}(\div\varphi)\) is such that \(Q_a(e)=E\) and \(Q^+_a(e)=\emptyset\), and \(\mathcal{M}^{\div\varphi}\) is such that \(R_a(w)=R_a^{\div\varphi}(w)\). So we have that \((v,f)\in R^{\mathcal{E}(\div\varphi)}_a(w,e)\) iff (by definition of generalized product update) \(v\in R_a(w)\) iff (by definition of \(\div\varphi\)-update) \(v\in R^{\div\varphi}_a(w)\), as we wanted to show. Suppose instead \(\mathcal{M},w\vDash B_a\varphi\). Assume \((v,f)\in R^{\mathcal{E}(\div\varphi)}_a(w,e)\). Then either \(v\in R_a(w)\) and \(f\in Q_a(e)\), or \(f\in Q^+_a(e)\). If \(v\in R_a(w)\), then \(v\in R^{\div\varphi}_a(w)\), as desired. If instead \(f\in Q^+_a(e)\), then \(\mathcal{M},v\vDash \neg \varphi\) and so \(v\in R^{\div\varphi}_a(w)\), as desired. For the other direction, assume \(v\in R^{\div\varphi}_a(w)\). Then either \(v\in R_a(w)\) or \(\mathcal{M},v\vDash \neg\varphi\). If \(v\in R_a(w)\), then since \(Q_a(e)=E\), \((v,f)\in R^{\mathcal{E}(\div\varphi)}_a(w,e)\). If instead \(\mathcal{M},v\vDash \neg\varphi\), then by \((v,f)\in W^{\mathcal{E}(\div\varphi)}\), \(pre(f)\vDash \neg\varphi\) by definition of \(\mathcal{E}(\div\varphi)\). Since \(\mathcal{M},w\vDash B_a\varphi\) then \(Q^+_a(e)=\{g\in E\colon pre(g)\vDash \neg\varphi\}\), and so \((v,f)\in R^{\mathcal{E}(\div\varphi)}_a(w,e)\). Hence in all cases we have the desired.\(\Box\)

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. Let \(\mathcal{M}=(W,R,V)\) be a Kripke model, let \(\mathcal{E}=(E,Q,Q^+,pre)\) be a generalized event model, and let \(\mathcal{M}\otimes\mathcal{E}=(W^\mathcal{E},R^\mathcal{E},V^\mathcal{E})\).

• A4: Note that, if \(\mathcal{M}, w\not\vDash pre(e)\), then the biconditional holds automatically at \((\mathcal{M}, w)\). Suppose \(\mathcal{M}, w\vDash pre(e)\) and \(\mathcal{M}, w\vDash [\mathcal{E}, e]\forall\varphi\). Then \(\mathcal{M}\otimes\mathcal{E}, (w,e)\vDash\forall\varphi\), i.e. for all \((v,f)\in W^\mathcal{E}\), \(\mathcal{M}\otimes\mathcal{E}, (v,f)\vDash\varphi\). In other words, for all \(f\in E\) and \(v\in W\) such that \(\mathcal{M}, v\vDash pre(f)\), \(\mathcal{M}, v\vDash[\mathcal{E},f]\varphi\). So \(\mathcal{M},w\vDash\bigwedge_{f\in E}\forall[\mathcal{E},f]\varphi\).

  Conversely, suppose \(\mathcal{M}, w\vDash pre(e)\) but \(\mathcal{M}, w\vDash \neg [\mathcal{E},e]\forall\varphi\), i.e. \(\mathcal{M}\otimes\mathcal{E}, (w,e)\not\vDash\forall\varphi\). So there is \((v,f)\in W^\mathcal{E}\) such that \(\mathcal{M}\otimes\mathcal{E}, (v,f)\not\vDash\varphi\). It follows that \(\mathcal{M}, v\vDash \neg [\mathcal{E},f]\varphi\) and so \(\mathcal{M}, w\vDash\neg\bigwedge_{f\in E}\forall [\mathcal{E}, f]\varphi\).

• A5: Suppose \(\mathcal{M}, w\vDash [\mathcal{E}, e]B_a\varphi\wedge pre(e)\). Let \(f\in Q_a^+(e)\). Then for any \(v\in W\), if \(\mathcal{M},v\vDash pre(f)\), we have \((v,f)\in R_a^\mathcal{E}((w,e))\) and so by assumption \(\mathcal{M}^\mathcal{E}, (v,f)\vDash \varphi\). Thus \(\mathcal{M}, w\vDash \bigwedge_{f\in Q_a^+(e)}\forall [\mathcal{E},f]\varphi\). Let \(f\in Q_a(e)\) and \(v\in R_a(w)\). Then \((v,f)\in R_a^\mathcal{E}((w,e))\) and so \(\mathcal{M}^\mathcal{E}, (v,f)\vDash \varphi\). Thus \(\mathcal{M}, v\vDash[\mathcal{E},f]\varphi\). So \(\mathcal{M}, w\vDash \bigwedge_{f\in Q_a(e)}B_a[\mathcal{E},f]\varphi\).

  Conversely, suppose \(\mathcal{M}, w\vDash pre(e)\rightarrow\bigwedge_{f\in Q_a^+(e)}\forall [\mathcal{E},f]\varphi\wedge\bigwedge_{f\in Q_a(e)}B_a[\mathcal{E},f]\varphi\) and let \((v,f)\in R_a^\mathcal{E}((w,e))\). Either \(f\in Q_a^+(e)\) or \(f\in Q_a(e)\) and \(v\in R_a(w)\). In the first case, since \(\mathcal{M}, w\vDash \forall [\mathcal{E},f]\varphi\), we have \(\mathcal{M}, v\vDash[\mathcal{E},f] \varphi\). In the second case, since \(\mathcal{M}, w\vDash B_a[\mathcal{E},f]\varphi\), we have \(\mathcal{M}, v\vDash [\mathcal{E},f]\varphi\). So either way, \(\mathcal{M}^\mathcal{E}, (v,f)\vDash\varphi\) and so \(\mathcal{M}^\mathcal{E}, (w,e)\vDash B_a\varphi\).

• A6: The proof mainly requires showing that there exists an isomorphism between \((\mathcal{M}\otimes\mathcal{E})\otimes\mathcal{F}=(W^{\mathcal{E}\mathcal{F}},R^{\mathcal{E}\mathcal{F}},V^{\mathcal{E}\mathcal{F}})\) and \(\mathcal{M}\otimes(\mathcal{E}\circ\mathcal{F})=(W^{\mathcal{E}\circ\mathcal{F}},R^{\mathcal{E}\circ\mathcal{F}},V^{\mathcal{E}\circ\mathcal{F}})\). By invariance of truth under isomorphism, this will imply the desired. We use notation \(\mathcal{M}\otimes\mathcal{E}=(W^{\mathcal{E}},R^{\mathcal{E}},V^{\mathcal{E}})\), and \(\mathcal{E}=(E^\mathcal{E},Q^\mathcal{E},Q^{+\mathcal{E}},pre^\mathcal{E})\) and \(\mathcal{F}=(E^\mathcal{F},Q^\mathcal{F},Q^{+\mathcal{F}},pre^\mathcal{F})\).

  To show the existence of the isomorphism, let \(h: W^{\mathcal{E}\mathcal{F}}\rightarrow W^{\mathcal{E}\circ\mathcal{F}}\) be defined by \(h((w,e),f)=(w,(e,f))\). Clearly, \(h\) is a bijection: \(((w,e),f)\in W^{\mathcal{E}\mathcal{F}}\) iff \(\mathcal{M},w\models pre^\mathcal{E}(e) \quad\text{and}\quad \mathcal{M}\otimes\mathcal{E},(w,e)\models pre^\mathcal{F}(f),\) iff \(\mathcal{M},w\models pre^\mathcal{E}(e)\wedge[\mathcal{E},e]pre^\mathcal{F}(f),\) iff \((w,(e,f))\in W^{\mathcal{E}\circ\mathcal{F}}\). It also preserves valuations, since for every atom \(p\in At\), \(((w,e),f)\in V^{\mathcal{E}\mathcal{F}}(p)\) iff \(w\in V(p)\) iff \((w,(e,f))\in V^{\mathcal{E}\circ\mathcal{F}}(p)\). Finally, \(h\) preserves accessibility relations. Let \(((w',e'),f')\in R^{\mathcal{E}\mathcal{F}}_a(((w,e),f))\). We want to show that \((w',(e',f'))\in R^{\mathcal{E}\circ\mathcal{F}}_a((w,(e,f)))\). Let \(((w',e'),f')\in R^{\mathcal{E}\mathcal{F}}_a(((w,e),f))\). Two cases: either \(f'\in Q_a^{+\mathcal{F}}(f)\) or \((w',e')\in R^\mathcal{E}_a((w,e))\) and \(f'\in Q_a^{\mathcal{F}}(f)\). If \(f'\in Q_a^{+\mathcal{F}}(f)\) then \((e', f')\in Q^{+\mathcal{E}\circ\mathcal{F}}_a(e,f)\) and so \((w',(e',f'))\in R^{\mathcal{E}\circ\mathcal{F}}_a((w,(e,f)))\). If \((w',e')\in R^\mathcal{E}_a((w,e))\) and \(f'\in Q_a^{\mathcal{F}}(f)\), then again two cases, either \(e'\in Q_a^{+\mathcal{E}}(e)\), or \(w'\in R_a(w)\) and \(e'\in Q_a^{\mathcal{E}}(e)\). If \(e'\in Q_a^{+\mathcal{E}}(e)\) then by \(f'\in Q_a^{\mathcal{F}}(f)\) and definition of composition, \((e', f')\in Q^{+\mathcal{E}\circ\mathcal{F}}_a((e,f))\), which implies \((w',(e',f'))\in R^{\mathcal{E}\circ\mathcal{F}}_a((w,(e,f)))\). If \(w'\in R_a(w)\) and \(e'\in Q_a^{\mathcal{E}}(e)\), then by \(f'\in Q_a^{\mathcal{F}}(f)\) and definition of composition we have \((e', f')\in Q^{\mathcal{E}\circ\mathcal{F}}_a((e,f))\), and so \((w',(e',f'))\in R^{\mathcal{E}\circ\mathcal{F}}_a((w,(e,f)))\). Hence, in all cases the desired holds. The other direction (that is, if \((w',(e',f'))\in R^{\mathcal{E}\circ\mathcal{F}}_a((w,(e,f)))\) then \(((w',e'),f')\in R^{\mathcal{E}\mathcal{F}}_a((w,e),f)\)) follows by a similar straightforward application of the definition of composition and generalized product update.

  Thus, \(h\) is an isomorphism. By invariance of truth under isomorphisms, for every \(((w,e),f)\in W^{\mathcal{E}\mathcal{F}}\) and every \(\varphi\in \mathcal{L}_{\text{DEL}}\), we have \(((\mathcal{M}\otimes\mathcal{E})\otimes\mathcal{F},((w,e),f))\vDash\varphi\) iff \((\mathcal{M}\otimes(\mathcal{E}\circ\mathcal{F}),(w,(e,f)))\vDash\varphi\). It remains only to connect this with the truth conditions for the dynamic modalities. Let \(w\in W\). If \(\mathcal{M},w\not\vDash pre^\mathcal{E}(e)\), then both \([\mathcal{E},e][\mathcal{F},f]\varphi\) and \([\mathcal{E}\circ\mathcal{F},(e,f)]\varphi\) are true at \(w\) vacuously, since \(pre^{\mathcal{E}\circ\mathcal{F}}(e,f)=pre^\mathcal{E}(e)\wedge[\mathcal{E},e]pre^\mathcal{F}(f)\). If \(\mathcal{M},w\vDash pre^\mathcal{E}(e)\) but \(\mathcal{M}\otimes\mathcal{E},(w,e)\not\vDash pre^\mathcal{F}(f)\), then again \([\mathcal{E},e][\mathcal{F},f]\varphi\) is true at \(w\) vacuously, and so is \([\mathcal{E}\circ\mathcal{F},(e,f)]\varphi\), since \(\mathcal{M},w\not\vDash pre^{\mathcal{E}\circ\mathcal{F}}(e,f)\). Finally, if \(\mathcal{M},w\vDash pre^\mathcal{E}(e)\) and \(\mathcal{M}\otimes\mathcal{E},(w,e)\vDash pre^\mathcal{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, \(\mathcal{M},w\vDash[\mathcal{E},e][\mathcal{F},f]\varphi\) iff \(\mathcal{M},w\vDash[\mathcal{E}\circ\mathcal{F},(e,f)]\varphi\). Since \(\mathcal{M}\) and \(w\) were arbitrary, the equivalence is valid.

Completeness of GDEL follows from the completeness of K with the universal modality by standard reduction arguments.\(\Box\)

Proof of Theorem 7.8. Let \(\mathcal{M}=(W,R,V)\) be a Kripke model and \(\mathcal{E}=(E,Q,Q^+,pre)\) be a generalized event model. Notationally, let \(\mathcal{M}\otimes \mathcal{E}=(W^\mathcal{E},R^\mathcal{E},V^\mathcal{E})\). Our proof strategy is to define a submodel of \(\mathcal{M}\otimes\mathcal{E}\) that serves as the intermediate refinement step, and then show that \(\mathcal{M}\otimes\mathcal{E}\) is a simulation of that model. Let \((W^{\mathcal{E}^-}, R^{\mathcal{E}^-},V^{\mathcal{E}^-})\) be a Kripke model such that \(W^{\mathcal{E}^-}= W^\mathcal{E}\), \(R_a^{\mathcal{E}^-}(w,e)=\{(v,f)\in W^\mathcal{E}\colon v\in R_a(w), f\in Q_a(e)\}\), for all \(a\in Ag\), and \(V^{\mathcal{E}^-}=V^\mathcal{E}\). This is a submodel of \(\mathcal{M}\otimes \mathcal{E}\), only missing the edges between worlds that the \(Q^+\) relation added. It is then clear that we recover the full \(R^\mathcal{E}\) by taking the union of \(R^{\mathcal{E}^-}\) with the set containing those edges, that is \(R_a^{\mathcal{E}}(w,e)=R_a^{\mathcal{E}^-}(w,e)\cup \{(v,f)\in W^\mathcal{E}\colon f\in Q^+_a(e)\}\), for all \(a\in Ag\) and \((w,e)\in W^\mathcal{E}\). Now, \((W^{\mathcal{E}^-}, R^{\mathcal{E}^-},V^\mathcal{E})\) is a standard DEL update, and it is a well known result that it is a refinement of \(\mathcal{M}\) [@bozzelli2014refinement]. We now show that \(\mathcal{M}\otimes\mathcal{E}\) is a simulation of \(\mathcal{M}\otimes\mathcal{E}^-\), from which we can conclude that \(\mathcal{M}\otimes\mathcal{E}\) is a simulation of a refinement of \(\mathcal{M}\). Let \(Z\subseteq W^{\mathcal{E}^-}\times W^\mathcal{E}\) be such that \(((w,e),(w,e))\in Z\). As \(R^\mathcal{E}\) only adds edges to \(R^{\mathcal{E}^-}\) without removing any, it clearly holds that if \((v,f)\in R^{\mathcal{E}^-}_a(w,e)\), then \((v,f)\in R^{\mathcal{E}}_a(w,e)\), and since \(((v,f),(v,f))\in Z\) then \(Z\) is a simulation. \(\Box\)

---

1. For presentation purposes, in this section we only introduce the basic doxastic language without dynamic modalities. We introduce the full language of DEL in the last section, where we also use it. For an introduction to DEL, see [@sep-dynamic-epistemic].↩︎

2. In the most general form of DEL, the precondition function assigns to each event a formula from the dynamic language (i.e. \(\mathcal{L}\) extended with dynamic formulas). We keep it simple here and consider this general DEL form in the last section.↩︎

3. Note that we assume the plausibility order to be connected. This is more restrictive than usual [@baltag2008qualitative], but it is justified here as our framework only models belief and omits knowledge.↩︎

4. Recall that two Kripke (or plausibility) models \(\mathcal{K}=(W,R,V)\) and \(\mathcal{K}'=(W',R',V')\) are modally equivalent with respect to \(\mathcal{L}\) if for every formula \(\varphi \in \mathcal{L}\) and every state \(w \in W\), there exists a state \(w' \in W'\) such that \(\mathcal{K},w \vDash \varphi\) iff \(\mathcal{K}',w' \vDash \varphi\), and conversely, for every \(w' \in W'\) there exists a state \(w \in W\) with the same property.↩︎

5. The name hedged public announcement reflects 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” [@benton2020hedged].↩︎

6. In PAL, the formula \([!\varphi]\psi\) intuitively says \(\psi\) is true after eliminating all \(\neg\varphi\)-possibilities from the model; see [@van2008dynamic] and references therein for more on PAL.↩︎

7. The proof that (i) implies (ii) is analogous to the “only if”-direction of [@van2008dynamic], 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, suppose \(Ag=\{a\}\), let \(\varphi\mathrel{\vcenter{:}}= p\wedge B_a\neg p\wedge \neg B_a\bot\), and consider a Kripke model and a world \(w\) in it where such \(\varphi\) is true. Then, after the public announcement of \(\varphi\), which eliminates all possibilities where \(\varphi\) is not true and so also all worlds that were accessible for \(a\) at \(w\), \(a\) will have inconsistent beliefs at \(w\) and believe (trivially) that \(\varphi\) is true. Hence, \([!\varphi]B_a\varphi\) is valid. On the other hand, \([!\varphi]\varphi\) is invalid and in particular \([!\varphi]\neg B_a\bot\) is invalid.↩︎

8. Note that the Moorean sentence \(p\wedge B_a\neg p\) is unsatisfiable in S5, while \(p\wedge\exists B_a\neg p\) is satisfiable even if belief is factive.↩︎

9. As an anonymous referee pointed out, the result does not generalize to the multi-agent setting.↩︎

10. Notice, however, that Recovery does not hold in general in this framework: while the contraction operator \([\div\varphi]\) can informally be viewed as a dual of the public announcement operator \([!\varphi]\), it is not a formal dual, in the sense that contraction by \(\varphi\) followed by expansion by \(\varphi\) 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.↩︎

11. This mirrors the AGM constraint that beliefs in validities cannot be given up [@alchurron1985logic; @sep-logic-belief-revision].↩︎

12. Note that, unlike the axiomatization of HPAL, the axiomatization of GDEL includes 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.↩︎

13. Recall that \(\mathcal{K}=(W, R, V)\) is distinguished if for every world \(w\) there is a unique formula \(\varphi\) such that \(\mathcal{M}, w\vDash \varphi\). The simulation strategy is similar to the strategy used in [@ditmarsch2008semantic] to show that in DEL with 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.↩︎