A Modal-Logic Translation of the AGM Axioms for Belief Revision 1

Abstract

Building on the analysis of Bonanno G. Artificial Intelligence 339 we introduce a simple modal logic containing three modal operators: a unimodal belief operator $B$ , a bimodal conditional operator > and the unimodal global operator $◻$ . For each AGM axiom for belief revision, we provide a corresponding modal axiom. The correspondence is as follows: each AGM axiom is characterized by a property of the Kripke–Lewis frames considered in Bonanno G. Artificial Intelligence 339 and, in turn, that property characterizes the corresponding modal axiom.

1. Introduction

The notions of belief and of belief revision have been studied extensively in the literature, although following different approaches.

Starting with Hintikka’s (Hintikka, 1962) seminal contribution, the notion of belief has been studied mainly within the context of modal logic. On the syntactic side a belief operator $B$ is introduced, with the intended interpretation of $B\varphi$ as ‘‘the agent believes $\varphi$ .’’ Properties of beliefs are then expressed by means of axioms, such as the positive introspection axiom $B\varphi \to BB\varphi$ , which says that if the agent believes $\varphi$ then she believes that she believes $\varphi$ . On the semantic side Kripke structures (Kripke, 1963) are used, consisting of a set of states $S$ together with a binary relation $\mathcal{B}$ on $S$ , with the interpretation of $s\mathcal{B}{s}^{\prime }$ as ‘‘at state $s$ the individual considers state $s^{\prime }$ doxastically possible.’’ The connection between syntax and semantics is then obtained by means of a valuation $V$ which associates with every atomic sentence $p$ the set of states where $p$ is true. The pair $⟨S,\mathcal{B}⟩$ is called a frame and the addition of a valuation $V$ to a frame yields a model. Rules are given for determining the truth of an arbitrary formula at every state of a model; in particular, the formula $B\varphi$ is true at state $s$ if and only if $\varphi$ is true at every state $s^{\prime }$ such that $s\mathcal{B}{s}^{\prime }$ . A property of the accessibility relation $\mathcal{B}$ is said to correspond to an axiom if every instance of the axiom is true at every state of every model based on a frame that satisfies the property and vice versa. For example, the positive introspection axiom $B\varphi \to BB\varphi$ corresponds to transitivity of the relation $\mathcal{B}$ .

On the other hand, the theory of belief revision, known as the AGM theory due to the seminal work of Alchourrón et al. (1985), has followed a different path. In this literature initial beliefs are modeled as a set of formulas $K$ in a propositional (modal-free) language and belief revision is modeled as a function that takes as input a Boolean formula $\varphi$ (thought of as new information) and gives as output a new set of formulas $K*\varphi$ interpreted as the revised beliefs. Properties of belief revision are expressed as properties of this function.

Several attempts have been made to bring the theory of belief revision within the umbrella of modal logic. Various modal languages have been proposed: some making use of conditionals (Boutilier, 1994; Giordano et al., 1998, 2001, 2005; Günther & Sisti, 2022), some employing belief, information and branching-time operators (Bonanno, 2007, 2012), some based on a revision operator and either a plausibility operator (Segerberg, 1998) or a conditional operator (Fuhrmann, 1991), some making use of knowledge, plausibility and time operators (Friedman & Halpern, 1997). Although all these papers aimed at formulating modal languages that captured the principles of AGM belief revision, none of them established a clear correspondence between the AGM axioms and modal axioms.

In this paper we provide a more systematic and principled integration of AGM belief revision into the apparatus of modal logic, thus unifying the theories of belief and belief revision under a common approach. We make use of the semantics introduced in Bonanno (2025)—based on frames consisting of a set of states, a Kripke belief relation and a Lewis selection function—to establish a precise correspondence between each AGM axiom and a modal axiom in a logic that contains three modal operators: a unimodal belief operator $B$ , a bimodal conditional operator > and the unimodal global operator $◻$ . The interpretation of $B\varphi$ is ‘‘the agent believes $\varphi$ ,’’ the interpretation of $\varphi >\psi$ is ‘‘if $\varphi$ is (or were) the case then $\psi$ is (or would be) the case’’ and the interpretation of $◻\varphi$ is ‘‘ $\varphi$ is necessarily true.’’ Adding a valuation to a frame yields a model. Given a model and a state $s$ , we identify the initial belief set $K_s$ with the set of formulas that are believed at state $s$ (i.e., $K_s=\{\varphi :s\models B\varphi \}$ ) and we identify the revised belief set $K_s*\varphi$ (prompted by the input represented by formula $\varphi$ ) as the set of formulas that are the consequent of conditionals that (1) are believed at state $s$ and (2) have $\varphi$ as antecedent (i.e., $K_s*\varphi =\{\psi :s\models B(\varphi >\psi )\}$ ). For each AGM axiom we provide a corresponding property of the Kripke–Lewis frames and identify an axiom in the modal language that, in turn, corresponds to that property, thereby providing a translation of each AGM axiom for belief revision into an axiom in the modal language.

The next section briefly reviews the AGM axioms for belief revision and the semantics put forward in Bonanno (2025), while Section 3 introduces the modal logic and provides axioms in that logic that correspond to the semantic properties that characterize the AGM axioms. Section 4 concludes. The longer proofs are relegated to the Appendix.

2. AGM Axioms and Their Semantic Characterization

We consider a propositional logic based on a countable set At of atomic formulas. We denote by ${\mathrm{\Phi }}_0$ the set of Boolean formulas constructed from At as follows: $\mathtt{\text{At}}\subset {\mathrm{\Phi }}_0$ and if $\varphi ,\psi \in {\mathrm{\Phi }}_0$ then $\mathrm{\neg }\varphi$ and $\varphi \vee \psi$ belong to ${\mathrm{\Phi }}_0$ . Define $\varphi \to \psi$ , $\varphi \wedge \psi$ , and $\varphi \leftrightarrow \psi$ in terms of $\mathrm{\neg }$ and $\vee$ in the usual way (e.g. $\varphi \to \psi$ is a shorthand for $\mathrm{\neg }\varphi \vee \psi$ ).

Given a subset $K$ of ${\mathrm{\Phi }}_0$ , its deductive closure $Cn(K)\subseteq {\mathrm{\Phi }}_0$ is defined as follows: $\psi \in Cn(K)$ if and only if there exist ${\varphi }_1,\dots ,{\varphi }_n\in K$ (with $n\ge 0$ ) such that $({\varphi }_1\wedge \cdots \wedge {\varphi }_n)\to \psi$ is a tautology. A set $K\subseteq {\mathrm{\Phi }}_0$ is consistent if $Cn(K)\ne {\mathrm{\Phi }}_0$ ; it is deductively closed if $K=Cn(K)$ . Given a set $K\subseteq {\mathrm{\Phi }}_0$ and a formula $\varphi \in {\mathrm{\Phi }}_0$ , the expansion of $K$ by $\varphi$ , denoted by $K+\varphi$ , is defined as follows: $K+\varphi =Cn(K\cup \{\varphi \})$ .

Let $K\subseteq {\mathrm{\Phi }}_0$ be a consistent and deductively closed set representing the agent’s initial beliefs and let $\mathrm{\Psi }\subseteq {\mathrm{\Phi }}_0$ be a set of formulas representing possible informational inputs. A belief change function based on $\mathrm{\Psi }$ and $K$ is a function $\circ :\mathrm{\Psi }\to 2^{{\mathrm{\Phi }}_0}$ ( $2^{{\mathrm{\Phi }}_0}$ denotes the set of subsets of ${\mathrm{\Phi }}_0$ ) that associates with every formula $\varphi \in \mathrm{\Psi }$ a set $K\circ \varphi \subseteq {\mathrm{\Phi }}_0$ , interpreted as the change in $K$ prompted by the input $\varphi$ . We follow the common practice of writing $K\circ \varphi$ instead of $\circ (\varphi )$ which has the advantage of making it clear that the belief change function refers to a given, fixed, $K$ . If $\mathrm{\Psi }\ne {\mathrm{\Phi }}_0$ then $\circ$ is called a partial belief change function, while if $\mathrm{\Psi }={\mathrm{\Phi }}_0$ then $\circ$ is called a full-domain belief change function.

Definition 2.1

Let $\circ :\mathrm{\Psi }\to 2^{{\mathrm{\Phi }}_0}$ be a partial belief change function (thus $\mathrm{\Psi }⊊{\mathrm{\Phi }}_0$ ) and ${\circ }^{\prime }:{\mathrm{\Phi }}_0\to 2^{{\mathrm{\Phi }}_0}$ a full-domain belief change function. We say that ${\circ }^{\prime }$ is an extension of $\circ$ if ${\circ }^{\prime }$ coincides with $\circ$ on the domain of $\circ$ , that is, if, for every $\varphi \in \mathrm{\Psi }$ , $K{\circ }^{\prime }\varphi =K\circ \varphi$ .

2.1. AGM Axioms

The following postulates for belief revision were proposed by Alchourrón, Gärdenfors and Makinson in Alchourrón et al. (1985) and are known as the AGM axioms.

Definition 2.2

A belief revision function, based on the consistent and deductively closed set $K\subset {\mathrm{\Phi }}_0$ (representing the initial beliefs), is a full domain belief change function $*:{\mathrm{\Phi }}_0\to 2^{{\mathrm{\Phi }}_0}$ that satisfies the following axioms: $\mathrm{\forall }\varphi ,\psi \in {\mathrm{\Phi }}_0$ ,

$(K*1)K*\varphi =Cn(K*\varphi )$ .

$(K*2)\varphi \in K*\varphi$ .

$(K*3)K*\varphi \subseteq K+\varphi$ .

$(K*4)\text{if}\mathrm{\neg }\varphi \notin K,\text{then}K\subseteq K*\varphi$ .

$(K*5)\{\begin{array}{ll}(K*5a)& \text{If }\mathrm{\neg }\varphi \text{ is a tautology, then }K*\varphi ={\mathrm{\Phi }}_0.\\ (K*5b)& \text{If }\mathrm{\neg }\varphi \text{ is not a tautology, then }K*\varphi \ne {\mathrm{\Phi }}_0.\end{array}$

$(K*6)\text{if}\varphi \leftrightarrow \psi \mathit{\text{ is a tautology then }}K*\varphi =K*\psi$ .

$(K*7)K*(\varphi \wedge \psi )\subseteq (K*\varphi )+\psi$ .

$(K*8)\text{ if }\mathrm{\neg }\psi \notin K*\varphi ,\text{ then }(K*\varphi )+\psi \subseteq K*(\varphi \wedge \psi ).$

$K*\varphi$ is interpreted as the revised belief set in response to the input represented by formula $\varphi$ . For a discussion of the above axioms see, for example, Fermé and Hansson (2018) and Gärdenfors (1988).

2.2. Kripke–Lewis Semantics

Definition 2.3

A Kripke–Lewis frame is a triple $⟨S,\mathcal{B},f⟩$ where

$S$ is a set of states; subsets of $S$ are called events.

$\mathcal{B}\subseteq S\times S$ is a binary belief relation on $S$ which is serial: $\mathrm{\forall }s\in S,\mathrm{\exists }{s}^{\prime }\in S$ , such that $s\mathcal{B}{s}^{\prime }$ ( $s\mathcal{B}{s}^{\prime }$ is an alternative notation for $(s,s^{\prime })\in \mathcal{B}$ ). We denote by $\mathcal{B}(s)$ the set of states that are reachable from $s$ by $\mathcal{B}$ : $\mathcal{B}(s)=\{s^{\prime }\in S:s\mathcal{B}{s}^{\prime }\}$ . $\mathcal{B}(s)$ is interpreted as the set of states that initially the agent considers doxastically possible at state $s$ .

$f:S\times (2^S\setminus \varnothing )\to 2^S$ is a selection function that associates with every state-event pair $(s,E)$ (with $E\ne \varnothing$ ) a set of states $f(s,E)\subseteq S$ . $f(s,E)$ is interpreted as the set of states that are closest (or most similar) to $s$ , conditional on event $E$ .

We require seriality of the belief relation because it ensures that the initial beliefs at state $s$ , represented by the non-empty set $\mathcal{B}(s)$ , are consistent, as assumed in the AGM approach. Similarly, the requirement that $f(s,E)$ is defined only if $E\ne \varnothing$ ensures that the informational input is consistent (the reaction to inconsistent information is discussed in Section 3). Note the absence, in Definition 2.3, of the extra properties imposed on the selection function in Bonanno (2025), namely,

$f(s,E)\subseteq E$ (Identity).

$f(s,E)\ne \varnothing$ (Normality).

if $s\in E$ then $s\in f(s,E)$ (Weak Centering).

The reason why we do not impose any properties on the selection function is that we want to highlight the role of each property in the characterization of the AGM axioms. For example, Identity (localized to $\mathcal{B}(s)$ ) plays a role in the characterization of $(K*2)$ but not in the characterization of the other axioms, Normality (localized to $\mathcal{B}(s)$ ) is used to characterize axiom $(K*5b)$ but not the other axioms, ² and a weaker form of Weak Centering is used in the characterization of axiom $(K*3)$ .

Adding a valuation to a frame yields a model. Thus a model is a tuple $⟨S,\mathcal{B},f,V⟩$ where $⟨S,\mathcal{B},f⟩$ is a frame and $V:\mathtt{\text{At}}\to 2^S$ is a valuation that assigns to every atomic formula $p\in \mathtt{\text{At}}$ the set of states where $p$ is true.

Definition 2.4

Given a model $M=⟨S,\mathcal{B},f,V⟩$ define truth of a Boolean formula $\varphi \in {\mathrm{\Phi }}_0$ at a state $s\in S$ in model $M$ , denoted by $s{\models }_M\varphi$ , as follows:

1. (1)

if $p\in \mathtt{\text{At}}$ then $s{\models }_{M}p$ if and only if $s\in V(p)$ ,

(2)

$s{\models }_M\mathrm{\neg }\varphi$ if and only if $s{⊭}_M\varphi$ ,

(3)

$s{\models }_M(\varphi \vee \psi )$ if and only if $s{\models }_M\varphi$ or $s{\models }_M\psi$ (or both).

We denote by $\Vert \varphi {\Vert }_M$ the truth set of formula $\varphi$ in model $M$ : $\Vert \varphi {\Vert }_M=\{s\in S:s{\models }_M\varphi \}.$

Given a model $M=⟨S,\mathcal{B},f,V⟩$ and a state $s\in S$ , let $K_{s,M}=\{\varphi \in {\mathrm{\Phi }}_0:\mathcal{B}(s)\subseteq \Vert \varphi {\Vert }_M\}$ ; thus a Boolean formula $\varphi$ belongs to $K_{s,M}$ if and only if at state $s$ the agent believes $\varphi$ , in the sense that $\varphi$ is true at every state that the agent considers doxastically possible at state $s$ . We identify $K_{s,M}$ with the agent’s initial beliefs at state $s$ . It is shown in Bonanno (2025) that the set $K_{s,M}\subseteq {\mathrm{\Phi }}_0$ so defined is deductively closed and consistent (recall the assumption that the belief relation $\mathcal{B}$ is serial).

Next, given a model $M=⟨S,\mathcal{B},f,V⟩$ and a state $s\in S$ , let ${\mathrm{\Psi }}_M=\{\varphi \in {\mathrm{\Phi }}_0:\Vert \varphi {\Vert }_M\ne \varnothing \}$ ³ and define the following partial belief change function $\circ :{\mathrm{\Psi }}_M\to 2^{{\mathrm{\Phi }}_0}$ based on $K_{s,M}$ :

$$\begin{array}{r}\begin{array}{l}\psi \in K_{s,M}\circ \varphi \text{ if and only if, }\mathrm{\forall }{s}^{\prime }\in \mathcal{B}(s),f(s^{\prime },\Vert \varphi {\Vert }_M)\subseteq \Vert \psi {\Vert }_M.\end{array}\end{array}$$

(RI)

Given the customary interpretation of selection functions in terms of conditionals, (RI) can be interpreted as stating that $\psi \in K_{s,M}\circ \varphi$ if and only if at state $s$ the agent believes that ‘‘if $\varphi$ is (were) the case then $\psi$ is (would be) the case.’’ ⁴   This interpretation will be made explicit in the modal logic considered in Section 3. In what follows, when stating an axiom for a belief change function, we implicitly assume that it applies to every formula in its domain. For example, the axiom $\varphi \in K\circ \varphi$ asserts that, for all $\varphi$ in the domain of $\circ$ ,   $\varphi \in K\circ \varphi$ .

Definition 2.5

An axiom for belief change functions is valid on a frame $F$ if, for every model based on that frame and for every state $s$ in that model, the partial belief change function defined by (RI) satisfies the axiom. An axiom is valid on a set of frames $\mathcal{F}$ if it is valid on every frame $F\in \mathcal{F}$ .

2.3. Frame Correspondence

A stronger notion than validity is that of frame correspondence. The following definition mimics the notion of frame correspondence in modal logic.

Definition 2.6

We say that an axiom $A$ of belief change functions is characterized by, or corresponds to, or characterizes, a property $P$ of frames if the following is true:

1. (1)

axiom $A$ is valid on the class of frames that satisfy property $P$ , and

(2)

if a frame does not satisfy property $P$ then axiom $A$ is not valid on that frame, that is, there is a model based on that frame and a state in that model where the partial belief change function defined by (RI) violates axiom $A$ .

The table in Figure 1 shows, for every AGM axiom, the characterizing property of frames. ⁵ The reason for the absence of axiom $(K*5a)$ from the table is explained in the next section.

Figure 1.

Semantic Characterization of the AGM Axioms.

The characterization for $(K*4),(K*7)$ and $(K*8)$ is proved in Propositions 9, 3 and 10, respectively, in Bonanno (2025). For the remaining AGM axioms we note the following.

Validity of $(K*1)$ on all frames is a consequence of Part (B) of Lemma 1 in Bonanno (2025).

Sufficiency for $(K*2)$ is proved in Item 2 of Proposition 1 in Bonanno (2025). For necessity, consider a frame that violates Property $(P*2)$ , that is, there exist $s\in S$ , $\varnothing \ne E\subseteq S$ and $s^{\prime }\in \mathcal{B}(s)$ such that $f(s^{\prime },E)⊈E$ . Construct a model where, for some atomic sentence $p$ , $\Vert p\Vert =E\ne \varnothing$ . Then, since $f(s^{\prime },\Vert p\Vert )⊈\Vert p\Vert$ and $s^{\prime }\in \mathcal{B}(s)$ , $p\notin K_s*p$ , yielding a violation of $(K*2)$ .

The proof for $(K*3)$ is as follows.

(A) Sufficiency. Consider a model based on a frame that satisfies Property $(P*3)$ . Let $\varphi \in {\mathrm{\Phi }}_0$ be such that $\Vert \varphi \Vert \ne \varnothing$ and let $s\in S$ and $\psi \in {\mathrm{\Phi }}_0$ be such that $\psi \in K_s*\varphi$ , that is, for every $s^{\prime }\in \mathcal{B}(s)$ , $f(s^{\prime },\Vert \varphi \Vert )\subseteq \Vert \psi \Vert$ , so that $\bigcup _{x\in \mathcal{B}(s)}f(x,\Vert \varphi \Vert )\subseteq \Vert \psi \Vert$ . Fix an arbitrary $s^{\prime }\in \mathcal{B}(s)$ . If $s^{\prime }\notin \Vert \varphi \Vert$ (i.e., $s^{\prime }\models \mathrm{\neg }\varphi$ ) then $s^{\prime }\models (\varphi \to \psi )$ . If $s^{\prime }\in \Vert \varphi \Vert$ , then by Property $(P*3)$ , $s^{\prime }\in \bigcup _{x\in \mathcal{B}(s)}f(x,\Vert \varphi \Vert )$ and hence $s^{\prime }\in \Vert \psi \Vert$ ; thus $s^{\prime }\models (\varphi \to \psi )$ . It follows that $(\varphi \to \psi )\in K_s$ and thus $\psi \in K_s+\varphi$ (since, by Lemma 2 in Bonanno (2025), $K_s$ is deductively closed) .

(B) Necessity. Consider a frame that violates $(P*3)$ , that is, there exist $s\in S$ , $s^{\prime }\in \mathcal{B}(s)$ and $E\subseteq S$ such that $s^{\prime }\in E$ (thus $E\ne \varnothing$ ) and $s^{\prime }\notin \bigcup _{x\in \mathcal{B}(s)}f(x,E)$ . Construct a model based on this frame where, for some atomic sentences $p$ and $q$ , $\Vert p\Vert =E\ne \varnothing$ and $\Vert q\Vert =\bigcup _{x\in \mathcal{B}(s)}f(x,E)=\bigcup _{x\in \mathcal{B}(s)}f(x,\Vert p\Vert )$ . Then, for every $x\in \mathcal{B}(s)$ , $f(x,\Vert p\Vert )\subseteq \Vert q\Vert$ so that $q\in K_s*p$ . Since $s^{\prime }\in \Vert p\Vert$ and $s^{\prime }\notin \Vert q\Vert$ , $s^{\prime }⊭(p\to q)$ from which it follows (since $s^{\prime }\in \mathcal{B}(s)$ ) that $(p\to q)\notin K_s$ and thus $q\notin K_s+p$ . Hence, since $q\in K_s*p$ but $q\notin K_s+p$ , $K_s*p⊈K_s+p$ .

For axiom $(K*5b)$ the proof is as follows.

Sufficiency. Consider a model based on a frame that satisfies Property $(P*5)$ . Let $\varphi \in {\mathrm{\Phi }}_0$ be such that $\Vert \varphi \Vert \ne \varnothing$ and fix an arbitrary $s\in S$ . By $(P*5)$ there exists an $s^{\prime }\in \mathcal{B}(s)$ such that $f(s^{\prime },\Vert \varphi \Vert )\ne \varnothing$ . Let $p\in \mathtt{\text{At}}$ be an atomic sentence . Then $f(s^{\prime },\Vert \varphi \Vert )⊈\Vert p\wedge \mathrm{\neg }p\Vert =\varnothing$ . Hence, since $s^{\prime }\in \mathcal{B}(s)$ , $(p\wedge \mathrm{\neg }p)\notin K_s*\varphi$ so that $K_s*\varphi \ne {\mathrm{\Phi }}_0$ .

Necessity. Consider a frame that violates $(P*5)$ , that is, there exist $s\in S$ and $\varnothing \ne E\subseteq S$ such that, $\mathrm{\forall }{s}^{\prime }\in \mathcal{B}(s)$ , $f(s^{\prime },E)=\varnothing$ . Construct a model based on this frame where, for some atomic sentence $p$ , $\Vert p\Vert =E\ne \varnothing$ . Fix an arbitrary $\varphi \in {\mathrm{\Phi }}_0$ . Then, $\mathrm{\forall }{s}^{\prime }\in \mathcal{B}(s)$ , $f(s^{\prime },\Vert p\Vert )=\varnothing \subseteq \Vert \varphi \Vert$ , so that, by $(RI)$ , $\varphi \in K_s*p$ . Thus $K_s*p={\mathrm{\Phi }}_0$ .

Validity of $(K*6)$ on all frames is a consequence of the fact that if $\varphi \leftrightarrow \psi$ is a tautology, then, in every model, $\Vert \varphi \Vert =\Vert \psi \Vert$ .

In Bonanno (2025) it is shown that the class ${\mathcal{F}}_{*}$ of frames that satisfy the properties listed in Figure 1 characterizes the set of AGM belief revision functions in the following sense (for simplicity we omit the subscript $M$ that refers to a given model, for example, we write $\Vert \varphi \Vert$ instead of $\Vert \varphi {\Vert }_M$ ):

1. (A)

   For every model based on a frame in ${\mathcal{F}}_{*}$ and for every state $s$ in that model, the partial belief change function $\circ$ (based on $K_s=\{\varphi \in {\mathrm{\Phi }}_0:\mathcal{B}(s)\subseteq \Vert \varphi \Vert \}$ and $\mathrm{\Psi }=\{\varphi \in {\mathrm{\Phi }}_0:\Vert \varphi \Vert \ne \varnothing \}$ ) defined by (RI) can be extended to a full-domain belief revision function $*$ that satisfies the AGM axioms $(K*1)$ - $(K*8)$ .

2. (B)

   Let $K\subset {\mathrm{\Phi }}_0$ be a consistent and deductively closed set and let $*:{\mathrm{\Phi }}_0\to 2^{{\mathrm{\Phi }}_0}$ be a belief revision function based on $K$ that satisfies the AGM axioms. Then there exists a frame in ${\mathcal{F}}_{*}$ , a model based on that frame and a state $s$ in that model such that (a) $K=K_s=\{\varphi \in {\mathrm{\Phi }}_0:\mathcal{B}(s)\subseteq \Vert \varphi \Vert \}$ and (b) the partial belief change function $\circ$ (based on $K_s$ and $\mathrm{\Psi }=\{\varphi \in {\mathrm{\Phi }}_0:\Vert \varphi \Vert \ne \varnothing \}$ ) defined by (RI) is such that $K_s\circ \varphi =K_s*\varphi$ for every consistent formula $\varphi$ .

3. A Modal Logic for Belief Revision

We now introduce a simple language with three modal operators: a unimodal belief operator $B$ , a bimodal conditional operator > and the unimodal global operator $◻$ . The interpretation of $B\varphi$ is ‘‘the agent believes $\varphi$ ,’’ the interpretation of $\varphi >\psi$ is ‘‘if $\varphi$ is (or were) the case then $\psi$ is (or would be) the case’’ and the interpretation of $◻\varphi$ is ‘‘ $\varphi$ is necessarily true.’’

The set $\mathrm{\Phi }$ of formulas in the language is defined as follows. The reasons why we consider a restricted language are discussed in Section 4.

Let ${\mathrm{\Phi }}_0$ be the set of Boolean formulas defined in Section 2.

Let ${\mathrm{\Phi }}_{>}$ be the set of formulas of the form $\varphi >\psi$ with $\varphi ,\psi \in {\mathrm{\Phi }}_0$ . ⁶

Let ${\mathrm{\Phi }}_1$ be the set of Boolean combinations of formulas in ${\mathrm{\Phi }}_0\cup {\mathrm{\Phi }}_{>}$ .

Let ${\mathrm{\Phi }}_B$ be the set of formulas of the form $B\varphi$ with $\varphi \in {\mathrm{\Phi }}_1$ . ⁷

Let ${\mathrm{\Phi }}_{◻}$ be the set of formulas of the form $◻\varphi$ with $\varphi \in {\mathrm{\Phi }}_0$ . ⁸

Finally, let $\mathrm{\Phi }$ be the set of Boolean combinations of formulas in ${\mathrm{\Phi }}_1\cup {\mathrm{\Phi }}_B\cup {\mathrm{\Phi }}_{◻}$ .

3.1. Kripke–Lewis Semantics

As semantics for this modal logic we take the Kripke–Lewis frames of Definition 2.3. A model based on a frame is obtained, as before, by adding a valuation $V:\mathtt{\text{At}}\to 2^S$ . The following definition expands Definition 2.4 by adding validation rules for formulas of the form $◻\varphi$ , $\varphi >\psi$ and $B\varphi$ .

Definition 3.1

Truth of a formula $\varphi$ at state $s$ in model $M$ (denoted by $s{\models }_M\varphi$ ) is defined as follows:

1. (1)

if $p\in \mathtt{\text{At}}$ then $s{\models }_{M}p$ if and only if $s\in V(p)$ .

(2)

For $\varphi \in \mathrm{\Phi }$ , $s{\models }_M\mathrm{\neg }\varphi$ if and only if $s{⊭}_M\varphi$ .

(3)

For $\varphi \in \mathrm{\Phi }$ , $s{\models }_M(\varphi \vee \psi )$ if and only if $s{\models }_M\varphi$ or $s{\models }_M\psi$ (or both).

(4)

For $\varphi \in {\mathrm{\Phi }}_0$ , $s{\models }_M◻\varphi$ if and only if, $\mathrm{\forall }{s}^{\prime }\in S$ , $s^{\prime }{\models }_M\varphi$ (thus $s{\models }_M\mathrm{\neg }◻\mathrm{\neg }\varphi$ if and only if, for some $s^{\prime }\in S$ , $s^{\prime }{\models }_M\varphi$ ).

(5)

For $\varphi ,\psi \in {\mathrm{\Phi }}_0$ , $s{\models }_M(\varphi >\psi )$ if and only if, either

$s{\models }_M◻\mathrm{\neg }\varphi$ (i.e., $\Vert \varphi {\Vert }_M=\varnothing$ ), or

$s{\models }_M\mathrm{\neg }◻\mathrm{\neg }\varphi$ (i.e., $\Vert \varphi {\Vert }_M\ne \varnothing$ ) and, for every $s^{\prime }\in f(s,\Vert \varphi {\Vert }_M)$ , $s^{\prime }{\models }_M\psi$ (i.e., $f(s,\Vert \varphi {\Vert }_M)\subseteq \Vert \psi {\Vert }_M$ ). ⁹

(6)

For $\varphi \in {\mathrm{\Phi }}_1$ , $s{\models }_{M}B\varphi$ if and only if, $\mathrm{\forall }{s}^{\prime }\in \mathcal{B}(s)$ , $s^{\prime }{\models }_M\varphi$ (i.e., $\mathcal{B}(s)\subseteq \Vert \varphi {\Vert }_M$ ).

The definition of validity is as in the previous section.

Definition 3.2

A formula $\varphi \in \mathrm{\Phi }$ is valid on a frame $F$ if, for every model $M$ based on that frame and for every state $s$ in that model, $s{\models }_M\varphi$ . A formula $\varphi \in \mathrm{\Phi }$ is valid on a set of frames $\mathcal{F}$ if it is valid on every frame $F\in \mathcal{F}$ .

3.2. Frame Correspondence

Definition 3.3

A formula $\varphi \in \mathrm{\Phi }$ is characterized by, or corresponds to, or characterizes, a property $P$ of frames if the following is true:

1. (1)

$\varphi$ is valid on the class of frames that satisfy property $P$ , and

(2)

if a frame does not satisfy property $P$ then $\varphi$ is not valid on that frame.

The table in Figure 2 shows, for every property of frames considered in Figure 1, the modal formula that corresponds to it. The proofs of the characterizations results are given in the Appendix.

Figure 2.

Modal Characterization of the Frame Properties of Figure 1.

Putting together Figures 1 and 2, we have a modal-logic characterization of AGM axioms $(K*2)$ , $(K*3)$ , $(K*4)$ , $(K*5b)$ , $(K*7)$ and $(K*8)$ . For instance, the modal axiom $B(\varphi >\varphi )$ corresponds to AGM axiom $(K*2)$ ( $\varphi \in K*\varphi$ ) in the following sense: $(K*2)$ is characterized by frame Property $(P*2)$ which, in turn, characterizes $B(\varphi >\varphi )$ ; in other words, $B(\varphi >\varphi )$ can be viewed as a ‘‘translation’’ into our modal logic of AGM axiom $(K*2)$ .

To complete the analysis we need to account for AGM axioms $(K*1)$ , $(K*5a)$ and $(K*6)$ .

The modal counterpart of $(K*1)$ ( $K*\varphi =Cn(K*\varphi )$ ) can be taken to be the following axiom: for $\varphi ,\psi ,\chi \in {\mathrm{\Phi }}_0$ ,

$$\begin{array}{r}(B(\varphi >\psi )\wedge B(\varphi >(\psi \to \chi )))\to B(\varphi >\chi )\end{array}$$

which is valid on all the frames considered in this paper. ¹⁰

axiom $(K*5a)$ (if $\varphi$ is a contradiction, then $K*\varphi ={\mathrm{\Phi }}_0$ ) can be captured in our logic by the following rule of inference: if $\mathrm{\neg }\varphi$ is a tautology (a theorem of propositional calculus) then $B(\varphi >\psi )$ is a theorem.

AGM axiom $(K*6)$ (if $\varphi \leftrightarrow \psi$ is a tautology then $K*\varphi =K*\psi$ ) can be captured in our logic by the following rule of inference: if $\varphi \leftrightarrow \psi$ is a tautology then $B(\varphi >\chi )\leftrightarrow B(\psi >\chi )$ is a theorem (for $\varphi ,\psi ,\chi \in {\mathrm{\Phi }}_0$ ), which is clearly validity preserving in every model, since if $\varphi \leftrightarrow \psi$ is a tautology then $\Vert \varphi \Vert =\Vert \psi \Vert$ .

In Axioms $(A3)$ and $(A5b)$ the clause $\mathrm{\neg }◻\mathrm{\neg }\varphi$ in the antecedent ensures that, on the semantic side, $\Vert \varphi \Vert \ne \varnothing$ , so that $f(s,\Vert \varphi \Vert )$ is defined; similarly for $\mathrm{\neg }◻\mathrm{\neg }(\varphi \wedge \psi )$ in Axiom $(A7)$ .

While the comparison of properties $(P*3)$ and $(P*7)$ is not straightforward, a comparison of the corresponding Axioms $(A3)$ and $(A7)$ makes it very clear that the two are closely related. First of all, note that $(A3)$ can be equivalently written as $\mathrm{\neg }◻\mathrm{\neg }(\varphi \wedge \psi )\wedge B((\varphi \wedge \psi )>\chi )\to B((\varphi \to (\psi \to \chi ))$ (to obtain the original formulation, first replace $\psi$ by $\varphi$ and then replace $\chi$ by $\psi$ and note that $(\varphi \wedge \psi )\to \chi$ is tautologically equivalent to $\varphi \to (\psi \to \chi )$ ). Comparing $(A3)$ and  $(A7)$ ,

$$\begin{array}{r}\begin{array}{cccc}(A3)& \mathrm{\neg }◻\mathrm{\neg }(\varphi \wedge \psi )\wedge B((\varphi \wedge \psi )>\chi )& \to & B(\varphi \to (\psi \to \chi ))\\ (A7)& \mathrm{\neg }◻\mathrm{\neg }(\varphi \wedge \psi )\wedge B((\varphi \wedge \psi )>\chi )& \to & B(\varphi >(\psi \to \chi ))\end{array}\end{array}$$

we see that the antecedent is the same in both while in the consequent $(A3)$ has ’ $\varphi \to$ ’ (the material conditional) while $(A7)$ has ’ $\varphi >$ ’ (the counterfactual conditional).

A similar comparison $(A4)$ and $(A8)$ shows that they are closely related. Note that $(A4)$ can be equivalently written as

$$\begin{array}{r}(\mathrm{\neg }B\mathrm{\neg }(\varphi \wedge \psi )\wedge B((\varphi \wedge \psi )\to \chi ))\to B((\varphi \wedge \psi )>\chi )\end{array}$$

(1)

(to obtain the original formulation, first replace $\psi$ by $\varphi$ and then replace $\chi$ by $\psi$ ). Next observe that (1) $\mathrm{\neg }(\varphi \wedge \psi )$ is tautologically equivalent to $\varphi \to \mathrm{\neg }\psi$ , so that $\mathrm{\neg }B\mathrm{\neg }(\varphi \wedge \psi )$ is equivalent to $\mathrm{\neg }B(\varphi \to \mathrm{\neg }\psi )$ , and (2) $(\varphi \wedge \psi )\to \chi )$ is tautologically equivalent to $\varphi \to (\psi \to \chi )$ , so that $B((\varphi \wedge \psi )\to \chi )$ is equivalent to $B(\varphi \to (\psi \to \chi ))$ ; thus, (2) can be written as shown below:

$$\begin{array}{r}\begin{array}{llll}(A4)& \mathrm{\neg }B(\varphi \to \mathrm{\neg }\psi )\wedge B(\varphi \to (\psi \to \chi ))& \to & B((\varphi \wedge \psi )>\chi )\\ (A8)& \mathrm{\neg }B(\varphi >\mathrm{\neg }\psi )\wedge B(\varphi >(\psi \to \chi ))& \to & B((\varphi \wedge \psi )>(\psi \wedge \chi ))\end{array}\end{array}$$

The difference between $(A4)$ and $(A8)$ is that the first two instances of the material conditional ’ $\to$ ’ in the antecedent of $(A4)$ are replaced by the counterfactual conditional ’>’ in $(A8)$ , ¹¹ and in the consequent $\chi$ in $(A4)$ ir replaced by $\psi \wedge \chi$ in $(A8)$ .

The table in Figure 3 synthesizes Figures 1 and 2 by showing the correspondence between each AGM axiom and its modal counterpart.

Figure 3.

The Correspondence Between AGM Axioms and their Modal Counterparts.

4. Conclusion

The modal language considered in Section 3 is a restricted one which allows for nesting of some modal operators (e.g., formulas such as $B(\varphi >\psi )$ ) but not others (see Footnotes 5, 6 and 7). The purpose of this paper was to identify the smallest language that ‘‘does the job,’’ that is, that allows one to translate the AGM axioms into modal axioms. Furthermore, the simple language affords easier tractability and interpretability. We leave to future research the investigation of extensions of the language that allow for more nesting of the operators, for example, formulas such as $B(\varphi >(\psi >\chi ))$ or $B(\varphi >B(\psi >\chi ))$ , which might be appropriate for modeling iterated belief revision (Darwiche & Pearl, 1997; Peppas, 2014), or formulas such as the strict conditional $◻(\varphi >\psi )$ or $◻B\varphi$ or $BB\varphi$ . Such a richer language would allow one to model belief introspection and higher-order doxastic reasoning as well as, perhaps, iterated belief revision.

As noted in the Introduction, one benefit of recasting the AGM theory of belief revision in the language of modal logic is that both belief and belief revision can then by analyzed within the same framework. Furthermore, the language of modal logic affords greater expressiveness: for example, it allows one to express introspective properties of belief, which cannot be done in the AGM approach. It also allows one to distinguish between different kinds of conditional beliefs such as ‘‘I believe that if $\varphi$ were the case then $\psi$ would be the case’’ ( $B(\varphi >\psi )$ ) and ”if $\varphi$ were the case then I would believe $\psi$ ” ( $\varphi >B\psi$ ) and ”if I were to believe $\varphi$ then I would believe $\psi$ ” ( $B\varphi >B\psi$ ). Leitgeb (Leitgeb, 2007) suggests that $\psi \in K*\varphi$ in the AGM approach ought to be understood in terms of the conditional $B\varphi >B\psi$ , while we provided a translation of the AGM axioms in terms of the conditional $B(\varphi >\psi )$ . Presumably, the three types of conditional beliefs express different concepts and obey different principles; modal logic allows one to analyze such differences.

In this paper we have focused on AGM belief revision, but—as shown in Bonanno (2023) and Bonanno (2025)—the Kripke–Lewis semantics can be used also to provide a characterization of AGM belief contraction (Gärdenfors, 1988) and of Katsuno–Mendelzon belief update (Katsuno & Mendelzon, 1991). Extending the results of this paper to contraction and update is left to future research.

A connection between conditional logic and AGM belief revision has been pointed out in several contributions, in particular (Giordano et al., 1998, 2001, 2005; Günther & Sisti, 2022). Although there are some similarities between our approach and those contributions, there are also some important differences. For a detailed discussion see Bonanno (2025).