Paper deep dive
The logic of KM belief update is contained in the logic of AGM belief revision
Giacomo Bonanno
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 92%
Last extracted: 7/20/2026, 8:53:09 AM
Summary
The paper establishes that the logic of Katsuno-Mendelzon (KM) belief update is contained within the logic of Alchourrón-Gärdenfors-Makinson (AGM) belief revision. By translating both sets of axioms into a modal logic with belief, conditional, and necessity operators, the author demonstrates that every KM axiom is a theorem of the AGM logic. This implies AGM belief revision can be viewed as a special case or strengthening of KM belief update, with the difference narrowing to a single axiom concerning unsurprising information in the strong version of KM update.
Entities (11)
Relation Signals (8)
L_AGM → contains → L_KM
confidence 95% · show that the latter contains the former... every axiom of L_KM is a theorem of L_AGM
KM belief update → introducedby → Katsuno and Mendelzon
confidence 95% · notion of belief update introduced by Katsuno and Mendelzon (KM)
AGM belief revision → introducedby → Alchourrón, Gärdenfors and Makinson
confidence 95% · notion of belief revision introduced by Alchourrón, Gärdenfors and Makinson (AGM)
AGM belief revision → isspecialcaseof → KM belief update
confidence 90% · Thus AGM belief revision can be seen as a special case of KM belief update.
L_AGM → usesoperator → B
confidence 90% · modal logic containing three modal operators: a unimodal belief operator B
L_AGM → usesoperator → >
confidence 90% · a bimodal conditional operator >
L_AGM → usesoperator → square
confidence 90% · the unimodal necessity operator □
belief update → modeledby → Kripke-Lewis semantics
confidence 85% · semantically, their notion of belief update corresponds to... Kripke-Lewis semantics
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:For each axiom of KM belief update we provide a corresponding axiom in a modal logic containing three modal operators: a unimodal belief operator $B$, a bimodal conditional operator $>$ and the unimodal necessity operator $\square$. We then compare the resulting logic to the similar logic obtained from converting the AGM axioms of belief revision into modal axioms and show that the latter contains the former. Denoting the latter by $\mathcal L_{AGM}$ and the former by $\mathcal L_{KM}$ we show that every axiom of $\mathcal L_{KM}$ is a theorem of $\mathcal L_{AGM}$. Thus AGM belief revision can be seen as a special case of KM belief update. For the strong version of KM belief update we show that the difference between $\mathcal L_{KM}$ and $\mathcal L_{AGM}$ can be narrowed down to a single axiom, which deals exclusively with unsurprising information, that is, with formulas that were not initially disbelieved.
Tags
Links
- Source: https://arxiv.org/abs/2602.23302v2
- Canonical: https://arxiv.org/abs/2602.23302v2
Trouble viewing inline? Open PDF directly →
Full Text
104,722 characters extracted from source content.
Expand or collapse full text
The logic of KM belief update is contained in the logic of AGM belief revision Giacomo Bonanno University of California, Davis, USA gfbonanno@ucdavis.edu Abstract For each axiom of KM belief update we provide a corresponding axiom in a modal logic containing three modal operators: a unimodal belief operator B, a bimodal conditional operator >> and the unimodal necessity operator □ . We then compare the resulting logic to the similar logic obtained from converting the AGM axioms of belief revision into modal axioms and show that the latter contains the former. Denoting the latter by ℒAGML_AGM and the former by ℒKML_KM we show that every axiom of ℒKML_KM is a theorem of ℒAGML_AGM. Thus AGM belief revision can be seen as a special case of KM belief update. For the strong version of KM belief update we show that the difference between ℒKML_KM and ℒAGML_AGM can be narrowed down to a single axiom, which deals exclusively with unsurprising information, that is, with formulas that were not initially disbelieved. Keywords: belief update, belief revision, conditional, Kripke relation, Lewis selection function. 1 Introduction In [4] every AGM axiom for belief revision ([1]) was translated into a corresponding axiom in a logic containing three modal operators: a unimodal belief operator B, a bimodal conditional operator >> and the unimodal necessity (or global) operator □ . The interpretation of BϕBφ is "the agent believes ϕφ", the interpretation of ϕ>ψφ>ψ is "if ϕφ is (or were) the case then ψ is (or would be) the case" and the interpretation of □ϕ φ is "ϕφ is necessarily true". Letting K be the initial belief set, the fact that ψ∈K∗ϕψ∈ K φ, that is, that ψ belongs to the revised belief set K∗ϕK φ prompted by the informational input ϕφ, is expressed in [4] by the formula B(ϕ>ψ)B(φ>ψ) (the agent believes that if ϕφ were the case then ψ would be the case). For example, in [4] AGM axiom (K∗2)(K 2) (ϕ∈K∗ϕφ∈ K φ) is translated into the modal axiom B(ϕ>ϕ)B(φ>φ) and AGM axiom (K∗4)(K 4) (if ¬ϕ∉K φ∉ K then K+ϕ⊆K∗ϕK+φ K φ) is translated into the modal axiom (¬B¬ϕ∧B(ϕ→ψ))→B(ϕ>ψ) ( B φ B(φ→ψ) )\,→\,B(φ>ψ). The translation was done by means of the Kripke-Lewis semantics put forward in [3]: for every AGM axiom a characterizing property of Kripke-Lewis frames was obtained, which was then shown to characterize a corresponding modal-logic axiom. In this paper we extend the analysis to the notion of belief update introduced by Katsuno and Mendelzon (KM) in [7] by providing, for every KM axiom, a corresponding modal axiom. We then show that the modal logic – denoted by ℒAGML_AGM – obtained by adding the modal AGM axioms to the basic logic, contains the logic – denoted by ℒKML_KM – obtained by adding the modal KM axioms to the basic logic, in the sense that every axiom of ℒKML_KM is a theorem of logic ℒAGML_AGM. Thus we confirm the conclusion reached in [10] – for the case of the strong version of KM update – and reinforced in [3], that the notion of AGM belief revision can be viewed as a strengthening of the notion of KM belief update. This conclusion becomes even more conspicuous when comparing the logic of AGM belief revision to the logic of the strong version of KM belief update: in this case the difference between the two notions reduces to a single axiom which deals with an item of information ϕφ that is not surprising, in the sense that it is not the case that, initially, the agent believed ¬ϕ φ. The paper is structured as follows. In Section 2 we review the KM theory of belief update and characterize each KM axiom in terms of a property of the Kripke-Lewis frames introduced in [3]. In Section 3 we review the modal logic ℒL with the three modal operators B, >> and □ described above and provide a modal axiom corresponding to each of the frame properties given in Section 2. In Section 4 we recall the modal axiomatization of AGM belief revision introduced in [4] and compare it to the logic of belief update given in Section 3. Section 5 concludes. All the proofs are given in the Appendix. 2 The KM theory of belief update We consider a propositional logic based on a countable set At of atomic formulas. We denote by Φ0 _0 the set of Boolean formulas constructed from At as follows: At⊂Φ0 At⊂ _0 and if ϕ,ψ∈Φ0φ,ψ∈ _0 then ¬ϕ φ and ϕ∨ψφ ψ belong to Φ0 _0. Define ϕ→ψφ→ψ, ϕ∧ψφ ψ, and ϕ↔ψφ ψ in terms of ¬ and ∨ in the usual way (e.g. ϕ→ψφ→ψ is a shorthand for ¬ϕ∨ψ φ ψ); furthermore, ⊤ denotes a tautology and ⊥ a contradiction. Given a subset K of Φ0 _0, its deductive closure Cn(K)⊆Φ0Cn(K) _0 is defined as follows: ψ∈Cn(K)ψ∈ Cn(K) if and only if there exist ϕ1,…,ϕn∈K _1,..., _n∈ K (with n≥0n≥ 0) such that (ϕ1∧…∧ϕn)→ψ( _1 ... _n)→ψ is a tautology. A set K⊆Φ0K _0 is consistent if Cn(K)≠Φ0Cn(K)≠ _0; it is deductively closed if K=Cn(K)K=Cn(K). Given a set K⊆Φ0K _0 and a formula ϕ∈Φ0φ∈ _0, the expansion of K by ϕφ, denoted by K+ϕK+φ, is defined as follows: K+ϕ=Cn(K∪ϕ)K+φ=Cn (K∪\φ\ ). Let K⊆Φ0K _0 be a consistent and deductively closed set representing the agent’s initial beliefs and let Ψ⊆Φ0 _0 be a set of formulas representing possible informational inputs. A belief change function based on Ψ and K is a function ∘:Ψ→2Φ0 : → 2 _0 (2Φ02 _0 denotes the set of subsets of Φ0 _0) that associates with every formula ϕ∈Ψφ∈ a set K∘ϕ⊆Φ0K φ _0, interpreted as the change in K prompted by the input ϕφ. We follow the common practice of writing K∘ϕK φ instead of ∘(ϕ) (φ) which has the advantage of making it clear that the belief change function refers to a given, fixed, K. If Ψ≠Φ0 ≠ _0 then ∘ is called a partial belief change function, while if Ψ=Φ0 = _0 then ∘ is called a full-domain belief change function. 2.1 The KM theory of belief update We consider the notion of belief update introduced by Katsuno and Mendelzon (KM) in [7] and, in Section 4, we compare it to the notion of belief revision introduced by Alchourrón, Gärdenfors and Makinson (AGM) in [1]. The formalism in the two theories is somewhat different. In [7] a belief state is represented by a sentence in a finite propositional calculus and belief update is modeled as a function over formulas, while in [1] a belief state is represented (as we did above) as a set of formulas. Note that, while [7] allows for the possibility of inconsistent initial beliefs, following [10] we take as starting point a consistent belief set. We follow closely the axiomatization of belief update proposed by [2, 9, 10], which has the advantage of making update directly comparable to revision (note, however, that [2, 9, 10] only cover the case of "strong" update, where axioms (K⋄6)(K 6) and (K⋄7)(K 7) are replaced by (K⋄9)(K 9): see Section 4 below). Consider the following version of the KM axioms of belief update based on the consistent and deductively closed set K (representing the initial beliefs): ∀ϕ,ψ∈Φ0∀φ,ψ∈ _0, (K⋄0)(K 0) K⋄ϕ=Cn(K⋄ϕ)K φ=Cn(K φ). (K⋄1)(K 1) ϕ∈K⋄ϕφ∈ K φ. (K⋄2)(K 2) If ϕ∈Kφ∈ K then K⋄ϕ=K φ=K. (K⋄3a)(K 3a) If ϕφ is a contradiction then K⋄ϕ=Φ0K φ= _0. (K⋄3b)(K 3b) If ϕφ is not a contradiction then K⋄ϕ≠Φ0K φ≠ _0. (K⋄4)(K 4) If ϕ↔ψφ ψ is a tautology then K⋄ϕ=K⋄ψK φ=K ψ. (K⋄5)(K 5) K⋄(ϕ∧ψ)⊆(K⋄ϕ)+ψK (φ ψ) (K φ)+ψ. (K⋄6(K 6) If ψ∈K⋄ϕψ∈ K φ and ϕ∈K⋄ψφ∈ K ψ then K⋄ϕ=K⋄ψK φ=K ψ . (K⋄7(K 7) If K is complete111A belief set K is complete if, for every formula ϕ∈Φ0φ∈ _0, either ϕ∈Kφ∈ K or ¬ϕ∈K φ∈ K. then (K⋄ϕ)∩(K⋄ψ)⊆K⋄(ϕ∨ψ)(K φ)∩(K ψ) K (φ ψ). Remark 1. Katsuno and Mendelzon provide an additional axiom (they name it U8), which they call the "disjunction rule". [2, 9, 10] translate it into the following "axiom", which makes use of maximally consistent sets of formulas (MCS), also called possible worlds.222A set of formulas Δ⊂Φ0 ⊂ _0 is maximally consistent if it is consistent and, furthermore, ∀ϕ∈Φ0∖Δ∀φ∈ _0 , Δ∪ϕ ∪\φ\ is inconsistent. Every MCS is deductively closed and complete. If K is consistent, then K is complete if and only if ⟦K⟧ K is a singleton, where ⟦K⟧ K denotes the set of maximally consistent sets of formulas that contain all the formulas in K. Given a set of formulas Γ⊆Φ0 _0, let ⟦Γ⟧ be the set of MCS that contain all the formulas in Γ .333Following the common notation in the literature, we denote by W the set of MCS, or possible worlds, and by w an element of W (hence w∈Ww∈ W is a set of formulas). Thus, w∈⟦Γ⟧w∈ if and only if w∈Ww∈ W and Γ⊆w w. The additional axiom is the following (note that ⟦K⟧≠∅ K ≠ if and only if K is consistent): (K⋄8)If ⟦K⟧≠∅ then K⋄ϕ=⋂w∈⟦K⟧(w⋄ϕ).(K 8) K ≠ then K φ= _w∈ K (w φ). (K⋄8K 8) is of a different nature than the other axioms, since it applies the update operator not only to the initial belief set K but also to the individual MCS contained in ⟦K⟧ K . (K⋄8K 8) can be viewed more as a condition on the interpretation or semantics rather than a real axiom; it is superfluous in our framework since its role is directly captured by the semantics described below; for a more detailed discussion see [3]. (K⋄0)(K 0) does not appear in the list of axioms provided by Katsuno and Mendelzon, since their formalism is not in terms of belief sets. For i∈1,2,4,5,6,7i∈\1,2,4,5,6,7\, axiom (K⋄i)(K i) is a translation of Katsuno and Mendelzon’s axiom (Ui)(Ui) (for details see [9]). The conjunction of (K⋄3a)(K 3a) and (K⋄3b)(K 3b) is the translation of Katsuno and Mendelzon’s axiom (U3)(U3) when attention is restricted to the case where the initial belief set K is consistent.444Katsuno and Mendelzon allow for the possibility that the initial beliefs are inconsistent, in which case the conjunction of (K⋄3aK 3a) and (K⋄3bK 3b) would be stated as follows: K⋄ϕ=Φ0K φ= _0 if and only if either K is inconsistent or ϕφ is a contradiction. It should be noted that one important difference between update and revision is precisely that updating an inconsistent K by a consistent formula ϕφ yields the inconsistent belief set Φ0 _0, while revising an inconsistent K by a consistent formula ϕφ yields a consistent set (AGM axiom (K∗5bK 5b): see Section 4). The following lemma, proved in the Appendix, shows that axiom (K⋄7)(K 7) can be replaced by the following, seemingly stronger, axiom (obtained from (K⋄7)(K 7) by dropping the clause ‘if K is complete’): (K⋄7s)(K∘ϕ)∩(K∘ψ)⊆K∘(ϕ∨ψ).(K 7s) (K φ)∩(K ψ) K (φ ψ). Lemma 1. (K⋄7s)(K 7s) follows from (K⋄7)(K 7) and (K⋄8)(K 8) In order to facilitate the conversion to a modal formula, we replace (K⋄6)(K 6) with the following weaker form, which – in the presence of (K⋄0)(K 0) – is equivalent to (K⋄6)(K 6) (the role of the added clause ‘⊤∈K⋄(ϕ∧ψ) ∈ K (φ ψ)’ is explained in Remark 2): (K⋄6w)If ψ∈K⋄ϕ and ϕ∈K⋄ψ and ⊤∈K⋄(ϕ∧ψ) then K⋄ϕ=K⋄ψ(K 6w) ψ∈ K φ and φ∈ K ψ and ∈ K (φ ψ) then K φ=K ψ In view of Lemma 1 and the above observation that (K⋄8)(K 8) is superfluous in our framework, we define a KM belief update as follows. Definition 1. A KM belief update function, based on the consistent and deductively closed set K, is a full domain belief change function ⋄:Φ0→2Φ0 : _0→ 2 _0 that satisfies axioms (K⋄0)(K 0)-(K⋄5)(K 5), (K⋄6w)(K 6w) and (K⋄7s)(K 7s). Katsuno and Mendelzon show that, semantically, their notion of belief update corresponds to partial pre-orders on the set of maximally consistent sets of formulas. We will, instead, make use of the Kripke-Lewis semantics introduced in [3], to which we now turn. 2.1.1 Kripke-Lewis semantics Definition 2. A Kripke-Lewis frame is a triple ⟨S,ℬ,f⟩ S,B,f where 1. S is a set of states; subsets of S are called events. 2. ℬ⊆S×SB S× S is a binary relation on S which is serial: ∀s∈S,∃s′∈S∀ s∈ S,∃ s ∈ S, such that sℬs′sBs (sℬs′sBs is an alternative notation for (s,s′)∈ℬ(s,s ) ). We denote by ℬ(s)B(s) the set of states that are reachable from s by ℬB: ℬ(s)=s′∈S:sℬs′B(s)=\s ∈ S:sBs \. ℬ(s)B(s) is interpreted as the set of states that, initially, the agent considers doxastically possible at state s. 3. f:S×(2S∖∅)→2Sf:S×(2^S )→ 2^S is a selection function that associates with every state-event pair (s,E)(s,E) (with E≠∅E≠ ) a set of states f(s,E)⊆Sf(s,E) S, interpreted as the set of states that are closest (or most similar) to s, conditional on event E. We require seriality of the belief relation because it ensures that the initial beliefs at state s, represented by the non-empty set ℬ(s)B(s), are consistent. Similarly, the requirement that f(s,E)f(s,E) is defined only if E≠∅E≠ ensures that the informational input is consistent (how to deal with inconsistent information is discussed in Section 3). Note the absence, in Definition 2, of the extra properties imposed on the selection function in [3], namely, f(s,E)⊆Ef(s,E) E (Identity). f(s,E)≠∅f(s,E)≠ (Normality). if s∈Es∈ E then s∈f(s,E)s∈ f(s,E) (Weak Centering). The reason why we do not impose any properties on the selection function is that we want to highlight the role of each property in the characterization of the KM axioms. For example, Identity (localised to ℬ(s)B(s)) plays a role in the characterization of (K⋄2)(K 2) but not in the characterization of the other axioms, Normality (localised to ℬ(s)B(s)) is used to characterize axiom (K⋄3b)(K 3b) but not the other axioms.555In conditional logic, Identity corresponds to the axiom ”if ϕφ then ϕφ”, denoted by ϕ>ϕφ>φ, and Normality validates the axiom (ϕ>ψ)→¬(ϕ>¬ψ)(φ>ψ)→ (φ> ψ) for consistent ϕφ: see [8]. Adding a valuation to a frame yields a model. Thus a model is a tuple ⟨S,ℬ,f,V⟩ S,B,f,V where ⟨S,ℬ,f⟩ S,B,f is a frame and V:At→2SV: At→ 2^S is a valuation that assigns to every atomic formula p∈Atp∈ At the set of states where p is true. Definition 3. Given a model M=⟨S,ℬ,f,V⟩M= S,B,f,V define truth of a Boolean formula ϕ∈Φ0φ∈ _0 at a state s∈Ss∈ S in model M, denoted by s⊧Mϕs _Mφ, as follows: 1. if p∈Atp∈ At then s⊧Mps _Mp if and only if s∈V(p)s∈ V(p), 2. s⊧M¬ϕs _M φ if and only if s⊧̸Mϕs _Mφ, 3. s⊧M(ϕ∨ψ)s _M(φ ψ) if and only if s⊧Mϕs _Mφ or s⊧Mψs _Mψ (or both). We denote by ‖ϕ‖M\|φ\|_M the truth set of formula ϕφ in model M: ‖ϕ‖M=s∈S:s⊧Mϕ.\|φ\|_M=\s∈ S:s _Mφ\. Given a model M=⟨S,ℬ,f,V⟩M= S,B,f,V and a state s∈Ss∈ S, let Ks,M=ϕ∈Φ0:ℬ(s)⊆‖ϕ‖MK_s,M=\φ∈ _0:B(s) \|φ\|_M\; thus a formula ϕφ belongs to Ks,MK_s,M if and only if at state s the agent believes ϕφ, in the sense that ϕφ is true at every state that the agent considers doxastically possible at s. We identify Ks,MK_s,M with the agent’s initial beliefs at state s. It is shown in [3] that the set Ks,M⊆Φ0K_s,M _0 so defined is deductively closed and consistent (the latter property follows from seriality of the belief relation ℬB). Next, given a model M=⟨S,ℬ,f,V⟩M= S,B,f,V and a state s∈Ss∈ S, let ΨM=ϕ∈Φ0:‖ϕ‖M≠∅ _M=\φ∈ _0:\|φ\|_M≠ \666Since, in any given model, there are formulas ϕφ such that ‖ϕ‖M=∅\|φ\|_M= (at the very least all the contradictions), ΨM _M is a proper subset of Φ0 _0. and define the following partial belief change function ∘:ΨM→2Φ0 : _M→ 2 _0 based on ΨM _M and Ks,MK_s,M: ψ∈Ks,M∘ϕif and only if, ∀s′∈ℬ(s),f(s′,‖ϕ‖M)⊆‖ψ‖Mor, equivalently, ⋃s′∈ℬ(s)f(s′,‖ϕ‖M)⊆‖ψ‖M array[]*20lψ∈ K_s,M φ&if and only if, \,\,∀ s (s),\,f (s ,\|φ\|_M ) \|ψ\|_M\\[10.0pt] &or, equivalently, _s (s)f (s ,\|φ\|_M )\, \,\|ψ\|_M array (RI) Given the customary interpretation of selection functions in terms of conditionals, (RI) can be interpreted as stating that ψ∈Ks,M∘ϕψ∈ K_s,M φ if and only if at state s the agent believes that "if ϕφ is (were) the case then ψ is (would be) the case".777Note that we allow for both the indicative and the subjunctive conditional. The indicative form (if ϕφ is the case then ψ is the case) seems to be more appropriate when the initial belief set does not contain ¬ϕ φ (that is, if the agent initially considers ϕφ possible), while the subjunctive form (if ϕφ were the case then ψ would be the case) seems to be more appropriate when the agent initially believes ¬ϕ φ. This interpretation will be made explicit in the modal logic considered in Section 3. Remark 2. Consider an arbitrary model M and state s and let ∘:ΨM→2Φ0 : _M→ 2 _0 be the partial belief change function defined by (RI). Then, for every consistent formula χ∈Φ0χ∈ _0, ‖χ‖M≠∅ if and only if ⊤∈Ks,M⋄χ.\|χ\|_M≠ if and only if ∈ K_s,M χ. In what follows, when stating an axiom for a belief change function, we implicitly assume that it applies to every formula in its domain. For example, the axiom ϕ∈K∘ϕφ∈ K φ asserts that, for all ϕφ in the domain of ∘ , ϕ∈K∘ϕφ∈ K φ. Definition 4. An axiom for belief change functions is valid on a frame F if, for every model based on that frame and for every state s in that model, the partial belief change function defined by (RI) satisfies the axiom. An axiom is valid on a set of frames ℱF if it is valid on every frame F∈ℱF . A stronger notion than validity is that of frame correspondence. The following definition mimics the notion of frame correspondence in modal logic. Definition 5. We say that an axiom A of belief change functions is characterized by, or corresponds to, or characterizes, a property P of frames if the following is true: (1) axiom A is valid on the class of frames that satisfy property P, and (2) if a frame does not satisfy property P then axiom A is not valid on that frame, that is, there is a model based on that frame and a state in that model where the partial belief change function defined by (RI) violates axiom A. KM axiom Frame property(K⋄0)K⋄ϕ=Cn(K⋄ϕ)No additional property(K⋄1)ϕ∈K⋄ϕ(P⋄1∗2)∀s∈S,∀E∈2S∖∅,⋃s′∈ℬ(s)f(s′,E)⊆E(K⋄2)If ϕ∈K then K⋄ϕ=K(P⋄2)∀s∈S,∀E∈2S∖∅, if ℬ(s)⊆E then, ⋃s′∈ℬ(s)f(s′,E)=ℬ(s)(K⋄3b)If ¬ϕ is not a tautologythen K⋄ϕ≠Φ0(P⋄3b∗5b)∀s∈S,∀E∈2S∖∅,∃s′∈ℬ(s) such that f(s′,E)≠∅(K⋄4)if ϕ↔ψ is a tautologythen K⋄ϕ=K⋄ψNo additional property(K⋄5)K⋄(ϕ∧ψ)⊆(K⋄ϕ)+ψ(P⋄5∗7)∀s∈S,∀E,F∈2S with E∩F≠∅,⋃s′∈ℬ(s)(f(s′,E)∩F)⊆⋃s′∈ℬ(s)f(s′,E∩F)(K⋄6w)If ψ∈K⋄ϕ and ϕ∈K⋄ψ and ⊤∈K⋄(ϕ∧ψ) then K⋄ϕ=K⋄ψ(P⋄6w)∀s∈S,∀E,F∈2S with E∩F≠∅if ⋃s′∈ℬ(s)f(s′,E)⊆F and⋃s′∈ℬ(s)f(s′,F)⊆Ethen ⋃s′∈ℬ(s)f(s′,E)=⋃s′∈ℬ(s)f(s′,F)(K⋄7s)(K⋄ϕ)∩(K⋄ψ)⊆K⋄(ϕ∨ψ)(P⋄7s)∀s∈S,∀E,F∈2S∖∅⋃s′∈ℬ(s)f(s′,E∪F)⊆(⋃s′∈ℬ(s)f(s′,E))∪(⋃s′∈ℬ(s)f(s′,F)) array[]*20l 18.49988pt KM axiom && 18.49988pt Frame property\\ (K 0) K φ=Cn(K φ)& &No additional property\\ (K 1) φ∈ K φ& &(P^*2_ 1) array[]l∀ s∈ S,∀ E∈ 2^S ,\\[-10.0pt] _s (s)f(s ,E) E array\\ (K 2) φ∈ K then K φ=K& &(P 2) array[]l∀ s∈ S,∀ E∈ 2^S ,\\[-10.0pt] if B(s) E then, \\[-10.0pt] _s (s)f(s ,E)\,=\,B(s) array\\ (K 3b) array[]lIf φ is not a tautology\\[-10.0pt] then K φ≠ _0 array& & array[]l(P^*5b_ 3b)&∀ s∈ S,∀ E∈ 2^S ,\\[-10.0pt] &∃ s (s) such that f(s ,E)≠ array\\ (K 4) array[]lif φ ψ is a tautology\\[-10.0pt] then K φ=K ψ array& &No additional property\\ (K 5) K (φ ψ) (K φ)+ψ& & array[]l(P^*7_ 5) ∀ s∈ S,∀ E,F∈ 2^S with E∩ F≠ ,\\[-10.0pt] _s (s) (f(s ,E)∩ F )\,\, \,\, _s (s)f(s ,E∩ F) 6.0pt plus 2.0pt minus 2.0pt array\\ (K 6w) array[]lIf ψ∈ K φ and φ∈ K ψ\\[-8.0pt] and ∈ K (φ ψ)\\[-8.0pt] then K φ=K ψ array& & array[]l(P 6w) ∀ s∈ S,∀ E,F∈ 2^S with E∩ F≠ \\[-6.0pt] if _s (s)f(s ,E) F and _s (s)f(s ,F) E\\[-4.0pt] then _s (s)f(s ,E)\,\,=\, _s (s)f(s ,F) 6.0pt plus 2.0pt minus 2.0pt array\\ (K 7s) (K φ)∩(K ψ) K (φ ψ)& & array[]l(P 7s) 18.49988pt∀ s∈ S,∀ E,F∈ 2^S \\[-6.0pt] _s (s)f(s ,E∪ F)\\[8.0pt] ( _s (s)f(s ,E) )\,\,∪\, ( _s (s)f(s ,F) ) array array Figure 1: Semantic characterization of the KM axioms. The table in Figure 1 lists, for every KM axiom, the characterizing property of frames.999Some of the properties in Figure 1 are related to properties of the selection function discussed in the literature on conditionals ([8]). For example, (P⋄1∗2)(P 2_ 1) is related to Identity and (P⋄3b∗5b)(P 5b_ 3b) to Normality. The remaining properties do not seem to be related to properties discussed in that literature. The proofs are given in the Appendix. The reason for the absence of axiom (K⋄3a)(K 3a) from the table in Figure 1 will become clear in the next section. When a KM axiom coincides with an AGM axiom, the name of the corresponding semantic property reflects this; for example, since KM axiom (K⋄1)(K 1) coincides with AGM axiom (K∗2)(K 2), the corresponding property is denoted by (P⋄1∗2)(P^*2_ 1).101010The AGM axioms are listed in Section 4. 3 A modal logic for belief update We now turn to the modal language considered in [4], which contains three modal operators: a unimodal belief operator B, a bimodal conditional operator >> and the unimodal necessity operator □ . The interpretation of BϕBφ is "the agent believes ϕφ", the interpretation of ϕ>ψφ>ψ is "if ϕφ is (or were) the case then ψ is (or would be) the case" and the interpretation of □ϕ φ is "ϕφ is necessarily true". The set Φ of formulas in the language is defined as follows: • Φ0⊆Φ _0 (recall that Φ0 _0 is the set of Boolean formulas built on the countable set of atomic sentences At), • if α,β∈Φα,β∈ then all of the following belong to Φ : □α α, BαBα, α>βα>β and all their Boolean combinations. We focus on the basic normal logic, denoted by ℒL, consisting of the following axioms and rules of inference.111111We follow the nomenclature in [5, p.115]. We denote general formulas by α, β and γ, while ϕφ, ψ and χ are reserved for Boolean formulas (e.g. in Figures 2-4). • Every formula that has the form of a classical tautology is a theorem. • The consistency axiom D for B: (DB)Bα→¬B¬α. (D_B) Bα→ B α. • The conjunction axiom C for □ , B and >>: (C□)□α∧□β→□(α∧β)(CB)Bα∧Bβ→B(α∧β)(C>)(γ>α)∧(γ>β)→(γ>(α∧β)) array[]l(C_ )& α β\,→\, (α β)\\ (C_B)&Bα Bβ\,→\,B(α β)\\ (C_>)&(γ>α) (γ>β)\,→\,(γ>(α β))\\ array • The necessity-to-belief axiom: (NB)□α→Bα(NB) α→ Bα • The rule of inference Modus Ponens: (MP)α,α→β(MP) α\,,\,α→β • The rule of inference Necessitation for □ and >>: (N□)α□α(N>)βα>β(N_ ) α α (N_>) βα>β • The rule of inference RMRM for □ , B and >>: (RM□)α→β□α→□β(RMB)α→βBα→Bβ(RM>)α→β(γ>α)→(γ>β) array[]l(RM_ )& α→β α→ β&(RM_B)& α→βBα→ Bβ\\[16.0pt] (RM_>)& α→β(γ>α)→(γ>β)&& array Remark 3. (A) The following (which will be used in the proofs) are theorems of logic ℒL: (C¬□¬)¬□¬(α∧β)→¬□¬α(CBinv)B(α∧β)→Bα∧Bβ(K>)(α>β)∧(α>(β→γ))→(α>γ)(A⋄0∗1)B(α>β)∧B(α>(β→γ))→B(α>γ) array[]l(C_ )& (α β)\,→\, α\\ (C_B^inv)&B(α β)\,→\,Bα Bβ\\ (K_>)&(α>β) (α>(β→γ))\,→\,(α>γ)\\ (A^*1_ 0)&B(α>β) B(α>(β→γ))\,→\,B(α>γ) array (B) The following are derived rules of inference in logic ℒL: (RM¬□¬)α→β¬□¬α→¬□¬β(NB)αBα(RMB>)α→βB(γ>α)→B(γ>β) array[]l(RM_ )& α→β α→ β\\[18.0pt] (N_B)& αBα\\[18.0pt] (RM_B>)& α→βB(γ>α)→ B(γ>β) array 3.1 Frame correspondence As semantics for this modal logic we take the Kripke-Lewis frames of Definition 2. A model based on a frame is obtained, as before, by adding a valuation V:At→2SV: At→ 2^S. The following definition expands Definition 3 by adding validation rules for formulas of the form □α α, α>βα>β and BαBα. Definition 6. Truth of a formula α∈Φα∈ at state s in model M (denoted by s⊧Mαs _Mα) is defined as follows: 1. if p∈Atp∈ At then s⊧Mps _Mp if and only if s∈V(p)s∈ V(p). 2. s⊧M¬αs _M α if and only if s⊧̸Mαs _Mα. 3. s⊧M(α∨β)s _M(α β) if and only if s⊧Mαs _Mα or s⊧Mβs _Mβ (or both). 4. s⊧M□αs _M α if and only if, ∀s′∈S∀ s ∈ S, s′⊧Mαs _Mα (thus s⊧M¬□¬αs _M α if and only if, for some s′∈Ss ∈ S, s′⊧Mαs _Mα, that is, ‖α‖M≠∅\|α\|_M≠ ). 5. s⊧M(α>β)s _M(α>β) if and only if, either (a) s⊧M□¬αs _M α (that is, ‖α‖M=∅\|α\|_M= ), or (b) s⊧M¬□¬αs _M α (that is, ‖α‖M≠∅\|α\|_M≠ ) and, for every s′∈f(s,‖α‖M)s ∈ f(s,\|α\|_M), s′⊧Mβs _Mβ (that is, f(s,‖α‖M)⊆‖β‖Mf(s,\|α\|_M) \|β\|_M).121212Recall that, by definition of frame, f(s,E)f(s,E) is defined only if E≠∅E≠ . 6. s⊧MBαs _MBα if and only if, ∀s′∈ℬ(s)∀ s (s), s′⊧Mαs _Mα (that is, ℬ(s)⊆‖α‖MB(s) \|α\|_M). The definitions of validity and characterization are as in the previous section. Definition 7. A formula α∈Φα∈ is valid on a frame F if, for every model M based on that frame and for every state s in that model, s⊧Mαs _Mα. A formula α∈Φα∈ is valid on a set of frames ℱF if it is valid on every frame F∈ℱF . Definition 8. A formula α∈Φα∈ is characterized by, or corresponds to, or characterizes, a property P of frames if the following is true: (1) α is valid on the class of frames that satisfy property P, and (2) if a frame does not satisfy property P then α is not valid on that frame. The table in Figure 2 shows, for every property of frames considered in Figure 1, the modal formula that corresponds to it. When a KM axiom coincides with an AGM axiom, the name of the corresponding modal formula reflects this; for example, since KM axiom (K⋄1)(K 1) coincides with AGM axiom (K∗2)(K 2), the corresponding modal formula is denoted by (A⋄1∗2)(A^*2_ 1).131313The AGM axioms are listed in Section 4. The proofs of the characterizations results are given in the Appendix. In axioms (A⋄3b∗5b)(A^*5b_ 3b) and (A⋄7s)(A 7s) the clause ¬□¬ϕ φ in the antecedent ensures that, on the semantic side, ‖ϕ‖≠∅\|φ\|≠ ; in particular, it rules out that ϕφ is a contradiction; similarly for the clauses ¬□¬ψ ψ and ¬□¬(ϕ∧ψ) (φ ψ). The interpretation of the axioms is as follows: (A⋄1∗2)the agent believes that if ϕ were the case, then ϕ would bethe case(A⋄2)if the agent initially believes that ϕ then she believes that ψif and only if she believes that if ϕ were the case, then ψ would be the case(A⋄3b∗5b)if ϕ is not necessarily false and the agent believes that if ϕ werethe case, then ψ would be the case, then the agent does notbelieve that if ϕ were the case, then ψ would not be the case(A⋄5∗7)if the conjunction ϕ∧ψ is not necessarily false and the agentbelieves that if ϕ∧ψ were the case, then χ would be the casethen she believes that if ϕ were the case, then it would be thecase that either ψ is false or χ is true (that is, that ψ→χ)(A⋄6)if ϕ∧ψ is not necessarily false and the agent believes thatif ϕ were the case, then ψ would be the case and that if ψ werethe case, then ϕ would be the case, then she believes that ifϕ were the case, then χ would be the case if and only if shebelieves that if ψ were the case, then χ would be the case(A⋄7s)if neither ϕ nor ψ is necessarily false, and the agent believesthat if ϕ were the case, then χ would be the case and thatif ψ were the case, then χ would be the case, then shebelieves that if ϕ∨ψ were the case, then χ would be the case array[]l(A^*2_ 1)&the agent believes that if φ were the case, then φ would be\\ &the case\\[5.0pt] (A 2)&if the agent initially believes that φ then she believes that ψ\\ &if and only if she believes that if φ were the case, then ψ\\ & would be the case\\[5.0pt] (A^*5b_ 3b)&if φ is not necessarily false and the agent believes that if φ were\\ &the case, then ψ would be the case, then the agent does not\\ &believe that if φ were the case, then ψ would not be the case\\[5.0pt] (A^*7_ 5)&if the conjunction φ ψ is not necessarily false and the agent\\ &believes that if φ ψ were the case, then χ would be the case\\ &then she believes that if φ were the case, then it would be the\\ &case that either ψ is false or χ is true (that is, that ψ→χ)\\[5.0pt] (A 6)&if φ ψ is not necessarily false and the agent believes that\\ &if φ were the case, then ψ would be the case and that if ψ were\\ &the case, then φ would be the case, then she believes that if\\ &φ were the case, then χ would be the case if and only if she\\ &believes that if ψ were the case, then χ would be the case\\[5.0pt] (A 7s)&if neither φ nor ψ is necessarily false, and the agent believes\\ &that if φ were the case, then χ would be the case and that\\ &if ψ were the case, then χ would be the case, then she\\ &believes that if φ ψ were the case, then χ would be the case 12.0pt plus 4.0pt minus 4.0pt array Figure 3 puts together Figures 1 and 2 by showing for each KM axiom the corresponding modal axiom or rule of inference. Note that (A⋄0∗1)(A^*1_ 0) is a theorem of ℒL (see Remark 3). We denote by ℒKML_KM the extension of logic ℒL obtained by adding the modal axioms and rules of inference listed in Figure 3. In the next section we define a similar extension of ℒL, denoted by ℒAGML_AGM, that captures the logic of AGM belief revision and show that ℒKML_KM is contained in ℒAGML_AGM. Frame propertyCorresponding modal formulaIn all the formulas, ϕ,ψ,χ are Boolean(P⋄1∗2)∀s∈S,∀E∈2S∖∅,⋃s′∈ℬ(s)f(s′,E)⊆E(A⋄1∗2)B(ϕ>ϕ)(P⋄2)∀s∈S,∀E∈2S∖∅,if ℬ(s)⊆E then ⋃s′∈ℬ(s)f(s′,E)=ℬ(s)(A⋄2)Bϕ→(Bψ↔B(ϕ>ψ))(P⋄3b∗5b)∀s∈S,∀E∈2S∖∅,∃s′∈ℬ(s) such that f(s′,E)≠∅(A⋄3b∗5b)(¬□¬ϕ∧B(ϕ>ψ))→¬B(ϕ>¬ψ)(P⋄5∗7)∀s∈S,∀E,F∈2S with E∩F≠∅,⋃s′∈ℬ(s)(f(s′,E)∩F)⊆⋃s′∈ℬ(s)f(s′,E∩F)(A⋄5∗7)¬□¬(ϕ∧ψ)∧B((ϕ∧ψ)>χ)→B(ϕ>(ψ→χ))(P⋄6w)∀s∈S,∀E,F∈2S with E∩F≠∅if ⋃s′∈ℬ(s)f(s′,E)⊆F and⋃s′∈ℬ(s)f(s′,F)⊆Ethen ⋃s′∈ℬ(s)f(s′,E)=⋃s′∈ℬ(s)f(s′,F)(A⋄6w)¬□¬(ϕ∧ψ)∧B(ϕ>ψ)∧B(ψ>ϕ)→(B(ϕ>χ)↔B(ψ>χ))(P⋄7s)∀s∈S,∀E,F∈2S∖∅⋃s′∈ℬ(s)f(s′,E∪F)⊆(⋃s′∈ℬ(s)f(s′,E))∪(⋃s′∈ℬ(s)f(s′,F))(A⋄7s)¬□¬ϕ∧¬□¬ψ∧B(ϕ>χ)∧B(ψ>χ)→B((ϕ∨ψ)>χ) array[]*20l 18.49988pt Frame property&&\,\, Corresponding modal formula\\[-12.0pt] &&In all the formulas, φ,ψ,χ are Boolean\\ (P^*2_ 1) array[]l∀ s∈ S,∀ E∈ 2^S ,\\[-10.0pt] _s (s)f(s ,E) E array& &(A^*2_ 1) 18.49988ptB(φ>φ)\\ (P 2)\,\, array[]l∀ s∈ S,∀ E∈ 2^S ,\\[-10.0pt] if B(s) E then \\[-8.0pt] _s (s)f(s ,E)=B(s) array& &(A 2) 18.49988ptBφ\,→\, (Bψ B(φ>ψ) )\\ (P^*5b_ 3b)\,\, array[]l∀ s∈ S,∀ E∈ 2^S ,\\[-10.0pt] ∃ s (s) such that f(s ,E)≠ array& & array[]l(A^*5b_ 3b)\\[-5.0pt] ( φ B(φ>ψ) )→ B(φ> ψ) array\\ array[]l(P^*7_ 5)\\[-5.0pt] ∀ s∈ S,∀ E,F∈ 2^S with E∩ F≠ ,\\[-10.0pt] _s (s) (f(s ,E)∩ F )\,\, \,\, _s (s)f(s ,E∩ F) 6.0pt plus 2.0pt minus 2.0pt array& & array[]l(A^*7_ 5)\\[-5.0pt] (φ ψ)\, \,B((φ ψ)>χ)\\[-5.0pt] → B (φ>(ψ→χ) ) array\\ array[]l(P 6w)\\[-5.0pt] ∀ s∈ S,∀ E,F∈ 2^S with E∩ F≠ \\[-6.0pt] if _s (s)f(s ,E) F and _s (s)f(s ,F) E\\[-4.0pt] then _s (s)f(s ,E)\,\,=\, _s (s)f(s ,F) 6.0pt plus 2.0pt minus 2.0pt array& & array[]l(A 6w)\\[-5.0pt] (φ ψ) B(φ>ψ) B(ψ>φ)\\[-5.0pt] → (B(φ>χ) B(ψ>χ) ) array\\ array[]l(P 7s)\\[-5.0pt] ∀ s∈ S,∀ E,F∈ 2^S \\[-6.0pt] _s (s)f(s ,E∪ F)\\[8.0pt] ( _s (s)f(s ,E) )\,\,∪\, ( _s (s)f(s ,F) ) array& & array[]l(A 7s)\\[-5.0pt] φ ψ B(φ>χ) B(ψ>χ)\\[-5.0pt] → B ((φ ψ)>χ ) 6.0pt plus 2.0pt minus 2.0pt array\\ array Figure 2: The frame properties of Figure 1 and the corresponding modal formulas KM axiomModal axiom/Rule of inferenceIn all the formulas, ϕ,ψ,χ are Boolean(K⋄0)K⋄ϕ=Cn(K⋄ϕ)(A⋄0∗1)B(ϕ>ψ)∧B(ϕ>(ψ→χ))→B(ϕ>χ)(K⋄1)ϕ∈K⋄ϕ(A⋄1∗2)B(ϕ>ϕ)(K⋄2)If ϕ∈K then K⋄ϕ=K(A⋄2)Bϕ→(Bψ↔B(ϕ>ψ))(K⋄3a)If ¬ϕ is a tautologythen K⋄ϕ=Φ0Rule of inference (R⋄3a∗5a)¬ϕB(ϕ>ψ)(K⋄3b)If ¬ϕ is not a tautologythen K⋄ϕ≠Φ0(A⋄3b∗5b)(¬□¬ϕ∧B(ϕ>ψ))→¬B(ϕ>¬ψ)(K⋄4)if ϕ↔ψ is a tautologythen K⋄ϕ=K⋄ψRule of inference (R⋄4∗6)ϕ↔ψB(ϕ>χ)↔B(ψ>χ)(K⋄5)K⋄(ϕ∧ψ)⊆(K⋄ϕ)+ψ(A⋄5∗7)¬□¬(ϕ∧ψ)∧B((ϕ∧ψ)>χ)→B(ϕ>(ψ→χ))(K⋄6w)If ψ∈K⋄ϕ and ϕ∈K⋄ψ and ⊤∈K⋄(ϕ∧ψ) then K⋄ϕ=K⋄ψ(A⋄6w)¬□¬(ϕ∧ψ)∧B(ϕ>ψ)∧B(ψ>ϕ)→(B(ϕ>χ)↔B(ψ>χ))(K⋄7s)(K⋄ϕ)∩(K⋄ψ)⊆K⋄(ϕ∨ψ)(A⋄7s)¬□¬ϕ∧¬□¬ψ∧B(ϕ>χ)∧B(ψ>χ)→B((ϕ∨ψ)>χ) array[]*20l 18.49988pt KM axiom&& 18.49988pt Modal axiom/Rule of inference\\[-8.0pt] && 18.49988ptIn all the formulas, φ,ψ,χ are Boolean\\ (K 0)\,\,\,K φ=Cn(K φ)& & array[]l(A^*1_ 0)\\[-5.0pt] B(φ>ψ) B(φ>(ψ→χ))\,→\,B(φ>χ) array\\ (K 1)\,\,\,φ∈ K φ& &(A^*2_ 1) 18.49988ptB(φ>φ)\\ (K 2)\,\,\,If φ∈ K then K φ=K& &(A 2) 18.49988ptBφ\,→\, (Bψ B(φ>ψ) )\\ (K 3a)\,\, array[]lIf φ is a tautology\\[-10.0pt] then K φ= _0 array& &\,\, array[]lRule of inference \\[-5.0pt] (R^*5a_ 3a) 18.49988pt φB(φ>ψ) 6.0pt plus 2.0pt minus 2.0pt array\\ (K 3b)\,\, array[]lIf φ is not a tautology\\[-10.0pt] then K φ≠ _0 array& &\,\, array[]l(A^*5b_ 3b)\\[-5.0pt] ( φ B(φ>ψ) )→ B(φ> ψ) array\\ (K 4)\,\, array[]lif φ ψ is a tautology\\[-10.0pt] then K φ=K ψ array& & array[]lRule of inference \\[-5.0pt] (R^*6_ 4) 18.49988pt φ ψB(φ>χ) B(ψ>χ) 6.0pt plus 2.0pt minus 2.0pt array\\ (K 5)\,\,\,K (φ ψ) (K φ)+ψ& & array[]l(A^*7_ 5)\\[-5.0pt] (φ ψ)\, \,B((φ ψ)>χ)\\[-5.0pt] → B (φ>(ψ→χ) ) array\\ (K 6w) array[]lIf ψ∈ K φ and φ∈ K ψ\\[-8.0pt] and ∈ K (φ ψ)\\[-8.0pt] then K φ=K ψ array& & array[]l(A 6w)& (φ ψ) B(φ>ψ) B(ψ>φ)\\[-5.0pt] &→ (B(φ>χ) B(ψ>χ) ) array\\ (K 7s)\,\,(K φ)∩(K ψ) K (φ ψ)& & array[]l(A 7s)\\[-5.0pt] φ ψ B(φ>χ) B(ψ>χ)\\[-5.0pt] → B ((φ ψ)>χ ) 6.0pt plus 2.0pt minus 2.0pt array\\ array Figure 3: The KM axioms and the corresponding modal axioms/rules of inference 4 Relating KM logic to AGM logic In [4] every AGM axiom of belief revision was translated into a corresponding modal axiom in a way similar to what was done in the previous section for the KM axioms. Figure 4 (which reproduces Figure 3 in [4], with the modal axioms renamed to match the names in this paper) shows the correspondence between AGM axioms and modal axioms.141414In [3] (K∗4)(K 4) was given in a weaker form, namely if ¬ϕ∉K φ∉ K then K⊆K∗ϕK K φ. However, in the presence of (K∗1)(K 1) and (K∗2)(K 2), the two are equivalent. That the stronger version used in Figure 4 implies the weaker version follows from the fact that K⊆K+ϕK K+\φ\. To prove the converse, let ψ∈K+ϕψ∈ K+φ. Then since K is deductively closed, (ϕ→ψ)∈K(φ→ψ)∈ K so that, by the weaker version, (ϕ→ψ)∈K∗ϕ(φ→ψ)∈ K φ. By (K∗2)(K 2), ϕ∈K∗ϕφ∈ K φ and by (K∗1)(K 1) K∗ϕK φ is deductively closed. Thus, since ϕ,(ϕ→ψ)∈K∗ϕφ,(φ→ψ)∈ K φ it follows that ψ∈K∗ϕψ∈ K φ. We denote by ℒAGML_AGM the extension of logic ℒL obtained by adding the modal axioms and rules of inference listed in Figure 4. According to the following proposition, which is proved in the Appendix, AGM belief revision can be viewed as a strengthening of KM belief update. Proposition 1. The logic ℒKML_KM of KM belief update is contained in the logic ℒAGML_AGM of AGM belief revision, that is, every axiom of ℒKML_KM is a theorem of ℒAGML_AGM. We conclude this section by considering a stronger version of belief update suggested by [7]. Katsuno and Mendelzon obtain this stronger version by replacing their axioms (U6)(U6) and (U7)(U7) with a stronger axiom, which they call (U9)(U9).151515The authors then show that this stronger notion of belief update corresponds semantically to total pre-orders on the set of possible worlds. In our framework their axiom (U9)(U9) can be translated as follows (see [2, 9, 10]): (K⋄9)If K is complete and ¬ψ∉K⋄ϕ then (K⋄ϕ)+ψ⊆K⋄(ϕ∧ψ).(K 9) K is complete and ψ∉ K φ then (K φ)+ψ K (φ ψ). The following Lemma is proved in the Appendix. Lemma 2. The following (seemingly stronger) version of (K⋄9)(K 9) (obtained by dropping the clause ‘if K is complete’ from (K⋄9)(K 9)) follows from (K⋄0)(K 0), (K⋄8)(K 8) and (K⋄9)(K 9): (K⋄9s)If ¬ψ∉K⋄ϕ then (K⋄ϕ)+ψ⊆K⋄(ϕ∧ψ)(K 9s) ψ∉ K φ then (K φ)+ψ K (φ ψ) AGM axiomModal axiom/Rule of Inference(for ϕ,ψ,χ∈Φ0)(K∗1)K∗ϕ=Cn(K∗ϕ)(A⋄0∗1)B(ϕ>ψ)∧B(ϕ>(ψ→χ))→B(ϕ>χ)(K∗2)ϕ∈K∗ϕ(A⋄1∗2)B(ϕ>ϕ)(K∗3)K∗ϕ⊆K+ϕ(A∗3)(¬□¬ϕ∧B(ϕ>ψ)→B(ϕ→ψ)(K∗4)if ¬ϕ∉K then K+ϕ⊆K∗ϕ(A∗4)(¬B¬ϕ∧B(ϕ→ψ))→B(ϕ>ψ)(K∗5a)If ¬ϕ is a tautology, then K∗ϕ=Φ0rule of inference:(R⋄3a∗5a)¬ϕB(ϕ>ψ)(K∗5b)If ¬ϕ is not a tautologythen K∗ϕ≠Φ0(A⋄3b∗5b)(¬□¬ϕ∧B(ϕ>ψ))→¬B(ϕ>¬ψ)(K∗6)if ϕ↔ψ is a tautologythen K∗ϕ=K∗ψrule of inference:(R⋄4∗6)ϕ↔ψB(ϕ>χ)↔B(ψ>χ)(K∗7)K∗(ϕ∧ψ)⊆(K∗ϕ)+ψ(A∗7)¬□¬(ϕ∧ψ)∧B((ϕ∧ψ)>χ)→B(ϕ>(ψ→χ))(K∗8)If ¬ψ∉K∗ϕ, then(K∗ϕ)+ψ⊆K∗(ϕ∧ψ)(A⋄9s∗8)¬B(ϕ>¬ψ)∧B(ϕ>(ψ→χ))→B((ϕ∧ψ)>(ψ∧χ)) array[]*20l AGM axiom&& array[]c Modal axiom/Rule of Inference\\[-10.0pt] \,(for φ,ψ,χ∈ _0) array\\ (K*1)\,\,\,K*φ=Cn(K*φ)& & array[]l(A^*1_ 0)&B(φ>ψ) B(φ>(ψ→χ))\\[-10.0pt] &→ B(φ>χ) array\\ (K*2)\,\,\,φ∈ K*φ& &(A^*2_ 1) B(φ>φ)\\ (K*3)\,\,\,K*φ K+φ& &(A*3) ( φ B(φ>ψ )→ B(φ→ψ)\\ (K*4)\,\,\, array[]*20lif φ∉ K\\[-10.0pt] then K+φ K*φ array& &(A*4) ( B φ B(φ→ψ) )→ B(φ>ψ)\\ (K*5a)\,\, array[]*20lIf φ is a tautology, then \\[-10.0pt] K*φ= _0 array& & array[]lrule of inference:&\\[-10.0pt] (R^*5a_ 3a)& φB(φ>ψ) array\\ (K*5b)\,\, array[]*20lIf φ is not a tautology\\[-10.0pt] then K*φ≠ _0 array& &(A^*5b_ 3b) ( φ B(φ>ψ) )→ B(φ> ψ)\\ (K*6)\,\, array[]*20lif φ ψ is a tautology\\[-10.0pt] then K*φ=K*ψ array& & array[]lrule of inference:\\[-10.0pt] (R^*6_ 4)& φ ψB(φ>χ) B(ψ>χ) 6.0pt plus 2.0pt minus 2.0pt array\\ (K*7)\,\,\,K*(φ ψ) (K*φ)+ψ& & array[]*20l(A*7)& (φ ψ)\, \,B((φ ψ)>χ)\\[-10.0pt] &→ B (φ>(ψ→χ) ) array\\ (K*8)\,\, array[]*20lIf ψ∉ K*φ, then\\[-10.0pt] (K*φ)+ψ K*(φ ψ) array& & array[]*20l(A^*8_ 9s)& B(φ> ψ) B(φ>(ψ→χ))\\[-10.0pt] &→\,B ((φ ψ)>(ψ χ) ) array array Figure 4: The correspondence between AGM axioms and their modal counterparts. Definition 9. A strong belief update function is a full-domain belief change function ⋄:Φ0→2Φ0 : _0→ 2 _0 that satisfies axioms (K⋄0)(K 0)-(K⋄5)(K 5) and (K⋄9s)(K 9s). Comparing the AGM axioms to the axioms of the strong version of KM update we can see that: • KM axiom (K⋄0(K 0) coincides with AGM axiom (K∗1)(K 1) and the corresponding modal axiom is the following, which is a theorem of ℒL (see Remark 3) (A⋄0∗1)B(ϕ>ψ)∧B(ϕ>(ψ→χ))→B(ϕ>χ)(A^*1_ 0) B(φ>ψ) B(φ>(ψ→χ))\,→\,B(φ>χ) • KM axiom (K⋄1(K 1) coincides with AGM axiom (K∗2)(K 2) and the corresponding modal axiom is (A⋄1∗2)B(ϕ>ϕ)(A^*2_ 1) B(φ>φ) • KM axiom (K⋄3a(K 3a) coincides with AGM axiom (K∗5a)(K 5a) and it corresponds to the rule of inference (R⋄3a∗5a)¬ϕB(ϕ>ψ)(R^*5a_ 3a) φB(φ>ψ) • KM axiom (K⋄3b(K 3b) coincides with AGM axiom (K∗5b)(K 5b) and the corresponding modal axiom is (A⋄3b∗5b)(¬□¬ϕ∧B(ϕ>ψ))→¬B(ϕ>¬ψ)(A^*5b_ 3b) ( φ B(φ>ψ) )→ B(φ> ψ) • KM axiom (K⋄4(K 4) coincides with AGM axiom (K∗6)(K 6) and it corresponds to the rule of inference (R⋄4∗6)ϕ↔ψB(ϕ>χ)↔B(ψ>χ)(R^*6_ 4) φ ψB(φ>χ) B(ψ>χ) • KM axiom (K⋄5(K 5) coincides with AGM axiom (K∗7)(K 7) and the corresponding modal axiom is (A⋄5∗7)¬□¬(ϕ∧ψ)∧B((ϕ∧ψ)>χ)→B(ϕ>(ψ→χ))(A^*7_ 5) (φ ψ)\, \,B((φ ψ)>χ)\,→\,B (φ>(ψ→χ) ) • KM axiom (K⋄9s(K 9s) coincides with AGM axiom (K∗8)(K 8) and the corresponding modal axiom is (A⋄9s∗8)¬B(ϕ>¬ψ)∧B(ϕ>(ψ→χ))→B((ϕ∧ψ)>(ψ∧χ))(A^*8_ 9s) B(φ> ψ) B(φ>(ψ→χ))\,→\,B ((φ ψ)>(ψ χ) ) Thus the difference between AGM belief revision and the strong version of KM belief update is that the former contains axioms (K∗3)(K 3) and (K∗4)(K 4) while the latter only requires axiom (K⋄2)(K 2). First of all, note that axiom (A⋄2)(A 2) – corresponding to (K⋄2)(K 2) – is a theorem of ℒAGML_AGM (see Lemma 4 in the Appendix) and thus the logic ℒAGML_AGM contains also the logic of the strong version of KM belief update. The following lemma, proved in the Appendix, shows that the modal axiom corresponding to AGM axiom (K∗3)(K 3) is provable in logic ℒKML_KM. Lemma 3. Axiom (A∗3)(¬□¬ϕ∧B(ϕ>ψ)→B(ϕ→ψ)(A 3) ( φ B(φ>ψ )→ B(φ→ψ) (which is the modal counterpart to AGM axiom (K∗3)(K 3)) is provable in logic ℒKML_KM. Thus, the difference between AGM belief revision and the strong version of KM belief update reduces to one axiom. Axiom (A⋄2)Bϕ∧Bψ→B(ϕ>ψ)(A 2) Bφ \ Bψ\,→\,B(φ>ψ) in the latter is replaced, in the former, by the stronger axiom (A∗4)¬B¬ϕ∧B(ϕ→ψ)→B(ϕ>ψ)(A 4) B φ B(φ→ψ)\,→\,B(φ>ψ) Axiom (A∗4)(A 4) covers the case where the informational input ϕφ is initially not disbelieved (¬ϕ∉K φ∉ K). Comparing the frame property (P⋄2)(P 2) corresponding to KM axiom (A⋄2)(A 2) (see Figure 2) with the following property, which is implied by the property corresponding to AGM axiom (A∗4)(A 4)161616For completeness, since the (standard) version of (K∗4)(K 4) used here is somewhat different from the one used in [3, 4] (see Footnote 14) we prove the correspondence results for (K∗4)(K 4) and (A∗4)(A 4) in Lemma 7 in the Appendix. Note that Property (P∗4)(P 4) given in Lemma 7 implies the above property. In fact, since ℬ(s)=(ℬ(s)∩(S∖E))∪(ℬ(s)∩E)⊆(S∖E)∪(ℬ(s)∩E)B(s)= (B(s)∩(S E) )∪ (B(s)∩ E ) (S E)∪ (B(s)∩ E ), taking F in (P∗4)(P 4) to be ℬ(s)∩EB(s)∩ E we get the above property. if ℬ(s)∩E≠∅ then ⋃s′∈ℬ(s)f(s′,E)⊆B(s)∩Eif B(s)∩ E≠ \, then _s (s)f(s ,E)\, \,B(s)∩ E we can see that the AGM theory requires that (letting E=‖ϕ‖E=\|φ\|) the revised beliefs be concentrated on the ϕφ-states in ℬ(s)B(s), while the strong version of KM update allows the revised beliefs to include ϕφ-states outside of ℬ(s)B(s). On the other hand, there is no difference between the two theories when the informational input ϕφ is initially disbelieved, that is, when the agent initially believes ¬ϕ φ. 5 Conclusion As remarked in [4], translating the AGM axioms of belief revision and the KM axioms of belief update into modal formulas has the advantage of unifying the treatment of belief, belief revision and belief update under the same umbrella. Starting with Hintikka’s [6] seminal contribution, the notion of belief has been studied within the context of modal logic, which allows one to express properties such as positive introspection of beliefs (Bϕ→BBϕBφ→ Bφ), negative introspection of beliefs (¬Bϕ→B¬Bϕ Bφ→ B Bφ), the relationship between knowledge and belief, etc. The modal AGM axioms and KM axioms listed in Figures 3 and 4 are restricted axioms in that the formulas ϕφ, ψ and χ that appear in them are required to be Boolean. Some of those axioms involve some nesting of the operators, such as B(ϕ>ψ)B(φ>ψ). Logic ℒL opens the door to investigating properties of belief change that go beyond those considered in the AGM theory and the KM theory. For example, one can investigate introspection properties for suppositional beliefs: B(ϕ>ψ)→BB(ϕ>ψ)B(φ>ψ)→ B(φ>ψ) and ¬B(ϕ>ψ)→B¬B(ϕ>ψ) B(φ>ψ)→ B B(φ>ψ). Other nestings of the operators that go beyond those considered in Figures 3 and 4 may also be worth considering, such as B(Bϕ>Bψ)B(Bφ>Bψ) (the agent believes that if she were to believe ϕφ then she would believe ψ) or B(ϕ>(ψ>χ))B (φ>(ψ>χ) ) (the agent believes that if ϕφ were the case then if ψ were the case then χ would be the case). Perhaps some of these more complex formulas will turn out to be useful in characterizing the notions of iterated belief revision or iterated belief update. The main result of this paper is that the modal logic ℒKML_KM of KM belief update is contained in the modal logic ℒAGML_AGM of AGM belief revision, thus highlighting the fact that there is no conceptual difference between the two notions: one is merely a special case of the other. Furthermore, if one focuses on the strong version of KM belief update, then the difference between the two theories can be narrowed down to the different ways in which they deal with unsurprising information (that is, with formulas ϕφ that were not initially disbelieved), while there is no difference in how the two treat surprising information, that is, information that contradicts the initial beliefs. Appendix A Proofs Lemma 1. (K⋄7s)(K 7s) follows from (K⋄7)(K 7) and (K⋄8)(K 8). Proof. By (K⋄8)(K 8) (recall the assumption that K is consistent so that ⟦K⟧≠∅ K ≠ ), K⋄ϕ∩K⋄ψ=(⋂w∈⟦K⟧(w⋄ϕ))∩(⋂w∈⟦K⟧(w⋄ψ))=⋂w∈⟦K⟧((w⋄ϕ)∩(w⋄ψ)) array[]lK φ\,∩\,K ψ&=& ( _w∈ K (w φ ) )\,∩\, ( _w∈ K (w ψ ) )\\[24.0pt] &=& _w∈ K ( (w φ )\,∩\, (w ψ ) ) array (1) By (K⋄7)(K 7) (since every MCS is complete), for every w∈⟦K⟧w∈ K , (w⋄ϕ)∩(w⋄ψ)⊆w⋄(ϕ∨ψ) (w φ )\,∩\, (w ψ )\, \,w (φ ψ); thus, ⋂w∈⟦K⟧((w⋄ϕ)∩(w⋄ψ))⊆⋂w∈⟦K⟧w⋄(ϕ∨ψ) _w∈ K ( (w φ )\,∩\, (w ψ ) )\, \, _w∈ K w (φ ψ) (2) It follows from (1) and (2) that (K⋄ϕ∩K⋄ψ)⊆⋂w∈⟦K⟧w⋄(ϕ∨ψ) (K φ∩ K ψ )\, \, _w∈ K w (φ ψ) (3) and by (K⋄8)(K 8) ⋂w∈⟦K⟧w⋄(ϕ∨ψ)=K⋄(ϕ∨ψ) _w∈ K w (φ ψ)\ =\,K (φ ψ) (4) Thus, by (3) and (4), K⋄ϕ∩K⋄ψ⊆K⋄(ϕ∨ψ)K φ\,∩\,K ψ\, \,K (φ ψ) ∎ Proofs of the semantic characterizations listed in Figure 1. The correspondence for - (K⋄1)(K 1) is proved in [4, p.4] (since (K⋄1)(K 1) coincides with AGM axiom (K∗2)(K 2)). - (K⋄3b)(K 3b) is proved in [4, p.4] (since (K⋄3b)(K 3b) coincides with AGM axiom (K∗5b)(K 5b)). - (K⋄5)(K 5) is proved in Proposition 3 in [3].171717The characterization there was proved for a differently worded property, namely∀G∈2S, if ⋃s′∈ℬ(s)f(s′,E∩F)⊆G then ⋃s′∈ℬ(s)(f(s′,E)∩F)⊆G∀ G∈ 2^S, if _s (s)f(s ,E∩ F) G then _s (s)(f(s ,E)∩ F) G. It is straightforward to verify that this property is equivalent to property (P⋄5∗7)(P^*7_ 5) in Figure 1. Thus we only need to prove the characterization for (K⋄2)(K 2), (K⋄6w)(K 6w) and (K⋄7s)(K 7s), which is done in the following three propositions.181818A weaker property than (P⋄2)(P 2) (where in the consequent ’⊆ ’ was used instead of ’==’) was sufficient in [3] to characterize (K⋄2)(K 2) because in that paper the definition of frame, unlike in this paper, included the property of Weak Centering: if s∈Es∈ E then s∈f(s,E)s∈ f(s,E). Proposition 2. Frame property (P⋄2)∀s∈S,∀E∈2S∖∅,if ℬ(s)⊆E then⋃s′∈ℬ(s)f(s′,E)=ℬ(s)(P 2) ∀ s∈ S,∀ E∈ 2^S ,\,if B(s) E then _s (s)f(s ,E)\,=\,B(s) characterizes the following KM axiom: (K⋄2)if ϕ∈K then K⋄ϕ=K(K 2) φ∈ K then K φ=K. Proof. (A) Fix an arbitrary model based on a frame that satisfies Property (P⋄2)(P 2), an arbitrary state s∈Ss∈ S and let ⋄ be the partial belief change function based on KsK_s defined by (RI). Let ϕ∈Φ0φ∈ _0 be such that ϕ∈Ksφ∈ K_s, that is, ℬ(s)⊆‖ϕ‖B(s) \|φ\| (thus, by seriality of ℬB, ‖ϕ‖≠∅\|φ\|≠ ). We need to show that, for every formula ψ∈Φ0ψ∈ _0, ψ∈K⋄ϕψ∈ K φ if and only if ψ∈Kψ∈ K, that is, ⋃s′∈ℬ(s)f(s′,‖ϕ‖)⊆‖ψ‖ _s (s)f(s ,\|φ\|) \|ψ\| if and only if ℬ(s)⊆‖ψ‖B(s) \|ψ\| . This is an immediate consequence of (P⋄2)(P 2) with E=∥ϕ∥)E=\|φ\|). (B) Conversely, fix a frame that violates Property (P⋄2)(P 2). Then there exist s∈Ss∈ S and E∈2SE∈ 2^S such that ℬ(s)⊆EB(s) E (thus, by seriality of ℬB, E≠∅E≠ ) but ⋃s′∈ℬ(s)f(s′,E)≠ℬ(s) _s (s)f(s ,E) (s). Two cases are possible. CASE 1: ⋃s′∈ℬ(s)f(s′,E)⊈ℬ(s) _s (s)f(s ,E) (s). Let p,q∈Atp,q∈ At be atomic formulas and construct a model where ‖p‖=E\|p\|=E and ‖q‖=ℬ(s)\|q\|=B(s). Then, since ℬ(s)⊆E=‖p‖B(s) E=\|p\|, p∈Ksp∈ K_s and, since ℬ(s)⊆‖q‖B(s) \|q\|, q∈Ksq∈ K_s but, since ⋃s′∈ℬ(s)f(s′,‖p‖)⊈‖q‖ _s (s)f(s ,\|p\|) \|q\|, q∉Ks⋄pq∉ K_s p. Hence Ks⋄p≠KsK_s p≠ K_s. CASE 2: ℬ(s)⊈⋃s′∈ℬ(s)f(s′,‖p‖)B(s) _s (s)f(s ,\|\ p\|). Let p,q∈Atp,q∈ At be atomic formulas and construct a model where ‖p‖=E\|p\|=E and ‖q‖=⋃s′∈ℬ(s)f(s′,E)\|q\|= _s (s)f(s ,E). Then, p∈Ksp∈ K_s and q∈Ks⋄pq∈ K_s p but q∉Ksq∉ K_s, so that Ks⋄p≠KsK_s p≠ K_s. ∎ Proposition 3. Frame property (P⋄6w)∀s∈S,∀E,F∈2S with E∩F≠∅if ⋃s′∈ℬ(s)f(s′,E)⊆F and⋃s′∈ℬ(s)f(s′,F)⊆Ethen ⋃s′∈ℬ(s)f(s′,E)=⋃s′∈ℬ(s)f(s′,F)(P 6w) array[]l∀ s∈ S,∀ E,F∈ 2^S with E∩ F≠ \\[8.0pt] if _s (s)f(s ,E) F and _s (s)f(s ,F) E\\[16.0pt] then _s (s)f(s ,E)\,\,=\, _s (s)f(s ,F) array characterizes the following KM axiom: (K⋄6w)If ψ∈K⋄ϕ and ϕ∈K⋄ψ and ⊤∈K⋄(ϕ∧ψ) then K⋄ϕ=K⋄ψ(K 6w) ψ∈ K φ and φ∈ K ψ and ∈ K (φ ψ) then K φ=K ψ Proof. Fix a frame that satisfies property (P⋄6w)(P 6w), an arbitrary model M based on it and an arbitrary state s∈Ss∈ S and let ⋄ be the belief change function defined by (RI). Let ϕ,ψ,(ϕ∧ψ)∈Φ0φ,ψ,(φ ψ)∈ _0 be in the domain of ⋄ (hence ‖ϕ∧ψ‖≠∅\|φ ψ\|≠ and thus ‖ϕ‖≠∅\|φ\|≠ and ‖ψ‖≠∅\|ψ\|≠ ) and suppose that ψ∈Ks⋄ϕψ∈ K_s φ and ϕ∈Ks⋄ψφ∈ K_s ψ (note that, by Remark 2, ⊤∈K⋄(ϕ∧ψ) ∈ K (φ ψ) ). Then, ⋃s′∈ℬ(s)f(s′,‖ϕ‖)⊆‖ψ‖ _s (s)f(s ,\|φ\|) \|ψ\| and ⋃s′∈ℬ(s)f(s′,‖ψ‖)⊆‖ϕ‖ _s (s)f(s ,\|ψ\|) \|φ\| and thus, by Property (P⋄6w)(P 6w) (with E=‖ϕ‖E=\|φ\| and F=‖ψ‖F=\|ψ\|; note that ‖ϕ‖∩‖ψ‖=‖ϕ∧ψ‖≠∅\|φ\|∩\|ψ\|=\|φ ψ\|≠ ) ⋃s′∈ℬ(s)f(s′,‖ϕ‖)=⋃s′∈ℬ(s)f(s′,‖ψ‖) _s (s)f(s ,\|φ\|)= _s (s)f(s ,\|ψ\|) (5) It follows from (5) that, for every χ∈Φ0χ∈ _0, χ∈Ks⋄ϕχ∈ K_s φ if and only if χ∈Ks⋄ψχ∈ K_s ψ, that is, Ks⋄ϕ=Ks⋄ψK_s φ=K_s ψ Conversely, fix a frame that violates property (P⋄6w)(P 6w). Then there exist s∈Ss∈ S and E,F∈2SE,F∈ 2^S such that E∩F≠∅E∩ F≠ , ⋃s′∈ℬ(s)f(s′,E)⊆F _s (s)f(s ,E) F and ⋃s′∈ℬ(s)f(s′,F)⊆E _s (s)f(s ,F) E but ⋃s′∈ℬ(s)f(s′,E)≠⋃s′∈ℬ(s)f(s′,F) _s (s)f(s ,E)≠ _s (s)f(s ,F) Two cases are possible: CASE 1: ⋃s′∈ℬ(s)f(s′,E)⊈⋃s′∈ℬ(s)f(s′,F) _s (s)f(s ,E)\, \, _s (s)f(s ,F). CASE 2: ⋃s′∈ℬ(s)f(s′,F)⊈⋃s′∈ℬ(s)f(s′,E) _s (s)f(s ,F)\, \, _s (s)f(s ,E). In Case 1, let p,q,r∈Atp,q,r∈ At be atomic sentences and construct a model based on this frame where ‖p‖=E\|p\|=E, ‖q‖=F\|q\|=F and ‖r‖=⋃s′∈ℬ(s)f(s′,F)\|r\|= _s (s)f(s ,F). Then, since ⋃s′∈ℬ(s)f(s′,‖p‖)⊆‖q‖ _s (s)f(s ,\|p\|) \|q\|, q∈Ks⋄pq∈ K_s p and, since ⋃s′∈ℬ(s)f(s′,‖q‖)⊆‖p‖ _s (s)f(s ,\|q\|) \|p\|, p∈Ks⋄qp∈ K_s q and, since ‖p∧q‖≠∅\|p q\|≠ , ⊤∈K⋄(p∧q) ∈ K (p q) (see Remark 2). Furthermore, r∈Ks⋄qr∈ K_s q, but, since ⋃s′∈ℬ(s)f(s′,∥p∥))⊈∥r∥ _s (s)f(s ,\|p\|))\, \,\|r\|, r∉Ks⋄pr∉ K_s p. Thus Ks⋄p≠Ks⋄qK_s p≠ K_s q. In Case 2, let p,q,r∈Atp,q,r∈ At be atomic sentences and construct a model based on this frame where ‖p‖=E\|p\|=E, ‖q‖=F\|q\|=F and ‖r‖=⋃s′∈ℬ(s)f(s′,E)\|r\|= _s (s)f(s ,E). Then, q∈Ks⋄pq∈ K_s p and p∈Ks⋄qp∈ K_s q and r∈Ks⋄pr∈ K_s p and (since ‖p∧q‖≠∅\|p q\|≠ ) ⊤∈K⋄(p∧q) ∈ K (p q) (see Remark 2) but, since ⋃s′∈ℬ(s)f(s′,∥q∥))⊈∥r∥ _s (s)f(s ,\|q\|))\, \,\|r\|, r∉Ks⋄qr∉ K_s q. Thus Ks⋄p≠Ks⋄qK_s p≠ K_s q. ∎ Proposition 4. Frame property (P⋄7s)∀s∈S,∀E,F∈2S∖∅⋃s′∈ℬ(s)f(s′,E∪F)⊆(⋃s′∈ℬ(s)f(s′,E))∪(⋃s′∈ℬ(s)f(s′,F))(P 7s) array[]l∀ s∈ S,∀ E,F∈ 2^S \\[4.0pt] _s (s)f(s ,E∪ F)\, \, ( _s (s)f(s ,E) )\,\,∪\, ( _s (s)f(s ,F) ) array characterizes the following KM axiom: (K⋄7s)(K⋄ϕ)∩(K⋄ψ)⊆K⋄(ϕ∨ψ)(K 7s) (K φ)∩(K ψ) K (φ ψ) Proof. Fix a frame that satisfies property (P⋄7s)(P 7s), an arbitrary model based on it, an arbitrary state s∈Ss∈ S and let ⋄ be the partial belief change function based on KsK_s defined by (RI). Let ϕ,ψ∈Φ0φ,ψ∈ _0 be in the domain of ⋄ (thus ‖ϕ‖≠∅\|φ\|≠ and ‖ψ‖≠∅\|ψ\|≠ ) and fix an arbitrary χ∈(Ks⋄ϕ)∩(Ks⋄ψ)χ∈(K_s φ)∩(K_s ψ). Then, by (RI), ⋃s′∈ℬ(s)f(s′,‖ϕ‖)⊆‖χ‖ _s (s)f(s ,\|φ\|) \|χ\| and ⋃s′∈ℬ(s)f(s′,‖ψ‖)⊆‖χ‖ _s (s)f(s ,\|ψ\|) \|χ\| and thus, by Property (P⋄7s)(P 7s) (with E=‖ϕ‖E=\|φ\| and F=‖ψ‖F=\|ψ\|) and the fact that ‖ϕ‖∪‖ψ‖=‖ϕ∨ψ‖\|φ\|∪\|ψ\|=\|φ ψ\|, ⋃s′∈ℬ(s)f(s′,‖ϕ∨ψ‖)⊆‖χ‖ _s (s)f(s ,\|φ ψ\|) \|χ\|, that is, by (RI), χ∈Ks⋄(ϕ∨ψ)χ∈ K_s (φ ψ). Conversely, fix a frame that violates property (P⋄7s)(P 7s). Then there exist s∈Ss∈ S and E,F∈2S∖∅E,F∈ 2^S such that ⋃s′∈ℬ(s)f(s′,E∪F)⊈⋃s′∈ℬ(s)f(s′,E)∪⋃s′∈ℬ(s)f(s′,F) _s (s)f(s ,E∪ F)\, \, _s (s)f(s ,E)\,\,∪\,\, _s (s)f(s ,F) (6) Let p,q,r∈Atp,q,r∈ At be atomic formulas and construct a model where ‖p‖=E\|p\|=E, ‖q‖=F\|q\|=F and ‖r‖=⋃s′∈ℬ(s)f(s′,E)∪⋃s′∈ℬ(s)f(s′,F)\|r\|= _s (s)f(s ,E)\,\,∪\,\, _s (s)f(s ,F). Then, by (6) (since ‖p‖∪‖q‖=‖p∨q‖\|p\|∪\|q\|=\|p q\|), ⋃s′∈ℬ(s)f(s′,‖p∨q‖)⊈‖r‖ _s (s)f(s ,\|p q\|) \|r\| and thus, by (RI), r∉Ks⋄(p∨q)r∉ K_s (p q). On the other hand, since ⋃s′∈ℬ(s)f(s′,‖p‖)⊆‖r‖ _s (s)f(s ,\|p\|) \|r\| and ⋃s′∈ℬ(s)f(s′,‖q‖)⊆‖r‖ _s (s)f(s ,\|q\|) \|r\|, r∈K⋄pr∈ K p and r∈K⋄qr∈ K q, yielding a violation of axiom (K⋄7s)(K 7s). ∎ Proofs of the syntactic characterizations listed in Figure 2. The characterizations of (A⋄1∗2)(A^*2_ 1), (A⋄3b∗5b)(A^*5b_ 3b) and (A⋄5∗7)(A^*7_ 5) are proved in [4].191919Since (K⋄1)(K 1) coincides with AGM axiom (K∗2)(K 2), (K⋄3b)(K 3b) coincides with AGM axiom (K∗5b)(K 5b) and (K⋄5)(K 5) coincides with AGM axiom (K∗7)(K 7). For (A⋄2)(A 2), (A⋄6w)(A 6w) and (A⋄7s)(A 7s) the proofs are given in the following three propositions. Proposition 5. The modal formula (A⋄2)Bϕ→(Bψ)↔B(ϕ>ψ))(A 2) Bφ\,→\, (Bψ) B(φ>ψ) ) is characterized by the following property of frames: (P⋄2)∀s∈S,∀E∈2S∖∅, if ℬ(s)⊆E, then ⋃s′∈ℬ(s)f(s′,E)=ℬ(s) array[]l(P 2)&∀ s∈ S,∀ E∈ 2^S , if B(s) E, then _s (s)f(s ,E)=B(s) array Proof. (A) Fix an arbitrary model based on a frame that satisfies Property (P⋄2)(P 2), an arbitrary state s∈Ss∈ S and an arbitrary formula ϕ∈Φ0φ∈ _0 and suppose that s⊧Bϕs Bφ, that is, ℬ(s)⊆‖ϕ‖B(s) \|φ\| (thus, by seriality of ℬB, ‖ϕ‖≠∅\|φ\|≠ ). We need to show that, for every formula ψ∈Φ0ψ∈ _0, s⊧Bψ↔B(ϕ>ψ)s Bψ B(φ>ψ), that is, s⊧Bψs Bψ if and only if s⊧B(ϕ>ψ)s B(φ>ψ). By Property (P⋄2)(P 2) (with E=‖ϕ‖E=\|φ\|), ⋃s′∈ℬ(s)f(s′,‖ϕ‖)=ℬ(s) _s (s)f(s ,\|φ\|)=B(s) and thus, ℬ(s)⊆‖ψ‖B(s) \|ψ\| (that is, s⊧Bψs Bψ) if and only if ⋃s′∈ℬ(s)f(s′,‖ϕ‖)⊆‖ψ‖ _s (s)f(s ,\|φ\|) \|ψ\| (that is s⊧B(ϕ>ψ)s B(φ>ψ)). (B) Fix a frame that violates property (P⋄2)(P 2). Then there exist a state s∈Ss∈ S and an event E⊆SE S such that (a) ℬ(s)⊆EB(s) E, (b) ⋃s′∈ℬ(s)f(s′,E)≠ℬ(s) _s (s)f(s ,E) (s). Two cases are possible. CASE 1: ⋃s′∈ℬ(s)f(s′,E)⊈ℬ(s) _s (s)f(s ,E) (s). Let p,q∈Atp,q∈ At be atomic formulas and construct a model where ‖p‖=E\|p\|=E and ‖q‖=ℬ(s)\|q\|=B(s). Then s⊧Bps Bp and s⊧Bqs Bq but, since ⋃s′∈ℬ(s)f(s′,‖p‖)⊈‖q‖ _s (s)f(s ,\|p\|) \|q\|, s⊧̸B(p>q)s B(p>q) so that s⊧̸(Bq↔B(p>q)s (Bq B(p>q). Hence s⊧̸Bp→(Bq↔B(p>q))s Bp→ (Bq B(p>q) ). CASE 2: ℬ(s)⊈⋃s′∈ℬ(s)f(s′,E)B(s) _s (s)f(s ,E). Let p,q∈Atp,q∈ At be atomic formulas and construct a model where ‖p‖=E\|p\|=E and ‖q‖=⋃s′∈ℬ(s)f(s′,E)=⋃s′∈ℬ(s)f(s′,‖p‖)\|q\|= _s (s)f(s ,E)= _s (s)f(s ,\|p\|). Then, s⊧Bps Bp and s⊧B(p>q)s B(p>q) but, since ℬ(s)⊈‖q‖B(s) \|q\|, s⊧̸qs q so that s⊧̸Bp→(Bq↔B(p>q))s Bp→ (Bq B(p>q) ). ∎ Proposition 6. The modal formula (A⋄6w)¬□¬(ϕ∧ψ)∧B(ϕ>ψ)∧B(ψ>ϕ)→(B(ϕ>χ)↔B(ψ>χ)) array[]l(A 6w)& (φ ψ) B(φ>ψ) B(ψ>φ)\\[10.0pt] &→ (B(φ>χ) B(ψ>χ) ) array is characterized by the following property of frames: (P⋄6w)∀s∈S,∀E,F∈2S with E∩F≠∅, if ⋃s′∈ℬ(s)f(s′,E)⊆Fand ⋃s′∈ℬ(s)f(s′,F)⊆E then ⋃s′∈ℬ(s)f(s′,E)=⋃s′∈ℬ(s)f(s′,F)\ array[]l(P 6w)&∀ s∈ S,∀ E,F∈ 2^S with E∩ F≠ ,\, if _s (s)f(s ,E) F\\[12.0pt] &and _s (s)f(s ,F) E\, then _s (s)f(s ,E)= _s (s)f(s ,F) array Proof. (A) Fix an arbitrary model based on a frame that satisfies Property (P⋄6w)(P 6w), an arbitrary state s∈Ss∈ S and arbitrary formulas ϕ,ψ,χ∈Φ0φ,ψ,χ∈ _0 and suppose that s⊧¬□¬(ϕ∧ψ)∧B(ϕ>ψ)∧B(ψ>ϕ)s (φ ψ) B(φ>ψ) B(ψ>φ), that is, ‖ϕ∧ψ‖≠∅\|φ ψ\|≠ (and thus ‖ϕ‖≠∅\|φ\|≠ and ‖ψ‖≠∅\|ψ\|≠ ), ⋃s′∈ℬ(s)f(s′,‖ϕ‖)⊆‖ψ‖ _s (s)f(s ,\|φ\|) \|ψ\| and ⋃s′∈ℬ(s)f(s′,‖ψ‖)⊆‖ϕ‖ _s (s)f(s ,\|ψ\|) \|φ\|. We need to show that s⊧B(ϕ>χ)↔B(ψ>χ)s B(φ>χ) B(ψ>χ). By Property (P⋄6w)(P 6w) (with E=‖ϕ‖E=\|φ\| and F=‖ψ‖F=\|ψ\| so that E∩F=‖ϕ‖∩‖ψ‖=‖ϕ∧ψ‖≠∅E∩ F=\|φ\|∩\|ψ\|=\|φ ψ\|≠ ), ⋃s′∈ℬ(s)f(s′,‖ϕ‖)=⋃s′∈ℬ(s)f(s′,‖ψ‖) _s (s)f(s ,\|φ\|)= _s (s)f(s ,\|ψ\|) (7) Suppose that s⊧B(ϕ>χ)s B(φ>χ). Then ⋃s′∈ℬ(s)f(s′,‖ϕ‖)⊆‖χ‖ _s (s)f(s ,\|φ\|) \|χ\| and thus, by (7), ⋃s′∈ℬ(s)f(s′,‖ψ‖)⊆‖χ‖ _s (s)f(s ,\|ψ\|) \|χ\|, that is, s⊧B(ψ>χ)s B(ψ>χ). Conversely, suppose that s⊧B(ψ>χ)s B(ψ>χ). Then ⋃s′∈ℬ(s)f(s′,‖ψ‖)⊆‖χ‖ _s (s)f(s ,\|ψ\|) \|χ\| and thus, by (7), ⋃s′∈ℬ(s)f(s′,‖ϕ‖)⊆‖χ‖ _s (s)f(s ,\|φ\|) \|χ\|, that is, s⊧B(ϕ>χ)s B(φ>χ). Thus, s⊧B(ϕ>χ)↔B(ψ>χ)s B(φ>χ) B(ψ>χ). (B) Conversely, fix a frame that violates Property (P⋄6w)(P 6w). Then there exist s∈Ss∈ S, E,F∈2S with E∩F≠∅E,F∈ 2^S with E∩ F≠ such that ⋃s′∈ℬ(s)f(s′,E)⊆F _s (s)f(s ,E) F and ⋃s′∈ℬ(s)f(s′,F)⊆E _s (s)f(s ,F) E but ⋃s′∈ℬ(s)f(s′,E)≠⋃s′∈ℬ(s)f(s′,F) _s (s)f(s ,E)≠ _s (s)f(s ,F). One of the following two cases must hold. Case 1: ⋃s′∈ℬ(s)f(s′,E)⊈⋃s′∈ℬ(s)f(s′,F) _s (s)f(s ,E) _s (s)f(s ,F), or Case 2: ⋃s′∈ℬ(s)f(s′,F)⊈⋃s′∈ℬ(s)f(s′,E) _s (s)f(s ,F) _s (s)f(s ,E). In Case 1 let p, q and r be atomic formulas and construct a model where ‖p‖=E\|p\|=E, ‖q‖=F\|q\|=F and ‖r‖=⋃s′∈ℬ(s)f(s′,F)\|r\|= _s (s)f(s ,F). Since ∅≠‖p‖∩‖q‖=‖p∧q‖ ≠\|p\|∩\|q\|=\|p q\|, s⊧¬□¬(p∧q)s (p q); furthermore, s⊧B(p>q)∧B(q>p)∧B(q>r)s B(p>q) B(q>p) B(q>r) but s⊧̸B(p>r)s B(p>r). In Case 2 construct a model where ‖p‖=E\|p\|=E, ‖q‖=F\|q\|=F and ‖r‖=⋃s′∈ℬ(s)f(s′,E)\|r\|= _s (s)f(s ,E). Again, since ∅≠‖p‖∩‖q‖=‖p∧q‖ ≠\|p\|∩\|q\|=\|p q\|, s⊧¬□¬(p∧q)s (p q); furthermore, s⊧B(p>q)∧B(q>p)∧B(p>r)s B(p>q) B(q>p) B(p>r) but s⊧̸B(q>r)s B(q>r). ∎ Proposition 7. The modal formula (A⋄7s)¬□¬ϕ∧¬□¬ψ∧B(ϕ>χ)∧B(ψ>χ)→B((ϕ∨ψ)>χ) array[]l(A 7s)& φ ψ B(φ>χ) B(ψ>χ)\\[10.0pt] &→ B ((φ ψ)>χ ) array is characterized by the following property of frames: (P⋄7s)∀s∈S,∀E,F∈2S∖∅⋃s′∈ℬ(s)f(s′,E∪F)⊆(⋃s′∈ℬ(s)f(s′,E))∪(⋃s′∈ℬ(s)f(s′,F)) array[]l(P 7s)&∀ s∈ S,∀ E,F∈ 2^S \\[8.0pt] & _s (s)f(s ,E∪ F)\, \, ( _s (s)f(s ,E) )\,\,∪\, ( _s (s)f(s ,F) ) array Proof. Fix a frame that satisfies property (P⋄7s)(P 7s), an arbitrary model based on it, an arbitrary state s∈Ss∈ S and arbitrary ϕ,ψ,χ∈Φ0φ,ψ,χ∈ _0 and assume that s⊧¬□¬ϕ∧¬□¬ψ∧B(ϕ>χ)∧B(ψ>χ)s φ ψ B(φ>χ) B(ψ>χ). Then ‖ϕ‖≠∅\|φ\|≠ , ‖ψ‖≠∅\|ψ\|≠ , ⋃s′∈ℬ(s)f(s′,‖ϕ‖)⊆‖χ‖ _s (s)f(s ,\|φ\|) \|χ\| and ⋃s′∈ℬ(s)f(s′,‖ψ‖)⊆‖χ‖ _s (s)f(s ,\|ψ\|) \|χ\|. Thus, by property (P⋄7s)(P 7s) (with E=‖ϕ‖E=\|φ\| and F=‖ψ‖F=\|ψ\| and using the fact that ‖ϕ‖∪‖ψ‖=‖ϕ∨ψ‖\|φ\|∪\|ψ\|=\|φ ψ\|), ⋃s′∈ℬ(s)f(s′,‖ϕ∨ψ‖)⊆‖χ‖ _s (s)f(s ,\|φ ψ\|) \|χ\|, so that s⊧B((ϕ∨ψ)>χ)s B ((φ ψ)>χ ). Conversely, fix a frame that violates property (P⋄7s)(P 7s). Then there exist s,∈Ss,∈ S and E,F∈2S∖∅E,F∈ 2^S such that ⋃s′∈ℬ(s)f(s′,E∪F)⊈⋃s′∈ℬ(s)f(s′,E)∪⋃s′∈ℬ(s)f(s′,F) _s (s)f(s ,E∪ F)\, \, _s (s)f(s ,E)\,\,∪\,\, _s (s)f(s ,F) (8) Let p,q,r∈Atp,q,r∈ At be atomic formulas and construct a model where ‖p‖=E\|p\|=E, ‖q‖=F\|q\|=F and ‖r‖=⋃s′∈ℬ(s)f(s′,E)∪⋃s′∈ℬ(s)f(s′,F)\|r\|= _s (s)f(s ,E)\,\,∪\,\, _s (s)f(s ,F). Then, since ‖p‖≠∅\|p\|≠ and ‖q‖≠∅\|q\|≠ , s⊧¬□¬p∧¬□¬qs p q; furthermore, s⊧B(p>r)∧B(q>r)s B(p>r) B(q>r). On the other hand, since (noting that ‖p‖∪‖q‖=‖p∨q‖\|p\|∪\|q\|=\|p q\|) ⋃s′∈ℬ(s)f(s′,‖p∨q‖)⊈‖r‖ _s (s)f(s ,\|p q\|)\, \,\|r\|, s⊧̸B((p∨q)>r)s B ((p q)>r ), yielding a violation of axiom (A⋄7s)(A 7s). ∎ Proof of Proposition 1. Every axiom of ℒKML_KM is a theorem of ℒAGML_AGM. Since some of the AGM axioms coincide with KM axioms, we only need to prove that (A⋄2)(A 2), (A⋄6w)(A 6w) and (A⋄7s)(A 7s) are theorems of ℒAGML_AGM. This is done in the following three lemmas. In the proofs ’PL’ stands for ’Propositional Logic’. Lemma 4. The following modal KM axiom: (A⋄2)Bϕ→(Bψ↔B(ϕ>ψ))(A 2) Bφ\,→\, (Bψ B(φ>ψ) ) is a theorem of ℒAGML_AGM. Proof. We first prove that Bϕ→(Bψ→B(ϕ>ψ))Bφ\,→\, (Bψ→ B(φ>ψ) ) is a theorem of ℒAGML_AGM. 1.Bϕ→¬B¬ϕaxiom DB2.ψ→(ϕ→ψ)tautology3.Bψ→B(ϕ→ψ)rule (RMB)4.(Bϕ∧Bψ)→(¬B¬ϕ∧B(ϕ→ψ))1, 3, PL5.(¬B¬ϕ∧B(ϕ→ψ))→B(ϕ>ψ)AGM axiom (A∗4)6.(Bϕ∧Bψ)→B(ϕ>ψ)4, 5, PL.7.Bϕ→(Bψ→B(ϕ>ψ))6, PL array[]l1.&Bφ→ B φ&axiom D_B\\ 2.&ψ→(φ→ψ)&tautology\\ 3.&Bψ→ B (φ→ψ )&rule (RM_B)\\ 4.&(Bφ Bψ)→ ( B φ B(φ→ψ) )&1, 3, PL\\ 5.& ( B φ B(φ→ψ) )→ B(φ>ψ)&AGM axiom (A*4)\\ 6.&(Bφ Bψ)→ B(φ>ψ)&4, 5, PL.\\ 7.&Bφ\,→\, (Bψ→ B(φ>ψ) )&6, PL array Next we prove that Bϕ→(B(ϕ>ψ)→Bψ)Bφ\,→\, (B(φ>ψ)→ Bψ ) is a theorem of ℒAGML_AGM. 8.□¬ϕ→B¬ϕaxiom (NB)9.¬B¬ϕ→¬□¬ϕ8, PL10.Bϕ→¬□¬ϕ1, 9, PL11.(Bϕ∧B(ϕ>ψ))→(¬□¬ϕ∧B(ϕ>ψ))10, PL12.(¬□¬ϕ∧B(ϕ>ψ))→B(ϕ→ψ)AGM axiom (A∗3)13.(Bϕ∧B(ϕ>ψ))→B(ϕ→ψ)11, 12, PL array[]l8.& φ→ B φ&axiom (NB)\\ 9.& B φ→ φ&8, PL\\ 10.&Bφ→ φ&1, 9, PL\\ 11.& (Bφ B(φ>ψ) )\,→\, ( φ B(φ>ψ) )&10, PL\\ 12.& ( φ B(φ>ψ) )→ B(φ→ψ)&AGM axiom (A*3)\\ 13.& (Bφ B(φ>ψ) )\,→\,B(φ→ψ)&11, 12, PL array 14.(Bϕ∧B(ϕ>ψ))→(Bϕ∧B(ϕ→ψ))13, PL15.(Bϕ∧B(ϕ→ψ))→B(ϕ∧(ϕ→ψ))axiom (CB)16.ϕ∧(ϕ→ψ)→ψtautology17.B(ϕ∧(ϕ→ψ))→Bψ16, rule (RMB)18.(Bϕ∧B(ϕ>ψ))→Bψ14, 15, 17, PL19.Bϕ→(B(ϕ>ψ)→Bψ)18, PL array[]l14.& (Bφ B(φ>ψ) )\,→\, (Bφ B(φ→ψ) )&13, PL\\ 15.& (Bφ B(φ→ψ) )\,→\,B (φ (φ→ψ) )&axiom (C_B)\\ 16.&φ (φ→ψ)\,→\,ψ&tautology\\ 17.&B(φ (φ→ψ))\,→\,Bψ&16, rule (RM_B)\\ 18.& (Bφ B(φ>ψ) )\,→\,Bψ&14, 15, 17, PL\\ 19.&Bφ\,→\, (B(φ>ψ)→ Bψ )&18, PL array Axiom (A⋄2)(A 2) follows from lines 7 and 19. ∎ Lemma 5. The following modal KM axiom: (A⋄6w)¬□¬(ϕ∧ψ)∧B(ϕ>ψ)∧B(ψ>ϕ)→(B(ϕ>χ)↔B(ψ>χ))(A 6w) (φ ψ) B(φ>ψ) B(ψ>φ)\,→\, (B(φ>χ) B(ψ>χ) ) is a theorem of ℒAGML_AGM. Proof. First we show that the following formula is a theorem of ℒAGML_AGM: (¬□¬(ϕ∧ψ)∧B(ϕ>ψ))→(B(ϕ>χ)→B((ϕ∧ψ)>χ)) ( (φ ψ) B(φ>ψ) )\,→\, (B(φ>χ)→ B ((φ ψ)>χ) ) 1. ¬□¬(ϕ∧ψ)→¬□¬ϕ (φ ψ)\,→\, φ (C¬□¬)(C_ ) (see Remark 3) 2. (¬□¬(ϕ∧ψ)∧B(ϕ>ψ))→(¬□¬ϕ∧B(ϕ>ψ)) ( (φ ψ) B(φ>ψ) )\,→\, ( φ B(φ>ψ) ) 1, PL 3. (¬□¬ϕ∧B(ϕ>ψ))→¬B(ϕ>¬ψ) ( φ B(φ>ψ) )→ B(φ> ψ) axiom (A⋄3b∗5b)axiom (A^*5b_ 3b) 4. (¬□¬(ϕ∧ψ)∧B(ϕ>ψ))→¬B(ϕ>¬ψ) ( (φ ψ) B(φ>ψ) )\,→\, B(φ> ψ) 2, 3, PL 5. χ→(ψ→χ)χ→(ψ→χ) tautology 6. B(ϕ>χ)→B(ϕ>(ψ→χ))B(φ>χ)→ B (φ>(ψ→χ) ) 5, rule (RMB>)5, rule (RM_B>) (see Remark 3) 7. ¬□¬(ϕ∧ψ)∧B(ϕ>ψ)∧B(ϕ>χ) (φ ψ) B(φ>ψ) B(φ>χ) →¬B(ϕ>¬ψ)∧B(ϕ>(ψ→χ))→\, B(φ> ψ) B (φ>(ψ→χ) ) 4, 6, PL 8. ¬B(ϕ>¬ψ)∧B(ϕ>(ψ→χ)) B(φ> ψ) B (φ>(ψ→χ) ) →B((ϕ∧ψ)>(ψ∧χ))→\,B ((φ ψ)>(ψ χ) ) axiom (A∗8)axiom (A*8) 9. ¬□¬(ϕ∧ψ)∧B(ϕ>ψ)∧B(ϕ>χ) (φ ψ) B(φ>ψ) B(φ>χ) →B((ϕ∧ψ)>(ψ∧χ))→\,B ((φ ψ)>(ψ χ) ) 7, 8, PL 10. (ψ∧χ)→χ(ψ χ)→χ tautology 11. B((ϕ∧ψ)>(ψ∧χ))→B((ϕ∧ψ)>χ)B ((φ ψ)>(ψ χ) )\,→\,B ((φ ψ)>χ ) 10, rule (RMB>)10, rule (RM_B>) (see Remark 3) 12. (¬□¬(ϕ∧ψ)∧B(ϕ>ψ)∧B(ϕ>χ))→B((ϕ∧ψ)>χ) ( (φ ψ) B(φ>ψ) B(φ>χ) )\,→\,B ((φ ψ)>χ ) 9, 11, PL 13. (¬□¬(ϕ∧ψ)∧B(ϕ>ψ))→(B(ϕ>χ)→B((ϕ∧ψ)>χ)) ( (φ ψ) B(φ>ψ) )\,→\, (B(φ>χ)→ B ((φ ψ)>χ ) ) 12, PL Next, repeating steps 1-13 with ϕφ replaced by ψ and with ψ replaced by ϕφ we get 14.(¬□¬(ϕ∧ψ)∧B(ψ>ϕ))→(B(ψ>χ)→B((ϕ∧ψ)>χ)) array[]l14.& ( (φ ψ) B(ψ>φ) )\,→\, (B(ψ>χ)→ B ((φ ψ)>χ ) ) 6.0pt plus 2.0pt minus 2.0pt array The next step is to show that the following is a theorem of ℒAGML_AGM: (¬□¬(ϕ∧ψ)∧B(ϕ>ψ))→(B((ϕ∧ψ)>χ)→B(ϕ>χ)) ( (φ ψ) B(φ>ψ) )\,→\, (B ((φ ψ)>χ )→ B(φ>χ) ) 15. ¬□¬(ϕ∧ψ)∧B((ϕ∧ψ)>χ) (φ ψ) B ((φ ψ)>χ ) →B(ϕ>(ψ→χ))→\,B (φ>(ψ→χ) ) axiom (A∗7)axiom (A*7) 16. ¬□¬(ϕ∧ψ)∧B((ϕ∧ψ)>χ)∧B(ϕ>ψ) (φ ψ) B ((φ ψ)>χ ) B(φ>ψ) →(B(ϕ>ψ)∧B(ϕ>(ψ→χ)))→\, (B(φ>ψ) B (φ>(ψ→χ) ) ) 15, PL 17. (B(ϕ>ψ)∧B(ϕ>(ψ→χ))→B(ϕ>χ) (B(φ>ψ) B(φ>(ψ→χ) )\,→\,B(φ>χ) axiom (A⋄0∗1)axiom (A^*1_ 0) 18. (¬□¬(ϕ∧ψ)∧B(ϕ>ψ)∧B((ϕ∧ψ)>χ))→B(ϕ>χ) ( (φ ψ) B(φ>ψ) B ((φ ψ)>χ ) )\,→\,B(φ>χ) 16, 17, PL 19. (¬□¬(ϕ∧ψ)∧B(ϕ>ψ))→(B((ϕ∧ψ)>χ)→B(ϕ>χ)) ( (φ ψ) B(φ>ψ) )\,→\, (B ((φ ψ)>χ )→ B(φ>χ) ) 18, PL Next, repeating steps 15-19 with ϕφ replaced by ψ and with ψ replaced by ϕφ we get 20.(¬□¬(ϕ∧ψ)∧B(ψ>ϕ))→(B((ϕ∧ψ)>χ)→B(ψ>χ)) array[]l20.& ( (φ ψ) B(ψ>φ) )\,→\, (B ((φ ψ)>χ )→ B(ψ>χ) )& array From 13 and 19 we get 21.(¬□¬(ϕ∧ψ)∧B(ϕ>ψ))→(B((ϕ∧ψ)>χ)↔B(ϕ>χ)) array[]l21.& ( (φ ψ) B(φ>ψ) )\,→\, (B ((φ ψ)>χ ) B(φ>χ) ) array and from 14 and 20 we get 22.(¬□¬(ϕ∧ψ)∧B(ψ>ϕ))→(B((ϕ∧ψ)>χ)↔B(ψ>χ)) array[]l22.& ( (φ ψ) B(ψ>φ) )\,→\, (B ((φ ψ)>χ ) B(ψ>χ) ) array Thus, 23.(¬□¬(ϕ∧ψ)∧B(ϕ>ψ)∧B(ψ>ϕ))→((B((ϕ∧ψ)>χ)↔B(ϕ>χ))∧(B((ϕ∧ψ)>χ)↔B(ψ>χ)))21, 22, PL24.(B((ϕ∧ψ)>χ)↔B(ϕ>χ))∧(B((ϕ∧ψ)>χ)↔B(ψ>χ))→(B(ϕ>χ)↔B(ψ>χ))tautology25.¬□¬(ϕ∧ψ)∧B(ϕ>ψ)∧B(ψ>ϕ)→(B(ϕ>χ)↔B(ψ>χ))23, 24, PL;this is (A⋄6) array[]l23.& ( (φ ψ) B(φ>ψ) B(ψ>φ) )&\\ &→\, ( (B ((φ ψ)>χ ) B(φ>χ) )&\\ & (B ((φ ψ)>χ ) B(ψ>χ) ) )&21, 22, PL\\[6.0pt] 24.& (B ((φ ψ)>χ ) B(φ>χ) ) (B ((φ ψ)>χ ) B(ψ>χ) )&\\[6.0pt] &→\, (B(φ>χ) B(ψ>χ) )&tautology\\[8.0pt] 25.& (φ ψ) B(φ>ψ) B(ψ>φ)&\\[6.0pt] &→\, (B(φ>χ) B(ψ>χ) )&23, 24, PL;\\ &&this is (A 6) array ∎ Lemma 6. The following modal KM axiom: (A⋄7s)¬□¬ϕ∧¬□¬ψ∧B(ϕ>χ)∧B(ψ>χ)→B((ϕ∨ψ)>χ)(A 7s) φ ψ B(φ>χ) B(ψ>χ)\\ → B ((φ ψ)>χ ) is a theorem of ℒAGML_AGM. Proof. First we prove that the following formula is a theorem of ℒAGML_AGM: ¬□¬ϕ∧B(ϕ>χ)→B((ϕ∨ψ)>(ϕ→χ)) φ B(φ>χ)\,→\,B ((φ ψ)>(φ→χ) ) 1. ϕ↔((ϕ∨ψ)∧ϕ)φ ((φ ψ) φ ) tautology 2. B(ϕ>χ)↔B(((ϕ∨ψ)∧ϕ)>χ)B(φ>χ) B ( ((φ ψ) φ )>χ ) 1, rule (R⋄4∗6)1, rule (R^*6_ 4) 3. B(ϕ>χ)→B(((ϕ∨ψ)∧ϕ)>χ)B(φ>χ)→ B ( ((φ ψ) φ )>χ ) 2, PL 4. ϕ→((ϕ∨ψ)∧ϕ)φ→ ((φ ψ) φ ) tautology 5. ¬□¬ϕ→¬□¬((ϕ∨ψ)∧ϕ) φ→ ((φ ψ) φ ) 1, rule (RM¬□¬)1, rule (RM_ ) (see Remark 3)(see Remark REM:derivedAxRul) 6. ¬□¬ϕ∧B(ϕ>χ) φ B(φ>χ) →¬□¬((ϕ∨ψ)∧ϕ)∧B(((ϕ∨ψ)∧ϕ)>χ)→\, ((φ ψ) φ )\, \,B ( ((φ ψ) φ )>χ ) 3,5,PL3,5,PL 7. ¬□¬((ϕ∨ψ)∧ϕ)∧B(((ϕ∨ψ)∧ϕ)>χ) ((φ ψ) φ )\, \,B ( ((φ ψ) φ )>χ ) →B((ϕ∨ψ)>(ϕ→χ))→\,B ((φ ψ)>(φ→χ) ) axiom (A⋄5∗7)axiom (A^*7_ 5) 8. ¬□¬ϕ∧B(ϕ>χ)→B((ϕ∨ψ)>(ϕ→χ)) φ B(φ>χ)\,→\,B ((φ ψ)>(φ→χ) ) 6, 7, PL Repeating steps 1-8 with ϕφ replaced by ψ and ψ by ϕφ we get 9.¬□¬ψ∧B(ψ>χ)→B((ϕ∨ψ)>(ψ→χ))9. ψ B(ψ>χ)\,→\,B ((φ ψ)>(ψ→χ) ) Thus, 10. ¬□¬ϕ∧B(ϕ>χ)∧¬□¬ψ∧B(ψ>χ) φ B(φ>χ) ψ B(ψ>χ) →B((ϕ∨ψ)>(ϕ→χ))∧B((ϕ∨ψ)>(ψ→χ))→\,B ((φ ψ)>(φ→χ) ) B ((φ ψ)>(ψ→χ) ) 8, 9, PL 11. B((ϕ∨ψ)>(ϕ→χ))∧B((ϕ∨ψ)>(ψ→χ))B ((φ ψ)>(φ→χ) ) B ((φ ψ)>(ψ→χ) ) →B((ϕ∨ψ)>(ϕ→χ∧ψ→χ))→ B ((φ ψ)>(φ→χ ψ→χ) ) axiom (CB)axiom (C_B) 12. (ϕ→χ)∧(ψ→χ)→((ϕ∨ψ)→χ)(φ→χ) (ψ→χ)\,→ ((φ ψ)→χ ) tautology 13. B((ϕ∨ψ)>(ϕ→χ∧ψ→χ))B ((φ ψ)>(φ→χ ψ→χ) ) →B((ϕ∨ψ)>((ϕ∨ψ)→χ))→ B ((φ ψ)> ((φ ψ)→χ ) ) 12, rule (RMB>)12, rule (RM_B>) (see Remark 3) 14. ¬□¬ϕ∧B(ϕ>χ)∧¬□¬ψ∧B(ψ>χ) φ B(φ>χ) ψ B(ψ>χ) →B((ϕ∨ψ)>((ϕ∨ψ)→χ))→\,B ((φ ψ)> ((φ ψ)→χ ) ) 10, 11, 13, PL 15. B((ϕ∨ψ)>(ϕ∨ψ))B ((φ ψ)>(φ ψ) ) axiom (A⋄1∗2)axiom (A^*2_ 1) 16. B((ϕ∨ψ)>((ϕ∨ψ)→χ))B ((φ ψ)> ((φ ψ)→χ ) ) →B((ϕ∨ψ)>(ϕ∨ψ))∧B((ϕ∨ψ)>((ϕ∨ψ)→χ))→ B ((φ ψ)>(φ ψ) ) B ((φ ψ)> ((φ ψ)→χ ) ) 15, PL 17. B((ϕ∨ψ)>(ϕ∨ψ))∧B((ϕ∨ψ)>((ϕ∨ψ)→χ))B ((φ ψ)>(φ ψ) ) B ((φ ψ)>((φ ψ)→χ) ) →B((ϕ∨ψ)>χ)→\,B ((φ ψ)>χ ) axiom (A⋄0∗1)axiom (A^*1_ 0) (with ϕ and ψ(with φ and ψ replaced by ϕ∨ψ)replaced by φ ψ) 18. B((ϕ∨ψ)>((ϕ∨ψ)→χ))→B((ϕ∨ψ)>χ)B ((φ ψ)> ((φ ψ)→χ ) )\,→ B ((φ ψ)>χ ) 16, 17, PL 19. ¬□¬ϕ∧B(ϕ>χ)∧¬□¬ϕ∧B(ψ>χ) φ B(φ>χ) φ B(ψ>χ) →B((ϕ∨ψ)>χ)→\,B ((φ ψ)>χ ) 14, 18, PL this is (A⋄7s)this is (A 7s) ∎ Lemma 2. (K⋄9s)(K 9s) follows from (K⋄0)(K 0), (K⋄8)(K 8) and (K⋄9)(K 9). Proof. Fix arbitrary ϕ,ψ∈Φ0φ,ψ∈ _0. By (K⋄8)(K 8) (recall that ⟦K⟧=w∈W:K⊆w K =\w∈ W:K w\) K⋄ϕ=⋂w∈⟦K⟧(w⋄ϕ)K φ\,=\, _w∈ K (w φ) (9) Let A=w∈⟦K⟧:¬ψ∉w⋄ϕA= \w∈ K : ψ∉ w φ \ and B=w∈⟦K⟧:¬ψ∈w⋄ϕB= \w∈ K : ψ∈ w φ \ (clearly ⟦K⟧=A∪B K =A∪ B). Assume that ¬ϕ∉K⋄ϕ φ∉ K φ. Then A≠∅A≠ . First note that ∀w∈B,(w⋄ϕ)+ψ=Φ0; thus, ⋂w∈B((w⋄ϕ)+ψ)=Φ0∀ w∈ B,\,(w φ)+ψ= _0; thus, _w∈ B ((w φ)+ψ )= _0 (10) It follows from (10) that ⋂w∈⟦K⟧((w⋄ϕ)+ψ)=⋂w∈A((w⋄ϕ)+ψ)∩Φ0=⋂w∈A((w⋄ϕ)+ψ) _w∈ K ((w φ)+ψ )= _w∈ A ((w φ)+ψ )\,∩\, _0= _w∈ A ((w φ)+ψ ) (11) By (K⋄9)(K 9) (since each w is complete), ∀w∈A,(w⋄ϕ)+ψ⊆w⋄(ϕ∧ψ)∀ w∈ A, (w φ)+ψ\, \,w (φ ψ) (12) Next, note that, by (K⋄0)(K 0) (which ensures that K⋄ϕ=Cn(K⋄ϕ)K φ=Cn (K φ ) and w⋄ϕ=Cn(w⋄ϕ)w φ=Cn (w φ )) and (9),202020Since K⋄ϕK φ is deductively closed, for every χ∈Φ0χ∈ _0, χ∈K⋄ϕ+ψχ∈ K φ+ψ if and only if (ψ→χ)∈K⋄ϕ(ψ→χ)∈ K φ. Since, ∀w∈W∀ w∈ W, w⋄ϕw φ is deductively closed, ⋂w∈⟦K⟧(w⋄ϕ) _w∈ K (w φ) is deductively closed and thus χ∈(⋂w∈⟦K⟧(w⋄ϕ))+ψχ∈ ( _w∈ K (w φ) )+ψ if and only if (ψ→χ)∈⋂w∈⟦K⟧(w⋄ϕ)(ψ→χ)∈ _w∈ K (w φ) if and only if χ∈⋂w∈⟦K⟧(w⋄ϕ+ψ)χ∈ _w∈ K (w φ+ψ ). (K⋄ϕ)+ψ=(⋂w∈⟦K⟧(w⋄ϕ))+ψ=⋂w∈⟦K⟧(w⋄ϕ+ψ)(K φ)+ψ\,=\, ( _w∈ K (w φ) )+ψ\,=\, _w∈ K (w φ+ψ) (13) It follows from (11), (12) and (13) that (K⋄ϕ)+ψ⊆⋂w∈⟦K⟧(w⋄(ϕ∧ψ))(K φ)+ψ\, \, _w∈ K (w (φ ψ)) (14) and, by (K⋄8)(K 8), ⋂w∈⟦K⟧(w⋄(ϕ∧ψ))=K⋄(ϕ∧ψ) _w∈ K (w (φ ψ))=K (φ ψ). ∎ Lemma 3. (A∗3)(¬□¬ϕ∧B(ϕ>ψ)→B(ϕ→ψ)(A 3) ( φ B(φ>ψ )→ B(φ→ψ) is provable in logic ℒKML_KM. Proof. Recall that (A⋄2)(A 2) is the following axiom, for χ,ξ∈Φ0χ,ξ∈ _0, Bχ→(Bξ↔B(χ>ξ))Bχ→ (Bξ B(χ>ξ) ); in line 1 we take the instance of (A⋄2)(A 2) with χ=ϕ∨¬ϕχ=φ φ and ξ=ϕ→ψξ=φ→ψ. Recall also that (A⋄5)(A 5) is the following axiom, for χ,ξ,θ∈Φ0χ,ξ,θ∈ _0, (¬□¬(χ∧ξ)∧B((χ∧ξ)>θ))→B(χ>(ξ→θ)) ( (χ ξ) B ((χ ξ)>θ ) )\,→\,B(χ>(ξ→θ)); in line 5 we take the instance of (A⋄5)(A 5) with χ=ϕ∨¬ϕχ=φ φ and ξ=ϕξ=φ and θ=ψθ=ψ. 1. B(ϕ∨¬ϕ)→(B(ϕ→ψ)↔B((ϕ∨¬ϕ)>(ϕ→ψ)))B(φ φ)\,→\, (B(φ→ψ) B ((φ φ)>(φ→ψ) ) ) axiom (A⋄2)axiom (A 2) 2. ϕ∨¬ϕφ φ tautology 3. B(ϕ∨¬ϕ)B(φ φ) 2, rule (NB)2, rule (N_B) 4. B(ϕ→ψ)↔B((ϕ∨¬ϕ)>(ϕ→ψ))B(φ→ψ) B ((φ φ)>(φ→ψ) ) 1, 3, rule (MP)1, 3, rule (MP) 5. ¬□¬((ϕ∨¬ϕ)∧ϕ)∧B((ϕ∨¬ϕ)∧ϕ)>ψ) ((φ φ) φ) B ((φ φ) φ)>ψ ) →B((ϕ∧¬ϕ)>(ϕ→ψ))→ B((φ φ)>(φ→ψ)) axiom (A⋄5)axiom (A 5) 6. ϕ→(ϕ∨¬ϕ)∧ϕφ→(φ φ) φ tautology 7. ¬□¬ϕ→¬□¬((ϕ∨¬ϕ)∧ϕ) φ\,→\, ((φ φ) φ) 6, rule (RM¬□¬)6, rule (RM_ ) see Remark 3 8. B(ϕ>ψ)→B((ϕ∨¬ϕ)∧ϕ)>ψ)B(φ>ψ)\,→\,B ((φ φ) φ)>ψ ) 6, rule (RMB>)6, rule (RM_B>) see Remark 3 9. ¬□¬ϕ∧B(ϕ>ψ) φ B(φ>ψ) →¬□¬((ϕ∨¬ϕ)∧ϕ)∧B((ϕ∨¬ϕ)∧ϕ)>ψ)→\, ((φ φ) φ) B ((φ φ) φ)>ψ ) 7, 8 PL 10. ¬□¬ϕ∧B(ϕ>ψ)→B((ϕ∧¬ϕ)>(ϕ→ψ)) φ B(φ>ψ)\,→\,B((φ φ)>(φ→ψ)) 9, 5, PL 11. ¬□¬ϕ∧B(ϕ>ψ)→B(ϕ→ψ) φ B(φ>ψ)\,→\,B(φ→ψ) 10, 4, PL ∎ We conclude by proving the semantic correspondence for AGM axiom (K∗4)(K 4) and its modal counterpart (A∗4)(A 4). Lemma 7. The following property of frames: (P∗4)∀s∈S,∀E,F∈2S, if ℬ(s)∩E≠∅ and ℬ(s)⊆(S∖E)∪F then ⋃s′∈ℬ(s)f(s′,E)⊆F(P 4) array[]l∀ s∈ S,∀ E,F∈ 2^S,\\[4.0pt] if B(s)∩ E≠ and B(s) (S E)∪ F then _s (s)f(s ,E)\, \,F array characterizes the AGM axiom (K∗4)If ¬ϕ∉K then K+ϕ⊆K∗ϕ(K 4) φ∉ K then K+φ K φ and its modal counterpart (A∗4)¬B¬ϕ∧B(ϕ→ψ)→B(ϕ>ψ)(A 4) B φ B(φ→ψ)\,→\,B(φ>ψ) Proof. (A) First we prove that (P∗4)(P 4) characterizes (K∗4)(K 4). Fix an arbitrary model based on a frame that satisfies Property (P∗4)(P 4), an arbitrary state s and an arbitrary formula ϕφ and suppose that ¬ϕ∉Ks φ∉ K_s, that is, ℬ(s)∩‖ϕ‖≠∅B(s)∩\|φ\|≠ . Let ψ∈Ks+ϕψ∈ K_s+φ; then, since KsK_s is deductively closed, ϕ→ψ∈Ksφ→ψ∈ K_s, that is, ℬ(s)⊆∥ϕ→ψ∥=(S∖∥ϕ∥)∪∥ψ∥B(s) \|φ→ψ\|=(S \|φ\|)∪\|ψ\|. Then by Property (P∗4)(P 4) (with E=‖ϕ‖E=\|φ\| and F=‖ψ‖F=\|ψ\|) ⋃s′∈ℬ(s)f(s′,‖ϕ‖)⊆‖ψ‖ _s (s)f(s ,\|φ\|)\, \,\|ψ\|, that is, ψ∈K⋄ϕψ∈ K φ. Conversely, fix a frame that violates Property (P∗4)(P 4). Then there exist s∈Ss∈ S and E,F∈2SE,F∈ 2^S such that ℬ(s)∩E≠∅B(s)∩ E≠ and ℬ(s)⊆(S∖E)∪FB(s) (S E)∪ F but ⋃s′∈ℬ(s)f(s′,E)⊈F _s (s)f(s ,E)\, \,F. Let p,q∈Atp,q∈ At be atomic sentences and construct a model based on this frame where ‖p‖=E\|p\|=E and ‖q‖=F\|q\|=F. Then, since ℬ(s)∩‖p‖≠∅B(s)∩\|p\|≠ , ¬p∉Ks p∉ K_s and, since ℬ(s)⊆(S∖∥p∥)∪∥q∥=∥p→q∥B(s) (S \|p\|)∪\|q\|=\|p→ q\|, (p→q)∈Ks(p→ q)∈ K_s, that is q∈Ks+pq∈ K_s+p; however, since ⋃s′∈ℬ(s)f(s′,‖p‖)⊈‖q‖ _s (s)f(s ,\|p\|)\, \,\|q\|, q∉K⋄pq∉ K p. (B) Next we prove that (P∗4)(P 4) characterizes (A∗4)(A 4). Fix an arbitrary model based on a frame that satisfies Property (P∗4)(P 4), an arbitrary state s and arbitrary formulas ϕφ and ψ and suppose that s⊧¬B¬ϕ∧B(ϕ→ψ)s B φ B(φ→ψ). We need to show that s⊧B(ϕ>ψ)s B(φ>ψ). Since s⊧¬B¬ϕs B φ, ℬ(s)∩‖ϕ‖≠∅B(s)∩\|φ\|≠ . Since s⊧B(ϕ→ψ)s B(φ→ψ), ℬ(s)⊆∥ϕ→ψ∥=(S∖∥ϕ∥)∪∥ψ∥B(s) \|φ→ψ\|=(S \|φ\|)∪\|ψ\|. Thus, by Property (P∗4)(P 4) (with E=∥ϕ∥)E=\|φ\|) and F=∥ψ∥)F=\|ψ\|), ⋃s′∈ℬ(s)f(s′,‖ϕ‖)⊆‖ψ‖ _s (s)f(s ,\|φ\|)\, \,\|ψ\|, that is, s⊧B(ϕ>ψ)s B(φ>ψ). Conversely, fix a frame that violates Property (P∗4)(P 4). Then there exist s∈Ss∈ S and E,F∈2SE,F∈ 2^S such that ℬ(s)∩E≠∅B(s)∩ E≠ and ℬ(s)⊆(S∖E)∪FB(s) (S E)∪ F but ⋃s′∈ℬ(s)f(s′,E)⊈F _s (s)f(s ,E)\, \,F. Let p,q∈Atp,q∈ At be atomic sentences and construct a model based on this frame where ‖p‖=E\|p\|=E and ‖q‖=F\|q\|=F. Then, since ℬ(s)∩‖p‖≠∅B(s)∩\|p\|≠ , s⊧¬B¬ps B p and, since ℬ(s)⊆(S∖∥p∥)∪∥q∥=∥p→q∥B(s) (S \|p\|)∪\|q\|=\|p→ q\|, s⊧B(p→q)s B(p→ q); however, since ⋃s′∈ℬ(s)f(s′,‖p‖)⊈‖q‖ _s (s)f(s ,\|p\|)\, \,\|q\|, s⊧̸B(p>q).s B(p>q). ∎ References [1] Alchourrón, C., Gärdenfors, P., and Makinson, D. On the logic of theory change: partial meet contraction and revision functions. The Journal of Symbolic Logic 50 (1985), 510–530. [2] Aravanis, T. On the consistency between belief revision and belief update. Journal of Artificial Intelligence Research 82 (2025), 1743–1771. [3] Bonanno, G. A Kripke-Lewis semantics for belief update and belief revision. Artificial Intelligence 339 (2025). [4] Bonanno, G. A modal-logic translation of the AGM axioms for belief revision. The European Journal on Artificial Intelligence 0, 0 (2025), 1–14. [5] Chellas, B. Modal logic: an introduction. Cambridge University Press, 1984. [6] Hintikka, J. Knowledge and belief: an introduction to the logic of the two notions. Cornell University Press, Cornell, 1962. [7] Katsuno, H., and Mendelzon, A. O. On the difference between updating a knowledge base and revising it. In Proceedings of the Second International Conference on Principles of Knowledge Representation and Reasoning (San Francisco, 1991), KR’91, Morgan Kaufmann Publishers Inc., p. 387–394. [8] Lewis, D. Completeness and decidability of three logics of counterfactual conditionals. Theoria 37, 1 (1971), 74–85. [9] Peppas, P. Belief change and reasoning about action: an axiomatic approach to modelling dynamic worlds and the connection to the logic of theory change. PhD thesis, University of Sydney, 1993. [10] Peppas, P., Nayak, A., Pagnucco, M., Foo, N. Y., Kwok, R., and Prokopenko, M. Revision vs. update: taking a closer look. In ECAI ’96: 12th European Conference on Artificial Intelligence (1996), W. Wahlster, Ed., John Wiley & Sons, Ltd, p. 95–99.