1 Introduction↩︎

Multi-agent epistemic reasoning about actions and planning has garnered much research attention recently, as a formal framework for controlling heterogeneous, collaborative—or competitive—agents and robots. An example are service robots that interact with humans [1]; other emerging applications for dynamic epistemic reasoning include the combination with large language models in order to plan interactions based on user beliefs [2]; model reconciliation [3]; and reasoning about epistemic responsibility [4] applied in legal contexts.

Dynamic epistemic logic (DEL) is considered a quasi standard as the most expressive formalism for modeling these domains [5], [6]. In this setting, the knowledge that different agents have, both of the environment and of each others’ knowledge, is represented by a single Kripke model of the possible states that the environment could be in according to the limited information of the agents. Such a multi-agent Kripke structure encodes all the beliefs of all agents, including those of higher order, i.e., beliefs about each other’s beliefs. The latter is essential in most settings for dynamic epistemic reasoning when agents need to take into account what they know of the other (cooperating or competing) agents’ knowledge or beliefs. The use of a single Kripke model to encode all beliefs of all agents in epistemic planning is motivated by efficiency: In order to predict the effects of a sequence of actions for the purpose of planning, it suffices to update one initial Kripke model action by action [6], [7].

Actions are encoded by event models, which similarly represent what the different agents know and can observe about the effects of an action. Combining one with the other, known as event model update, results in a new Kripke model representing the updated knowledge after the action [8]. As an example, the Kripke model on the left in the figure below represents the beliefs of two agents \(a\) and \(b\) about the status of a coin (\(h\): heads up); the event model in the middle (with colored arrows) encodes the pulic announcement of \(\neg h\); and the rightmost model represents the beliefs of \(a,b\) after the announcement:

Since event models can be complex to specify directly because they represent all possible views on an action occurrence, several high-level languages for describing actions in epistemic multi-agent environments have been developed [9], [10]. Multi-agent epistemic reasoning and planning is thus well-understood when agents have (incomplete) knowledge of their environment; and event model update provides a clear semantics of how to update that knowledge after an action.

In reality, however, actions and sensors are often uncertain, so that agents can only hold beliefs. These may be wrong, in which case they may need to be revised as a result of an action that reveals a false belief. But there is no established theory of how a Kripke structure should be updated to reflect this, and yet at the same time, multi-agent belief revision is becoming ever more important in the area of agentic AI: in collaborative plan execution, for example, when agents have different beliefs about the precondition of actions they need to execute; when a chatbot tries to persuade a user to purchase a product and must be able to reason about the mental state of the user to decide on a ‘right’ price; when an AI system wishes to convince a human of its trustworthiness and has to reconcile its beliefs about the human’s model with its own beliefs in order to provide explanations about its actions; and for formal accounts of responsibility by reasoning about beliefs of plaintiffs and defendants.

Classical belief revision deals with the problem of identifying the beliefs of a single agent in the presence of a new piece of information. In their seminal work, [11] ([11]) proposed the foundational properties, referred to as AGM Postulates, that a rational belief revision operator should satisfy. [12] ([12]) added four properties for iterated belief revision, commonly referred to as DP Postulates, which focus on sequences of revisions. The postulates have been extensively studied in the literature, including concrete revision operators based on the distance between models before and after a revision [13], [14]; belief revision based on possible worlds [15] and in the context of answer set programming [16], [17]; and iterated belief revision and change for dynamic worlds [18]–[22].

Multi-agent revision has also been considered very early on; however, most of this work [23]–[26] focuses on maintaining the consistency of the local knowledge bases of agents in a distributed manner. Proposals for changing the beliefs of multiple agents in dynamic environments mostly focus on belief updates [7], [27]–[32]. To the best of our knowledge, the only systematic study on the AGM and the DP postulates in belief revision in multi-agent environements is by [33] ([33]), who considers belief sets represented by all Kripke models consistent with a set of belief formulas. This allows for a straightforward application of the AGM postulates to a multi-agent setting but does not address the issue of revising a single Kripke model as used in practical approaches to epistemic reasoning about actions and planning.

In this paper, we expand the logic of belief revision to the dynamic, multi-agent setting in order to provide a general, systematic framework for assessing multi-agent belief revision operators that are defined over a single Kripke model as used in dynamic epistemic reasoning about actions and planning. To this end, we develop a suitable multi-agent generalization of the AGM postulates. We present a simple, generalized so-called full-meet multi-agent belief revision operator and prove that it satisfies the generalized AGM postulates. We also generalize the DP postulates to iterated multi-agent belief revision and show that full-meet satisfies all but one of them. We then develop a more sophisticated, event model-based belief revision operator and analyze different strategies to define such operators and discuss their consequences in satisfying the DP posulates.

This is an extended version, with full proofs in the appendix, of a paper accepted at KR 2026.

2 Background↩︎

We begin with a concise outline of the formal foundations of dynamic epistemic reasoning and belief revision

2.0.1 Dynamic Epistemic Reasoning↩︎

A multi-agent domain is defined by a pair \(\langle {\mathcal{A}}, {\mathcal{P}}\rangle\) where \({\mathcal{A}}\) is a finite and non-empty set of agents and \({\mathcal{P}}\) a set of propositions. Belief formulas over \(\langle {\mathcal{A}}, {\mathcal{P}}\rangle\) are defined by the BNF: \(\varphi \:\: {:}{:}{=} \:\: p \mid \neg \varphi \mid (\varphi \wedge \varphi) \mid (\varphi \vee \varphi) \mid {\mathbf{B}}_i\varphi\) where \(p \in {\mathcal{P}}\) and \(i \in {\mathcal{A}}\). Standard connectives like \(\rightarrow\) and \(\leftrightarrow\) are used through their usual abbreviations. A belief formula which does not contain any occurrence of \({\mathbf{B}}_i\) is referred to as a proposition formula. \({\mathcal{L}}_{\mathcal{P}}\) (resp. \({\mathcal{L}}_{\mathcal{A}}\)) denotes the set of proposition formulas over \({\mathcal{P}}\) (resp. the set of belief formulas over \(\langle {\mathcal{A}}, {\mathcal{P}}\rangle\)).

Satisfaction of belief formulas is defined over pointed Kripke structures (a.k.a.pointed Kripke models or epistemic states) [34]. A Kripke structure/model \(M\) is a tuple \(\langle W, \{R_{a}\}_{a \in {\mathcal{A}}},\pi\rangle\), where \(W\) is a set of worlds, \(\pi: W \mapsto 2^{\mathcal{P}}\) is a function that associates an interpretation of \({\mathcal{P}}\) to each element of \(W\), and for \(a \in {\mathcal{A}}\), \(R_{a} \subseteq W \times W\) is a binary relation over \(W\). We write \(R_a(u,w)\) and use this notation interchangeably with \((u,w) \in R_a\). For \(u \in W\) and \(\varphi \in {\mathcal{L}}_{\mathcal{P}}\), \(M[\pi](u)\) and \(M[\pi](u)(\varphi)\) denote the interpretation associated with \(u\) via \(\pi\) and the truth value of \(\varphi\) with respect to \(M[\pi](u)\). For a world \(s \in W\), referred to as true state of the world, \((M,s)\) is a pointed Kripke structure.

The satisfaction relation \(\models\) between a state \((M,s)\) and belief formulas is defined as follows: (i) \((M,s) \models p\) if \(p \in {\mathcal{P}}\) and \(M[\pi](s) \models p\); (ii) \((M,s) \models {\mathbf{B}}_{i}\varphi\) if \(\forall t.[(s,t) \in R_{i} \Rightarrow (M,t) \models \varphi]\); (iii) \((M,s) \models \neg\varphi\) if \((M,s) \not\models \varphi\); (iv) \((M,s) \models \varphi_1 \vee \varphi_2\) if \((M,s) \models \varphi_1\) or \((M,s) \models \varphi_2\); (v) \((M,s) \models \varphi_1 \wedge \varphi_2\) if \((M,s)\models \varphi_1\) and \((M,s) \models \varphi_2\).

Two pointed Kripke structures \(\langle W, \{R_{a}\}_{a \in {\mathcal{A}}},\pi\rangle\) and \(\langle W', \{R'_{a}\}_{a \in {\mathcal{A}}},\pi'\rangle\) are bisimilar if there is a relation \({\mathcal{Z}}\subseteq W\times W'\) such that for all \((w,w')\in{\mathcal{Z}}\): (i) \(M[\pi](w)=M'[\pi'](w')\); (ii) for each \(w_1\in W\) such that \(R_a(w,w_1)\), \(R'_a(w',w_1')\) for some \((w_1,w_1')\in{\mathcal{Z}}\); (iii) for each \(w'_1\in W'\) such that \(R'_a(w',w'_1)\), \(R_a(w,w_1)\) for some \((w_1,w_1')\in{\mathcal{Z}}\).

For a set of formulas \(A\), \(Cn(A)\) denotes the set of logical consequences of \(A\). \(Cn\) is assumed to be supraclassical, i.e., if \(p\) can be derived from \(A\) by classical truth-functional logic, then \(p \in Cn(A)\). \(Cn\) satisfies the following properties: (i) \(A \subseteq Cn(A)\); (ii) if \(A \subseteq B\) then \(Cn(A) \subseteq Cn(B)\); (ii) \(Cn(A) = Cn(Cn(A))\). We say that \(A\) is a belief set if and only if \(A = Cn(A)\).

For a set \(K\) of formulas, \(K \vdash p\) (resp. \(K \not\vdash p\)) is an alternative notation for \(p {\in} Cn(K)\) (resp. \(p \not\in Cn(K)\)). \(Cn(\emptyset)\) is the set of tautologies. The expansion of \(K\) by a formula \(p\), i.e., the operation that just adds \(p\) and removes nothing, is denoted \(K+p\) and defined by: \(K + p = Cn(K \cup \{p\}\)).

2.0.2 Logic of Belief Revision and AGM Postulates↩︎

We follow [12] ([12]) and state the standard postulates on the basis of epistemic states \(M\), which implicitly determine a set of beliefs \(K_M\). Two epistemic states are equivalent, written \(M_1\equiv M_2\), iff \(K_{M_1}=K_{M_2}\), that is, they entail the same beliefs. The intuitive meaning of \(M * p\) is to revise the beliefs so as to ensure that \(K_{M *p}\) contains \(p\) and is consistent (unless \(p\) is inconsistent). [11] ([11]), a.k.a.AGM, proposed the following eight basic postulates for one-shot belief revision:

• Closure: \(K_{M * p} = {\rm\em Cn\/}(K_{M*p})\)

• Success: \(p \in K_{M*p}\)

• Inclusion: \(K_{M * p} \subseteq K_M + p\)

• Vacuity: if \(\neg p \not\in K\) then \(K_{M * p} = K_M + p\)

• Consistency: \(K_{M * p}\) is consistent if \(p\) is consistent

• Extensionality: if \(\vdashp \leftrightarrow q\) then \(M * p \equiv M * q\)

• Superexpansion: \(K_{M * (p \wedge q)} \subseteq K_{M * p} + q\)

• Subexpansion: \(K_{M * p} + q \subseteq K_{M * (p \wedge q)}\) if \(\neg q \not\in K_{M* p}\)

[12] ([12]) augmented the AGM framework by four more postulates for iterated revision:

(DP1)

if \(q \vdashp\) then \(K_{(M*p) * q} = K_{M*q}\)

(DP2)

if \(q \vdash\neg p\) then \(K_{(M*p) * q} = K_{M*q}\)

(DP3)

if \(p\in K_{M*q}\) then \(p\in K_{(M*p) * q}\)

(DP4)

if \(\neg p\not\in K_{M*q}\) then \(\neg p\not\in K_{(M*p) * q}\)

Another standard postulate, which strengthens (DP3) and (DP4), is the following [35]:

(IN)

Independence: if \(\neg p\not\in K_{M*q}\) then \(p\in K_{(M*p) * q}\)

3 Multi-agent Belief Revision (MBR) — Basic Concepts↩︎

We begin by discussing in detail the foundations for multi-agent belief revision in the context of dynamic epistemic reasoning, where single Kripke models represent the beliefs of all agents. In the section that follows, we then develop generalizations of the AGM postulates to this setting.

3.0.1 Belief sets↩︎

As customary in epistemic reasoning about actions and planning, a belief set in MBR shall be represented by a single, pointed Kripke structure \((M,s)\) and is the set of all formulas entailed by \((M,s)\): \[K_{(M,s)}\,=\,\{\varphi\in {\mathcal{L}}_{\mathcal{A}}\mid (M,s)\,\models\,\varphi\}\] From now on, we will assume that for any pointed Kripke structure \((M,s)\) in discussion, \(s\) is the true state of the world.

As an example, Fig. 1 shows two pointed Kripke structures, with agents \(a\) and \(b\), side by side. The egdes labelled \(a,b\) from the actual world into a world in which \(\neg p\) holds indicate that both agents consider it possible that \(p\) is false. In fact, agent \(b\) (falsely) believes in \(\neg p\) because this is the only \(b\)-accessible world from the true world, \(s\). Agent \(a\), on the other hand, considers both \(p\) and \(\neg p\) possible because there is also a self-loop on \(s\) labelled \(a\). Also, in both belief sets \(K_1\) and \(K_2\), \(b\) believes that \(a\) does not believe in either, that is, \({\mathbf{B}}_b[(\neg{\mathbf{B}}_a p)\wedge(\neg{\mathbf{B}}_a\neg p)]\), because from the only \(b\)-accessible world there is one \(a\)-accessible world with \(p\) and one with \(\neg p\). The two belief sets differ in another higher-degree belief, however: Only in \(K_1\), \(a\) believes that \(b\) believes \(\neg p\). Formally, \({\mathbf{B}}_a {\mathbf{B}}_b\, \neg p\in K_1\) whereas \(\neg{\mathbf{B}}_a {\mathbf{B}}_b\, \neg p\in K_2\), because in \((M_2,s)\) there is an additional \(a\)-accessible world in which \(b\) does believe \(p\).

Note that bisimilar multi-agent Kripke models define the same belief set provided the two designated worlds coincide in their interpretation. When two structures are dissimilar, they still induce the same belief set if they entail the same belief formulas from the respective true state of the world.

3.0.2 Deductive closure of a belief set↩︎

For a belief set \(K\), the deductive closure \({\rm\em Cn\/}(K)\) is given by the entailment relation “\(\vdash\)”. Any belief set therefore satisfies \({\rm\em Cn\/}(K)=K\).

3.0.3 Consistent beliefs/belief sets↩︎

Agents can have inconsistent beliefs: By definition, \({\mathbf{B}}_a\bot\in K_{(M,s)}\) if, and only if, \(R_a(s)=\emptyset\) in \(M\). Agents can also believe that other agents have inconsistent beliefs etc., but a belief set itself is always consistent because \(M[\pi](s)\not\models\bot\) for any pointed Kripke structure. Hence, the concept of consistency in the classical AGM postulates needs to be adapted to consistency of the beliefs of individual agents in the multi-agent setting when representing a belief set by a single Kripke structure.

3.0.4 Revision↩︎

With the aim to model actions that change the beliefs of agents (e.g., sensing actions, announcement actions) in a multi-agent environment, we consider revising belief sets to reflect the result of one agent making an observation or receiving some information about the environment. Formally, a belief set will be revised by first-degree belief formulas. These are defined as \[{\mathcal{B}}_{{\mathcal{A}},{\mathcal{P}}} = \{{\mathbf{B}}_a\varphi \mid a\in{\mathcal{A}},\;\varphi\;proposition formula over\;{\mathcal{P}}\}\] The belief set after revision by a first-degree belief \({\mathbf{B}}_a\varphi\in{\mathcal{B}}_{{\mathcal{A}},{\mathcal{P}}}\) should again be represented by a single, pointed Kripke structure, denoted by \((M,s)*{\mathbf{B}}_a\varphi\). We will simply write \(K*{\mathbf{B}}_a\varphi\) to refer to the belief set \(K_{(M,s)*{\mathbf{B}}_a\varphi}\) when it is clear from the context that \((M,s)\) is the underlying Kripke model of the belief set \(K\).

3.0.5 Subset relation over belief sets↩︎

The classical postulates also require us to define the concept of a subset relation among belief sets. Because every belief set is represented by a single Kripke structure, we cannot define this relation based on the set of all formulas entailed, since otherwise the subset relation would be satisfied only if the two Kripke structures entail identical sets of formulas. Therefore, and in line with the definiton of revision formulas, we consider all formulas of the form \({\mathbf{B}}_a\varphi\), where \(a\in{\mathcal{A}}\) and \(\varphi\) is a proposition formula over \({\mathcal{P}}\), when comparing two belief sets: \[\begin{array}{c} K_{(M_1,s_1)}\subseteq K_{(M_2,s_2)} \\ iff \\ \forall\, {\mathbf{B}}_a\varphi\in {\mathcal{B}}_{{\mathcal{A}},{\mathcal{P}}}. [(M_1,s_1)\models {\mathbf{B}}_a\varphi\Rightarrow (M_2,s_2)\models {\mathbf{B}}_a\varphi] \end{array}\] Recall, for example, the belief sets represented in Fig. 1. Although \(K_1\not=K_2\), both of them entail the same first-degree belief formulas. This follows from the fact that for both Kripke structures \((M,s)\), we have \[\begin{array}{l} \exists (s,w),(s,w')\in R_a.\;M[\pi](w)\models p\,\wedge\, M[\pi](w')\models \neg p \\ \wedge\;\forall (s,w)\in R_b.\;M[\pi](w)\models p \end{array}\] Hence, in both models it holds that \((M,s)\models {\mathbf{B}}_a\varphi\) iff \(\varphi\) is a tautological propositional formula while \((M_i,s)\models {\mathbf{B}}_b\varphi\) iff \(p\vdash\varphi\). Consequently, \(K_1\subseteq K_2\) and \(K_2\subseteq K_1\).

3.0.6 Minimal belief sets↩︎

A consequence of the above definition is that the “smallest” (w.r.t.the subset relation) representable belief sets are exactly those that include only first-degree belief formulas of the form \({\mathbf{B}}_a\varphi\) with \(\varphi\) a propositional tautology over \({\mathcal{P}}\). There are different Kripke structures that can be used to represent this set; a generic minimal Kripke structure can be constructed as follows: \(M_\emptyset=\langle W,\{R_a\}_{a\in{\mathcal{A}}},\pi\rangle\) with \(W=2^{{\mathcal{P}}}\), \(R_i=W\times W\) for all \(i\in{\mathcal{A}}\), and \(\pi(w)=w\).

It is worth stressing that not all smallest belief sets are equal as they can be based on structurally different Kripke models and hence contain different nested beliefs. For example, \((M_\emptyset,s)\) always entails \({\mathbf{B}}_a\neg{\mathbf{B}}_b\varphi\) for all agents \(a,b\in{\mathcal{A}}\) and non-tautological proposition formulas \(\varphi\), that is, every agent believes that no agent believes in anything other than tautological properties about the environment. This may not be the case in other minimal belief sets.

3.0.7 Expansion↩︎

A key concept in the classical AGM postulates is the expansion of a belief set by a new belief. The intuition behind this concept is to add a new belief while retaining the existing beliefs, together with all the logical consequences of the old and new beliefs, but in a minimal fashion. The intuition behind the following generalization of this concept to multi-agent beliefs given by a pointed Kripke structure, is that \(K+{\mathbf{B}}_a\varphi\) is obtained by constructing a new structure that is a combination of: (1) \(M\) (the old structure); (2) a new true state of the world \(s'\); and (3) a “replica” structure obtained from \(M\) by (i) removing all links labeled \(a\) into a world in which \(\varphi\) is false, and (ii) adding links labeled \(a\) going from \(s'\) to worlds in which there is a link labeled \(a\).

Formally, let \(M = (W, \{R_a\}_{a \in \mathcal{A}}, \pi)\), then expanding a pointed Kripke model \((M,s)\) by a first-degree belief formula results in the pointed Kripke model \((M,s) + {\mathbf{B}}_a \varphi = (M',s')\) with \(M' = (W', \{R'_a\}_{a \in \mathcal{A}}, \pi')\) such that

• \(W' = W \cup W^r \cup \{s'\}\) with \(W^r = \{s^r \mid s \in W\}\) — the replica of \(W\) — and where \(s'\) is a new world symbol that does not occur in \(W \cup W^r\);

• for \(w \in W\) and \(w' \in \{w, w^r\}\), \(\pi'(w') = \pi(w)\); and \(\pi'(s') = \pi(s)\);

• for \(x \in \mathcal{A} \setminus \{a\}\),

  • if \((u, v) \in R_x\) then \((u,v)\) and \((u^r,v^r)\) belong to \(R'_x\),

  • if \((s, v) \in R_x\) then \((s', v)\) belongs to \(R'_x\);

• for \(x = a\),

  • if \((u, v) \in R_x\) and \(\pi(v)\models \varphi\) then \((u,v)\) and \((u^r,v^r)\) belong to \(R'_x\),

  • if \((u, v) \in R_x\) and \(\pi(v)\not\models \varphi\) then \((u,v)\) is in \(R'_x\),

  • if \((s, v) \in R_x\) and \(\pi(v)\models \varphi\) then \((s',v^r)\) is in \(R'_x\).

Let \(K\) be a belief set represented by the pointed Kripke model \((M,s)\), and let \({\mathbf{B}}_a\varphi\in{\mathcal{B}}_{{\mathcal{A}},{\mathcal{P}}}\), then the expansion \(K+{\mathbf{B}}_a\varphi\) is defined as the belief set \(K_{(M',s')}\) where \((M,s')=(M,s)+{\mathbf{B}}_a\varphi\).

As an example, Fig. 2 depicts the results of expanding the Kripke structure to the left in Fig. 1 by \({\mathbf{B}}_a p\). Obviously, agent \(a\) now believes in \(p\), i.e.\({\mathbf{B}}_a p\in K_1+{\mathbf{B}}_a p\), since the only \(a\)-accessible world from \(s'\) satisifies \(p\). We can also see that \(b\) retains exactly her old beliefs, e.g., \({\mathbf{B}}_b\neg p\in K_1+{\mathbf{B}}_A p\) and also \({\mathbf{B}}_b((\neg{\mathbf{B}}_a p)\wedge(\neg{\mathbf{B}}_a\neg p))\in K_1+{\mathbf{B}}_a p\). This is so because the \(b\)-accessible worlds from \(s'\) are exactly those that were previously accessible from \(s\), and with the same structure. Meanwhile, \(a\) also retained his belief that \(b\) believes in \(\neg p\), that is, \({\mathbf{B}}_a{\mathbf{B}}_b\neg p\in K_1+{\mathbf{B}}_a p\).

The next lemma shows that expanding a belief set with \({\mathbf{B}}_a \varphi\) does not change the first-degree beliefs of other agents.

The definition of expansion applies to any multi-agent Kripke structure and new first-degree belief, including when no world in the model satisfies the new belief. The example depicted in Fig. 3 illustrates that in this case the resulting expanded model still does not include a world that satisfies the new belief, here: \({\mathbf{B}}_a \neg p\). This implies that there are no \(a\)-reachable worlds at all from the new designated state, which in turn means that agent \(a\) ends up with inconsistent beliefs (and hence, in particular, believes \(\neg p\)). This is very much in the spirit of expansion in the classical case, when expanding by a new belief that is inconsistent with the current ones results in an inconsistent belief set [11]. In the multi-agent generalization, all other agents maintain their beliefs, however (cf. Lemma 2).

It is easy to prove that expanding a belief set with \({\mathbf{B}}_a \varphi\) always results in agent \(a\) believing \(\varphi\) when \(a\) ends up with consistent beliefs; and if the result is that \(a\) has inconsistent beliefs, then again, vacuously, \(a\) believes in \(\varphi\).

The next lemma shows that the first-degree beliefs of agent \(a\) are exactly the logical consequences of its old beliefs plus the new belief.

4 Generalizing AGM Postulates↩︎

Using the basic formal concepts for multi-agent belief sets represented by a single, pointed Kripke strucure as developed in the previous section, we can now define generalizations of the standard postulates, beginning with the AGM potulates for one-shot revision.

4.0.1 Closure↩︎

A revised belief set is deductively closed, denoted by \({\rm\em Cn\/}\), under the modal logic being interpreted: \[K * {\mathbf{B}}_a\varphi = {\rm\em Cn\/}(K * {\mathbf{B}}_a\varphi)\] Since the set of belief formulas entailed by a single Kripke structure is deductively closed, this postulate holds when a revised belief set is represented by a pointed Kripke model.

4.0.2 Success↩︎

The result of revising a Kripke model by a first-degree belief formula should include the new belief: \[{\mathbf{B}}_a\varphi \in K*{\mathbf{B}}_a\varphi\]

4.0.3 Inclusion↩︎

A revised Kripke model should only contain first-degree belief formulas that would be included in the expanded Kripke model: \[K * {\mathbf{B}}_a\varphi \subseteq K + {\mathbf{B}}_a\varphi\] From Lemma 2 and 4 it follows that under the Inclusion principle, a revised Kripke model contains only first-degree belief formulas that follow logically from the old and new first-degree beliefs.

Worthy of note, this generalized Inclusion postulate does not stipulate any requirements about second- or higher-degree belief formulas. In particular it allows for another agent, \(b\), to change her beliefs about agent \(a\) believing in \(\varphi\). Hence, \(K*{\mathbf{B}}_a\varphi\) may contain beliefs that are not included in \(K+{\mathbf{B}}_a\varphi\) if these are not first-order beliefs.

4.0.4 Vacuity↩︎

If a Kripke model is revised by a first-degree belief that is consistent with the current beliefs, then the result should contain all first-degree belief formulas that are included in the expanded Kripke model: \[{\mathbf{B}}_a\neg \varphi \not\in K\;\Rightarrow\;K + {\mathbf{B}}_a\varphi \subseteq K * {\mathbf{B}}_a\varphi\] By Lemma 2 and 4 it follows that under the Vacuity principle, a revised Kripke model contains all first-degree belief formulas that follow logically from the old and new first-degree beliefs, provided the old beliefs did not include the opposite of the new belief.

Similar to the generalized Inclusion principle, the Vacuity postulate does allow for belief revision operators in which other agents change their belief about the belief of agent \(a\) in \(\varphi\) as a result of this revision.

It should also be noted that Vacuity and Inclusion together are a weaker requirement than stipulating that revision be identical to expansion in case a new belief is consistent with the old ones. They merely postulate that the first-degree beliefs are the same, while they do not demand anything about other belief formulas. In particular, they do not prescribe the specific structure from our definition of expansion of a pointed Kripke model with a new belief (cf.Section 3).

4.0.5 Consistency 1↩︎

Any revision by a logically consistent belief should result in a consistent belief for the agent: \[\not\vdash\varphi\rightarrow\bot\;\Rightarrow\; {\mathbf{B}}_a\bot \not\in K * {\mathbf{B}}_a\varphi\] It is worth noting that this does not postulate overall consistency of beliefs as it cannot be generally assumed that one agent changing their beliefs would always mean that any other agent that may have had inconsistent beliefs would automatically end up with consistent beliefs too. However, while it is possible that other agents change their beliefs about agent \(a\)’s beliefs, it is reasonable to postulate that they do not end up with inconsistent beliefs as a result if they had consistent beliefs beforehand. For this reason, we suggest the following additional postulate on consistency.

4.0.6 Consistency 2↩︎

If a new belief \({\mathbf{B}}_a\varphi\) is consistent, then any agent with consistent beliefs will have consistent beliefs after the revision: \[{\mathbf{B}}_b\bot\not\in K\;\wedge\;\not\vdash\varphi\rightarrow\bot\;\Rightarrow\; {\mathbf{B}}_b\bot \not\in K * {\mathbf{B}}_a\varphi\]

4.0.7 Extensionality↩︎

If two new belief formulas are logically equivalent w.r.t.the underlying modal logic, then a belief set revised by either of the two should give the same result: \[\vdash{\mathbf{B}}_a\varphi \leftrightarrow {\mathbf{B}}_b\psi\;\Rightarrow\;K * {\mathbf{B}}_a\varphi = K * {\mathbf{B}}_b\psi\] It is easy to see that \({\mathbf{B}}_a\varphi\) and \({\mathbf{B}}_b\psi\) are logically equivalent under any pointed Kripke structure if, and only if, \(a=b\) and \(\varphi\) and \(\psi\) are logically equivalent proposition formulas.

4.0.8 Superexpansion↩︎

Revising a belief set by a conjunction \(\varphi\wedge\psi\) of two new beliefs of an agent \(a\) should not result in more first-degree beliefs than the expansion by \({\mathbf{B}}_a\psi\) of the result of revising by \({\mathbf{B}}_a\varphi\): \[K * {\mathbf{B}}_a(\varphi \wedge \psi) \subseteq (K * {\mathbf{B}}_a\varphi) + {\mathbf{B}}_a\psi\] Similarly to Inclusion and Vacuity, this generalized postulate does not make any assumptions about second- or higher-degree belief formulas of any agent. This is also true for the following counterpart, subexpansion.

4.0.9 Subexpansion↩︎

If the second belief \({\mathbf{B}}_a\psi\) is consistent with the result of revising a belief set by the first belief \({\mathbf{B}}_a\varphi\), then revision by the conjunction of the two should not result in fewer first-degree beliefs than the expansion by \({\mathbf{B}}_a\psi\) of the result of revising by \({\mathbf{B}}_a\varphi\): \[{\mathbf{B}}_a\neg \psi \not\in K* {\mathbf{B}}_a\varphi \Rightarrow (K * {\mathbf{B}}_a\varphi) + {\mathbf{B}}_a\psi \subseteq K * {\mathbf{B}}_a(\varphi \wedge \psi)\]

5 Multi-agent Belief Revision Operators↩︎

Having defined generalized AGM postulates for MBR, in this section we present a generalization of the well-known “full-meet” revision operator for classical Belief Revision [36] and show that it satisfies all generalized AGM postulates.

We define this multi-agent full meet revision, denoted by the opeartor name \({\,*_{\scriptsize\rm fm}\,}\), as follows: \[K_{(M,s)}{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi\,=\! \left\{\!\!\! \renewcommand{\arraystretch}{0.7} \begin{array}{ll} K_{(M,s)}+{\mathbf{B}}_a\varphi & \!\!\!if{\mathbf{B}}_a\neg\varphi\not\in K_{(M,s)}\!\!\!\! \\ \\ K_{(M_\emptyset,s)}+{\mathbf{B}}_a\varphi & \!\!\!otherwise \end{array} \right.\] The principle behind this definition is the same as for classical full-meet revision [11]. If a new belief is consistent with the current beliefs, the underlying Kripke structure is simply expanded by that belief. Otherwise, the new belief is incorporated in the most conservative manner by starting with the minimal belief set \(K_{(M_\emptyset,s)}\) (cf.Section 3), in which it is common knowledge that no agent believes in anything but tautological proposition formulas, and then expanding the undelying Kripke model \((M_\emptyset,s)\) by the new belief.

It should be noted, however, that unlike with the classical full-meet belief revision operator, the belief set resulting from revision by a belief that is inconsistent with the old beliefs does entail more beliefs than follow logically from the new one. This is so because the generic Kripke structure \((M_\emptyset,s)\) makes strong assumptions about higher-degree beliefs. For example, full-meet revision of the Kripke structure depicted on the left-hand side in Figure 3 by \({\mathbf{B}}_a\neg p\) results in agent \(b\) not only losing both her first-degree belief in \(p\) as well as her higher-degree belief that \(p\) is common knowledge, but also gaining second-order beliefs of “ignorance”, such as, say, \({\mathbf{B}}_b\left(\neg{\mathbf{B}}_a p\wedge\neg{\mathbf{B}}_a\neg p\right)\).

This notwithstanding, the generalized full-meet operator provably satisfies all of the generalized AGM postulates.

Proof. Due to limited space, we include below only the proof for Superexpansion as it is somewhat more complicated than the others. Detailed proofs for all theorems and lemmas

can be found in the appendix.

1. Suppose \({\mathbf{B}}_a\neg(\varphi\wedge\psi)\not\in K\). Since \(K\) is deductively closed, it follows that \({\mathbf{B}}_a\neg\varphi\not\in K\). Hence, agent \(a\) has consistent beliefs in \(K+{\mathbf{B}}_a(\varphi\wedge\psi)\), in \(K+{\mathbf{B}}_a\varphi\), and in \((K+{\mathbf{B}}_a\varphi)+{\mathbf{B}}_a\psi\). By Lemma 4 it follows that \((M,s)+{\mathbf{B}}_a(\varphi\wedge\psi)\models{\mathbf{B}}_a\chi\) iff \(\chi\in{\rm\em Cn\/}(\{\varphi\wedge\psi\}\cup\{\phi\in{\mathcal{B}}_{{\mathcal{A}},{\mathcal{P}}} \mid\;{\mathbf{B}}_a\phi\in K\})\). This is equivalent to \(\chi\in{\rm\em Cn\/}(\{\psi\}\cup{\rm\em Cn\/}(\{\varphi\}\cup\{\phi\in{\mathcal{B}}_{{\mathcal{A}},{\mathcal{P}}} \mid\;{\mathbf{B}}_a\phi\in K\}))\), which in turn by Lemma 4 is equivalent to \(\left(K+{\mathbf{B}}_a\varphi\right) + {\mathbf{B}}_a\psi\models{\mathbf{B}}_a\chi\). By Lemma 2 it follows that all other agents too have the same beliefs in \(K+{\mathbf{B}}_a(\varphi\wedge\psi)\) and in \((K+{\mathbf{B}}_a\varphi)+{\mathbf{B}}_a\psi\). Hence, \(K {\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a(\varphi \wedge \psi) \subseteq (K {\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi) + {\mathbf{B}}_a\psi\).

2. Suppose \({\mathbf{B}}_a\neg(\varphi\wedge\psi)\in K\). By definition of \((M_\emptyset,s)+{\mathbf{B}}_a(\varphi\wedge\psi)\) and Lemma 4 it follows that, for any first-degree belief, \({\mathbf{B}}_a\phi\in K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a(\varphi\wedge\psi)\) iff \(\phi\in{\rm\em Cn\/}(\varphi\wedge\psi)\), and for \(x\in{\mathcal{A}}\setminus\{a\}\), \({\mathbf{B}}_x\phi\in K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a(\varphi\wedge\psi)\) iff \(\models\phi\).

   We distinguish two cases: If \({\mathbf{B}}_a\neg\varphi\not\in K\), then \((K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi)+{\mathbf{B}}_a\psi=(K+{\mathbf{B}}_a\varphi)+{\mathbf{B}}_a\psi\). From \({\mathbf{B}}_a\neg(\varphi\wedge\psi)\in K\) it follows that \({\mathbf{B}}_a\neg\psi\in K+{\mathbf{B}}_a\varphi\). Hence, \(a\) has inconsistent beliefs in \((K+{\mathbf{B}}_a\varphi)+{\mathbf{B}}_a\psi\) while the beliefs of all other agents \(x\in{\mathcal{A}}\setminus\{a\}\) are the same in \((K+{\mathbf{B}}_a\varphi)+{\mathbf{B}}_a\psi\) and \(K+{\mathbf{B}}_a(\varphi\wedge\psi)\). If, on the other hand, \({\mathbf{B}}_a\neg\varphi\in K\), then \((K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi)+{\mathbf{B}}_a\psi=(K_{(M_\emptyset,s)}+{\mathbf{B}}_a\varphi)+{\mathbf{B}}_a\psi\). Hence, \(a\)’s first-degree beliefs in \((K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi)+{\mathbf{B}}_a\psi\) are exactly the logical consequences of \(\varphi\wedge\psi\) while the beliefs of all other agents \(x\in{\mathcal{A}}\setminus\{a\}\) are the same in \((K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi)+{\mathbf{B}}_a\psi\) and \(K+{\mathbf{B}}_a(\varphi\wedge\psi)\). Thus, \(K {\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a(\varphi \wedge \psi) \subseteq (K {\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi) + {\mathbf{B}}_a\psi\). \(\Box\)

While satisfying all our generalized postulates for one-shot revision, multi-agent full-meet revision makes for a very drastic revision in cases where simple expansion would leave an agent with inconsistent beliefs. We introduce a more refined alternative in Section 7; prior to this, we first turn to the question of successive multi-agent revisions.

6 Generalized Postulates for Iterated MBR↩︎

We complete our framework for belief revision for multiagent epistemic reasoning and planning by generalizing the standard postulates for iterated revision.

6.0.1 DP1 – Successive revision respect↩︎

Revision by one belief followed by revising by a stronger belief makes the first revision redundant: \[\vdash{\mathbf{B}}_b\psi \rightarrow {\mathbf{B}}_a\varphi\;\Rightarrow\;(K*{\mathbf{B}}_a\varphi) * {\mathbf{B}}_b\psi \doteq K*{\mathbf{B}}_b\psi\] Here, \(K_1\dot{=}K_2\) means \(K_1\subseteq K_2\) and \(K_2\subseteq K_1\).

6.0.2 DP2 – Irrelevance of superseded beliefs↩︎

If for two successive revisions, the second belief contradicts the first one, then the resulting beliefs for all agents should be the same as from revising according to the second belief only. \[\vdash{\mathbf{B}}_b\psi \rightarrow {\mathbf{B}}_a\neg\varphi\;\Rightarrow\;(K*{\mathbf{B}}_a\varphi) * {\mathbf{B}}_b\psi \doteq K*{\mathbf{B}}_b\psi\]

6.0.3 DP3 – Consistency preservation across revisions↩︎

If one agent’s first-degree belief would be contained in the belief set after revision by any other first-degree belief, then in case the former is used to revise the belief set first, that first belief should be preserved through the second revision: \[{\mathbf{B}}_a\varphi\in K*{\mathbf{B}}_b\psi \;\Rightarrow\;{\mathbf{B}}_a\varphi \in (K*{\mathbf{B}}_a\varphi) * {\mathbf{B}}_b\psi\]

6.0.4 DP4 – Minimal change when reaffirming a belief↩︎

After two consecutive revisions, the first agent should not end up believing the opposite unless they would do so if the belief set was revised by the second belief only: \[{\mathbf{B}}_a\neg\varphi\not\in K*{\mathbf{B}}_b\psi \;\Rightarrow\;{\mathbf{B}}_a\neg\varphi \not\in (K*{\mathbf{B}}_a\varphi) * {\mathbf{B}}_b\psi\]

6.0.5 IN – Independence↩︎

After two consecutive revisions, the belief of the first agent should be preserved unless they would believe the opposite if the belief set was revised by the second belief only: \[{\mathbf{B}}_a\neg\varphi\not\in K*{\mathbf{B}}_b\psi \;\Rightarrow\;{\mathbf{B}}_a\varphi \in (K*{\mathbf{B}}_a\varphi) * {\mathbf{B}}_b\psi\]

Interestingly, while in the classical, single-agent case the Independence postulate IN strengthens both DP3 and DP4 [35] for any operator that satisfies the AGM postulates, in the generalized case Independence only strengthens DP4.

It is noteworthy that IN would not entail DP4 without the additional Consistency 2 postulate, which guarantees that agent \(a\) does not end up believing in both \(\varphi\) and \(\neg \varphi\) as a result of further revision by \({\mathbf{B}}_b\psi\) after revising by \({\mathbf{B}}_a\varphi\).

IN does not imply DP3 even if an operator satisfies all multi-agent AGM postulates, for the following reason: If \({\mathbf{B}}_a\bot\in K*{\mathbf{B}}_b\psi\) then IN vacuously holds while DP3 is violated if \({\mathbf{B}}_a\bot\not\in (K*{\mathbf{B}}_a\bot\varphi)*{\mathbf{B}}_b\psi\). This is possible if an operator allows an agent to regain consistent beliefs when revising a multi-agent belief set by another agent’s belief.

The next theorem summarizes the satisfaction of the generalized DP postulates of \({\,*_{\scriptsize\rm fm}\,}\).

Proof. (DP2) Generalized full-meet does not satisfy DP2 for the following reason: If \({\mathbf{B}}_b\psi\) is consistent with the current belief set \(K\) then \(K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_b\psi=K+{\mathbf{B}}_b\psi\), hence by Lemma 2, all agents retain all their beliefs when revising \(K\) by \(b\)’s new belief. But if \(K\) is revised by \({\mathbf{B}}_a\varphi\) first and \(\models{\mathbf{B}}_b\psi\rightarrow{\mathbf{B}}_a\varphi\) holds then \((K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_b\varphi){\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_b\psi=K_{(M_\emptyset,s)}+{\mathbf{B}}_b\psi\), which implies that the beliefs of all other agents have been erased.

The fact that full-meet does not satisfy DP2 mirrors a result in classical, single-agent belief revision [35]. To show that full-meet multi-agent belief revision satisfies one direction of DP2 (namely, that revising by a belief that is then superseded by a second, contradictory belief never introduces more beliefs than revision with the second belief directly) we make a case distinction.

1. Suppose that \(\models\varphi\leftrightarrow\bot\), then \({\mathbf{B}}_a\neg\varphi\in K\), hence \(K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi=K_{(M_\emptyset,s)}+{\mathbf{B}}_a\bot\), that is, there is no \(a\)-accessible world in \(s\) while all other agents’ first-degree beliefs are tautological proposition formulas. Consequently, \((K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi){\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_b\psi\subseteq K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_b\psi\).

2. Otherwise, \(\models{\mathbf{B}}_b\psi\rightarrow{\mathbf{B}}_a\varphi\) implies \(a=b\) and \(\psi\models\neg\varphi\), hence \(\varphi\models\neg\psi\). It follows that \({\mathbf{B}}_b\psi\not\in K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi\), hence \((K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi){\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_b\psi=K_{(M_\emptyset,s)}+{\mathbf{B}}_b\psi\), which implies \((K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi){\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_b\psi\subseteq K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_b\psi\). \(\Box\)

7 Event Model-Based Belief Revision↩︎

While full-meet is an instructive operator to show that all generalized AGM and most DP postulates can be simultaneously satisfied, it is obviously too strong for practical purposes in that any (non-tautological) belief may be abandoned in case of a true revision. In this section, we introduce a more sophisticated operator for MBR based on event models. Event models (a.k.a.update models) have been used to describe transformations of epistemic states in multi-agent domains according to a predetermined transformation pattern [27]). This has also been used in modeling belief-altering actions in high-level action languages [7], [10]. Nonetheless, event models proposed for the purpose of updating beliefs of agents after an action occurrence are not suitable for revising the beliefs of agents. This is illustrated in Fig. 4:

In the model \((M,s)\) (left), simplified to consider only a single agent, \(a\) does not believe \(f\) nor \(\neg f\). The event model for sensing \(f\) is in the middle, whose update on \((M,s)\) is \((M',s')\) (right), which indicates that \(a\) believes \(\neg f\) after sensing \(f\). Such an update does not allow for the revision of \((M,s)\) with \({\mathbf{B}}_a f\).

For the discussion of the generalized postulates, we need some extra notation. A literal is either a proposition \(p \in {\mathcal{P}}\) or its negation \(\neg p\). For a literal \(\ell\), \(\neg \ell\) denotes its negation, with \(\neg \neg p = p\) for \(p \in {\mathcal{P}}\). An inference rule (or rule) among literals is of the form \(\lambda \rightarrow \delta\) where \(\lambda\) and \(\delta\) are sets of literals. Given a set of literals \(w\) and a set of rules \(R\), \(C_R(w)\) denotes the minimal set (w.r.t. \(\subseteq\)) of literals \(w'\) such that \(w \subseteq w'\) and, for every \(\lambda \rightarrow \delta\) in \(R\), if \(w \models \lambda\) then \(w' \models \delta\).

In the presence of the set of rules \(R\), the valuation function \(\pi\) of any Kripke model \(M\) must satisfy \(R\) as well. Therefore, we require that for every world \(u\) in \(M\), \(\pi(u)\) is consistent, i.e., \(\pi(u) = C_R(\pi(u))\). For a set of literals \(\varphi\) and an interpretation \(u\), let \(u \star \varphi\) denote an interpretation \(u'\) such that \(u' = C_R((u \cap u') \cup \varphi)\). In general, there might exist several interpretations \(u'\) satisfying the aforementioned equation. Fortunately, it is well-known that there are conditions on \(R\) such that there is a unique \(u'\) that satisfies the equation (see, e.g., [37]’s ([37]) work). In this paper, we will assume that \(R\) only consists of rules of the form \(p \rightarrow q\) where \(p, q\) are literals and, for each \(u\) and \(p\), there is a unique \(u' = C_R((u \cap u') \cup \{p\})\), since this is sufficient for dealing with the DP1 and DP2 postulates.

Consider \(a \in {\mathcal{A}}\) and a set of literals \(\varphi\). We define \(\mathbf{\Sigma}^a(\varphi)\), called the event model for revision by \({\mathbf{B}}_a \varphi\), as the event model \(\langle \Sigma, \{E_a\}_{a \in {\mathcal{A}}}, pre, \mathit{eff} \rangle\) where

• \(\Sigma = \{\sigma, \delta, \sigma_a, \delta_a, \epsilon\}\);

• \(E_a = \{(\sigma,\sigma_a), (\sigma_a,\epsilon), (\delta,\delta_a), (\delta_a,\epsilon), (\epsilon,\epsilon)\}\);

• \(E_x = \{(\eta,\epsilon) \mid \eta \in \Sigma\setminus\{\sigma_a,\delta_a\}\}\) for \(x \in {\mathcal{A}}\setminus \{a\}\);

• \(pre(\sigma) = \neg {\mathbf{B}}_a \neg \varphi\), \(pre(\delta) = {\mathbf{B}}_a \neg \varphi\), \(pre(\sigma_a) = \varphi\), \(pre(\delta_a) = \neg \varphi\), and \(pre(\epsilon) = \top\).

• for \(u \in W\), \(\mathit{eff}(u,\eta) = \pi(u)\) for \(\eta \in \Sigma \setminus \{\delta_a\}\), and \(\mathit{eff}(u,\delta_a) = \pi(u) \star \varphi\).

In the above definition, \(\Sigma\) is the set of events representing possible views of the event “\((M,s)\) is revised by \({\mathbf{B}}_a \varphi\)”. Intuitively, this revision could affect the worlds accessible by \(a\) in the following ways: If \(\neg {\mathbf{B}}_a \neg \varphi\) is true, i.e., \({\mathbf{B}}_a \varphi\) or \(\neg ({\mathbf{B}}_a \varphi \wedge {\mathbf{B}}_a \neg \varphi)\) holds, then some worlds accessible by \(a\) satisfy \(\varphi\) and \(a\) can just eliminate all worlds satisfying \(\neg \varphi\) from its accessibility.

This is represented by the events \(\sigma\) and \(\sigma_a\) (Fig. 5) where \(\sigma\) denotes a designated event and \(\sigma_a\) has the precondition \(\varphi\). If, on the other hand, \({\mathbf{B}}_a \neg \varphi\) is true, then agent \(a\) should revise his beliefs in every world accessible by \(a\), via the definition of \(\mathit{eff}\). This is represented by the events \(\delta\) and \(\delta_a\). For agent \(x \in {\mathcal{A}}\setminus \{a\}\), nothing changes and thus, \(x\)’s view is that only the event \(\epsilon\) occurs.

The revision of \({\mathbf{B}}_a \varphi\) in \((M,s)\), denoted by \((M,s) {\,*_{\scriptsize\rm ev}\,}{\mathbf{B}}_a \varphi\), is a pointed Kripke structure \((M^\varphi,s^\varphi)\) where \(M^\varphi = (W^\varphi, \{R^\varphi_x\}_{x \in {\mathcal{A}}}, \pi^\varphi)\) and

• \(W^\varphi = \{(u,\tau) \mid u \in W, \tau \in \Sigma, (M,u) \models pre(\tau)\}\);

• \(((u,\tau), (u',\tau')) \in R^\varphi_x\) iff \((u,\tau),(u',\tau')\in W^\varphi\) along with \((u,u') \in R_x\) and \((\tau,\tau') \in E_x\);

• \(\pi^\varphi((u,\tau)) = \mathit{eff}(u, \tau)\); and

• \(s^\varphi = (s, \sigma)\) if \((M,s) \models \neg {\mathbf{B}}_a \neg \varphi\); otherwise, \(s^\varphi = (s, \delta)\).

Before we discuss the properties of \({\,*_{\scriptsize\rm ev}\,}\) in detail, let us observe that if \(R_a(s) \ne \emptyset\) then \(R^\varphi_a(s^\varphi) \ne \emptyset\), i.e., \(a\) has consistent belief in \((M^\varphi, s^\varphi)\). This is the main difference between \({\,*_{\scriptsize\rm ev}\,}\) and \({\,*_{\scriptsize\rm fm}\,}\). We prove that beliefs of other agents do not change.

Proof. As above, proofs are given for selected interesting postulates only. We assume a consistent \(K\) that is represented by \((M,s)\) with \(M = (W, \{R_x\}_{x \in {\mathcal{A}}}, \pi)\). We use \((M,s) {\,*_{\scriptsize\rm ev}\,}{\mathbf{B}}_a \varphi\) and \((M^\varphi,s^\varphi)\) interchangeably where \(M^\varphi = (W^\varphi, \{R^\varphi_x\}_{x \in {\mathcal{A}}}, \pi^\varphi)\). Successive revisions such as \((K {\,*_{\scriptsize\rm ev}\,}{\mathbf{B}}_a \varphi) {\,*_{\scriptsize\rm ev}\,}{\mathbf{B}}_a \psi\) will be denoted by \((M^{\varphi; \psi}, s^{\varphi; \psi})\) etc. Furthermore, \(R_a(s|\varphi) = \{u \mid u \in R_a(s), \pi(u) \models \varphi\}\). Below, we use conjunctions of literals and sets of literals interchangeably, and we always assume that a conjunction of literals \(\varphi\) is consistent in the classical sense, i.e., \(\varphi \not\vdash \bot\). For a set of literals \(\varphi\), \(\neg \varphi\) denotes \(\{\neg \ell \mid \ell \in \varphi\}\).

(Success) We show \(K{\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a\varphi \models {\mathbf{B}}_a \varphi\) via two cases:

1. \((M,s) \models \neg {\mathbf{B}}_a \neg \varphi\), i.e., \(a\) does not believe in \(\neg \varphi\) before the revision. This implies that \(s^\varphi = (s, \sigma)\). Furthermore, because \(K\) is consistent, we have that \(R_a(s) \ne \emptyset\) and there exists some \(u \in W\) such that \((s,u) \in R_a\) and \(\pi(u) \models \varphi\), which implies that \(((s,\sigma), (u,\sigma_a)) \in R^\varphi_a\), i.e., \(R^\varphi(s^\varphi) \ne \emptyset\). In addition, if \(((s, \sigma), (u, \rho)) \in R^\varphi_a\) then \(\rho = \sigma_a\), and hence, \(\pi(u) \models \varphi\), because \(E_a\) contains only one element related to \(\sigma\), \((\sigma, \sigma_a)\), and \((s,u) \in R_a\). Thus, we have that \((M^\varphi, s^\varphi) \models {\mathbf{B}}_a \varphi\).

2. \((M,s) \models {\mathbf{B}}_a \neg \varphi\). This implies that \(s^\varphi = (s, \delta)\). Again, because \(K\) is consistent, we have that \(R_a(s) \ne \emptyset\) and for each \(u \in R_a(s)\), \(\pi(u) \models \neg \varphi\). By the construction of \((M^\varphi, s^\varphi)\), \(R^\varphi_a(s^\varphi) \ne \emptyset\). Consider \(u' \in R^\varphi_a(s^\varphi)\). We have that \(u ' = (u, \delta_a)\) for some \(u \in R_a(s)\), and hence, \(\pi^\varphi(u') = C_R((\pi(u) \cap \pi^\varphi(u')) \cup \{\varphi\})\), which implies \(\varphi \in \pi^\varphi(u')\). It follows that \((M^\varphi, s^\varphi) \models {\mathbf{B}}_a \varphi\). \(\Box\)

(Superexpansion) Consider a propositional formula \(\phi\), then Lemma 6 and Lemma 2 imply that to prove that \({\,*_{\scriptsize\rm ev}\,}\) satisfies this postulate, it suffices to show that \(K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a(\varphi \wedge \psi) \models {\mathbf{B}}_a \phi\) implies \((K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a\varphi) + {\mathbf{B}}_a \psi \models {\mathbf{B}}_a \phi\). Let \((M',s')\) denote \((M^{\varphi},s^{\varphi}) + {\mathbf{B}}_a \psi\). We consider two cases:

• \((M,s) \models \neg {\mathbf{B}}_a \neg (\varphi \wedge \psi)\). So, \(s^{\varphi \wedge \psi} = (s, \sigma^{\varphi \wedge \psi})\) and \((s^{\varphi \wedge \psi},u^{\varphi \wedge \psi}) \in R^{\varphi \wedge \psi}_a\) where \(u^{\varphi \wedge \psi} = (u,\sigma^{\varphi \wedge \psi}_a)\) iff \((s,u) \in R_a\) and \(\pi(u) \models (\varphi \wedge \psi)\). Since \((M,s) \models \neg {\mathbf{B}}_a \neg (\varphi \wedge \psi)\), we have that \((M,s) \models \neg {\mathbf{B}}_a \neg \varphi\), i.e., \(u \in R_a(s|\varphi \wedge \psi)\). Thus \(s^{\varphi} = (s, \sigma^{\varphi})\) and \((s^{\varphi},u^{\varphi}) \in R^{\varphi}_a\) where \(u^{\varphi} = (u,\sigma^{\varphi}_a)\) iff \((s,u) \in R_a\) and \(\pi(u) \models \varphi\), i.e., \(u \in R_a(s|\varphi)\). Because \(R_a(s|\varphi) = R_a(s|\varphi \wedge \psi) \cup R_a(s|\varphi \wedge \neg \psi)\) and the construction of \((K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a\varphi) \models {\mathbf{B}}_a \phi\) we have \(R'_a(s') = \{u^r \mid u \in R_a(s), \pi(u) \models \varphi \wedge \psi\}\), which proves the consequence of the postulate.

• \((M,s) \models {\mathbf{B}}_a \neg (\varphi \wedge \psi)\). Then, \(s^{\varphi \wedge \psi} = (s, \delta^{\varphi \wedge \psi})\) and for every \(u^{\varphi \wedge \psi}\) such that \((s^{\varphi \wedge \psi},u^{\varphi \wedge \psi}) \in R^{\varphi \wedge \psi}_a\) holds, we have \(u^{\varphi \wedge \psi} = (u,\delta^{\varphi \wedge \psi}_a)\) iff \((s,u) \in R_a\). Therefore, we can conclude that \(K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a(\varphi \wedge \psi) \models {\mathbf{B}}_a \phi\) iff for every \(u \in R_a(s)\), \(\pi(u) \star (\varphi \wedge \psi) \models \phi\). There are two cases:

  1. \((M,s) \models {\mathbf{B}}_a \neg \varphi\). In this case, similar arguments to the above allow us to conclude that \((s^{\varphi},u^{\varphi}) \in R^{\varphi}_a\) iff \(u^{\varphi} = (u,\delta^{\varphi}_a)\) for some \((s,u) \in R_a\) and \(\pi(u^\varphi) = \pi(u)\star \varphi\). Because of the construction of \((K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a\varphi) + {\mathbf{B}}_a\psi\), we have two sub-cases:

     1. \(K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a\varphi \models {\mathbf{B}}_a \neg \psi\). In this case, \(a\) has inconsistent beliefs in \((K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a\varphi) + {\mathbf{B}}_a\psi\), i.e., the postulate holds trivially.

     2. \(K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a\varphi \models \neg {\mathbf{B}}_a \neg \psi\). In this case, we can conclude that \(R'_a(s') \ne \emptyset\). Furthermore, \((s',u') \in R'_a\) iff \(u' = u^\varphi\) and \(\pi(u^\varphi) \models \psi\). Given that \(\star\) satisfies the classical AGM postulate of Superexpansion, we can conclude that \(K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a(\varphi \wedge \psi) \models {\mathbf{B}}_a \phi\) implies \(K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a\varphi + {\mathbf{B}}_a \psi \models {\mathbf{B}}_a \phi\).

  2. \((M,s) \models \neg {\mathbf{B}}_a \neg \varphi\). We have \(s^{\varphi} = (s, \sigma^{\varphi})\) and \((s^{\varphi},u^{\varphi}) \in R^{\varphi}_a\) where \(u^{\varphi} = (u,\sigma_a^{\varphi})\) iff \((s,u) \in R_a\) and \(\pi(u) \models \varphi\), which implies that \(\pi^{\varphi}(u^{\varphi}) \models \neg \psi\) for every \((s^{\varphi},u^{\varphi}) \in R^{\varphi}_a\). This means that \(a\)’s belief is inconsistent in \((K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a\varphi) + {\mathbf{B}}_a\psi\), and thus, the postulate also holds in this case. \(\Box\)

While \({\,*_{\scriptsize\rm ev}\,}\) satisfies all generalized AGM postulates, it does not satisfy DP1-DP2. This is because \({\,*_{\scriptsize\rm ev}\,}\) attempts to remove uncertainty in the beliefs of an agent before revising them, which is encoded in the event \(\sigma\) in which the agent is uncertain about \(\varphi\) and, due to the precondition of \(\sigma_a\), the operator only retains worlds satisfying \(\varphi\). Nevertheless, these postulates, in a simpler form where \(\varphi\) and \(\psi\) are literals, are satisfied under restricted conditions.

Proof. (DP1) Since \(\models {\mathbf{B}}_b p \rightarrow {\mathbf{B}}_a q\), we have that \(p \rightarrow q\) and \(a\) and \(b\) are identical. Therefore, we will show that \({\,*_{\scriptsize\rm ev}\,}\) satisfies this postulate by proving that if \(\models {\mathbf{B}}_a p \rightarrow {\mathbf{B}}_a q\) and \(K {\,*_{\scriptsize\rm ev}\,}{} B_a q \not\models {\mathbf{B}}_a \neg p\) hold then \((K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a q) {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a p \doteq K{\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a p\).

1. \((M,s) \models \neg {\mathbf{B}}_a \neg q\). So, if \((s^ q,u^ q) \in R^ q_a\) then \(u \in R_a(s)\) and \(\pi(u) \models q\) and \(\pi^q(u^q) = \pi(u)\). Since \((M,s) {\,*_{\scriptsize\rm ev}\,}{\mathbf{B}}_a q \models \neg {\mathbf{B}}_a \neg p\), for \(u^{ q; p} \in W^{ q; p}\) such that \((s^{ q; p}, u^{ q; p}) \in R^{ q; p}_a\) iff \((s^{ q}, u^{ q}) \in R^{ q}_a\) and \(\pi^{ q}(u^{ q}) \models p\). This implies that \(u^{ p} \in W^ p\) and \((s^ p, u^ p) \in R^ p_a\).

   \((M,s) {\,*_{\scriptsize\rm ev}\,}{\mathbf{B}}_a q \models \neg {\mathbf{B}}_a \neg p\) also implies that \((M,s) \models \neg {\mathbf{B}}_a \neg p\). Therefore, for every \(u\in R_a(s)\) such that \(u^{ p} \in W^ p\) and \((s^ p, u^ p) \in R^ p_a\), we can conclude that \((s^{ q; p}, u^{ q; p}) \in R^{ q; p}_a\) because \(\models p \rightarrow q\). The above imply that \((K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a q) {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a p \doteq K{\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a p\) for this case.

2. \((M,s) \models {\mathbf{B}}_a \neg q\). This implies that \((M,s) \models {\mathbf{B}}_a \neg p\) and \(s^ q = (s, \delta^ q)\) and \((s^ q,u^ q) \in R^ q_a\) iff \(u^ q = (u,\delta^ q_a)\) and \(\pi^ q(u^ q) = \pi(u) \star q\). By the definition of \(\star\), we can show that \((M,s) \models {\mathbf{B}}_a \neg p\) implies \(\pi^ q(u^ q) \models \neg p\). This implies that \(s^{ q; p} = ((s, \sigma^ q), \delta^{ q; p})\) and for every \(u \in R_s(a)\), \((s^{ q; p}, u^{ q; p}) \in R^{ q; p}_a\), \((s^ q, u^ q) \in R^ q_a\), and \(\pi^{ q; p}(u^{ q; p}) = (\pi(u) \star q) \star p\). On the other hand, by construction of \((M,s) {\,*_{\scriptsize\rm ev}\,}{} p\), \(s^ p = (s, \delta^ p)\) and, for every \(u \in W\), \((s^ p,u^ p) \in R^ p_a\) where \(u^ p = (u,\delta^ p_a)\) and \(\pi^ p(u^ p) = \pi(u) \star p\). Again by definition of \(\star\), we have that \(\pi(u) \star p = (\pi(u) \star q) \star p\) for every \(u \in R_a(s)\). This proves that \((K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a q) {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a p \doteq K{\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a p\) for this case. \(\Box\)

We conclude this section with the introduction of an event-based revision operator, denoted by \({\,*_{\scriptsize\rm rb}\,}\), that satisfies all the generalized postulates if the underlying classical revision operator satisfies the classical postulates. The operator \({\,*_{\scriptsize\rm rb}\,}\) differs from \({\,*_{\scriptsize\rm ev}\,}\) in that it does not attempt to remove the agent’s uncertainty before revision. It employs the event model \[\mathbf{\Sigma}^a_b(\varphi) = \langle \Sigma, \{E_a\}_{a \in {\mathcal{A}}}, pre, \mathit{eff} \rangle\] where \(\Sigma = \{\sigma, \sigma_a, \epsilon\}\) and

• \(E_a = \{(\sigma,\sigma_a), (\sigma_a,\epsilon), (\epsilon,\epsilon)\}\);

• \(E_x = \{(\sigma,\epsilon), (\sigma_a,\epsilon), (\epsilon,\epsilon)\}\) for \(x \in {\mathcal{A}}\setminus \{a\}\);

• \(pre(\eta) = \top\) for every \(\eta \in \Sigma\); and

• for \(u \in W\), \(\mathit{eff}(u,\eta) = \pi(u)\) for \(\eta \in \Sigma \setminus \{\sigma_a\}\), and \(\mathit{eff}(u,\sigma_a) = \pi(u) \star \varphi\).

\((M^\varphi, s^\varphi)\), the result of \((M,s) {\,*_{\scriptsize\rm rb}\,}{\mathbf{B}}_a \varphi\), is defined similar to \((M,s) {\,*_{\scriptsize\rm ev}\,}{\mathbf{B}}_a \varphi\) with two changes: (i) \(\mathbf{\Sigma}^a_b(\varphi)\) is used instead of \(\mathbf{\Sigma}^a(\varphi)\) and (ii) \(s^\varphi = (s, \sigma)\). \({\,*_{\scriptsize\rm rb}\,}\) satisfies every postulate.

As a short proof sketch for this theorem, we observe the following properties of \((M,s) {\,*_{\scriptsize\rm rb}\,}\varphi\): For every \(u \in W\) and \(\lambda \in \Sigma\), \(u^\varphi = (u, \lambda) \in W^\varphi\). Furthermore, \((s^\varphi, u^\varphi) \in R^\varphi_a\) iff \((s,u) \in R_a(s)\) and \(\pi^\varphi(u^\varphi) = \pi(u) \star \varphi\). The conclusion of the theorem then relies on the following observations:

• for every \(u\), \(\pi^\varphi(u^\varphi) = \pi(u) \star \varphi \models \varphi\); and

• for every \(u\), if \(\pi(u) \star \varphi \not\models \neg \psi\) then \(\pi(u) \star \varphi \wedge \psi = (\pi(u) \star \varphi) + \psi\), and if \(\pi(u) \star \varphi \models \neg \psi\) then \((\pi(u) \star \varphi) + \psi\) is inconsistent.

8 Discussion and Outlook↩︎

We defined the problem of multi-agent belief revision (MBR) based on a single Kripke model as commonly used in epistemic reasoning about actions and planning, and we proposed a generalization of the AGM and DP postulates to this multi-agent case. We identified the challenges faced by the task of constructing MBR operators that adhere to all generalized postulates including those for iterated revision, and we presented results with a generalized full-meet operator and an event-based revision operator that satisfy most but not all of them.

Theorem 2 indicates that our generalized full-meet operator \({\,*_{\scriptsize\rm fm}\,}\) does not satisfy DP2. This is because \(K {\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a \varphi\) may include \({\mathbf{B}}_b \neg \psi\), and then further revision by \({\mathbf{B}}_b\psi\) erases all beliefs other than the new one, hence the conclusion of the postulate does not hold. For this reason, it is generally challenging to construct belief revision operators that satisfy DP2. Looking at the definition of \({\,*_{\scriptsize\rm fm}\,}\), it is obvious that the first challenge is the problem of dealing with false beliefs, i.e., defining \(K * {\mathbf{B}}_a \varphi\) given that \({\mathbf{B}}_a \neg \varphi \in K\). The second challenge is related to the revision of the accessibility relation of \(a\). More precisely, let us denote with \(R_a|\eta\) the set \(\{(s, u) \in R_a \mid \pi(u) \models \eta\}\) for \(\eta \in {\mathcal{L}}_{\mathcal{P}}\). Operator \({\,*_{\scriptsize\rm fm}\,}\) essentially removes \(R_a| \neg \varphi\) from consideration in constructing \(K {\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a \varphi\). Thus, if \(R_a |\neg \varphi \ne \emptyset\) then the set of worlds accessible by \(a\) in \(K {\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a \varphi\) is a proper subset of \(R_a\), the set of worlds accessible by \(a\) in \(K\), which prevents \({\,*_{\scriptsize\rm fm}\,}\) from satisfying DP2.

The above discussion implies that for a belief revision operator to satisfy the generalized DP postulates, it must deal with false beliefs as well as the accessibility relations of agents properly. We expect that ideas from studies of reasoning with false beliefs in dynamic epistemic logic [38] or using update models [39] can be helpful in addressing the first issue. To deal with the second issue, approaches based on a pre-order relation between Kripke models (see, e.g., the works by [33] ([33]) and [40] ([40])) might be necessary. It is worth noting that the premise of DP2, \(\vdash{\mathbf{B}}_b \psi \rightarrow {\mathbf{B}}_a \neg \varphi\), could also be considered as a culprit for this postualte not to be satisfied by \({\,*_{\scriptsize\rm fm}\,}\). Modifying the premise to \({\mathbf{B}}_b \psi \rightarrow {\mathbf{B}}_a \neg \varphi\,\in\, K\), and also requiring that \(a \ne b\), could be a viable alternative to generalizing DP2 worthy of consideration.

Turning to the issue of higher-degree beliefs, the generalized revision postulates presented in this paper focus on first-degree beliefs, which are arguably the most fundamental ones, and postulating anything about the retention or revision of higher-degree beliefs seems more difficult to justify. But of course the concrete revision operators discussed in this paper all do precisely define how all higher-degree beliefs, including common beliefs, are changed upon revision, too. It is therefore an interesting direction for future work to develop further generalizations of the AGM and DP postulates to higher-order beliefs, with the aim of classifying concrete multi-agent belief revision operators according to their treatment of each nested belief.

It is worth noting that the strong relationship between MBR and announcements, a type of actions specific to multi-agent domains and very important for epistemic planning, raises several interesting problems worthy of consideration, too, especially since higher-degree beliefs of agents are an important subject of study in formalizing announcement actions in the literature. Several approaches to dealing with announcements have been proposed, but the majority of them place restrictions on the announcements (e.g., only considering public announcements) and the relationship between different methods is hardly understood. A systematic evaluation of these approaches under the lens of a set of generalized postulates for MBR could provide insights into the development of a general approach to dealing with announcements. In this regard, we note that [41] ([41]) also discuss belief revision in the multi-agent case, as we did in this paper. Our approach differs in two key respects, however: First, they employ epistemic plausibility models as the underlying representation, whereas we adopt Kripke structures as used in dynamic epistemtic reasoning and planning. Second, an epistemic plausibility model contains a priori plausibility relations for agents that dictate how agents would revise their beliefs. In our approach, agents do not have such policies. A detailed comparison between the two approaches will be one of our interesting research topics in the near future. Similarly, [42] ([42]) discuss belief updates for epistemic actions over belief bases, and thus could also be used for agents to revise their beliefs when an announcment is made. However, their focus is to define the updates. It would be interesting to determine whether the result of the update by a private announcement “agent \(a\) was told that \(\varphi\)” satisfies the generalized postulates discussed in this paper, similar to our \({\,*_{\scriptsize\rm ev}\,}\) operator. Again, we leave this for future work.

Acknowledgements↩︎

This research was partially supported by the Australian Research Council (grant #DP250101822) and by the Australian Government through the CRC-P project Urban Copilot – AI accelerating where we build Australia’s future. The second author acknowledges the partial support of the NSF grants #2139028, #2139028, #2151254, and the internal IAAM grant #139198.

AI Declaration↩︎

AI tools were used solely for automated spelling and grammar checks and to provide stylistic suggestions.

Full Meet and Generalized AGM Postulates↩︎

For simplicity of the presentation, we include the proofs of all items in this document. As such, some proofs presented in the main body of the paper are repeated here.

8.0.1 Closure↩︎

By our definition, it is clear that \[K {\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi = {\rm\em Cn\/}(K {\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi).\]

8.0.2 Success↩︎

By definition, if \((M',s')\) is the result of expanding a belief set by \({\mathbf{B}}_a\varphi\), then \(\pi(v)\models\varphi\) for all \(v^r\in W'\) such that \((s',v^r)\in R'_a\). This implies \(K {\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi \models {\mathbf{B}}_a \varphi\).

8.0.3 Inclusion↩︎

1. Suppose that \({\mathbf{B}}_a\neg\varphi\not\in K_{(M,s)}\), then the definition of \({\,*_{\scriptsize\rm fm}\,}\) implies that \(K_{(M,s)}{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi\subseteq K_{(M,s)}+{\mathbf{B}}_a\varphi\).

2. If \({\mathbf{B}}_a\neg\varphi\in K_{(M,s)}\), then

   1. \(R'_a(s')=\emptyset\) where \((M',s')=(M,s)+{\mathbf{B}}_a\varphi\), hence \(K+{\mathbf{B}}_a\varphi\models{\mathbf{B}}_a\bot\) by Lemma 3, which implies that \(K_{(M,s)}+{\mathbf{B}}_a\varphi\models{\mathbf{B}}_a\psi\) for any proposition formula \(\psi\);

   2. for \(x\in{\mathcal{A}}\setminus\{a\}\), \((M_\emptyset,s)\models{\mathbf{B}}_x\psi\) if, and only if, \(\models\psi\); by Lemma 2 this holds for \((M_\emptyset,s)+{\mathbf{B}}_a\varphi\) as well, hence \(K_{(M_\emptyset,s)}+{\mathbf{B}}_a\varphi\models{\mathbf{B}}_b\psi\) only for tautologies \(\psi\).

   Taken together, \(K_{(M_\emptyset,s)}+{\mathbf{B}}_a\varphi\subseteq K_{(M,s)}+{\mathbf{B}}_a\varphi\), hence \(K_{(M,s)}{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi\subseteq K_{(M,s)}+{\mathbf{B}}_a\varphi\).

8.0.4 Vacuity↩︎

This holds by definition.

8.0.5 Consistency 1↩︎

Suppose \({\mathbf{B}}_a\varphi\) is consistent, i.e., \(\not\models\varphi\rightarrow\bot\).

1. If \({\mathbf{B}}_a\neg\varphi\not\in K_{(M,s)}\), then \((s',v^r)\in R'_a\) for some \(v^r\in W'\) such that \(\pi[v^r]\models\varphi\), where \((M',s')=(M,s)+{\mathbf{B}}_a\varphi\). Hence, agent \(a\) has cosistent beliefs in \(K_{(M,s)}{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi\).

2. If \({\mathbf{B}}_a\neg\varphi\in K_{(M,s)}\), then \((s',v^r)\in R'_a\) for some \(v^r\in W'\) such that \(\pi[v^r]\models\varphi\), where \((M',s')=(M_\emptyset,s)+{\mathbf{B}}_a\varphi\). Hence, agent \(a\) has cosistent beliefs in \(K_{(M,s)}{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi\).

8.0.6 Consistency 2↩︎

If \({\mathbf{B}}_a\varphi\) is consistent with \(K\) then the beliefs of any agent other than \(a\) do not change as a result of expanding \((M,s)\) by \({\mathbf{B}}_a\varphi\). If \({\mathbf{B}}_a\varphi\) is inconsistent, then any agent other than \(a\) has tautological beliefs only, hence does not have inconsistent beliefs.

8.0.7 Extensionality↩︎

If \(\models \varphi\leftrightarrow\psi\) then \((M,s)+{\mathbf{B}}_a\varphi\) and \((M,s)+{\mathbf{B}}_a\psi\) are identical Kripke structures for any \((M,s)\) by definiton.

8.0.8 Superexpansion↩︎

1. Suppose \({\mathbf{B}}_a\neg(\varphi\wedge\psi)\not\in K\). Since \(K\) is deductively closed, it follows that \({\mathbf{B}}_a\neg\varphi\not\in K\). Hence, agent \(a\) has consistent beliefs in \(K+{\mathbf{B}}_a(\varphi\wedge\psi)\), in \(K+{\mathbf{B}}_a\varphi\), and in \((K+{\mathbf{B}}_a\varphi)+{\mathbf{B}}_a\psi\). By Lemma 4 it follows that \((M,s)+{\mathbf{B}}_a(\varphi\wedge\psi)\models{\mathbf{B}}_a\chi\) iff \(\chi\in{\rm\em Cn\/}(\{\varphi\wedge\psi\}\cup\{\phi\in{\mathcal{B}}_{{\mathcal{A}},{\mathcal{P}}} \mid\;{\mathbf{B}}_a\phi\in K\})\). This is equivalent to \(\chi\in{\rm\em Cn\/}(\{\psi\}\cup{\rm\em Cn\/}(\{\varphi\}\cup\{\phi\in{\mathcal{B}}_{{\mathcal{A}},{\mathcal{P}}} \mid\;{\mathbf{B}}_a\phi\in K\}))\), which in turn by Lemma 4 is equivalent to \(\left(K+{\mathbf{B}}_a\varphi\right) + {\mathbf{B}}_a\psi\models{\mathbf{B}}_a\chi\). By Lemma 2 it follows that all other agents too have the same beliefs in \(K+{\mathbf{B}}_a(\varphi\wedge\psi)\) and in \((K+{\mathbf{B}}_a\varphi)+{\mathbf{B}}_a\psi\). We conclude that \(K {\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a(\varphi \wedge \psi) \subseteq (K {\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi) + {\mathbf{B}}_a\psi\).

2. Suppose \({\mathbf{B}}_a\neg(\varphi\wedge\psi)\in K\). By definition of \((M_\emptyset,s)+{\mathbf{B}}_a(\varphi\wedge\psi)\) and Lemma 4 it follows that, for any first-degree belief, \({\mathbf{B}}_a\phi\in K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a(\varphi\wedge\psi)\) iff \(\phi\in{\rm\em Cn\/}(\varphi\wedge\psi)\), and for \(x\in{\mathcal{A}}\setminus\{a\}\), \({\mathbf{B}}_x\phi\in K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a(\varphi\wedge\psi)\) iff \(\models\phi\).

   1. Suppose \({\mathbf{B}}_a\neg\varphi\not\in K\), then \((K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi)+{\mathbf{B}}_a\psi=(K+{\mathbf{B}}_a\varphi)+{\mathbf{B}}_a\psi\). From \({\mathbf{B}}_a\neg(\varphi\wedge\psi)\in K\) it follows that \({\mathbf{B}}_a\neg\psi\in K+{\mathbf{B}}_a\varphi\). Hence, \(a\) has inconsistent beliefs in \((K+{\mathbf{B}}_a\varphi)+{\mathbf{B}}_a\psi\) while the beliefs of all other agents \(x\in{\mathcal{A}}\setminus\{a\}\) are the same in \((K+{\mathbf{B}}_a\varphi)+{\mathbf{B}}_a\psi\) and \(K+{\mathbf{B}}_a(\varphi\wedge\psi)\).

   2. Suppose \({\mathbf{B}}_a\neg\varphi\in K\), then \((K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi)+{\mathbf{B}}_a\psi=(K_{(M_\emptyset,s)}+{\mathbf{B}}_a\varphi)+{\mathbf{B}}_a\psi\). Hence, \(a\)’s first-degree beliefs in \((K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi)+{\mathbf{B}}_a\psi\) are exactly the logical consequences of \(\varphi\wedge\psi\) while the beliefs of all other agents \(x\in{\mathcal{A}}\setminus\{a\}\) are the same in \((K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi)+{\mathbf{B}}_a\psi\) and \(K+{\mathbf{B}}_a(\varphi\wedge\psi)\).

   Taken together, \(K {\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a(\varphi \wedge \psi) \subseteq (K {\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi) + {\mathbf{B}}_a\psi\).

8.0.9 Subexpansion↩︎

The proof is identical to cases 1 and 2(b) for superexpansion.

Full-Meet and Generalized DP Postulates↩︎

8.0.10 DP1 – Successive revision respect↩︎

Suppose \({\mathbf{B}}_a\psi\) is consistent with \(K\), then so is \({\mathbf{B}}_a\varphi\) since \(\psi\models\varphi\). It follows that \(K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\psi = K_{(M,s)+{\mathbf{B}}_a\psi}\) and \((K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi){\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\psi=K_{((M,s)+{\mathbf{B}}_a\varphi)+{\mathbf{B}}_a\psi}\). The two Kripke structures are bisimilar except for unreachable worlds, hence they entail the same set of belief formulas:

• \((M_\varphi,s_\varphi)=(M,s)+{\mathbf{B}}_a\varphi\) contains the worlds \(W\) in \(M\) plus a replicate \(W_\varphi\) of these worlds such that a world is \(a\)-accessible from \(s_\varphi\) if, and only if, it is in \(W_\varphi\) and satisfies \(\varphi\). \((M',s')=(M_\varphi,s_\varphi)+{\mathbf{B}}_a\psi\) contains the worlds \(W\cup W_\varphi\) plus a replicate of these, \(W'\cup W'_\varphi\), such that a world is \(a\)-accessible from \(s'\) iff it is in \(W'\cup W'_\varphi\) and satisfies \(\varphi\wedge\psi\), which is equivalent to saying it satisfies \(\psi\) since \(\psi\models\varphi\); while none of the worlds in \(W_\varphi\) are reachable from \(s'\) because the only links from \(s_\varphi\) into worlds in \(W_\varphi\) are labeled with agent \(a\).

• \((M_\psi,s_\psi)=(M,s)+{\mathbf{B}}_a\psi\) contains the worlds \(W\) in \(M\) plus a replicate \(W_\psi\) of these worlds such that a world is \(a\)-accessible from \(s_\psi\) iff it is in \(W_\psi\) and satisfies \(\psi\).

It is easy to define a bisimulation for all the worlds reachable from \(s'\) and \(s_\psi\), respectively, by which each world in \(W\) is identified with itself and its replica in \(W'\), and each world in \(W_\psi\) is identified with the corresponding world in \(W'_\varphi\).

Suppose \({\mathbf{B}}_a\varphi\) is inconsistent with \(K\), then so is \({\mathbf{B}}_a\psi\) since \(\psi\models\varphi\). It follows that \(K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\psi = K_{(M_\emptyset,s)+{\mathbf{B}}_a\psi}\) and \((K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi){\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\psi=K_{((M_\emptyset,s)+{\mathbf{B}}_a\varphi)+{\mathbf{B}}_a\psi}\). Similar to the above it can be shown that the resulting pointed Kripke models entail the same set of beliefs.

Suppose \({\mathbf{B}}_a\varphi\) is consistent with \(K\) but \({\mathbf{B}}_a\psi\) is not, then \(B_a\psi\) is also inconsistent with \(K+{\mathbf{B}}_a\varphi\). It follows that \((K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi){\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\psi = K_{(M_\emptyset,s)+{\mathbf{B}}_a\psi} = K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\psi\).

8.0.11 DP2 – Irrelevance of superseded beliefs↩︎

Generalized full-meet does not satisfy weak DP, for the following reason: If \({\mathbf{B}}_b\psi\) is consistent with the current belief set \(K\) then \(K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_b\psi=K+{\mathbf{B}}_b\psi\), hence by Lemma 2, all agents retain all their beliefs when revising \(K\) set by \(b\)’s new belief. But if \(K\) is revised by \({\mathbf{B}}_a\varphi\) first and \(\models{\mathbf{B}}_b\psi\rightarrow{\mathbf{B}}_a\varphi\) holds then \((K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_b\varphi){\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_b\psi=K_{(M_\emptyset,s)}+{\mathbf{B}}_b\psi\), which implies that all other agents’ beliefs have been erased. The fact that full-meet does not satisfy DP2 mirrors a result in classical, single-agent belief revision [35].

For this reason, full-meet multi-agent belief revision satisfies only one direction of DP2, namely, revising by a belief that is then superseded by a second, contradictory belief never introduces more beliefs than revision with the second belief directly. To show this, we make a case distinction:

1. Suppose \(\models\varphi\leftrightarrow\bot\) then \({\mathbf{B}}_a\neg\varphi\in K\), hence \(K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi=K_{(M_\emptyset,s)}+{\mathbf{B}}_a\bot\), that is, there is no \(a\)-accessible world in \(s\) while all other agents’ first-degree beliefs are tautological proposition formulas. Consequently, \((K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi){\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_b\psi\subseteq K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_b\psi\).

2. Otherwise, \(\models{\mathbf{B}}_b\psi\rightarrow{\mathbf{B}}_a\varphi\) implies \(a=b\) and \(\psi\models\neg\varphi\), hence \(\varphi\models\neg\psi\). It follows that \({\mathbf{B}}_b\psi\not\in K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi\), hence \((K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi){\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_b\psi=K_{(M_\emptyset,s)}+{\mathbf{B}}_b\psi\), which implies \((K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi){\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_b\psi\subseteq K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_b\psi\).

8.0.12 DP3 – Consistency preservation across revisions↩︎

If \(\models\varphi\leftrightarrow\top\) then DP3 holds trivially. Otherwise, \({\mathbf{B}}_a\varphi\in K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_b\psi\) implies that \({\mathbf{B}}_b\psi\) is consistent with \(K*B_a\varphi\) unless \(\models\psi\rightarrow\bot\). But if the latter is true, then \(K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_b\psi=(K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi){\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_\psi=K_{(M_\emptyset,s)+{\mathbf{B}}_b\bot}\). In either case, DP3 follows.

8.0.13 DP4 – Minimal change when reaffirming a belief↩︎

It is easy to see that DP4 holds if \({\mathbf{B}}_b\psi\) is inconsistent with \(K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi\). In case it is consistent, DP4 follows from Lemma 2 and 4.

8.0.14 Independence↩︎

While generalized full-meet satisfies both DP3 and DP4, it does not satisfy the stricter postulate of Independence: Consider two agents \(a\not=b\) and a satisfiable but non-tautological proposition formula \(\varphi\). Suppose further that \({\mathbf{B}}_a\varphi\) is consistent with \(K\) but \({\mathbf{B}}_b\psi\) is not, then \({\mathbf{B}}_b\psi\) is also inconsistent with \(K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi\). It follows that \({\mathbf{B}}_a\varphi\not\in (K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_a\varphi) {\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_b\psi\). But in this case, \(a\) only believes in tautological proposition formulas in the revised set \(K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_b\psi=K_{(M_\emptyset,s)}+{\mathbf{B}}_b\psi\), hence \({\mathbf{B}}_a\neg\varphi\not\in K{\,*_{\scriptsize\rm fm}\,}{\mathbf{B}}_b\psi\), thus violating the postulate.

\(*_{\textrm{ev}}\) and Generalized AGM Postulates (Theorem 3)↩︎

In the following, we will assume that \(K\) is consistent and represented by \((M,s)\) with \(M = (W, \{R_x\}_{x \in {\mathcal{A}}}, \pi)\). We use \((M,s) {\,*_{\scriptsize\rm ev}\,}{\mathbf{B}}_a \varphi\) and \((M^\varphi,s^\varphi)\) interchangably and \(M^\varphi = (W^\varphi, \{R^\varphi_x\}_{x \in {\mathcal{A}}}, \pi^\varphi)\). Successive revisions such as \((K {\,*_{\scriptsize\rm ev}\,}{\mathbf{B}}_a \varphi) {\,*_{\scriptsize\rm ev}\,}{\mathbf{B}}_a \psi\) will be denoted by \((M^{\varphi; \psi}, s^{\varphi; \psi})\) etc. The superscript \(^\varphi\) is also attached to elements of \(\mathbf{\Sigma}^a(\varphi)\) whenever it is needed to differentiate two revisions, e.g., \(\mathbf{\Sigma}^a(\varphi)\) and \(\mathbf{\Sigma}^a(\psi)\). Furthermore, \(R_a(s|\varphi) = \{u \mid u \in R_a(s), \pi(u) \models \varphi\}\). We first prove some properties of the \(\star\) operation that will be used in the proofs of some postulates. In the proofs, we use conjunction of literals and set of literals. Furthermore, whenever we refer to conjunction of literals such as \(\varphi\), we assume that \(\varphi\) is consistent in the classical sense, i.e., \(\varphi \not\models \bot\). For a set of literals \(\varphi\), \(\neg \varphi\) denotes \(\{\neg \ell \mid \ell \in \varphi\}\). Let \(R\) be a set of inference rules, \(\varphi\) and \(\psi\) be sets of literals, \(p\) and \(q\) are literals, and \(u, u'\) be consistent interpretations of \({\mathcal{P}}\).

The following lemma is similar to Lemma 8.

8.0.15 Closure↩︎

By our definition, it is clear that \[K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a\varphi = {\rm\em Cn\/}(K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a\varphi).\]

8.0.16 Success↩︎

We show that \(K{\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a\varphi \models {\mathbf{B}}_a \varphi\). Consider two cases:

1. \((M,s) \models \neg {\mathbf{B}}_a \neg \varphi\), i.e., \(a\) does not believe in \(\neg \varphi\) before the revision. This implies that \(s^\varphi = (s, \sigma)\). Furthermore, because \(K\) is consistent, we have that \(R_a(s) \ne \emptyset\) and there exists some \(u \in W\) such that \((s,u) \in R_a\) and \(\pi(u) \models \varphi\) which implies that \(((s,\sigma), (u,\sigma_a)) \in R^\varphi_a\), i.e., \(R^\varphi(s^\varphi) \ne \emptyset\). In addition, if \(((s, \sigma), (u, \rho)) \in R^\varphi_a\) then \(\rho = \sigma_a\), and hence, \(\pi(u) \models \varphi\), because \(E_a\) contains only one element related to \(\sigma\), \((\sigma, \sigma_a)\), and \((s,u) \in R_a\). Thus, we have that \((M^\varphi, s^\varphi) \models {\mathbf{B}}_a \varphi\).

2. \((M,s) \models {\mathbf{B}}_a \neg \varphi\). This implies that \(s^\varphi = (s, \delta)\). Again, because \(K\) is consistent, we have that \(R_a(s) \ne \emptyset\) and for each \(u \in R_a(s)\), \(\pi(u) \models \neg \varphi\).

   By the construction of \((M^\varphi, s^\varphi)\), \(R^\varphi_a(s^\varphi) \ne \emptyset\).

   Consider \(u' \in R^\varphi_a(s^\varphi)\). We have that \(u ' = (u, \delta_a)\) for some \(u \in R_a(s)\), and hence, \(\pi^\varphi(u') = C_R((\pi(u) \cap \pi^\varphi(u')) \cup \{\varphi\})\), which implies \(\varphi \in \pi^\varphi(u')\). Therefore, we have that \((M^\varphi, s^\varphi) \models {\mathbf{B}}_a \varphi\).

8.0.17 Inclusion↩︎

Due to Lemma 2 and Lemma 6, it suffices to show that if \({\mathbf{B}}_a \phi \in K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a\varphi\) then \({\mathbf{B}}_a \phi \in K + {\mathbf{B}}_a\varphi\) holds. By definition of \((M',s')=K + {\mathbf{B}}_a\varphi\), we have that \(R'_a(s') = \emptyset\), i.e., \(a\) has inconsistent belief in \(K + {\mathbf{B}}_a\varphi\) if \((M,s) \models {\mathbf{B}}_a \neg \varphi\). Thus, the postulate holds trivially in this case. Therefore, we only need to consider the case that \((M,s) \models \neg {\mathbf{B}}_a \neg \varphi\). In this case, as shown in Case 1 above, we have that \(s^\varphi = (s, \sigma)\) and \(((s, \sigma), (u,\sigma_a)) \in R^\varphi_a\) implies that \((s,u) \in R_a\) and \(\pi(u) \models \varphi\). This implies that \((s^r,u^r) \in R'_a\) (Definition of Expansion). On the other hand, if \((s',u^r) \in R'_a\) then we can also conclude that \(((s, \sigma), (u,\sigma_a)) \in R^\varphi_a\). This implies that \((M',s') \models {\mathbf{B}}_a \phi\) iff \((M^\varphi ,s^\varphi) \models {\mathbf{B}}_a \phi\).

8.0.18 Vacuity↩︎

The proof of this postulate is the second part of the proof for Inclusion.

8.0.19 Consistency↩︎

Since \(K\) and \({\mathbf{B}}_a\varphi\) are consistent, \(R_a(s) \ne \emptyset\) and exactly one out of two cases in the proof for Success occurs. In any case, \((M^\varphi,s^\varphi)\) is defined and \(R^\varphi_a(s^\varphi) \ne \emptyset\). Together with Lemma 6, we have that \(K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a \varphi\) is consistent.

8.0.20 Extensionality↩︎

Assume that \(\models {\mathbf{B}}_a\varphi \leftrightarrow {\mathbf{B}}_b\psi\). This implies that \(\varphi \leftrightarrow \psi\) and \(a = b\). It is easy to see that \((e, \eta^\varphi) \in W^\varphi\) iff \((e, \eta^\psi) \in W^\psi\). Similarly, \(((u, \eta^\varphi), (v, \xi^\varphi)) \in R^\varphi_x\) iff \(((u, \eta^\psi), (v,\xi^\psi)) \in R^\psi_x\) for any agent \(x \in {\mathcal{A}}\). This shows that there is a bijection between \((M^\varphi, s^\varphi)\) and \((M^\psi, s^\psi)\) which proves that \({\,*_{\scriptsize\rm ev}\,}{}\) satisfies this postulate.

8.0.21 Superexpansion↩︎

Consider a proposition formula \(\phi\), Lemma 6 and Lemma 2 shows that \(K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a(\varphi \wedge q) \models {\mathbf{B}}_x \phi\) iff \((K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a\varphi) + {\mathbf{B}}_a \psi \models {\mathbf{B}}_x \phi\) for \(x \ne a\). So, to prove that \({\,*_{\scriptsize\rm ev}\,}\) satisfies this postulate, it suffices to show that \(K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a(\varphi \wedge \psi) \models {\mathbf{B}}_a \phi\) implies that \((K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a\varphi) + {\mathbf{B}}_a \psi \models {\mathbf{B}}_a \phi\).

Let \((M',s')\) denotes \((M^{\varphi},s^{\varphi}) + {\mathbf{B}}_a \psi\). The proof considers two cases, similar to the proof of Success.

1. \((M,s) \models \neg {\mathbf{B}}_a \neg (\varphi \wedge \psi)\). In this case, \(s^{\varphi \wedge \psi} = (s, \sigma^{\varphi \wedge \psi})\) and \((s^{\varphi \wedge \psi},u^{\varphi \wedge \psi}) \in R^{\varphi \wedge \psi}_a\) where \(u^{\varphi \wedge \psi} = (u,\sigma^{\varphi \wedge \psi}_a)\) iff \((s,u) \in R_a\) and \(\pi(u) \models (\varphi \wedge \psi)\). Since \((M,s) \models \neg {\mathbf{B}}_a \neg (\varphi \wedge \psi)\), we have that \((M,s) \models \neg {\mathbf{B}}_a \neg \varphi\), i.e., \(u \in R_a(s|\varphi \wedge \psi)\). This implies that \(s^{\varphi} = (s, \sigma^{\varphi})\), and \((s^{\varphi},u^{\varphi}) \in R^{\varphi}_a\) where \(u^{\varphi} = (u,\sigma^{\varphi}_a)\) iff \((s,u) \in R_a\) and \(\pi(u) \models \varphi\), i.e., \(u \in R_a(s|\varphi)\). Because \(R_a(s|\varphi) = R_a(s|\varphi \wedge \psi) \cup R_a(s|\varphi \wedge \neg \psi)\) and the construction of \((K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a\varphi) \models {\mathbf{B}}_a \phi\) we have \(R'_a(s') = \{u^r \mid u \in R_a(s), \pi(u) \models \varphi \wedge \psi\}\) which proves the consequence of the postulate in this case.

2. \((M,s) \models {\mathbf{B}}_a \neg (\varphi \wedge \psi)\). In this case, \(s^{\varphi \wedge \psi} = (s, \delta^{\varphi \wedge \psi})\) and for every \(u^{\varphi \wedge \psi}\) such that \((s^{\varphi \wedge \psi},u^{\varphi \wedge \psi}) \in R^{\varphi \wedge \psi}_a\) holds, we have \(u^{\varphi \wedge \psi} = (u,\delta^{\varphi \wedge \psi}_a)\) iff \((s,u) \in R_a\). Therefore, we can conclude that \(K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a(\varphi \wedge \psi) \models {\mathbf{B}}_a \phi\) iff for every \(u \in R_a(s)\), \(\pi(u) \star (\varphi \wedge \psi) \models \phi\). There are two cases:

   1. \((M,s) \models {\mathbf{B}}_a \neg \varphi\). In this case, similar arguments to the above allow us to conclude that \((s^{\varphi},u^{\varphi}) \in R^{\varphi}_a\) iff \(u^{\varphi} = (u,\delta^{\varphi}_a)\) for some \((s,u) \in R_a\) and \(\pi(u^\varphi) = \pi(u)\star \varphi\). Because of the construction of \((K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a\varphi) + {\mathbf{B}}_a\psi\), we have two cases:

      1. \(K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a\varphi \models {\mathbf{B}}_a \neg \psi\). In this case, \(a\) has inconsistent beliefs in \((K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a\varphi) + {\mathbf{B}}_a\psi\). Thus, the postulate holds trivially.

      2. \(K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a\varphi \models \neg {\mathbf{B}}_a \neg \psi\). In this case, we can conclude that \(R'_a(s') \ne \emptyset\). Furthermore, \((s',u') \in R'_a\) iff \(u' = u^\varphi\) and \(\pi(u^\varphi) \models \psi\). Lemma 7, Item 2, allows us to conclude that \(K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a(\varphi \wedge \psi) \models {\mathbf{B}}_a \phi\) implies \(K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a\varphi + {\mathbf{B}}_a \psi \models {\mathbf{B}}_a \phi\).

   2. \((M,s) \models \neg {\mathbf{B}}_a \neg \varphi\). Similar arguments as in Case 1 of the proof of Success, we have \(s^{\varphi} = (s, \sigma^{\varphi})\), and \((s^{\varphi},u^{\varphi}) \in R^{\varphi}_a\) where \(u^{\varphi} = (u,\sigma_a^{\varphi})\) iff \((s,u) \in R_a\) and \(\pi(u) \models \varphi\) which implies that \(\pi^{\varphi}(u^{\varphi}) \models \neg \psi\) for every \((s^{\varphi},u^{\varphi}) \in R^{\varphi}_a\). This means that \(a\)’s belief is inconsistent in \((K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a\varphi) + {\mathbf{B}}_a\psi\), and thus, the postulate also holds in this case.

8.0.22 Subexpansion↩︎

Similar to the proof of Superexpansion, it suffices to show that \((K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a\varphi) + {\mathbf{B}}_a \psi \models {\mathbf{B}}_a \phi\) iff \((K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a (\varphi \wedge \psi) \models {\mathbf{B}}_a \phi\). We consider two cases:

1. \((M,s) \models \neg {\mathbf{B}}_a \neg \varphi\). Because of \({\mathbf{B}}_a \neg \psi \not\in K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a \varphi\), we can conclude that there exists some \(u \in R_a(s)\) such that \(\pi(u) \models \varphi \wedge \psi\). The proof of the postulate for this case is then similar to the proof in of Superexpansion, Case 1.

2. \((M,s) \models {\mathbf{B}}_a \neg \varphi\). This also implies that \((M,s) \models {\mathbf{B}}_a \neg (\varphi \wedge \psi)\). This means that \(s^\varphi = (s, \delta)\) and for every \(u^\varphi \in W^\varphi\) such that \((s^\varphi, u^\varphi) \in R^\varphi_a\), it holds that \(u^\varphi = (u, \delta_a^\varphi)\) for some \(u \in R_a(s)\) and \(\pi^\varphi(u^\varphi) = \pi(u) \star \varphi\).

   Because \((M,s) {\,*_{\scriptsize\rm ev}\,}{\mathbf{B}}_a \varphi \not\models {\mathbf{B}}_a \neg \psi\), we conclude that there exists some \(u \in R_a(s)\) such that \(\pi(u) \star \varphi \models \psi\). It means that \(R'_a\), the accessibility relation of \(a\) in \((M,s) {\,*_{\scriptsize\rm ev}\,}{\mathbf{B}}_a \varphi + {\mathbf{B}}_a \psi\), consists of \((s', (u^\varphi)^r) \in R'_a\) such that \(u^\varphi = (u, \delta_a^\varphi)\), \(\pi^\varphi(u^\varphi) = \pi(u) \star \varphi\), and \(\pi^\varphi(u^\varphi) \models \psi\).

   Lemma 7 shows that \(\pi(u) \star \varphi + \psi = \pi(u) \star (\varphi \wedge \psi)\) if \(\pi(u) \star \varphi \models \psi\). This implies that \((s^{\varphi \wedge \psi}, u^{\varphi \wedge \psi}) \in R^{\varphi \wedge \psi}_a\). This, together with the arguments similar to that used in Casse 2(a.ii) of the previous proof, allows us to conclude that \((K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a\varphi) + {\mathbf{B}}_a \psi \models {\mathbf{B}}_a \phi\) iff \((K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a (\varphi \wedge \psi) \models {\mathbf{B}}_a \phi\).

\(*_{\textrm{ev}}\) and Generalized DP Postulates (Theorem 4)↩︎

For these postulates, we will restrict the formulas \(\varphi\) and \(\psi\) to single literals.

8.0.23 DP1 – Successive revision respect↩︎

Since \(\models {\mathbf{B}}_b p \rightarrow {\mathbf{B}}_a q\), we have that \(p \rightarrow q\) and \(a\) and \(b\) are identical. Therefore, we will show that \({\,*_{\scriptsize\rm ev}\,}\) satisfies this postulate by showing that if \(\models {\mathbf{B}}_a p \rightarrow {\mathbf{B}}_a q\) and \(K {\,*_{\scriptsize\rm ev}\,}{} B_a q \not\models {\mathbf{B}}_a \neg p\) hold then \((K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a q) {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a p \doteq K{\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a p\).

1. \((M,s) \models \neg {\mathbf{B}}_a \neg q\). So, if \((s^ q,u^ q) \in R^ q_a\) then \(u \in R_a(s)\) and \(\pi(u) \models q\) and \(\pi^q(u^q) = \pi(u)\).

   Since \((M,s) {\,*_{\scriptsize\rm ev}\,}{\mathbf{B}}_a q \models \neg {\mathbf{B}}_a \neg p\), for \(u^{ q; p} \in W^{ q; p}\) such that \((s^{ q; p}, u^{ q; p}) \in R^{ q; p}_a\) iff \((s^{ q}, u^{ q}) \in R^{ q}_a\) and \(\pi^{ q}(u^{ q}) \models p\). This implies that \(u^{ p} \in W^ p\) and \((s^ p, u^ p) \in R^ p_a\).

   \((M,s) {\,*_{\scriptsize\rm ev}\,}{\mathbf{B}}_a q \models \neg {\mathbf{B}}_a \neg p\) also implies that \((M,s) \models \neg {\mathbf{B}}_a \neg p\). Therefore, for every \(u\in R_a(s)\) such that \(u^{ p} \in W^ p\) and \((s^ p, u^ p) \in R^ p_a\), we can conclude that \((s^{ q; p}, u^{ q; p}) \in R^{ q; p}_a\) because \(\models p \rightarrow q\).

   The above imply that \((K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a q) {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a p \doteq K{\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a p\) for this case.

2. \((M,s) \models {\mathbf{B}}_a \neg q\). This implies that \((M,s) \models {\mathbf{B}}_a \neg p\) and \(s^ q = (s, \delta^ q)\) and \((s^ q,u^ q) \in R^ q_a\) iff \(u^ q = (u,\delta^ q_a)\) and \(\pi^ q(u^ q) = \pi(u) \star q\). Because \((M,s) \models {\mathbf{B}}_a \neg p\), we have that \(\pi^ q(u^ q) \models \neg p\) (Lemma  9). This implies that \(s^{ q; p} = ((s, \sigma^ q), \delta^{ q; p})\) and for every \(u \in R_s(a)\), \((s^{ q; p}, u^{ q; p}) \in R^{ q; p}_a\), \((s^ q, u^ q) \in R^ q_a\), and \(\pi^{ q; p}(u^{ q; p}) = (\pi(u) \star q) \star p\). On the other hand, by construction of \((M,s) {\,*_{\scriptsize\rm ev}\,}{} p\), \(s^ p = (s, \delta^ p)\) and, for every \(u \in W\), \((s^ p,u^ p) \in R^ p_a\) where \(u^ p = (u,\delta^ p_a)\) and \(\pi^ p(u^ p) = \pi(u) \star p\). Lemma 9 indicates that \(\pi(u) \star p = (\pi(u) \star q) \star p\) for every \(u \in R_a(s)\). This proves that \((K {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a q) {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a p \doteq K{\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a p\) for this case.

8.0.24 DP2 – Irrelevance of superseded beliefs↩︎

As in DP1, \(\models{\mathbf{B}}_b p \rightarrow {\mathbf{B}}_a\neg q\) implies that \(a = b\) and \(p \rightarrow \neg q\). As such, we need to show that if \(K \models {\mathbf{B}}_a p \vee {\mathbf{B}}_a q\) then \({\mathbf{B}}_a p \models {\mathbf{B}}_a \neg q\;\Rightarrow\;(K{\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a q) {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a p \doteq K{\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a p\).

1. \((M,s) \models {\mathbf{B}}_a p\). Then, \((M,s) \models {\mathbf{B}}_a \neg q\). Therefore, \(s^ q = (s, \delta^ q)\) and for every \(u \in R_a(s)\), \((s^q,u^q) \in R^q_a\) where \(u^q=(u,\delta_a^q)\) and \(\pi^q(u^q) = \pi(u) \star q\). Lemma 9 implies that \(\pi^q(u^q) \models \neg p\). Thus, we can conclude that for every \(u \in R_a(s)\), \((s^{q;p},u^{q;p}) \in R^{q;p}_a\) where \(u^{q;p}=(u^q,\delta_a^{q;p})\) and \(\pi^{q;p}(u^{q;p}) = \pi^q(u^q) \star p = (\pi(u) \star q) \star p\). It is easy to see that \((\pi(u) \star q) \star p = u\) which, together with the fact \((M,s) \models {\mathbf{B}}_a p\), proves that \((K{\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a q) {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a p \doteq K{\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a p\).

2. \((M,s) \models {\mathbf{B}}_a q\). Then, \((M,s) \models {\mathbf{B}}_a \neg p\). Then, we can easily show that for every \(u \in R_a(s)\),

   • \(u^{q;p} = ((u, \sigma^q), \delta^{q;p}_a) \in R_a(s^{q;p}\) and \(\pi^{q;p}(u^{q;p}) = \pi^q(u^q) \star p = (\pi(u) \star q) \star p = \pi(u) \star p\); and

   • \(u^{p} = (u, \delta^{p}_a) \in R_a(s^{p}\) and \(\pi^{p}(u^{p}) = \pi(u) \star p\).

   The above two properties show that \((K{\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a q) {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a p \doteq K{\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a p\).

8.0.25 DP3 – Consistency preservation across revisions↩︎

The operator \({\,*_{\scriptsize\rm ev}\,}{}\) satisfies this postulate due to Lemma 6 and the Success postulate: \({\mathbf{B}}_a\varphi \in (K{\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a\varphi)\).

8.0.26 DP4 – Minimal change when reaffirming a belief↩︎

Assume that \(a\) has consistent belief in \(K\). Because of Lemma 6, \({\mathbf{B}}_a\varphi \in (K{\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_a\varphi) {\,*_{\scriptsize\rm ev}\,}{} {\mathbf{B}}_b \psi\). if \({\mathbf{B}}_a \neg \varphi \in (K{\,*_{\scriptsize\rm ev}\,}{}{\mathbf{B}}_a\varphi) {\,*_{\scriptsize\rm ev}\,}{}{\mathbf{B}}_b \psi\), it means that \(a\) has inconsistent belief in \(K{\,*_{\scriptsize\rm ev}\,}{}{\mathbf{B}}_a\varphi\) which implies that \(a\) has inconsistent belief in \(K\). This contradicts the assumption. This proves the postulate.

8.0.27 Independence↩︎

Similar to DP4.

Properties of \(*_{\textrm{rb}}\) (Theorem 5)↩︎

To prove this theorem, we observe the following properties of \((M,s) {\,*_{\scriptsize\rm rb}\,}\varphi\): for every \(u \in W\) and \(\lambda \in \Sigma\), \(u^\varphi = (u, \lambda) \in W^\varphi\). Furthermore, \((s^\varphi, u^\varphi) \in R^\varphi_a\) iff \((s,u) \in R_a(s)\) and \(\pi^\varphi(u^\varphi) = \pi(u) \star \varphi\). It is easy to see that the generalized AGM postulates hold because of the following properties of the propositional belief operator \(\star\)

• for every \(u\), \(\pi(u^\varphi) = \pi(u) \star \varphi \models \varphi\);

• for every \(u\) if \(\pi(u) \star \varphi \not\models \neg \psi\) then \(\pi(u) \star \varphi \wedge \psi = (\pi(u) \star \varphi) + \psi\); and if \(\pi(u) \star \varphi \models \neg \psi\) then \((\pi(u) \star \varphi) + \psi\) is inconsistent.

The generalized DP postulates also hold because of the properties of \(\star\) (Lemma 8-9) and the fact that successive revisions do not remove from or add elements to the accessibility relation of \(a\).

References↩︎