Belief Contraction in Dynamic Epistemic Logic Gaia Belardinelli
Snow Zhang
Department of Philosophy Stanford University Stanford, USA [email protected]
Department of Philosophy University of California, Berkeley Berkeley, USA [email protected]
Dynamic epistemic logic (DEL) 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 ϕ 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.
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 [6], 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 [12, 8]. Then, belief contraction about a factual proposition p consists in coming to judge that a ¬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 [8, 23], 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 M. Bílková, M. Gattinger, I. van der Giessen, M. Girlando, Y. Wang (Eds.): Advances in Modal Logic 2026 (AiML 2026) EPTCS 447, 2026, pp. 137–157, doi:10.4204/EPTCS.447.8
© G. Belardinelli & S. Zhang This work is licensed under the Creative Commons Attribution License.
138
Belief Contraction in Dynamic Epistemic Logic
models of beliefs, with no assumptions on the doxastic accessibility relations. Roughly, a hedged announcement that ϕ might be false triggers 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 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 [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 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 [32, 27, 10]. 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.1 Let At be a countable set of atomic formulas and Ag be a finite set of agents. Let L be the doxastic language generated from At by the following grammar: ϕ := ⊤ | p | ¬ϕ | ϕ ∧ ϕ | Ba ϕ, where p ∈ At and a ∈ Ag. We write ⊥ for ¬⊤ and Bea ϕ for V ¬Ba ¬ϕ. A literal is an atomic formula p or its negation ¬p. Let ϕ∈S ϕ = ⊤ if S is empty. We adopt the standard semantics of epistemic logic, where a Kripke model is a triple M = (W, R,V ) with W ̸= 0/ a set of worlds, Ra ⊆ (W ×W ) an accessibility relation defined for all a ∈ Ag, and V : At → ℘(W ) is a valuation function. We use notation Ra (w) = {v ∈ W : (w, v) ∈ Ra } to represent the set of possible worlds compatible with agent a’s belief at w. The satisfaction relation between a Kripke model M = (W, R,V ) with world w ∈ W and a formula ϕ ∈ L is defined as standard, where in particular the semantics of the belief modality is given by: M , w ⊨ Ba ϕ
iff
M , v ⊨ ϕ for all v ∈ Ra (w).
A formula ϕ is valid in a model M (notation: M ⊨ ϕ), if for all worlds w in M , M , w ⊨ ϕ. A formula ϕ is valid in a class of models L (notation: ⊨L ϕ), if for all models M in L, ϕ is valid in M . A standard event model is a triple E = (E, Q, pre) where E ̸= 0/ is a finite set of events, Qa ⊆ (E × E) is an accessibility relation between events, for all a ∈ Ag, and pre : E → L a precondition function.2 We use notation Qa (e) = { f ∈ E : (e, f ) ∈ Qa } for the set of events that are considered possible by a at e. For a Kripke model M = (W, R,V ) and a standard event model E = (E, Q, pre), the standard product update of M with E is the Kripke model M ⊗ E = (W E , RE ,V E ) where W 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 of DEL in the last section, where we also use it. For an introduction to DEL, see [7]. 2 In the most general form of DEL, the precondition function assigns to each event a formula from the dynamic language (i.e. L extended with dynamic formulas). We keep it simple here and consider this general DEL form in the last section.
G. Belardinelli & S. Zhang
139
pre(e)}, REa (w, e) = {(v, f ) ∈ W E : v ∈ Ra (w) and f ∈ Qa (e)}, and V E (p) = {(w, e) ∈ W E : w ∈ V (p)}, for all p ∈ 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 [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 that her office door was open. Alice trusts Bob and revises her beliefs accordingly. 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. M
a
¬p w
a
p v
E
p e
a
M ⊗E
p (v, e)
Figure 1: Left: The Kripke model M = (W, R,V ) representing Alice’s initial belief state. An edge from a world v to a world w means w ∈ Ra (v). We have M ⊨ Ba ¬p∧¬Ba p. Middle: The standard event model E = (E, Q, pre) representing Bob’s announcement. The event e contains its own precondition pre(e) = p. The loop on e means e ∈ Qa (e). Right: The Kripke model M ⊗ E = (W E , RE ,V E ) representing Alice’s belief state after the update, where REa ((v, e)) = 0/ and so e.g. M ⊗ E ⊨ Ba p ∧ Ba ¬p.
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 [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 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 ⊴⊆ S × S such that every non-empty subset S′ ⊆ S has at least one ⊴-minimal element, i.e. Min⊴ (S′ ) = {w ∈ S′ : ∀v ∈ S′ , w ⊴ v} ̸= 0. / 3 A plausibility model is a Kripke model (W, ⪯,V ) with ⪯a a plausibility order on W , for all agents a ∈ Ag. We write ≺a for its asymmetric component, i.e. w ≺a v if w ⪯a v and v ̸⪯a w. The semantics of 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: M , w ⊨ Ba ϕ iff M , v ⊨ ϕ for all v ∈ Min⪯a (W ). A plausibility event model is an event model E = (E, ≤, pre) with ≤a a plausibility order on E for all a ∈ Ag. We write <a for its asymmetric component. As in standard DEL, event models update plausibility models via product update. The plausibility-update of M = (W, ⪯,V ) with E is the plausibility model M ∗ E = (W E , ⪯E ,V E ) where W E and V E are defined as in standard product updates and ⪯E is given 3 Note that we assume the plausibility order to be connected. This is more restrictive than usual [8], but it is justified here as our framework only models belief and omits knowledge.
140
Belief Contraction in Dynamic Epistemic Logic
by (w, e) ⪯Ea (v, f ) iff e <a f , or e ≡a f and w ⪯a v. Figure 2 shows how to model Example 2.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. M a
¬p
p
a
w
E a
a
v
¬p f
a
p e
a
M ∗E a
¬p
a
(w, f )
p
a
(v, e)
Figure 2: Left: The plausibility model M = (W, ⪯,V ) representing Alice’s initial belief state. An edge from v to w means w ⪯a v. We have M ⊨ Ba ¬p ∧ ¬Ba p. Middle: The plausibility event model E = (E, ≤, pre) capturing a soft update that p holds. An edge from f to e means e ≤a f . Right: The plausibility model M ∗ E representing Alice’s belief state after updating, with M ∗ E ⊨ Ba p ∧ ¬Ba ¬p.
3.1
Limitations of plausibility models
One limitation of the plausibility model of beliefs is that it validates axiom 4: Ba ϕ → Ba Ba ϕ. 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 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 that her 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. Let p denote the proposition Alice’s office door is open. Alice’s belief states before and after the update can be modeled by M and N in Figure 3, respectively. M
a
¬p w
a
p v
a
N
a
¬p w
a
p
a
v
Figure 3: Left: The plausibility model M = (W, ⪯,V ) representing Alice’s initial belief state, where M ⊨ Ba ¬p ∧ ¬Ba p. Conventions for edges are as in Fig. 2. Right: The plausibility model N = (W, ⪯N ,V ) representing Alice’s belief state after updating on Bob’s testimony, where N ⊨ ¬Ba p ∧ ¬Ba ¬p. However, it turns out that this update cannot be modeled as a plausibility update. More precisely, let K ≡ K ′ denote modal equivalence between two models K and K ′ with respect to L .4 Then: Theorem 3.2. There is no plausibility event model E such that M ∗ E ≡ N . Proof. Let M = (W, ⪯,V ) and N = (W, ⪯N ,V ) be as depicted in Figure 3. Suppose towards a contradiction that there is a plausibility event model E = {E, ≤, pre} such that M ∗ E = (W E , ⪯E ,V E ) is a plausibility model that is modally equivalent to N . We claim that, for any (v, f ) ∈ W E , there exists a (v, f ′ ) ̸= (v, f ) such that (v, f ′ ) ≺Ea (v, f ). It follows then that M ∗ E contains an infinite descending 4 Recall that two Kripke (or plausibility) models K = (W, R,V ) and K ′ = (W ′ , R′ ,V ′ ) are modally equivalent with respect
to L if for every formula ϕ ∈ L and every state w ∈ W , there exists a state w′ ∈ W ′ such that K , w ⊨ ϕ iff K ′ , w′ ⊨ ϕ, and conversely, for every w′ ∈ W ′ there exists a state w ∈ W with the same property.
G. Belardinelli & S. Zhang
141
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) ⊨ ¬Ba p , we have (M ∗ E , (v, f )) ⊨ ¬Ba p. So there exists (w, e) ∈ W E such that (w, e) ⪯Ea (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)). Since N , w ⊨ Bea p, there exists (v, f ′ ) ∈ W E such that (v, f ′ ) ⪯Ea (w, e). Moreover, since v ̸⪯a w, we must have f ′ <a e ≤a f . So f ′ <a f and therefore (v, f ′ ) ≺Ea (v, f ). Note that if two models are not modally equivalent with respect to L , then they are not modally equivalent with respect to any extension of L . So it follows from Theorem 3.2 that there is no plausibility event model E such that M ∗ E is modally equivalent to N with respect to 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 E such that M ∗ E is bisimilar to N with 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 to hedged public announcements, like Bob’s testimony that Alice’s door might be open.5 Formally, we represent the effects of such announcements by the dynamic modality “[÷ϕ]ψ”. Intuitively, it says that ψ is the case after the hedged public announcement that ϕ might be false. Let the contraction language L ÷ be the language generated by the grammar of L extended with the following clauses for the dynamic modality and a universal modality: ϕ := [÷ϕ]ϕ | ∀ϕ. We define ∃ϕ := ¬∀¬ϕ. A standard (non-hedged) public announcement that ϕ is false is 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 false should 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 false has 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 model M = (W, R,V ) and a formula ϕ ∈ L ÷ . Let M ÷ϕ = (W, R÷ϕ ( ,V ) be defined by, for all a ∈ Ag and all w ∈ W : Ra (w) ∪ {v ∈ W : M , v ⊨ ¬ϕ} if M , w ⊨ Ba ϕ ÷ϕ Ra (w) = Ra (w) otherwise 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” [13].
142
Belief Contraction in Dynamic Epistemic Logic
Call M ÷ϕ the model obtained from M by contracting on ϕ. Note that it is always the case that Ra (w) ⊆ ÷ϕ Ra (w). This means that a hedged public announcement always extends the initial Kripke model. The semantics of L ÷ is given by the semantics of L over Kripke models extended with these clauses: M , w ⊨ [÷ϕ]ψ M , w ⊨ ∀ϕ
iff iff
M ÷ϕ , w ⊨ ψ; for all v ∈ W , M , v ⊨ ϕ.
Consider again Example 3.1. 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 (¬p), which amounts to adding world v to Alice’s set of doxastic possibilities at w and v. See Figure 4. M
a
¬p w
a
p v
M ÷¬p
a
¬p
a
p
a
w
v a Figure 4: Left: The Kripke model M (same as Figure 1), representing Alice’s initial belief state. Right: The Kripke model M ÷¬p representing Alice’s belief state after updating on Bob’s hedged announcement, obtained by contracting on ¬p. We have M ÷¬p ⊨ ¬Ba ¬p ∧ ¬Ba 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. CL ∀K ∀T ∀5 ∀B BK
all classical propositional tautologies ∀(ϕ → ψ) → (∀ϕ → ∀ψ) ∀ϕ → ϕ ¬∀ϕ → ∀¬∀ϕ ∀ϕ → Ba ϕ Ba (ϕ → ψ) → (Ba ϕ → Ba ψ)
A1 A2 A3 A4 A5
[÷ϕ]p ↔ p [÷ϕ]¬ψ ↔ ¬[÷ϕ]ψ [÷ϕ](ψ ∧ χ) ↔ [÷ϕ]ψ ∧ [÷ϕ]χ [÷ϕ]∀ψ ↔ ∀[÷ϕ]ψ [÷ϕ]Ba ψ ↔ (Ba [÷ϕ]ψ ∧ (Ba ϕ → ∀(¬ϕ → [÷ϕ]ψ)))
MP RE NEC
From ϕ and ϕ → ψ, infer ψ From ϕ ↔ ψ, infer χ[ϕ/p] ↔ χ[ψ/p] Necessitation rules for all modalities6
Table 1: The Theory of Hedged Public Announcement Logic (HPAL) Theorem 4.2. The dynamic logic of contraction updates is completely axiomatized by HPAL. Proof sketch. Soundness follows by straightforward validity arguments. For completeness, given the reduction axioms, every formula with dynamic modalities is provably equivalent in HPAL to a formula without. So the completeness of HPAL follows 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 logic K with 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. Zhang
143
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. In PAL, formulas that become false or are not believed after an announcement are both called unsuccessful formulas. Let [!ϕ] be the dynamic modality “after the announcement of ϕ” in PAL.7 There are thus two closely related notions of success in PAL: (i) what is announced is true after its announcement ([!ϕ]ϕ is valid); (ii) what is announced is believed after its announcement ([!ϕ]Ba ϕ is valid for all a ∈ Ag). For clarity, we will say ϕ is preserved in PAL if it satisfies (i); ϕ 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.8 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 ϕ is preserved if 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 ϕ is true eliminates all ¬ϕ-possibilities, a hedged public announcement that ϕ might be 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 (let L be a class of models that validates logic L): Definition 5.1 (Preservation). ϕ is preserved (in the logic L) if ⊨L ϕ → [÷¬ϕ]ϕ Not all formulas in L ÷ are preserved in HPAL. Consider Example 3.1 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 ∧ Ba ¬p. Figure 5 shows that this hedged announcement is not preserved. M
a
¬p w
a
p v
M ÷¬(p∧Ba ¬p)
a
¬p
a
p
w
a
v
a
Figure 5: Alice’s belief update as a contraction on ¬(p ∧ Ba ¬p). The formula p ∧ Ba ¬p is true at v before the update (on the left) but false at v after the update (on the right). Hence, p ∧ Ba ¬p is not preserved. More generally, say ϕ is self-refuting (in the logic L) if ⊨L ϕ → [÷¬ϕ]¬ϕ. Clearly, ϕ is not preserved if it is self-refuting. The above example is a special case of the following result: 7 In PAL, the formula [!ϕ]ψ intuitively says ψ is true after eliminating all ¬ϕ-possibilities from the model; see [20, Chapter
4] and references therein for more on PAL. 8 The proof that (i) implies (ii) 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, suppose Ag = {a}, let ϕ := p ∧ Ba ¬p ∧ ¬Ba ⊥, and consider a Kripke model and a world w in 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 for a at w, a will have inconsistent beliefs at w and believe (trivially) that ϕ is true. Hence, [!ϕ]Ba ϕ is valid. On the other hand, [!ϕ]ϕ is invalid and in particular [!ϕ]¬Ba ⊥ is invalid.
144
Belief Contraction in Dynamic Epistemic Logic
Proposition 5.2. The formulas p ∧ ∃Ba ¬p and p ∧ Ba ¬p are self-refuting in HPAL.9 Proof. Let ϕ := p ∧ ∃Ba ¬p. Suppose M , w ⊨ p ∧ ∃Ba ¬p. Then M ⊨ ∃Ba ¬p and so M ÷¬ϕ = M ÷¬p . Thus M ÷¬ϕ ⊨ ∀Bea p and so M ÷¬ϕ , w ⊨ ¬ϕ. Similarly, let ψ := p ∧ Ba ¬p. Suppose M , w ⊨ ψ. Since ÷¬ψ Ba ¬p ⊨ Ba ¬ψ, M , w ⊨ Ba ¬ψ. So w ∈ Ra (w). Since M , w ⊨ p, M ÷¬ψ , w ⊨ Bea p. Given that Bea p ⊨ ¬ψ, M ÷¬ψ , w ⊨ ¬ψ. So which formulas are preserved? Recall that a formula ϕ is existential if it is built only from literals, ∧, ∨ and Bea ; ϕ is universal if it is built only from literals, ∧, ∨ and Ba . 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 in HPAL to an existential formula, then it is preserved in HPAL. Proof. Suppose ϕ is equivalent in HPAL to an existential formula. Then ϕ is preserved under model extension [4]. Since M ÷¬ϕ extends M , if M , w ⊨ ϕ, then M ÷¬ϕ , w ⊨ ϕ, i.e. M , w ⊨ ϕ → [÷¬ϕ]ϕ. One upshot of Theorem 5.3 is that, while the “strong” Moorean sentence p ∧ Ba ¬p is never preserved, the “weak” Moorean sentence p ∧ ¬Ba 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 formula p ∧ Ba p (agent a has a true belief that p) is preserved. Proposition 5.4. The formula p ∧ Ba p is preserved in HPAL. ÷¬(p∧B p)
a Proof. Let M = (W, R,V ) be a Kripke model with M , w ⊨ p ∧ Ba p. As Ra (w) ⊆ Ra (w) ∪ {v ∈ W : M , v ⊨ p ∧ Ba p} ⊆ {v ∈ W : M , v ⊨ p} and p is preserved, then M ÷¬(p∧Ba p) , w ⊨ p ∧ Ba 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 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 L are preserved. Theorem 5.5. Suppose |Ag| = 1. Then every formula in L is preserved in HPAL extended with S5. Proof sketch. In S5, if M , w ⊨ ϕ with ϕ ∈ L , then every world in the equivalence class of w satisfies Bea ϕ and so contracting on ¬ϕ does not change relations inside those classes. Then, (M , w) and (M ÷¬ϕ , w) are bisimilar, and since L is bisimulation-invariant, ϕ is preserved. Note that model M in Figure 5 validates KD45, 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, representing 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 transformations. 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 contracting by ϕ, by the formula [÷ϕ]Ba χ. The modal version of the AGM axioms for contraction can then be expressed by the following formulas, where ϕ, ψ, χ ∈ L ÷ : 9 Note that the Moorean sentence p ∧ B ¬p is unsatisfiable in S5, while p ∧ ∃B ¬p is satisfiable even if belief is factive. a a 10 As an anonymous referee pointed out, the result does not generalize to the multi-agent setting.
G. Belardinelli & S. Zhang
145
• Closure. [÷ϕ](Ba (ψ → χ) → (Ba ψ → Ba χ)). • Success. ∃¬ϕ → [÷ϕ]¬Ba ϕ. • Inclusion. [÷ϕ]Ba ψ → Ba ψ. • Vacuity. ¬Ba ϕ → (χ ↔ [÷ϕ]χ). • Extensionality. If ⊨ ϕ ↔ ψ then ⊨ [÷ϕ]χ ↔ [÷ψ]χ. • Conjunctive Inclusion. [÷(ϕ ∧ ψ)]¬Ba ϕ → ([÷(ϕ ∧ ψ)]Ba χ → [÷ϕ]Ba χ). • Conjunctive Overlap. ([÷ϕ]Ba χ ∧ [÷ψ]Ba χ) → [÷(ϕ ∧ ψ)]Ba χ. • Consistency. ¬Ba ⊥ → [÷ϕ]¬Ba ⊥. From the list above we omitted the axiom called Recovery (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 called Consistency, which is discussed in [30, 26]. 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 ϕ is successful in PAL if it is believed after it is announced: [!ϕ]Ba ϕ is valid for all a ∈ Ag. A natural analogue of this notion in our contraction settings is that ϕ is not believed after a hedged announcement that it might be false, viz. [÷ϕ]¬Ba ϕ for all a ∈ 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 why Success is given by the conditional ∃¬ϕ → [÷ϕ]¬Ba ϕ. Say that a formula ϕ is successful if it satisfies this property. As with preservation, not all formulas are successful. For instance, the hedged announcement that p ∧ Ba ¬p might 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 ∧ Ba ¬p), Alice will come to believe that she believes neither p nor ¬p, and so she will believe that she doesn’t have a false belief that p (i.e. M ÷¬(p∧Ba ¬p) ⊨ Ba ¬(p ∧ Ba ¬p)). In PAL, if a formula remains true after being announced, then it is believed after the announcement [20, Proposition 4.32]. A similar result holds for HPAL. Proposition 6.1. In HPAL, if ¬ϕ ∈ L ÷ is preserved, then ϕ is successful. Proof. Let M = (W, R,V ) and suppose M , w ⊨ ∃¬ϕ. Assume that ¬ϕ is preserved. We show that M , w ⊨ [÷ϕ]¬Ba ϕ. There are two cases. First, suppose that M , w ⊨ ¬Ba ϕ. Then, there is v ∈ Ra (w) = ÷ϕ Ra (w) such that M , v ⊨ ¬ϕ. As ¬ϕ is preserved, M , v ⊨ [÷ϕ]¬ϕ and so M , w ⊨ [÷ϕ]¬Ba ϕ. Second, ÷ϕ suppose M , w ⊨ Ba ϕ. Since M , w ⊨ ∃¬ϕ, there is a v ∈ W with M , v ⊨ ¬ϕ and v ∈ Ra (w). By preservation of ¬ϕ, M , v ⊨ [÷ϕ]¬ϕ and so M , w ⊨ [÷ϕ]¬Ba ϕ. 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, that Recovery does 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].
146
Belief Contraction in Dynamic Epistemic Logic
Corollary 6.2. If ϕ ∈ L ÷ is equivalent in HPAL to a universal formula, then ϕ is successful in HPAL. Proof. If ϕ is equivalent to a universal formula, ¬ϕ is equivalent to an existential formula. By Theorem 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 that Success is not valid in HPAL. However, by Corollary 6.2, 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 (M , w ⊨ ¬Ba ¬Ba ¬p ∧ [÷¬p]Ba ¬Ba ¬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 K be the class of all Kripke models. Proposition 6.3. The following are valid in HPAL, where χ and λ are propositional and ϕ, ψ ∈ L ÷ : 1. Propositional Inclusion. [÷ϕ]Ba χ → Ba χ. 2. Propositional Conjunctive Inclusion. [÷λ ∧ ψ]¬Ba λ → ([÷λ ∧ ψ]Ba χ → [÷λ ]Ba χ). 3. Propositional Conjunctive Overlap. ([÷ϕ]Ba χ ∧ [÷ψ]Ba χ) → [÷ϕ ∧ ψ]Ba χ. ÷ϕ
Proof sketch. Propositional Inclusion follows from Ra (w) ⊆ Ra (w) and from propositional truth being unaffected by contraction. Propositional Conjunctive Inclusion and Overlap follow because contracting on a conjunction introduces no alternatives beyond those required to give up one of its conjuncts. Finally, while Vacuity is also among the properties that do not hold unrestrictedly, the following strong version holds: V • Strong Vacuity. a∈Ag ∀¬Ba ϕ → (χ ↔ [÷ϕ]χ). 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 [1, 30]. Proposition 6.4. Strong Vacuity is a theorem of HPAL. Proof. Let ϕ, χ ∈ L ÷ and consider a Kripke model M = (W, R,V ) and a world w in it. Assume that ÷ϕ M , w ⊨ ∀¬Ba ϕ, for all a ∈ Ag, i.e., M , u ⊨ ¬Ba ϕ for all u ∈ W and a ∈ Ag. Then Ra (u) = Ra (u) for all worlds u and all agents a, i.e., M = M ÷ϕ and so M , w ⊨ χ iff M ÷ϕ , w ⊨ χ, that is, M , w ⊨ χ iff M , w ⊨ [÷ϕ]χ.
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 LDEL be the language generated by the grammar of the doxastic language L extended with the following clauses ϕ ::= [E , e]ϕ | ∀ϕ, where E is a generalized event model (introduced below) and e is an event in it. The formula [E , e]ϕ reads “after (E , e) happens, ϕ is the case”.
G. Belardinelli & S. Zhang
147
Definition 7.1 (Generalized event model). A generalized event model is a tuple E = (E, Q, Q+ , pre) where E and Qa are defined as in standard event models, Q+ a ⊆ E × E is an accessibility relation between events defined for all agents a ∈ Ag, and pre : E → LDEL is a precondition function. A generalized event model is a standard event model extended with additional accessibility relations Q+ a , for each agent a ∈ Ag, and in which preconditions can be formulas of the dynamic language LDEL . + + As before, we use notation Q+ a (e) = { f ∈ E : (e, f ) ∈ Qa }. Intuitively, both Qa (e) and Qa (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 Qa (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 E in Figure 6, which is the event model corresponding to Example 3.1. 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 Qa ( f ) = Qa (h) = { f , h}, while Q+ a ( f ) = Qa (h) = {h}.
M
a
a
¬p w
p
E
v
¬p f
a+
p
a+ M ⊗E
¬p
a
(w, f )
h
a
p
a
(v, h)
Figure 6: Left: The Kripke model M representing Alice’s initial belief states. Middle: The generalized event model E = (E, Q, Q+ , pre) representing Bob’s announcement to Alice that p might hold. An edge from an event f to an event h labeled by +a means that h ∈ Q+ a ( f ). We omit the Q-edges since Qa (e) = E for all e ∈ E. Right: The Kripke model M ⊗ E = (W E , RE ,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 model M = (W, R,V ) and a generalized event model E = (E, Q, Q+ , pre), their product update M ⊗ E is defined as M ⊗ E = (W E , RE ,V E ) where W E and V E are defined as in standard product updates (cf. Section 2) and RE is given by: (v, f ) ∈ REa (w, e) iff either f ∈ Q+ a (e), or v ∈ Ra (w) and f ∈ Qa (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 ) 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 [20]: M , w ⊨ [E , e]ϕ
iff
if M , w ⊨ pre(e) then M ⊗ E , (w, e) ⊨ ϕ.
The following definition shows that generalized DEL can express contraction as induced by hedged public announcements. Definition 7.3 (Event model for contraction on ϕ). Let ϕ ∈ LDEL . An event model for contraction on ϕ is a generalized event model E (÷ϕ) = (E, Q, Q+ , pre) where 1. E = {ϕ ∧
a∈A ¬Ba ϕ ∧
V
a∈Ag\A Ba ϕ : A ⊆ Ag} ∪ {¬ϕ ∧
V
a∈A ¬Ba ϕ ∧
V
a∈Ag\A Ba ϕ : A ⊆ Ag}.
V
148
Belief Contraction in Dynamic Epistemic Logic
( { f ∈ E : pre( f ) ⊨ ¬ϕ} 2. For all a ∈ Ag and e ∈ E, Qa (e) = E and Q+ a (e) = 0/
if pre(e) ⊨ Ba ϕ; otherwise.
3. For all e ∈ E, pre(e) = e. Event model E (÷ϕ) contains events for all possible configurations of the truth value of ϕ and which agents believe ϕ. The relation Qa is universal, capturing that the announcement reveals nothing about which event occurred. The relation Q+ a captures contraction: agents who believed ϕ come to consider ¬ϕ-events possible, while the others are unaffected. Proposition 7.4. For any Kripke model M and formula ϕ ∈ L , M ÷ϕ is isomorphic to M ⊗ E (÷ϕ). Proof sketch. Both updates preserve all worlds of M , so there is an isomorphism between the updated ÷ϕ models: as Ra (w) ⊆ Ra (w) and Qa (e) = E for all a ∈ Ag, e ∈ E, all relations in M are preserved by both updates. Also, the only relations added in both cases are from Ba ϕ-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 model E as described below: (w, f )
f a a, c M
¬p w
a, c
p v
E
¬p
c
a a+ a p c a+ h
⊤ e
a, c
a M ⊗E
¬p a
a
c
(w, e) a, c ¬p
c
a, c
p
p
(v, h)
(v, e)
Figure 7: Left: The Kripke model M representing Alice and Clark’s initial belief states. We have M ⊨ Ba ¬p ∧ Bc ¬p ∧ Bc Ba ¬p. Middle: The generalized event model E = (E, Q, Q+ , pre) representing Bob’s private announcement to Alice that p might hold. An edge from an event f to an event h labeled by +a means that h ∈ Q+ a ( f ). If an edge’s label does not contain +, then the edge is a Q-relation, e.g. e ∈ Qc ( f ). Right: The Kripke model M ⊗ E = (W E , RE ,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 models E = (E E , QE , Q+E , preE ) and F = (E F , QF , Q+F , preF ), then their composition is E ◦ F = (E, Q, Q+ , pre) where • E = EE × EF ; • (e′ , f ′ ) ∈ Qa ((e, f )) iff e′ ∈ QEa (e) and f ′ ∈ QF a ( f ); ′ +F ′ F ′ +E • (e′ , f ′ ) ∈ Q+ a ((e, f )) iff f ∈ Qa ( f ), or f ∈ Qa ( f ) and e ∈ Qa (e);
• pre((e, f )) = preE (e) ∧ [E , e]preF ( f ).
G. Belardinelli & S. Zhang
149
CL ∀K ∀T ∀5 ∀B BK
all classical propositional tautologies ∀(ϕ → ψ) → (∀ϕ → ∀ψ) ∀ϕ → ϕ ¬∀ϕ → ∀¬∀ϕ ∀ϕ → Ba ϕ Ba (ϕ → ψ) → (Ba ϕ → Ba ψ)
A1 A2 A3 A4 A5 A6
[E , e]p ↔ (pre(e) → p) [E , e]¬ϕ ↔ (pre(e) → ¬[E , e]ϕ) [E , e](ϕ ∧ ψ) ↔ ([E , e]ϕ ∧ [E , e]ψ) V [E , e]∀ϕ ↔ (pre(e) → f ∈E ∀[E , f ]ϕ) V V [E , e]Ba ϕ ↔ (pre(e) → ( f ∈Q+a (e) ∀[E , f ]ϕ ∧ f ∈Qa (e) Ba [E , f ]ϕ)) [E , e][F , f ]ϕ ↔ [E ◦ F , (e, f )]ϕ MP and necessitation rules for all modalities
Table 2: The Theory GDEL 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 by GDEL. 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 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 Qa 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 [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 model M and generalized event model E , M ⊗ E is a simulation of a refinement of M . Proof sketch. The idea is to split a generalized update into two steps. First ignore the Q+ a edges and obtain a standard DEL update, 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 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.
150
Belief 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’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 N in Figure 8. z
u a, c M
pq
c
a, c
¬pq
p¬q
a, c
c
¬p¬q
a, c
c
pq
a, c N
c
c
z
u
a, c
c a
a c a, c
p¬q
c
¬pq
¬p¬q
a, c
w w v v Figure 8: Left: The Kripke model M representing Alice and Clark’s initial belief states. We have M ⊨ Bc (Ba p ∨ Ba ¬p) ∧ Bc (Ba q ∨ Ba ¬q). Right: The Kripke model N representing Alice and Clark’s belief states after Bob’s hedged announcement, where N , w ⊨ ¬Bc (Ba p ∨ Ba ¬p) ∧ Bc (Ba q ∨ Ba ¬q). Proposition 7.10. There is no formula ϕ ∈ L ÷ such that M ÷ϕ ≡ N . Proof. Suppose towards a contradiction that M ÷ϕ ≡ N for some ϕ ∈ L ÷ . Since every world in M satisfies a distinct set of propositional formulas and contraction preserves propositional valuation, it ÷ϕ follows that for all x ∈ W , (M ÷ϕ , x) ≡ (N , x). Since u ̸∈ Ra (w) but u ∈ Ra (w), we have M , w ⊨ Ba ϕ and M , u ⊨ ¬ϕ. Similarly, M , v ⊨ Ba ϕ and M , z ⊨ ¬ϕ. By the definition of contraction, {x ∈ W : M , x ⊨ ÷ϕ ÷ϕ ¬ϕ} ⊆ Ra (w). So z ∈ Ra (w). So M ÷ϕ , w ⊨ ¬Ba q. Since N , w ⊨ Ba q, this contradicts the assumption that (M ÷ϕ , w) and (N , w) are modally equivalent. 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 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+ / (iii) if a (e) = Qa (g) = 0) Alice believes ¬p, then Bob’s announcement makes her consider p possible without revising her beliefs + about q (Q+ a ( f ) = {e} and Qa (h) = {g}). It’s not hard to check that M ⊗ E = N . f
e pq
a+
¬pq
g p¬q
h a+
¬p¬q
Figure 9: The generalized event model E = (E, Q, Q+ , pre) representing Bob’s announcement to Alice and Clark. As before, we omit the Q-edges, since Qi (x) = E for all events x ∈ E and agents i ∈ {a, c}. Each event’s precondition is given by the conjunction of the literals listed inside the event. So for example event e has precondition p ∧ q.
G. Belardinelli & S. Zhang
8
151
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 [25], 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 [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 model K = (W, R,V ) into any Kripke model K ′ = (W ′ , R′ ,V ′ ) with W = W ′ and V = V ′ by adding the edges in K ′ without keeping any edges in K .14 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. 425500020B).
A
Proofs
Throughout, by logical equivalence we mean provable in K. We let JϕK = {w ∈ W : M , w ⊨ ϕ}, and JϕK÷ψ = {w ∈ W ÷ψ : M ÷ψ , w ⊨ ϕ}. Definition A.1 (Bisimulation, refinement, simulation). Let M = (W, R,V ) and M ′ = (W ′ , R′ ,V ′ ) be two Kripke models. A bisimulation between M and M ′ is a non-empty relation Z ⊆ W × W ′ such that for all (w, w′ ) ∈ Z and a ∈ Ag: (Atom): w ∈ V (p) iff w′ ∈ V ′ (p), for all p ∈ At; 14 Recall that K
= (W, R,V ) is distinguished if for every world w there is a unique formula ϕ such that M , w ⊨ ϕ. The simulation strategy is similar to the strategy used in [21] 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.
152
Belief Contraction in Dynamic Epistemic Logic (Forth): If v ∈ Ra (w) then there exists v′ ∈ W ′ such that v′ ∈ R′a (w′ ) and (v, v′ ) ∈ Z; (Back): If v′ ∈ R′a (w′ ) then there exists v ∈ W such that v ∈ Ra (w) and (v, v′ ) ∈ Z;
When a bisimulation exists between two models, we say that they are bisimilar. A relation that satisfies Atom and Back is a refinement. When a refinement exists between M and M ′ , we say that M ′ is a refinement of M . A relation that satisfies Atom and Forth is a simulation. When a simulation exists between M and M ′ , we say that M ′ is a simulation of M . Proof of Theorem 4.2. For soundness, the only non-trivial axiom is A5, namely [÷ϕ]Ba ψ ↔ (Ba [÷ϕ]ψ ∧ (Ba ϕ → ∀(¬ϕ → [÷ϕ]ψ))). Suppose M , w ⊨ [÷ϕ]Ba ψ. We claim that M , w ⊨ Ba [÷ϕ]ψ. Let v ∈ ÷ϕ Ra (w). Then v ∈ Ra (w). By assumption, M ÷ϕ , w ⊨ Ba ψ. So M ÷ϕ , v ⊨ ψ. Thus M , v ⊨ [÷ϕ]ψ. So M , w ⊨ Ba [÷ϕ]ψ. Next, we claim that, if M , w ⊨ Ba ϕ and M , w ⊨ [÷ϕ]Ba ψ, then for every v ∈ W , M , v ⊨ ¬ϕ → [÷ϕ]ψ. Let v ∈ W . Suppose M , v ⊨ ¬ϕ. Since M , w ⊨ Ba ϕ, v ∈ R÷ϕ (w). Since M , w ⊨ [÷ϕ]Ba ψ, M ÷ϕ , v ⊨ ψ. So M , v ⊨ [÷ϕ]ψ. Conversely, suppose M , w ⊨ Ba [÷ϕ]ψ ∧ (Ba ϕ → ∀(¬ϕ → [÷ϕ]ψ)). There are two cases, either M , w ⊨ ¬Ba ϕ or M , w ⊨ Ba ϕ. Suppose M , w ⊨ ¬Ba ϕ. Let v ∈ R÷ϕ (w). Then v ∈ Ra (w). Since M , w ⊨ Ba [÷ϕ]ψ, we have M , v ⊨ [÷ϕ]ψ. So M ÷ϕ , v ⊨ ψ. Thus M , w ⊨ [÷ϕ]Ba ψ. Now suppose M , w ⊨ Ba ϕ. So M , w ⊨ ∀(¬ϕ → [÷ϕ]ψ). Let v ∈ R÷ϕ (w). Either v ∈ Ra (w) or M , v ⊨ ¬ϕ. In the first case, by the assumption that M , w ⊨ Ba [÷ϕ]ψ, we have M ÷ϕ , v ⊨ ψ. In the second case, since M , w ⊨ ∀(¬ϕ → [÷ϕ]ψ), we have M , v ⊨ [÷ϕ]ψ or equivalently M ÷ϕ , v ⊨ ψ. So M , w ⊨ [÷ϕ]Ba ψ. We now show that RE is validity preserving. Suppose ⊨ ϕ ↔ ψ. We proceed by induction on the complexity of the environment χ. If χ is a propositional variable p ∈ 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 ⊨ Ba χ[ϕ/p]
iff iff iff
for all v ∈ Ra (w) M , v ⊨ χ[ϕ/p] for all v ∈ Ra (w) M , v ⊨ χ[ψ/p] M , w ⊨ Ba χ[ψ/p]
A similar argument shows that ⊨ ∀χ[ϕ/p] ↔ ∀χ[ψ/p]. Let λ ∈ L ÷ . Then M , w ⊨ [÷λ ]χ[ϕ/p]
iff iff iff
M ÷λ , w ⊨ χ[ϕ/p] M ÷λ , w ⊨ χ[ψ/p] M , w ⊨ [÷λ ]χ[ψ/p]
Lastly, for any Kripke model M = (W, R,V ), we claim that M ÷χ[ϕ/p] = M ÷χ[ψ/p] . It suffices to ÷χ[ϕ/p] ÷χ[ψ/p] (w) = Ra (w) for all w ∈ W and a ∈ Ag. Suppose M , w ⊨ ¬Ba χ[ϕ/p]. Then show that Ra ÷χ[ϕ/p] ÷χ[ψ/p] (w). Suppose by the inductive hypothesis, M , w ⊨ ¬Ba χ[ψ/p] and so Ra (w) = Ra (w) = Ra M , w ⊨ Ba χ[ϕ/p]. Then by IH, M , w ⊨ Ba χ[ψ/p] and ÷χ[ϕ/p]
Ra
(w)
= = =
Ra (w) ∪ {v ∈ W : M , v ⊨ ¬χ[ϕ/p]} Ra (w) ∪ {v ∈ W : M , v ⊨ ¬χ[ψ/p]} ÷χ[ψ/p] Ra (w)
So M ÷χ[ϕ/p] = M ÷χ[ψ/p] . Thus, for any Kripke model M and world w,
G. Belardinelli & S. Zhang
153 M , w ⊨ [÷χ[ϕ/p]]λ
iff iff iff
M ÷χ[ϕ/p] , w ⊨ λ M ÷χ[ψ/p] , w ⊨ λ M , w ⊨ [÷χ[ψ/p]]λ
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. □ Proof of Theorem 5.5. Suppose Ag = {a}. Let ϕ ∈ L . Let M = (W, R,V ) be a Kripke model that validates S5. Suppose M , w ⊨ ϕ. Since Ra is an equivalence relation, for all v ∈ Ra (w), M , v ⊨ Bea ϕ. ÷¬ϕ Then Ra (v) = Ra (v) for all v ∈ Ra (w). Consider Z = {(v, v) : v ∈ Ra (w)}. We claim that Z is a bisimulation between (M , w) and (M ÷¬ϕ , w). Clearly the two worlds satisfy the same proposition atoms. Let (v, v) ∈ Z. Then v ∈ Ra (w). Suppose u ∈ Ra (v). Since Ra is an equivalence relation, we ÷¬ϕ ÷¬ϕ have u ∈ Ra (w) and so (u, u) ∈ Z. Moreover, since Ra (v) = Ra (w) = Ra (w) = Ra (v), we have u ∈ ÷¬ϕ ÷¬ϕ ÷¬ϕ Ra (v). Similarly, suppose u ∈ Ra (v). Then u ∈ Ra (w) = Ra (w) = Ra (v). So Z is 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 world w in it. Notationally, let M ÷ϕ = (W ÷ϕ , R÷ϕ ,V ÷ϕ ), JψK = {w ∈ W : M , w ⊨ ψ} and JψK÷ϕ = {w ∈ W : M ÷ϕ , w ⊨ ψ}. ÷ϕ
1. Propositional Inclusion: Assume that M , w ⊨ [÷ϕ]Ba χ. Then M ÷ϕ , w ⊨ Ba χ. So Ra (w) ⊆ ÷ϕ JχK÷ϕ . By definition of contraction Ra (w) ⊆ Ra (w) ⊆ JχK÷ϕ . As χ is propositional, JχK = ÷ϕ JχK . Hence, M , w ⊨ Ba χ. 2. Propositional Conjunctive Inclusion: Suppose M , w ⊨ [÷λ ∧ ψ]¬Ba λ and M , w ⊨ [÷λ ∧ ψ]Ba χ. There are two cases: either M , w ⊨ ¬Ba (λ ∧ ψ) or M , w ⊨ Ba (λ ∧ ψ). Suppose the first. Then ÷λ ∧ψ ÷λ ∧ψ Ra (w) = Ra (w). Since M , w ⊨ [÷λ ∧ ψ]¬Ba λ , there exists v ∈ Ra (w) with M ÷λ ∧ψ , v ⊨ ÷λ ∧ψ ¬λ . As λ is propositional, then M , v ⊨ ¬λ , and since Ra (w) = Ra (w) then M , w ⊨ ¬Ba λ . So ÷λ ∧ψ ÷λ ÷λ Ra (w) = Ra (w). Hence, Ra (w) = Ra (w). So M , w ⊨ [÷λ ∧ ψ]Ba χ implies R÷λ a (w) = ÷λ ∧ψ ÷λ ∧ψ ÷λ Ra (w) ⊆ JχK = JχK , where the last identity holds as χ is propositional. Hence, M , w ⊨ [÷λ ]Ba χ. Now suppose the second case holds. Then M , w ⊨ Ba λ , and so R÷λ a (w) = ÷(λ ∧ψ) Ra (w) ∪ J¬λ K ⊆ Ra (w) ∪ J¬λ ∨ ¬ψK = Ra (w). As by assumption M , w ⊨ [÷λ ∧ ψ]Ba χ, ÷(λ ∧ψ) ÷(λ ∧ψ) ÷λ ÷λ and so M , w ⊨ [÷λ ]B χ. then Ra (w) ⊆ JχK = JχK . Hence, R÷λ a a (w) ⊆ JχK ÷ϕ
3. Propositional Conjunctive Overlap. Suppose that M , w ⊨ [÷ϕ]Ba χ ∧ [÷ψ]Ba χ. Then Ra (w) ⊆ ÷ψ ÷ϕ JχK÷ϕ and Ra (w) ⊆ JχK÷ψ . As χ is propositional, JχK÷ϕ = JχK÷ψ = JχK÷ϕ∧ψ , and so (Ra (w)∪ ÷ψ Ra (w)) ⊆ JχK÷ϕ∧ψ . Two cases: either M , w ⊨ Ba (ϕ ∧ ψ) or not. If the first, then M , w ⊨ Ba ϕ ÷ϕ ÷ψ ÷ϕ∧ψ and M , w ⊨ Ba ψ. So Ra (w) = Ra (w) ∪ J¬ϕK and Ra (w) = Ra (w) ∪ J¬ψK and Ra (w) = ÷ϕ ÷ψ ÷ϕ∧ψ Ra (w) ∪ J¬ϕ ∨ ¬ψK = Ra (w) ∪ J¬ϕK ∪ J¬ψK. Then, Ra (w) = Ra (w) ∪ Ra (w), and so ÷ϕ∧ψ (w) ⊆ JχK÷ϕ∧ψ . Hence, M , w ⊨ [÷ϕ ∧ ψ]Ba χ. Suppose instead that M , w ⊨ ¬Ba (ϕ ∧ ψ). Ra ÷ϕ∧ψ ÷ϕ (w) = Ra (w), and since by initial assumption Ra (w) ⊆ JχK÷ϕ∧ψ and by definition Then, Ra ÷ϕ of contraction Ra (w) ⊆ Ra (w), then Ra (w) ⊆ JχK÷ϕ∧ψ . Hence, M , w ⊨ [÷ϕ ∧ ψ]Ba χ. □ Proof of Proposition 7.4. Let M = (W, R,V ) be a Kripke model. Notationally, we let E (÷ϕ) = (E, Q, Q+ , pre), M ⊗ E (÷ϕ) = (W E (÷ϕ) , RE (÷ϕ) ,V E (÷ϕ) ) and M ÷ϕ = (W ÷ϕ , R÷ϕ ,V ÷ϕ ). The function h : W E (÷ϕ) → W ÷ϕ , defined by h((w, e)) = w, for all w ∈ W , is a bijection: first, notice that, by
154
Belief Contraction in Dynamic Epistemic Logic
definition of E (÷ϕ), for each world w ∈ W there is exactly one event e ∈ E such that M , w ⊨ pre(e), and so (w, e) ∈ W E (÷ϕ) iff w ∈ W . Then notice that, by definition of ÷ϕ-update, W ÷ϕ = W , and so (w, e) ∈ W E (÷ϕ) iff w ∈ W ÷ϕ . We now show that h preserves atomic valuations and accessibility relations. The atomic valuations are clearly preserved, as V E (÷ϕ) (p) = V (p) = V ÷ϕ (p) for all p ∈ At. For E (÷ϕ) the accessibility relations, let a ∈ Ag and (w, e) ∈ W E (÷ϕ) . We want to show that (v, f ) ∈ Ra (w, e) iff ÷ϕ v ∈ Ra (w). We consider two cases: either M , w ̸⊨ Ba ϕ, or M , w ⊨ Ba ϕ. Suppose M , w ̸⊨ Ba ϕ. Then ÷ϕ E (÷ϕ) is such that Qa (e) = E and Q+ / and M ÷ϕ is such that Ra (w) = Ra (w). So we have that a (e) = 0, E (÷ϕ) (v, f ) ∈ Ra (w, e) iff (by definition of generalized product update) v ∈ Ra (w) iff (by definition of ÷ϕE (÷ϕ) ÷ϕ update) v ∈ Ra (w), as we wanted to show. Suppose instead M , w ⊨ Ba ϕ. Assume (v, f ) ∈ Ra (w, e). ÷ϕ + Then either v ∈ Ra (w) and f ∈ Qa (e), or f ∈ Qa (e). If v ∈ Ra (w), then v ∈ Ra (w), as desired. If instead ÷ϕ ÷ϕ f ∈ Q+ a (e), then M , v ⊨ ¬ϕ and so v ∈ Ra (w), as desired. For the other direction, assume v ∈ Ra (w). E (÷ϕ) Then either v ∈ Ra (w) or M , v ⊨ ¬ϕ. If v ∈ Ra (w), then since Qa (e) = E, (v, f ) ∈ Ra (w, e). If inE (÷ϕ) stead M , v ⊨ ¬ϕ, then by (v, f ) ∈ W , pre( f ) ⊨ ¬ϕ by definition of E (÷ϕ). Since M , w ⊨ Ba ϕ then E (÷ϕ) Q+ (e) = {g ∈ E : pre(g) ⊨ ¬ϕ}, and so (v, f ) ∈ Ra (w, e). Hence in all cases we have the desired. □ a 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 M = (W, R,V ) be a Kripke model, let E = (E, Q, Q+ , pre) be a generalized event model, and let M ⊗ E = (W E , RE ,V E ). • A4: Note that, if M , w ̸⊨ pre(e), then the biconditional holds automatically at (M , w). Suppose M , w ⊨ pre(e) and M , w ⊨ [E , e]∀ϕ. Then M ⊗ E , (w, e) ⊨ ∀ϕ, i.e. for all (v, f ) ∈ W E , M ⊗ E , (v, f ) ⊨ ϕ. In other words, for all f ∈ E and v ∈ W such that M , v ⊨ pre( f ), M , v ⊨ [E , f ]ϕ. So V M , w ⊨ f ∈E ∀[E , f ]ϕ. Conversely, suppose M , w ⊨ pre(e) but M , w ⊨ ¬[E , e]∀ϕ, i.e. M ⊗ E , (w, e) ̸⊨ ∀ϕ. So there is (v, f ) ∈ W E such that M ⊗ E , (v, f ) ̸⊨ ϕ. It follows that M , v ⊨ ¬[E , f ]ϕ and so M , w ⊨ V ¬ f ∈E ∀[E , f ]ϕ. • A5: Suppose M , w ⊨ [E , e]Ba ϕ ∧ pre(e). Let f ∈ Q+ M , v ⊨ pre( f ), we a (e). Then for any v ∈ W , if V have (v, f ) ∈ REa ((w, e)) and so by assumption M E , (v, f ) ⊨ ϕ. Thus M , w ⊨ f ∈Q+a (e) ∀[E , f ]ϕ. Let f ∈ Qa (e) and v ∈ Ra (w). Then (v, f ) ∈ REa ((w, e)) and so M E , (v, f ) ⊨ ϕ. Thus M , v ⊨ [E , f ]ϕ. V So M , w ⊨ f ∈Qa (e) Ba [E , f ]ϕ. Conversely, suppose M , w ⊨ pre(e) → f ∈Q+a (e) ∀[E , f ]ϕ ∧ f ∈Qa (e) Ba [E , f ]ϕ and let (v, f ) ∈ REa ((w, e)). Either f ∈ Q+ a (e) or f ∈ Qa (e) and v ∈ Ra (w). In the first case, since M , w ⊨ ∀[E , f ]ϕ, we have M , v ⊨ [E , f ]ϕ. In the second case, since M , w ⊨ Ba [E , f ]ϕ, we have M , v ⊨ [E , f ]ϕ. So either way, M E , (v, f ) ⊨ ϕ and so M E , (w, e) ⊨ Ba ϕ. V
V
• A6: The proof mainly requires showing that there exists an isomorphism between (M ⊗ E ) ⊗ F = (W E F , RE F ,V E F ) and M ⊗ (E ◦ F ) = (W E ◦F , RE ◦F ,V E ◦F ). By invariance of truth under isomorphism, this will imply the desired. We use notation M ⊗ E = (W E , RE ,V E ), and E = (E E , QE , Q+E , preE ) and F = (E F , QF , Q+F , preF ). To show the existence of the isomorphism, let h : W E F → W E ◦F be defined by h((w, e), f ) = (w, (e, f )). Clearly, h is a bijection: ((w, e), f ) ∈ W E F iff M , w |= preE (e) and M ⊗E , (w, e) |= preF ( f ), iff M , w |= preE (e) ∧ [E , e]preF ( f ), iff (w, (e, f )) ∈ W E ◦F . It also preserves valuations, since for every atom p ∈ At, ((w, e), f ) ∈ V E F (p) iff w ∈ V (p) iff (w, (e, f )) ∈ V E ◦F (p). Finally, h preserves accessibility relations. Let ((w′ , e′ ), f ′ ) ∈ REa F (((w, e), f )). We want to show that (w′ , (e′ , f ′ )) ∈ RaE ◦F ((w, (e, f ))). Let ((w′ , e′ ), f ′ ) ∈ REa F (((w, e), f )). Two cases: either f ′ ∈
G. Belardinelli & S. Zhang
155
′ ′ +E ◦F (e, f ) and ′ +F ′ F ′ ′ E Q+F a ( f ) or (w , e ) ∈ Ra ((w, e)) and f ∈ Qa ( f ). If f ∈ Qa ( f ) then (e , f ) ∈ Qa ′ F ′ ′ E ′ ′ ′ E ◦F so (w , (e , f )) ∈ Ra ((w, (e, f ))). If (w , e ) ∈ Ra ((w, e)) and f ∈ Qa ( f ), then again two cases, ′ F ′ +E ′ ′ E either e′ ∈ Q+E a (e), or w ∈ Ra (w) and e ∈ Qa (e). If e ∈ Qa (e) then by f ∈ Qa ( f ) and defini′ ′ ′ E ◦F ′ ′ +E ◦F ((e, f )), which implies (w , (e , f )) ∈ Ra ((w, (e, f ))). If tion of composition, (e , f ) ∈ Qa ′ ′ E ′ ′ ′ w ∈ Ra (w) and e ∈ Qa (e), then by f ∈ QF a ( f ) and definition of composition we have (e , f ) ∈ E ◦F ′ ′ ′ E ◦F Qa ((e, f )), and so (w , (e , f )) ∈ Ra ((w, (e, f ))). Hence, in all cases the desired holds. The other direction (that is, if (w′ , (e′ , f ′ )) ∈ REa ◦F ((w, (e, f ))) then ((w′ , e′ ), f ′ ) ∈ REa F ((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 ) ∈ W E F and every ϕ ∈ LDEL , 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. Let w ∈ W . If M , w ̸⊨ preE (e), then both [E , e][F , f ]ϕ and [E ◦ F , (e, f )]ϕ are true at w vacuously, since preE ◦F (e, f ) = preE (e) ∧ [E , e]preF ( f ). If M , w ⊨ preE (e) but M ⊗ E , (w, e) ̸⊨ preF ( f ), then again [E , e][F , f ]ϕ is true at w vacuously, and so is [E ◦ F , (e, f )]ϕ, since M , w ̸⊨ preE ◦F (e, f ). Finally, if M , w ⊨ preE (e) and M ⊗ E , (w, e) ⊨ preF ( 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 ]ϕ iff M , w ⊨ [E ◦ F , (e, f )]ϕ. Since 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. □ Proof of Theorem 7.8. Let M = (W, R,V ) be a Kripke model and E = (E, Q, Q+ , pre) be a generalized event model. Notationally, let M ⊗ E = (W E , RE ,V E ). Our proof strategy is to define a submodel of M ⊗ E that serves as the intermediate refinement step, and then show that M ⊗ E is a simulation of that − − − − − model. Let (W E , RE ,V E ) be a Kripke model such that W E = W E , REa (w, e) = {(v, f ) ∈ W E : v ∈ − Ra (w), f ∈ Qa (e)}, for all a ∈ Ag, and V E = V E . This is a submodel of M ⊗ E , only missing the edges between worlds that the Q+ relation added. It is then clear that we recover the full RE by taking the union − − of RE with the set containing those edges, that is REa (w, e) = REa (w, e) ∪ {(v, f ) ∈ W E : f ∈ Q+ a (e)}, − − E E E E for all a ∈ Ag and (w, e) ∈ W . Now, (W , R ,V ) is a standard DEL update, and it is a well known result that it is a refinement of M [15]. We now show that M ⊗ E is a simulation of M ⊗ E − , from − which we can conclude that M ⊗ E is a simulation of a refinement of M . Let Z ⊆ W E ×W E be such − that ((w, e), (w, e)) ∈ Z. As RE only adds edges to RE without removing any, it clearly holds that if − (v, f ) ∈ REa (w, e), then (v, f ) ∈ REa (w, e), and since ((v, f ), (v, f )) ∈ Z then Z is 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 Logic 50(2), pp. 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, pp. 277–288, doi:10.1007/978-3-319-03680-9_30.
156
Belief 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. Synthese 194(7), pp. 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 logic 27(3), pp. 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 Science 231, pp. 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 Announcements 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, pp. 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, Stanford University. Available at https://plato.stanford.edu/archives/win2016/entries/ dynamic-epistemic/. [8] Alexandru Baltag & Sonja Smets (2008): A Qualitative Theory of Dynamic Interactive Belief Revision. In Giacomo Bonanno, Wiebe van der Hoek & Michael Wooldridge, editors: Logic and the Foundations of Game and Decision Theory (LOFT7), Texts in Logic and Games 3, Amsterdam University Press, pp. 13–60. Available at https://www.jstor.org/stable/j.ctt46mz4h.4. [9] Johan van Benthem (2007): Dynamic logic for belief revision. Journal of applied non-classical logics 17(2), pp. 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 IGPL 31(6), pp. 1135–1152, doi:10.1093/jigpal/jzac064. [11] Johan van Benthem & Fernando R. Velázquez-Quesada (2010): The dynamics of awareness. Synthese 177, pp. 5–27, doi:10.1007/s11229-010-9764-9. [12] Johan van Benthem and (2007): Dynamic logic for belief revision. Journal of Applied NonClassical Logics 17(2), pp. 129–155, doi:10.3166/jancl.17.129-155. [13] Matthew A. Benton & Peter Van Elswyk (2020): Hedged Assertion. In Sanford Goldberg, editor: The Oxford Handbook of Assertion, Oxford University Press, pp. 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 Science 53, Cambridge University Press, Cambridge, UK, doi:10.1017/CBO9781107050884. [15] Laura Bozzelli, Hans van Ditmarsch, Tim French, James Hales & Sophie Pinchinat (2014): Refinement modal logic. Information and Computation 239, pp. 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 Logics 21(3-4), pp. 375–395, doi:10.3166/jancl.21.375-395.
G. Belardinelli & S. Zhang
157
[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, pp. 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 Science 437, p. 379–398, doi:10.4204/eptcs.437.30. [19] Hans van Ditmarsch, Andreas Herzig, Jérôme Lang & Pierre Marquis (2009): Introspective forgetting. Synthese 169(2), pp. 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), pp. 87–117. Available at https://www.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 IGPL 23(6), pp. 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 at https://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, pp. 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, Stanford University. Available at https://plato.stanford.edu/archives/spr2022/entries/ logic-belief-revision/. [26] Andreas Herzig (2017): Dynamic Epistemic Logics: Promises, Problems, Shortcomings, and Perspectives. Journal of Applied Non-Classical Logics 27(3-4), pp. 328–341, doi:10.1080/11663081.2017.1416036. [27] Wesley H. Holliday & Thomas F. Icard III (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? Synthese 155(2), pp. 167–190, doi:10.1007/s11229-006-9143-8. [29] Jan Plaza (2007): Logics of public communications. doi:10.1007/s11229-007-9168-7.
Synthese 158(2), pp. 165–179,
[30] Krister Segerberg (1999): Two Traditions in the Logic of Belief: Bringing them Together, pp. 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. Synthese 190(Suppl 1), pp. 103–134, doi:10.1007/s11229-012-0233-5. [32] Seth Yalcin (2007): Epistemic modals. Mind 116(464), pp. 983–1026, doi:10.1093/mind/fzm983.