Two Logical Faces of Belief Revision

Abstract

This piece proposes a style of thinking using modal frame correspondence that puts Segerberg’s dynamic doxastic logic and ‘Dutch’ dynamic-epistemic logic for belief change in one setting. While our technical results are elementary, they do suggest new lines of thought.

Krister Segerberg’s seminal work has been a beacon in modal logic ever since the late 1960s. Add the attractive personality to the deep intellect, and one understands why my writing in this volume is a case of duty coinciding, not just with Kantian inclination, but with active desire.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Two Modal Logics for Belief Change

Belief revision theory is a small corner of the world of philosophy and computer science, and modal logic is a small corner of the world of logic. When two specialized topics come together, surely, there can be only one way of doing that? The dynamic-doxastic logic DDL of Segerberg’s [24, 25] ¹ has abstract modal operators describing transitions in abstract universes of models to describe changes in belief, and then encodes basic postulates on belief change in modal axioms that can be studied by familiar techniques. But there is also another line in the logical literature, started in [3, 31]² that works differently. Here belief changes are modeled in the framework of dynamic-epistemic logic (DEL) as acts of changing a plausibility ordering in a current model, and the update rule for doing that is made explicit, while its properties are axiomatized completely in modal terms. The contrast may be stated as follows. Segerberg follows AGM belief revision theory [9] in its postulational approach constraining spaces of all possible belief changes, while the DEL approach is constructive, studying specific update rules and the complete logics of their corresponding dynamic model-changing modalities. Stated this way, there need not be any conflict between the two approaches—and in fact, there is not. Still, there are many differences in their subsequent technical agenda.³ One could spend much time analyzing these differences, but my aim in this paper is modest. I want to suggest that, for colleagues from modal logic, DDL and DEL fit very well, if we use the method of frame correspondence. This suggestion occurs in [36], but I will pursue it more systematically here. My results are simple technically, but they suggest new perspectives. I start with knowledge in Sect. 2, exploring frame correspondences for ‘public announcement logic’ PAL. Many general methodological points can be made at this level, as they are not specific to belief. Next, I give modal correspondence for logics of belief change in Sect. 3. In Sect. 4, I discuss two generalizations: full dynamic-epistemic logic with product update over event models, and an extension of correspondence analysis to neighborhood models, using the DEL treatment in van [36]. Section 5 lists new general issues coming to light in my analysis, all of them ‘to be explored’. Section 6 states the conclusion of this paper, though it will already be clear right here at the start: the two existing styles of modal logic for belief revision live well together, and analyzing their connections actually reveals some interesting issues that will unfold in due course.

2 Correspondence for Information Update and Knowledge

We start with a phenomenon that is not very interesting in the AGM style, though it becomes wildly exciting when we study it in a constructive setting: update with new hard information that shrinks agents’ current ranges of epistemic options for the actual situation.

2.1 Hard Information, Knowledge, and Public Announcement Logic

Basic epistemic logic We start by recalling some basics. Standard epistemic logic EL describes semantic information encoded in agents’ ranges of uncertainty. The language extends propositional logic with modal operators $K_{i} \varphi$ (i knows that $\varphi$), for agents i, and $C_{G} \varphi$ ($\varphi$ is common knowledge in group G). Epistemic models ${{\varvec{M}}} = (W, \{\sim _{i}\}_{i\in I}, V)$ have a set of worlds $W$, accessibility relations $\sim _{i}$ for agents $i$ in some total group $I$, and a valuation $V$ for proposition letters. Pointed models (${{\varvec{M}}}, s$) mark a actual world $s$.⁴ The key truth condition is that ${{\varvec{M}}}, s \models K_{i}\varphi$ iff for all worlds $t$ with $s \sim _{i} t: {{\varvec{M}}}, t \models \varphi .$ ⁵ $^{,}$ ⁶ Complete logics capturing epistemic reasoning about oneself and others are known [8]. The base system is a minimal modal logic. A restriction to equivalence relations adds S5 axioms of positive and negative introspection, while the complete logic of common knowledge can be axiomatized with PDL-techniques.

Information update by elimination Now for the logical dynamics of information flow. An event $!\varphi$ yielding the information that $\varphi$ is true shrinks the current model to just those worlds that satisfy $\varphi$. This is the well-known notion of public hard information. More precisely, for any epistemic model ${{\varvec{M}}}$, world s, and formula $\varphi$ true at s, the new (${{\varvec{M}}} {\vert }\varphi , s$) (${{\varvec{M}}}$ relativized to $\varphi$ at s) is the sub-model of ${{\varvec{M}}}$ whose domain is the set $\{t\in {{\varvec{M}}} {\vert } {{\varvec{M}}}, t \models \varphi \}$. This mechanism models public communication, but also public observation. There is much more to this dynamics than meets the eye in standard views of ‘mere update’ with factual formulas. For instance, crucially, truth values of complex epistemic formulas may change after update: agents who did not know that $\varphi$ now do. Therefore, it makes sense to get clear on the exact dynamic logic behind this.

Public announcement logic The language of public announcement logic PAL adds action expressions to EL, plus matching modalities, defined by the syntax rules:

$$\begin{aligned}&\mathrm{{Formulas}}\quad \quad \quad \quad \,\, F: p\,\vert \,\lnot \,\varphi \,\vert \,\varphi {\vee } \psi \,\vert \,K_{i} \varphi \,{\vert }\,C_{G}\,\varphi \,{\vert }\,\langle A \rangle \varphi \\&\mathrm{{Action\ expressions}}\quad { A}: { !F} \end{aligned}$$

The semantic clause for the dynamic action modality looks ahead between models:

$$\begin{aligned} {{\varvec{M}}}, s \models \langle !\varphi \rangle \psi \quad {\text {iff}}\quad {{\varvec{M}}}, s \models \varphi \; and \; {{\varvec{M}}} {\vert }P, s \models \psi \end{aligned}$$

PAL is axiomatized by any complete logic over static models plus recursion axioms

$$\begin{aligned} \langle !\varphi \rangle q&\leftrightarrow (\varphi {\wedge } q)\; {\textit{for proposition letters}}\; q\\ \langle !\varphi \rangle (\psi {\vee } \chi )&\leftrightarrow (\langle !\varphi \rangle \psi {\vee }\langle !\varphi \rangle \chi )\\ \langle !\varphi \rangle \lnot \psi&\leftrightarrow (\varphi {\wedge } \lnot \langle !\varphi \rangle \psi )\\ \langle !\varphi \rangle \,\diamond \,\psi&\leftrightarrow (\varphi {\wedge } \diamondsuit \langle !\varphi \rangle \psi ) \end{aligned}$$

Intuitively, the final recursion axiom for knowledge captures the essence of getting hard information. We will see in just which sense this is true in our further analysis. For further theory and applications of PAL and related systems, cf. [1, 3, 28, 36].

2.2 Switching Directions: From Valid Axioms to Constraints

PAL is about one constructive way of taking incoming hard information: elimination of incompatible worlds. Now we reverse the perspective. Let us ask which postulates look plausible for hard update, of course, always keeping in mind that our intuitions need to be valid for arbitrary propositions, bringing the logic in harmony.⁷ Having done that, we can see which transformations of models validate them. This sounds grand. In what follows, however, I take a simple approach, investigating the recursion axioms of PAL themselves as postulates, since they have a lot of general appeal. To make this work, we need a suitably abstract setting—close to the models of DDL.⁸

Update universe and update relations Consider any family ${{\varvec{\mathsf{{ M}}}}}$ of pointed epistemic models $({{\varvec{M}}}, s)$, viewed as an ‘update universe’ where model changes can take place. Possible changes are given as a family of update relations $R_{P} ({{\varvec{M}}}, s) ({{\varvec{N}}}, t)$ relating pointed models, where the index set P is a subset of M: intuitively, the proposition triggering the update. One can think of the R as recording the action of some update operation

occurring in the syntax of our language that depends on the proposition P. Here different operations can have different effects: from our hard updates $!\varphi$ to the soft updates ${\Uparrow \!\!\varphi }$ to be discussed below. As just said, this is essentially the semantic setting of Krister Segerberg’s dynamic doxastic logic, where each transition relation has a matching modality.⁹ Now, for each formula $\varphi$, let $[[\varphi ]]$ be the set of worlds in ${{\varvec{M}}}$ satisfying $\varphi$. We set, for the update modality matching the relation R:

Remark To be yet more precise, we are really interpreting our language in a three-index format ${{\varvec{\mathsf{{ M}}}}},{{\varvec{M}}}, s$, and for the accessibility relations R in this update universe ${{\varvec{\mathsf{{ M}}}}}$, we have that $({{\varvec{M}}}, s) R ({{\varvec{M}}}, t)$ iff Rst in ${{\varvec{M}}}$, without any jumps out of the model ${{\varvec{M}}}$. This precision can be ignored for most of what follows, but it will come up occasionally.

2.3 A Correspondence Theorem for Eliminative Update

In what follows, the reader is supposed to know how modal frame correspondence works: cf. the textbooks van Blackburn, [5, 34]. We will analyze the PAL recursion axioms one by one in this style to see what they say, as a way of determining their total content as a correspondence constraint on update operations. But before doing so, we need to address a subtlety.

Substitution closure Correspondence arguments use frame truth of modal formulas, i.e., truth under all possible valuations for the proposition letters. Thus, if a formula is true, so are all its substitution instances: proposition letters are schematic variables for arbitrary propositions. But this sits badly with the system PAL, whose valid principles are not closed under substitution. In particular, the base axiom $\langle !\varphi \rangle q \leftrightarrow (\varphi {\wedge } q)$ is only valid for proposition letters q. Substituting to the general form $\langle !\varphi \rangle \psi \leftrightarrow (\varphi {\wedge } \psi )$ yields obviously invalid instances for epistemic assertions $\psi$. Much can be said about this phenomenon (cf. [14]), but in this paper, we take a simple line. We will first analyze the substitution-closed principles of PAL, and then return to the correspondence status of the base axiom. Thus, for the moment, we only look at the following obviously substitution-closed special case:

$$\begin{aligned} \langle !\varphi \rangle T \leftrightarrow \varphi \end{aligned}$$

In our correspondence setting, substitution failures relate to the semantics of atomic propositions p. Inside one epistemic model ${{\varvec{M}}}$, the obvious choice seems to be sets of worlds. But in an update universe ${{\varvec{\mathsf{{ M}}}}}$ as above, propositions range over all pairs (${{\varvec{M}}}, s$), and hence one p could have different truth values at pairs (${{\varvec{M}}}, s$), (${{\varvec{N}}}, s$). We will view Greek letters in axioms as standing for such general context-dependent propositions in what follows, returning to the original view of PAL-atoms as sets of worlds later on. Finally, here is one more important convention in what follows:

Remark Throughout, we will fix announced formulas $\varphi$ in contexts $\langle !\varphi \rangle \psi$, refraining from varying these in correspondence. Think of distinguished fixed propositions.

Now we are ready to go through the axioms:

Base axiom The axiom $\langle !\varphi \rangle T \leftrightarrow \varphi$ says that, given any model ${{\varvec{M}}}$, the domain of the transition relation $R_{[[\varphi ]]}$ is the set of worlds satisfying $\varphi$ in ${{\varvec{M}}}$. In other words, our abstract update action has the truth of $\varphi$ as a necessary and sufficient precondition.

Disjunction axiom There is no special constraint expressed by the modal formula $\langle !\varphi \rangle (\psi {\vee } \chi ) \leftrightarrow \langle !\varphi \rangle \psi {\vee } \langle !\varphi \rangle \chi$, since this law holds for any transition relation.

Negation axiom One direction of this axiom expresses no constraint on the update operation: $(\varphi {\wedge } \lnot \langle !\varphi \rangle \psi )\rightarrow \langle !\varphi \rangle \lnot \psi$ is valid, given that $\phi$ is equivalent to $\langle !\varphi \rangle T$.But the converse $\langle !\varphi \rangle \lnot \psi \rightarrow (\varphi {\wedge } \lnot \langle !\varphi \rangle \psi )$, even just $\langle !\varphi \rangle \lnot \psi \rightarrow \lnot \langle !\varphi \rangle \psi$, says by a standard correspondence argument that the transition relation is a partial function ¹⁰:

$$\begin{aligned} {\text {if}} ({{\varvec{M}}}, s) R_{[[\varphi ]]}({{\varvec{N}}}, t)\; {\text {and}}\; ({{\varvec{M}}}, s) R_{[[\varphi ]]}({{\varvec{K}}}, u),\; {\text {then}}\; ({{\varvec{N}}}, t) = ({{\varvec{K}}}, u). \end{aligned}$$

Using this observation, we now simplify the original transition relations $R_{P}$ in the update universe to partial functions $F_{P}$ on pointed models. In particular, given any model ${{\varvec{M}}}$ with a subset P, we can meaningfully talk about its image $F_{P}[{{\varvec{M}}}$].

Knowledge axiom So far, we were just doing preliminaries. The heart of the matter is evidently the recursion axiom for knowledge: $\langle !\varphi \rangle \diamondsuit \psi \leftrightarrow (\varphi {\wedge } \diamondsuit \langle !\varphi \rangle \psi )$. The two directions of this clearly express two constraints on the update function—and together, they enforce a well-known notion from modal logic [23]:

Fact

The update function satisfies frame truth of $\langle !\varphi \rangle \diamondsuit \psi \leftrightarrow (\varphi {\wedge } \diamondsuit \langle !\varphi \rangle \psi )\;$ iff every map $F_{P}$ is a p-morphism between ${{\varvec{M}}}$ and $F_{P}[{{\varvec{M}}}]$.

Proof

We do this first proof in a bit of detail, mainly to show how simple correspondence arguments for update functions are. Consider any model ${{\varvec{M}}}$, with $[[\varphi ]] = P$. First we show that $F_{P}$ is a homomorphism. Suppose that Rst in ${{\varvec{M}}}$, with s, t both in the domain of $F_{P}$. Now set $V(\psi ) = \{F_{P}(t)\}$. Then (${{\varvec{M}}}, s) \models \varphi {\wedge }\diamondsuit \langle !\varphi \rangle \psi$, and therefore also, $({{\varvec{M}}}, s) \models \langle !\varphi \rangle \diamondsuit \psi$. By the definition of $V(\psi )$, this implies that $R$ $F_{P}(s) F_{P}(t)$. Next, for the backward clause of being a p-morphism, suppose that $R$ $F_{P}(s) u$, and now set $V(\psi ) = \{u\}$. Then we have $({{\varvec{M}}} , s)\models \langle !\varphi \rangle \diamondsuit \psi$. It follows from the truth of our axiom that $({{\varvec{M}}}, s)\models \varphi \diamondsuit \langle !\varphi \rangle \psi$, and hence there exists a point t in ${{\varvec{M}}}$ with Rst and $F_{P}(t) = u$. $\blacksquare$

Collecting all our observations so far, we have the following result:

Theorem

An update universe satisfies the substitution-closed principles of PAL

iff its transition relations $F_{P}$ are partial p-morphisms defined on the sets P.

Discussion This is not quite the formation of submodels in standard elimination. Here is why. First, having a $p$-morphism is enough for validity of the PAL axioms, so we found a generalization of the standard semantics that may be of independent interest. Also, contracting several worlds into one during update occurs naturally in the setting of PAL: cf. [36] on the use of bisimulation contractions in updating.¹¹

The base axiom once more Still, the above outputs enforced by our update mechanism are relational subframes, rather than submodels. What about the atomic propositions? PAL update assumes that these stay the same when a world does not change. Here is how we can think of this. Consider the usual proposition letters of epistemic logic as distinguished atomic propositions. The base axiom tells us that these special propositions have a special behavior: if they hold for an pointed model $({{\varvec{M}}}, s)$, they also hold for any of its update images under a map $F_{P}$, and vice versa:

$$\begin{aligned} ({{\varvec{M}}}, s) \models p\quad {\text {iff }}\quad F_{P}({{\varvec{M}}} , s) \models p \end{aligned}$$

This might be the only content to the base axiom: update maps respect distinguished atomic propositions. But we can say a bit more in correspondence style. We assumed that proposition letters ranged over all sets of pointed models in the update universe. Now introduce special ‘context-independent’ proposition letters q ranging only over special sets of pointed models, with the property that they only depend on worlds:

$$\begin{aligned} ({{\varvec{M}}} , s) \models q\quad {\text {iff }}\quad ({{\varvec{N}}}, s) \models q,\quad {\text {for all models}}\; {{\varvec{M}}},{{\varvec{N}}}\ {\text {in}}\ {{\varvec{\mathsf{{ M}}}}} \end{aligned}$$

Fact

An update universe satisfies the base axiom $\langle !\varphi \rangle q \leftrightarrow (\varphi \; {\wedge } \;q)$ for all context-independent q iff the update maps are the identity on worlds:

$$\begin{aligned} F_{P} ({{\varvec{M}}}, s) = ({{\varvec{N}}}, s)\ {\text {for some model }} {{\varvec{N}}}. \end{aligned}$$

Proof

Consider any pointed model $({{\varvec{M}}}, s)$ in the domain of $F_{P}$. Now set $V(q) = \{({{\varvec{N}}}, s) {\vert } ({{\varvec{N}}}, s)$  is  in $\ {{\varvec{\mathsf{{ M}}}}}\}$. This is clearly a context-independent predicate. With this particular $V(q)$, the true implication $(\varphi \,{\wedge }\, q)\; \rightarrow \langle \varphi \rangle q$ then says that $F_{P} ({{\varvec{M}}}, s) = ({{\varvec{N}}}, s)$ for some model ${{\varvec{N}}}$.$\blacksquare$

Even so, models ${{\varvec{N}}}$ occurring in $F_{P}$-values for pointed models $({{\varvec{M}}}, t)$ with the same ${{\varvec{M}}}$ could still differ. We will soon see a further recursion law making this uniform.¹²

This concludes our discussion of the correspondence content of the PAL axioms.¹³

2.4 Variations, Extensions, and a Provocation

Recursion axioms as general postulates We have determined the update content of one specific axiom for update. But there is more to this. Dynamic-epistemic recursion axioms are not just ‘any sort of principle’. They have several features that make them candidates for general postulates on information update.¹⁴ In particular, our analysis says that the PAL recursion axiom for knowledge expresses a sort of partial bisimulation between the original model and the output of an update rule applied to it. I find abstract simulation behavior very appealing as a general semantic constraint on update functions, though I am not sure how to define it in its proper generality.¹⁵

Protocols Update universes also suggest a different setting, that has been proposed in dynamic-epistemic logic for independent reasons. So far, we had that $\langle !\varphi \rangle T \leftrightarrow \varphi$. This says that executing an action $!\varphi$ requires truth of the precondition $\varphi$, but also, whenever $\varphi$ is true, $!\varphi$ can be executed. But in civilized conversation or regimented inquiry, the latter assumption is often untenable. To represent this, ‘protocol models’ make restrictions on propositions that can be announced or observed. [15] shows how PAL changes in this setting, since the earlier recursion axioms will now be valid only with $\langle !\varphi \rangle T$ in the place of $\varphi$ on their right-hand sides. This move has many technical repercussions, though the system remains axiomatizable and decidable. From our correspondence perspective, nothing much changes: the only new thing is that the domain of an update map $F_{P}$ will now be a subset of P, but not necessarily all of P. Our analysis of the modified recursion axioms remains essentially as before.

Language extensions We analyzed update axioms for the epistemic base language. But PAL also has a complete version for the full epistemic language with common knowledge. The recursion axiom then requires a new notion of ‘conditional common knowledge’ [29]. Since the axiom for single-agent knowledge already fixed the PAL update rule, as we have seen, no further constraints arise. We will return later to what this ‘passive behavior’ of common knowledge vis-à-vis single-agent knowledge means in terms of definability or derivability.¹⁶ A useful language extension whose recursion axiom does add to our correspondence analysis introduces an existential modality $E\psi$ saying that $\psi$ is true in some world in the current model, accessible or not. In update universes ${{\varvec{\mathsf{{ M}}}}}$, we interpret this as saying, at a pointed model $({{\varvec{M}}}, s)$, that there is some t in ${{\varvec{M}}}$ with $\psi$ true at $({{\varvec{M}}}, t)$.

Fact

On update universes ${{\varvec{\mathsf{{ M}}}}}$ satisfying the earlier PAL update conditions, the axiom $\langle \varphi \rangle E\psi \leftrightarrow (\varphi \wedge E\langle !\varphi \rangle \psi )$ is frame-true iff, for every model ${{\varvec{M}}}$, the update images of worlds in ${{\varvec{M}}}$ have the same model ${{\varvec{N}}}$ throughout.

Proof

First, the axiom is clearly valid in the intended update universes. Conversely, its right to left direction implies the stated property. Consider any two worlds $({{\varvec{N}}}, t), ({{\varvec{K}}}, u)$ in the image $F_{P}{{\varvec{M}}}$. Set $V(\psi ) = \{({{\varvec{K}}}, u)\}$. Then the $F_{P}$-original of $({{\varvec{N}}}, t)$ in M satisfies $\varphi \wedge E\langle !\varphi \rangle \psi$. It follows that $\langle !\varphi \rangle E\psi$, and by the preceding definition, this only happens when $({{\varvec{N}}}, t)$ and $({{\varvec{K}}}, u)$ share the same model component.

$\blacksquare$

Finally, update universes suggest yet further language extensions. For instance, there is also a natural relation $({{\varvec{M}}}, s)$ $\sim ({{\varvec{N}}}, s)$ holding between different models sharing the same distinguished world. Its modality would make sense, even though it does not inside single epistemic models, the way basic epistemic logic works.

What is the right version of PAL? We conclude with a more provocative feature of our analysis. We started by analyzing what standard public announcement says about update, and then determined its force in update universes. But doing so involved a natural distinction between the substitution-closed principles of PAL and the more ‘accidental’ base axiom holding only for a restricted class of valuations. So, what is ‘public announcement logic’ after all? Is its base semantics perhaps the one on update universes with context-dependent propositions and substitution-closed validities? And if so, is what we call the ‘standard version’ perhaps an accident of formulation?

2.5 Other Natural Operations: Link Cutting

Update with hard information that $\varphi$ does show variety beyond the above elimination. In a well-known link-cutting variant, the operation ${\vert }\varphi$ performed announces whether $\varphi$ is the case. This means that the domain of worlds stays the same, but all epistemic links get cut between $\varphi$-worlds and $\lnot \varphi -worlds$ in the current model—an operation used by many authors. The changes induced in the PAL axioms are mainly these:

$$\begin{aligned}&\langle {\vert }\varphi \rangle q \leftrightarrow q\ (\text {this implies the substitution-closed instance} \langle {\vert }\varphi \rangle {\text { T}})\\&\langle {\vert }\varphi \rangle \diamondsuit \psi \leftrightarrow (\;(\varphi \,{\wedge }\, \diamondsuit (\varphi \,{\wedge }\, \langle {\vert }\varphi \rangle \psi ))\,{\vee }(\lnot \varphi \, {\wedge }\,\diamondsuit (\lnot \varphi \,{\wedge } \,\langle {\vert }\varphi \rangle \psi ))\;) \end{aligned}$$

The following result can be proved in the same correspondence style as before:

Fact

Link cutting is the only model-changing operation that satisfies the reduction axioms for the dynamic modality $\langle {\vert }\varphi \rangle$.

Proof

We merely give a sketch of the substitution-closed part. Start from any pointed model ${{\varvec{M}}}$, s. The modified base axiom tells us that the update map is now total on the whole domain of ${{\varvec{M}}}$. Next, the recursion axiom for knowledge, read from left to right, says that the only links in the image come from already existing links between either $\varphi$–worlds, or $\lnot \varphi$–worlds. Finally, from right to left, the axiom says that all links of the two mentioned types existing in ${{\varvec{M}}}$ get preserved into the image. $\blacksquare$

3 Correspondence Analysis of Modal Logics for Belief Change

Now that we have seen how to analyze principles of knowledge update by changing domains or accessibility relations, an extension to belief revision is straightforward. We mainly need to decide what models we will be working with.

3.1 Soft Information and Belief

Doxastic models are structures ${{\varvec{M}}}= (W, \{\le _{i}\}_{i\in I},V)$ where the $\le _{i}$ are binary comparison relations $\le _{i}$ xy saying that agent i considers x at least as plausible as y. As before, for convenience, we drop agent indices henceforth. These plausibility relations are usually taken to be reflexive and transitive, making the modal base logic S4—or also connected, like the ‘Grove models’ of belief revision theory, making the logic S4.3. Such options are important in practice, but they do not affect the analysis to follow.

These models encode varieties of information. While the whole domain represents our current hard information in the earlier sense, the most plausible worlds in the ordering $\le$ represent our soft information about the actual world. This soft information is the basis of our beliefs and actions based on these, but it is defeasible: the actual world may lie outside of the most plausible area, and we may learn this as a scenario unfolds. In this setting, belief is commonly interpreted as truth in all most plausible worlds¹⁷:

$$\begin{aligned} {{\varvec{M}}}, s \models B\varphi \ {\text {iff}}\ {{\varvec{M}}}, t \models \varphi \ { for\ all\ worlds\ t\ that\ are\ minimal\ in\ the\ ordering}\le \end{aligned}$$

But absolute belief does not suffice for most purposes. We need conditional belief ¹⁸:

$$\begin{aligned} {{\varvec{M}}}, s \models B^{\psi }\varphi \ {\text {iff}}\ {{\varvec{M}}}, t \models \varphi \ { for\ all}\ \le -{ minimal\ worlds\ in}\ \{u {\vert }{{\varvec{M}}}, u \models \psi \} \end{aligned}$$

This point returns with recursion axioms for belief change. From a systematic logical perspective, we should not analyze changes in beliefs only (the usual practice in belief revision theory), but also changes in conditional belief.

Conditional logic Complete logics for conditional belief can be found in close analogy with conditional logic based on similarity semantics [17]. One difference is that conditional models usually involve a ternary comparison ordering $\le _{z}$ xy: world x is closer to world z then world y. A generalization from binary to ternary relation also makes sense for plausibility semantics of belief, but we forego this here.¹⁹

Safe belief While the preceding belief modalities are interesting, it has become clear recently that the plain base modality of plausibility models has independent interest.

$$\begin{aligned} {{\varvec{M}}}, s \models \langle \le \rangle \varphi \quad {\text {iff}}\quad { there\ exists\ a\; point\; t}\ \ge s\ with\ {{\varvec{M}}}, t \models \varphi \end{aligned}$$

The matching universal modality offers an interesting doxastic notion in between knowledge and belief. Consider this picture with the actual world s in the middle:

$K\varphi$ describes what we know: $\varphi$ must be true in all three worlds in the range, less or more plausible than the current one. $B\varphi$ describes beliefs, which have to be true in the right-most world only. Now $[\le ]\varphi$ describes our safe beliefs, referring to the actual s plus the right-most world. These cannot be refuted by any future correct observations. Technically, safe belief can also define the other kinds of belief [6]:

$$\begin{aligned} \mathrm{{on\ finite\ pre}}\text {-}\mathrm{{orders}},\ B^{\psi }\varphi \ {\text {is defined by}}\ U(\psi \rightarrow \;\langle \le \rangle (\psi {\wedge } [\le ](\psi \rightarrow \, \varphi ))) \end{aligned}$$

with U the universal modality, or in epistemic-doxastic models, an appropriate knowledge modality. Thus, at least technically, an analysis of belief change might focus on safe belief without losing much.

3.2 Dynamic Logics of Belief Change

Now we can write complete logics for belief change. Indeed, there are several systems for this, depending on what kind of new information triggers the change.²⁰

Hard information For hard information, the complete dynamic logic is as follows:

Theorem

The logic of conditional belief under public announcements is axiomatized completely by

• (a) any complete static logic for the model class chosen,

• (b) the PAL recursion axioms for atomic facts and Boolean operations,

• (c) an axiom for conditional belief: $\langle !\varphi \rangle B^{\alpha }\psi \leftrightarrow (\varphi \,{\wedge }\,B\;^{\langle !\varphi \rangle ^\alpha }\langle \varphi \rangle \psi )$.

A similar analysis can be given for safe belief, with a simpler key recursion axiom

$$\begin{aligned} \langle !\varphi \rangle \langle \le \rangle \psi \leftrightarrow \;(\varphi \,{\wedge }\,\langle \le \rangle \langle !\varphi \rangle \psi ) \end{aligned}$$

Formally, this is just the earlier recursion axiom for a modality $\diamondsuit$.

Soft information and plausibility change Now comes a major further step. Triggers for belief change can be of many kinds, and we do not always expect the same model changes. In particular, incoming new information may be soft rather than hard, which means that it does not eliminate worlds, but merely rearranges the current plausibility order. A common example is a radical upgrade ${\Uparrow \!\!\varphi }$ changing the current ordering $\le$ between worlds in a model $({{\varvec{M}}}, s)$ to a new model $({{\varvec{M}}}{\Uparrow \!\!\varphi }, s)$ as follows:

$$\begin{aligned}&{\text {all }} \varphi {\text {--worlds in the current model become better than all}}\;\lnot \varphi {\text {--worlds}},\\&{\text {while, within those two zones, the old plausibility ordering remains}}. \end{aligned}$$

Like for public announcement, we introduce an upgrade modality into our language:

$$\begin{aligned} {{\varvec{M}}}, s \models \langle {\Uparrow \!\!\varphi } \rangle \psi \ \quad {\text {iff}}\quad \ {{\varvec{M}}} {\Uparrow \!\!\varphi }, s \models \psi \end{aligned}$$

The earlier techniques extend. Again there is a complete set of recursion axioms:

Theorem

The dynamic logic of lexicographic upgrade is axiomatized by

• (a) any complete static logic for the model class chosen,

• (b) the following recursion axioms:

  

Again, there is also an evident valid recursion axiom for changes in safe belief:

$$\begin{aligned} \langle {\Uparrow \!\!\varphi } \rangle \langle \le \rangle \psi \leftrightarrow { E}\;(\varphi \,{\wedge }\, \langle {\Uparrow \!\!\varphi } \rangle \psi )\, {\vee }\, (\lnot \varphi {\wedge } \langle \le \rangle \langle {\Uparrow \!\!\varphi } \rangle \psi ) \end{aligned}$$

Given the earlier modal definition of absolute and conditional belief in terms of safe belief, one can even derive the preceding recursion axioms from this one. Other belief change policies can be treated in the same style, using the relation transformers of [31] or the priority product update of [1].

3.3 Correspondence for Axioms of Belief Change

As before with knowledge, we can now invert the preceding results and use the key recursion axioms as constraints to determine the space of possible update operations. For update operations transforming plausibility relations only, leaving domains of models the same, a more complex correspondence proof than earlier ones shows:

Theorem

The recursion axioms of the dynamic logic of radical upgrade hold universally for an update operation on a universe of pointed plausibility models iff that operation is in fact radical upgrade.²¹

It is important to realize what is going on here. AGM-style postulates on changes in beliefs will not fix the relational transformation: we need to constrain the changes in conditional beliefs, since the new plausibility order encodes all of these. A similar analysis works for other revision policies, such as ‘conservative’ belief change. But actually, there is an easier road to such results, closer to earlier arguments.

Theorem

Radical upgrade is the only update operation validating the given recursion axioms for atoms, Booleans plus safe belief.

Proof

Suppose that the axiom is valid on a universe of plausibility models. The axiom for atoms tells us in particular that our update function is defined everywhere. Now consider any model $({{\varvec{M}}} , s)$. From left to right, taking $\psi$ to denote just one world $({{\varvec{N}}}, t)$ with $F_{P}({{\varvec{M}}} , s) \le ({{\varvec{N}}}, t)$, it follows that $({{\varvec{N}}}, t)$ was either the image of some $\varphi$–world in ${{\varvec{M}}}$, or $s \le$ u in ${{\varvec{M}}}$ for some world u mapped to $({{\varvec{N}}}, t)$, i.e., the new $\le$-link came from an old one originating in a $\lnot \varphi$–world. This means that each new relational link comes from the set defined by radical upgrade. That in fact all such links occur in the $F_{P}$-image of M follows by similar unpacking of the reverse implication of the recursion axiom. $\blacksquare$

Given this last correspondence result, the earlier more complex ones seem less urgent, since safe belief defines absolute and conditional belief. Indeed, philosophically plausible AGM-style postulates on ‘safe-belief change’ might be easier conceptually than those for regular belief.²²

3.4 Discussion: Generality of the Analysis

We have seen how recursion laws in constructive logics of belief change can serve as general postulates to constrain, and almost uniquely fix, possible updates. As before, this relates the DDL and DEL approaches to modal logics of belief change, softening a contrast that we started out with. Also as before, issues of generality arise. Are the recursion axioms too specific for belief change postulates? Here we repeat our earlier intuition of ‘simulation’ between input and output models of the transformation. One might add that a recursive postulate may itself be philosophically attractive as provi-ding the core ‘dynamic equation’ driving the process of update or revision. Finally, here is an issue more specific to belief. Given the overwhelming variety of belief revision policies, what is the general thrust of correspondence results like ours? We will return to this issue in Sect. 5, when discussing product update and other general mechanisms replacing a host of separate revision rules by one master rule plus richer input.²³ $^{,}$ ²⁴

4 Richer Formats as a Test Case

The style of analysis proposed here works on richer semantic formats for update than modal relational models. In this brief digression, we sketch two examples. These will also raise some issues about the scope and limitations of our earlier analysis.

4.1 Event Models and Product Update

While public announcement logic PAL is a good pilot system, its restriction to public information makes it unsuitable for analyzing individual differences in observation and communication. A much richer dynamic-epistemic logic for the latter tasks is true DEL [3, 10]. It uses action models ${{\varvec{E}}}$ that collect events with attached ‘preconditions’, with epistemic uncertainty links between events representing agents’ observational access to what actually happens. Action models have been used to represent a wide variety of triggers for information change. Next, by performing product update of an action model E with the current epistemic or doxastic model ${{\varvec{M}}}$ one obtains a new updated information model ${{\varvec{M}}} \times E$ displaying the right information for all agents involved after the event has taken place.

We assume that the reader knows how DEL update works, including its complete set of recursion axioms (cf. [36, 37] for details). We display two of these for later reference—suppressing agent indices as before, and using the letter R to denote the agent’s accessibility relation:

$$\begin{aligned}&\langle {{\varvec{E}}}, e \rangle T \quad \leftrightarrow \ Pre_{e}\\&\langle {{\varvec{E}}}, e \rangle \diamondsuit \psi \leftrightarrow (Pre_{e} {\wedge } \varvec{\vee }_{e R f \;in E}\diamondsuit \langle {{\varvec{E}}}, f \rangle \psi ) \end{aligned}$$

This mechanism changes epistemic or doxastic models much more drastically than the earlier world elimination or relation change. In particular, the set of new worlds $\{(s, e) {\vert } s \in {{\varvec{M}}}, e \in {{\varvec{E}}}, {{\varvec{M}}}, s \models Pre_{e}\}$ in ${{\varvec{M}}} \times E$ may grow beyond the size of the initial model ${{\varvec{M}}}$.

Theorem

The recursion axioms for the dynamic modality $\langle {{\varvec{E}}}, e \rangle \varphi$ of DEL determine product update uniquely modulo p-morphism.

The precise sense in which this definability assertion is true will emerge from the following discussion.

Proof sketch As in our study of PAL, we analyze the impact of the DEL recursion axioms on an update universe of epistemic models with an abstract transition relation for the update for the pointed event model $({{\varvec{E}}}, e)$. The negation axiom of DEL tells us that this is a partial function $F_{E, e}$. This functionality means that we can think of values $F_{E, e}({{\varvec{M}}}, s)$ as pairs $(s, e)$ without loss of information. Next, the substitution-closed base axiom tells us that $F_{E, e}$ is defined on those models $({{\varvec{M}}}, s)$ whose s satisfies the precondition of e in ${{\varvec{E}}}$. Finally, also as before, the DEL recursion axiom for individual knowledge puts constraints on the function $F_{E, e}$. First, if s R t in ${{\varvec{M}}}$, and e R f in ${{\varvec{E}}}$, while $F_{E, e}({{\varvec{M}}}, s)$, $F_{E, e}({{\varvec{M}}}, t)$ are both defined, then $(s, e) R (t, f)$ holds by the direction from right to left in the axiom. Vice versa, any link in the image of the model ${{\varvec{M}}}$ must also arise in this way, if we unpack the left-to-right direction of the axiom.²⁵

One update logic to bind them all? The preceding analysis may still be too piecemeal, ignoring a key innovation of DEL in the area of constructive update logics. An earlier trend had been to define specific model changes for particular kinds of informational event: ‘announcements that’, link cutting ‘announcements whether’, or more complex types of private information flow, such as sending a bcc message over email. One gets different complete logics for each case. But DEL changed the game. All relevant structure triggering different updates is put in matching event models ${{\varvec{E}}}$, and the logic for the special case is then a direct instance of the above ‘mother logic’ of $\langle {{\varvec{E}}}, e \rangle \varphi$. In this light, characterizing specific update functions may have some value, but the real logical insight is the general product update mechanism. Is the latter perspective, then, the best constructive counterpart to a postulational approach to update?

Belief and priority update Similar points can be made about belief revision. One can capture complete logics for specific revision policies, as we have shown. But one can also work at the level of product update with ‘plausibility event models’, where agents now may think it more plausible that one event occurred rather than another. Update works with the priority rule that strict event plausibility overrides prior plausibility²⁶:

$$\begin{aligned} (s, e) \le (t, f)\quad {\text {iff}}\quad (s \le t \;{\wedge }\; e \le f)\quad {\vee } e < f \end{aligned}$$

The key recursion axiom for the ‘mother logic’ is given in [1]:

$$\begin{aligned}&\langle {{\varvec{E}}}, e \rangle \langle \le \rangle \varphi \quad \leftrightarrow (Pre_{e} \,{\wedge }\, (\varvec{\vee }_{e \le f in E}\langle \le \rangle \langle {{\varvec{E}}}, f \rangle \varphi \, {\vee } ( \varvec{\vee } _{e < f in E}E\langle {{\varvec{E}}}, f \rangle \varphi )) \end{aligned}$$

We will not analyze this approach further, but as observed in our earlier discussion, this seems this seems the most general dynamic-epistemic counterpart to the postulational approach of dynamic doxastic logic.²⁷

4.2 Updating Neighborhood Models for Evidence

It is hard to roam for long in modal logic without finding Krister Segerberg’s traces. Another long-standing interest of his are neighborhood models [23] that have been used recently as a model for the epistemological notion of evidence and its dynamics (cf. [35] for technical details of what follows).

Static neighborhood logic An epistemic accessibility relation encodes an agent’s current range of worlds after some history of informational events. If we want to retain some of the latter ‘evidence’, a set of neighborhoods (sets of worlds) does well—where we think of the current range as the intersection of all evidence sets.²⁸ The simplest neighborhood models, and all that we consider here, have just one family ${{\varvec{\mathsf{{ N}}}}}$ of sets on a domain of worlds. We then interpret a matching evidence modality as follows:

$$\begin{aligned} {{\varvec{M}}}, s \models {\square } \varphi \quad {\text {iff}}\;\ { there\ is\ a\ set}\ X\ { in} \,{{\varvec{\mathsf{{ N}}}}}\ { with}\ {{\varvec{M}}}, t \models \varphi \ \textit{for}\ \textit{all}\ t\in X \end{aligned}$$

The base logic of this notion is that of a monotone modality that does not necessarily distribute over either disjunction or conjunction. This generalization of modal logic supports correspondence analysis.²⁹ Neighborhood models support many epistemic notions. At least in finite models, one can define (cautious evidence-based) belief as what is true in all intersections of maximally overlapping families of evidence.³⁰

Evidence dynamics: two samples In this setting, our pilot system PAL for information update can be seen as mixing different update actions into its public announcements $!\varphi$. The first is evidence addition +$\varphi$, adding the denotation $[[\varphi ]]$ in the current model as one more piece of evidence to the current evidence family ${{\varvec{\mathsf{{ N}}}}}$. The dynamic logic of this action can be determined completely. Here is one key recursion axiom:

$$\begin{aligned} \langle +\varphi \rangle \Box \psi \leftrightarrow (\Box \langle +\rangle \varphi \quad {\vee } U(\varphi \rightarrow \psi )) \end{aligned}$$

Again, the content of this principle can be determined by a correspondence argument:

Fact

An abstract update function on a universe of neighborhood models satisfies the recursion axiom for evidence addition iff each new evidence set is a superset of either some old evidence set or of the set $[[\varphi ]]$.³¹

A second aspect of a public announcement $!\varphi$ that now gets into its own is removal of the evidence for $\lnot \varphi$. The general new operation $-\psi$ removes all evidence sets from the current family ${{\varvec{\mathsf{{ N}}}}}$ that are included in $[[\psi ]]$. Complete recursion axioms are known for removal and the evidence modality, as well as belief, though a considerable extension of the standard static modal base languages over evidence models is required.³² Here is one relevant principle, using a notion of evidence conditional on $\lnot \varphi$ being true:

$$\begin{aligned} \langle -\varphi \rangle \Box \psi \;\leftrightarrow \; (E\lnot \varphi \; \rightarrow \; \Box _{\lnot \varphi }\langle -\varphi \rangle \psi ) \end{aligned}$$

We leave a correspondence analysis of recursion axioms for removal to future work.

Clearly, we have only scratched the surface here, but hopefully, the reader has seen that our analysis still makes sense when the semantic modeling of dynamic epistemic logic undergoes a drastic neighborhood extension of a sort that Krister Segerberg has long ago proposed for dynamic doxastic logic [11, 24].

5 Further Directions

We have shown how modal correspondence brings together the postulational format of AGM theory and dynamic doxastic logic with the constructive model transformation style of dynamic-epistemic logic. Our technical illustrations were very simple, and we opened up more new problems than closing old ones. Several technical and conceptual issues were already raised in the text. In this section we briefly mention a few more.

Extended semantic formats We have worked with binary accessibility relations for knowledge and belief. This analysis should be extended to ternary relational models, where plausibility can be world-dependent. Likewise, the analysis needs to be taken to the realm of neighborhood models, a natural finer modeling for belief and evidence.

Group knowledge and belief At the start of this paper, we said that a multi-agent perspective is crucial to DEL-style logics, but soon this social aspect vanished. One should also analyze update postulates for common knowledge or belief in our style.³³

‘Dancing with the stars’: propositional dynamic logic Common knowledge or belief go beyond the modal base language, being iterated modalities as found in dynamic logic PDL: another lifelong interest of Krister Segerberg. Iteration occurs naturally in dynamic-epistemic logic, also in the dynamic action component, as with repeated announcement or measurement. The resulting logical systems can be highly complex: cf. [19] on PAL with iteration, and [2] on limit phenomena with iterated radical update. Still PDL is no obstacle to our analysis. There have been some striking advances in the treatment of modal frame correspondence for non-first-order principles like Löb’s Axiom for provability logic of Segerberg’s Axiom for dynamic logic, making them fall under an extended Sahlqvist syntax matching the system LFP+FO, first-order logic with added fixed-point operators. New results and references are found in [27, 36].

Temporal setting and procedural information Both dynamic doxastic logic and DEL focus on single update steps. But equally essential is the temporal horizon. We make sense of local event in terms of global scenarios: a conversation, a process of inquiry, or a game. This ‘procedural information’ [15] suggests interfacing dynamic logics with temporal logics of knowledge and belief [1, 4, 20]. Existing results at interface take the form of representation theorems for ‘update evolution’: cf. [32]. One obvious question is how our correspondence results relate to representation theorems in the area of logics of belief. cf. [7].

General model theory The proofs in this paper were very simple. The recursion axioms all had Sahlqvist syntax (cf. the textbook [5]). One would like a correspondence analysis of axioms for belief change at the latter level of generality. Moreover, correspondence is not the only abstract analysis of concrete modal logics. The mechanism of model change behind the dynamic-epistemic logics in this paper invites reflection on their general features as modal logics. In an earlier book for Krister Segerberg, I gave a Lindström Theorem capturing basic modal logic in terms of bisimulation invariance and compactness. It would be of interest to take this further to capture the essentials of dynamic modal logics of model change.

Coda: have we really dealt with all logics of belief change? Do our two protagonists of dynamic-doxastic and dynamic-epistemic logic exhaust the field? My first attempt at doing modal logic of belief revision in [26] worked over a universe of information stages in the style of Beth or Kripke models for intuitionistic logic. An update with hard information was defined as a minimal upward move to a stage where the new information holds, while revision involved backtracking to the past and then going forward again to incorporate new information in conflict with what we thought so far. I am not sure how this third view relates to either DDL or DEL, though it, too, offers abstract spaces for a wide array of update actions.

6 Conclusion

We have shown how the two main logic approaches to belief change, Segerberg’s dynamic doxastic logic and the DEL tradition, co-exist in the perspective of modal frame correspondence. Indeed, ‘modal logic of belief revision’ has two dual aspects that belong together. This much was our contribution to translatability and interaction between frameworks. Our evidence was a set of very simple technical observations—but around these, many new problems came to light. To me, this agenda of unknowns seems a virtue of the proposed analysis. Krister and I have our work cut out for us. Finally, a confession is in order. In starting this study, I thought the main beneficiary would be DDL, as it could now import new ideas from the pressure-cooker of DEL. But as will be clear at various places in the paper, I now feel that a correspondence perspective also raises serious issues about best design for dynamic-epistemic logics, rethinking their striking deviant feature of being non-substitution-closed. And hence, I submit that both sides will benefit from the style of analysis presented here.