# minimal_change_in_modal_logic_s5__6b658180.pdf

Minimal Change in Modal Logic S5

Carlos Aguilera-Ventura*, Jonathan Ben-Naim*, Andreas Herzig*

IRIT, CNRS, Univ. Toulouse, France carlos.aguilera-ventura@irit.fr, Jonathan.Ben-Naim@irit.fr, Andreas.Herzig@irit.fr

We extend belief revision theory from propositional logic to the modal logic S5. Our first contribution takes the form of three new postulates (M1-M3) that go beyond the AGM ones and capture the idea of minimal change in the presence of modalities. Concerning the construction of modal revision operations, we work with set pseudo-distances, i.e., distances between sets of points that may violate the triangle-inequality. Our second contribution is the identification of three axioms (A3-A5) that go beyond the standard axioms of metrics. Loosely speaking, our main result states the following: if a pseudo-distance satisfies certain axioms, then the induced revision operation satisfies (M1-M3). We investigate three pseudo-distances from the literature (Dhaus, Dinj, Dsum), and the three induced revision operations ( Dhaus, Dinj, Dsum). Using our main result, we show that only Dsum satisfies (M1M3) all together. As a last contribution, we revisit a major criticism of AGM operations, namely that the revisions of p q and p (p q) are identical. We show that the problem disappears if instead of material implication we use the modal operator of strict implication that can be defined in S5.

1 Introduction Logical languages with modalities provide expressive power beyond propositional logic: they allow us to distinguish between necessary truths p p and contingent truths p p. This distinction accounts for things such as laws of nature and database integrity constraints. The belief revision literature in the AGM tradition (Alchourr on, G ardenfors, and Makinson 1985) has neglected the problem of how to revise belief sets containing modalities: as the SEP entry on belief revision says, it is fair to say that operations of AGM-style belief change have not yet been constructed that are generally recognized as able to deal adequately with conditional or modal sentences (Hansson 2022). We address this shortcoming by providing an axiomatic and semantic analysis of belief revision operations for modal logic. On the axiomatic side, we formulate three simple rationality postulates and argue why a reasonable revision operation should satisfy them. On the semantic side, the main difficulty is to lift the orderings (on which the semantics of

*These authors contributed equally. Copyright 2025, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

revision operations are based) from propositional logic valuations to Kripke models. For a start, we choose the modal logic S5 because it has an alternative, simpler semantics in terms of sets of valuations. We propose a family of distancebased revision operations. Each of them is based on a lifting of the Hamming distance from valuations to sets of valuations. The most interesting one sums up the minimal distances from each valuation of one set to the other set: we show that it validates all postulates. Our revision operations allow us to shed new light on an old debate in belief revision: whether revision operations should be syntax-sensitive or not. According to the AGM postulate of syntax insensitivity, when two logically equivalent belief bases are revised by the same new piece of information then the two outcomes should also be logically equivalent. The main argument against syntax insensitivity is that while the two belief bases {p, q} and {p, p q} are statically equivalent , they are not dynamically equivalent , in the sense that they have to be revised differently. We argue that this non-equivalence should be made formal by investigating revision for logics where these two belief bases fail to be equivalent. We show that the strict implication operator , defined in modal logic by φ ψ = (φ ψ), provides an interesting solution: the bases {p, q} and {p, p q} fail to be equivalent, and the revision of {p, q} by q entails {p, q} while that of {p, p q} by q entails { p, q}. The paper is organized as follows. We start by recalling distance-based revision operations and modal logics (Section 2). We then formulate three simple postulates for modal revision (Section 3). After that, we introduce a general way of lifting the Hamming distance between valuations to distances between pointed S5 models (Section 4). We then propose axioms for these distances and check the status of the modal revision postulates w.r.t. the induced revision operations (Section 5). Finally, we show that if we replace material implication by strict implication then the main counterexamples against syntax-insensitive revision can be handled satisfactorily (Section 6) and conclude (Section 8).

2 Background We suppose given a finite set Var = {p, q, r, . . .} of propositional variables. A valuation is a subset of Var. The set of all valuations is Val = Pow(Var). The set PFor is the set of all propositional formulas built from Var and the connectives ,

The Thirty-Ninth AAAI Conference on Artificial Intelligence (AAAI-25)

, and . The set of all propositional models of a formula φ PFor is noted ||φ||PC.

Revision In the original AGM framework, a revision operation maps a set of formulas B and a formula µ to a new set of formulas B µ, where the first argument of is a belief set: a set of formulas that is closed under logical theorems and modus ponens. Such sets are typically infinite. However, it has been argued in the philosophical as well as in the AI literature that this is not a realistic hypothesis, both in the case of human agents and in the case of computers: their memory can only contain finite sets of formulas that fail to be closed under theorems and modus ponens. Such finite sets are called belief bases. We follow the KM approach (Katsuno and Mendelzon 1991) and consider formulas instead of belief bases. In that presentation, a revision operation is a function mapping couples of formulas to a formula. Let φ, ψ, µ be formulas in some logic language. Let be a deduction relation for that language. A formula φ is consistent if φ ; and φ ψ abbreviates that both φ ψ and ψ φ. The KM postulates are: (R1) φ µ µ. (R2) If φ µ is consistent then φ µ φ µ. (R3) If µ is consistent then φ µ is consistent. (R4) If φ φ and µ µ then φ µ φ µ . (R5) (φ µ) ψ φ (µ ψ). (R6) If (φ µ) ψ is consistent then φ (µ ψ) (φ µ) ψ. A model-based propositional revision operation is a function from PFor PFor to Pow(Val). An important family of such operations was introduced in (Lehmann, Magidor, and Schlechta 2001; Ben-Naim 2006). All of them are built from arbitrary distances and are syntax-insensitive. The most prominent one is due to Dalal (1988) and is based on the Hamming distance between two valuations, which is the cardinality of their symmetric difference. Formally, the function h : Val Val N0 is such that for u, v Val, h(u, v) = |(u\v) (v\u)|. The lifting of h to sets is a function hs on Val Pow(Val) such that

hs(v, U) = ( min{h(v, u) : u U} if U , , |Var| otherwise,

for v Val and U Val. Then Dalal s model-based propositional revision operation is

φ h µ = Arg Minv ||µ||PChs(v, ||φ||PC).

Modal Logic There is not just one modal logic but a whole family. Here we focus on S5, our choice being mainly motivated by the simplicity of its semantics: beyond the usual Kripke models, S5 also has simpler models in terms of sets of valuations that we are going to use here. An (S5-)model is a non-empty subset V of Val; the set of all such models is noted Mod = Pow(Val). A pointed (S5-)model is a pair M = V, v such that V Mod and v V; the set of all such models is noted PMod. The actual world v describes the current state of the

world, while the elements of V describe the possible ways the world could be. For the sake of readability, in examples we underline the actual world and drop braces and commas in the description of valuations; we e.g. write { , pq} instead of { , {p, q}}, . The set MFor of modal formulas is defined by the grammar φ ::= p | | φ | φ φ | φ | φ

where p ranges over Var. The formula φ is read φ is necessary and φ is read φ is possible . Other boolean connectives such as , material implication , and material equivalence are defined as abbreviations. A formula φ MFor is propositional when and do not appear in φ, that is, when φ PFor. The modal operator of necessity allows us to distinguish necessary and contingent truth of a formula φ. Necessary truths can be viewed as laws of nature, or as integrity constraints in databases. For example, if we read p1 as Bob is a member of Department D1 and p2 as Bob is a member of Department D2 then p1 p2 is a contingent truth: p1 p2 is presently true but is not necessarily so and may change in the future. In contrast, (p1 p2) is a necessary truth expressing the integrity constraint that Bob cannot be a member of both D1 and D2. A formula of MFor is interpreted in a pointed model M = V, v according to the following truth conditions:

M p iff p v; M φ iff for every v V, V, v φ; M φ iff for some v V, V, v φ;

and as usual for the boolean operators. A pointed model of φ is a couple V, v such that V, v φ; the set of all pointed models of φ is noted ||φ||. If φ is without modal operators (that is, φ PFor) then ||φ|| equals the set of pointed models V, v PMod such that v ||φ||PC. When ||φ|| , then φ is (S5-)satisfiable; when ||φ|| = PMod then φ is (S5-)valid. We denote by |= the relation on MFor such that φ |= ψ iff ||φ|| ||ψ||. Finally, a model of φ is a set of valuations V Mod such that V, v φ for some v V. Several axiomatic systems for S5 exist; we here recall one from (Chellas 1980) which extends that of propositional logic by the following axiom schemas and inference rule:

(φ ψ) ( φ ψ); ; φ ψ φ ψ;

φ φ; φ φ; φ φ.

Provability of a formula φ from the axioms is noted φ. The (S5-)deduction relation φ ψ is defined as φ ψ. The axiomatics is sound and strongly complete: the relations and |= are identical (Chellas 1980). By φ ψ we mean both φ ψ and ψ φ. We say that φ is (S5-)consistent iff φ .

Fact 1. Let φ, ψ MFor. The following hold:

1. φ ψ is consistent iff φ and ψ have at least one pointed model in common. 2. φ ψ is consistent iff φ and ψ have at least one model in common.

3. φ ψ is consistent iff φ ψ is consistent. 4. If φ, ψ PFor then φ ψ is consistent iff φ is consistent and ψ is consistent.

3 The Modal Postulates A modal revision operation maps a base φ MFor and an input µ MFor to a revised base φ µ MFor. The new base φ µ should only differ minimally from φ, and a central idea in that perspective, embodied in the KM postulate (R2), is that when φ and µ are consistent then φ µ should be equivalent to φ µ. However, modal logic provides two perspectives on consistency: propositional consistency and modal consistency. Propositional consistency refers to cases where φ and µ share a pointed model. Modal consistency, on the other hand, occurs when φ and µ share a model, but not necessarily a pointed model. This requirement is weaker than propositional consistency. From now, when we use consistency to refer to propositional consistency. The KM postulate (R2) accounts for cases of propositional consistency but not for cases of modal consistency. We introduce three new postulates that, in conjunction with (R1) (R6), appropriately account for revision in the context of modal consistency. The new postulates can be viewed as refinements of the preservation postulate (R2). For a start, we state a consequence of (R2). Fact 2. Let be a modal revision operation satisfying the KM postulates. If φ and µ are propositionally consistent and µ µ then φ µ φ.1

Modal consistency is more liberal than propositional consistency. For example, p and p are modally consistent. By Fact 1 (item 2) this is the same as consistency of p p. While the idea of minimal change in the case of propositional consistency involves preserving the shared pointed models, the same should hold in the case of modal consistency; only the actual world should be (minimally) changed in order to obtain a model of the input. Let us illustrate the above point by a scenario where Detective Hercule Poirot is investigating a murder case. Initially, Poirot believes Antonio Foscarelli is innocent, because certain evidences prove that Foscarelli had no opportunity to be at the scene of the crime. But, as the investigation unfolds, those evidences proved to be false. Consequently, Poirot has to revise his beliefs accordingly, i.e., Poirot has to replace Foscarelli is innocent by Foscarelli is possibly innocent . This kind of revision (i.e., replace an actual fact by a possibility) cannot be done in the classical AGM framework, which motivates our modal framework. Our first new postulate conveys the following intuition: assume φ µ is consistent; then, φ should be preserved when φ is revised by µ; indeed, φ entails φ and µ is consistent with φ (thanks to our assumption). More formally:

(M1) If φ µ is consistent, then φ µ φ.

When base and input are modally inconsistent, we say we have a case of strong revision. In contrast, when base and

1Obviously, the hypothesis that µ µ can be dropped when is deduction in S5 because µ µ is an S5 theorem.

input are propositionally inconsistent, but modally consistent, we have a case of weak revision. The only things we can preserve in case of strong revision are possibilities. For example, the base p and the input p are modally inconsistent. However, p p in S5, and the possibility p is propositionally consistent with p; we therefore expect that p p p. Next, our second new postulate says the following: assume φ entails ψ, and µ is consistent with ψ; then ψ should be preserved when φ is revised by µ. More formally:

(M2) If µ propositional, ψ µ is consistent, and φ ψ then φ µ ψ.

Note that in (M2), the restriction to propositional µ cannot be dropped at least if our modal logic is S5. Consider e.g. φ = p1 p2, ψ1 = p1, ψ2 = p2, and µ = (p1 p2). Then φ µ would entail both p1 and p2; but as µ is S5equivalent to ( p1 p2), this would conflict with the success postulate (R1). We turn to our last postulate. It means the following: assume φ entails ψ, and µ is consistent with ψ; then, µ is consistent with ψ; thus, ψ should be preserved when φ is revised by µ. More formally:

(M3) If µ propositional, ψ µ is consistent, and φ ψ, then φ µ ψ.

The restriction in (M3) to propositional µ cannot be dropped, as exemplified by φ = (p1 p2), ψ1 = p1, ψ2 = p2, and µ = (p1 p2). We observe that in cases of weak revision, that is, when µ is consistent with φ, (M2) follows from the preservation postulate (R2), and (M3) follows from (M1).

4 Distance Between Pointed S5 Models Lifting the Hamming Distance to Sets Contrarily to distances, pseudo-distances need not satisfy the triangle inequality: we say that a pseudo-distance is a function D from Mod Mod to N0 satisfying the following two basic axioms:

(A1) D(U, V) = 0 iff U = V. (A2) D(U, V) = D(V, U).

The elements evaluated by D are not mere points, but subsets of Val. This allows us to formulate the following three supplementary axioms for D:

(A3) D({u}, {v}) < D({u }, {v }) iff h(u, v) < h(u , v ). (A4) w U \ V, D(U, V {w}) D(U, V) hs(w, V). (A5) w Val, D(U, U {w}) = hs(w, U).

A stronger version of (A3) was introduced in (Eiter and Mannila 1997): in the case of singletons the pseudo-distance D should equal h. (A4) says that the increased distance associated with the loss of common elements is bounded by the Hamming distance. (A5) says that if we add a new valuation to a model then the resulting model s distance from the original set is exactly the Hamming distance between this new valuation and the closest valuation from the original set. Note that the case w U is covered by (A1).

We now recall three specific such distances. First, the Hausdorff distance is the minimum of the maximum distances between corresponding points in V and U.

Dhaus(U, V) = max max u U min v V h(u, v), max v V min u U h(u, v) .

In (Song, Cai, and Immink 2020) a distance function based on injection is introduced. Let Inj(U, V) be the set of all injective functions from U to V. The injection-based pseudo-distance is defined by

Dinj(U, V) = min f Inj(X,Y)

u X h(u, f(u)) + |Var| (|Y| |X|)

where: X = U and Y = V, if |U| |V|; X = V and Y = U, if |V| < |U|. Finally, in (Niiniluoto 1987) the sum-based pseudodistance is defined by

Dsum(U, V) = X

u U hs(u, V) + X

v V hs(v, U).

Proposition 3. Dinj satisfies (A3), Dhaus satisfies (A3) and (A5), Dsum satisfies (A3)-(A5). In addition, Dhaus violates (A4), and Dinj violates (A4) and (A5). The following table summarizes the above proposition:

Dhaus Dinj Dsum (A3) (A4) (A5)

Table 1: Satisfaction of our new pseudo-distance axioms

Lexicographic Distance between Pointed Models We are going to view the set of accessible worlds V of a pointed model (V,v) as a first circle of possible fallback worlds in a system of spheres (Lindstr om and Rabinowicz 1999): when a new piece of information is false at the actual world v then the first try is to replace v by one of the other worlds in V. It is only when none of the elements of V satisfies the new piece of information that we have to modify V. In both cases, we are going to determine the resulting model through a distance measure. We define the distance between two pointed models (V,v) and (U,u) to be a pair of integers: Definition 4. Let D be a pseudo-distance. We denote by δD the function from PMod PMod to N0 N0. such that, M = U, u , N = V, v PMod, the following holds:

δD(M, N) = D(U, V), h(u, v) .

We denote by lex the linear order on N0 N0 such that, r = r1, r2 , s = s1, s2 N0 N0, the following holds:

r lex s iff r1 s1 or (r1 = s1 and r2 s2).

Fact 5. Let D be a pseudo-distance and M = U, u , N = V, v PMod. Then: u = v iff r N0, δD(M, N) = r, 0 ; U = V iff r N0, δD(M, N) = 0, r . Definition 6. Let D be a pseudo-distance. We denote by D the function on Pow(PMod) PMod such that, M PMod, N PMod, the following holds:

D(M, N) = min lex {δD(M, N) : M M}.

Slightly abusing notation, we also note D the minimum distance between two sets of pointed models w.r.t <lex. We now explain how the lexicographical order works using an example. To do so, we will focus on Dsum since, as will be seen in the next section, it gives rise to a revision operation that satisfies all the modal postulates. Example 7. We have:

Dsum || p||, ||p (p q)|| = 0, 1 (1) Dsum || p||, || p|| = 1, 0 (2) Dsum || p||, || p|| = 1, 1 (3) Dsum || p||, || p|| = 2, 1 (4)

To simplify explanations we assume that Var equals the atoms in the formula. For item (1), the distance cannot be 0, 0 because the intersection of || p|| and ||p (p q)|| is empty; since they are modal consistent they have at least one common model. Thus, the distance is at least 0, n . For the second element of the couple, {p, pq} || q|| and {p, pq} ||p q||, thus we have δDsum {p, pq}, {p, pq} = 0, 1 . For item (2), p has a single model, {{p}}; and p has two models: { } and { , {p}}. We have Dsum {{p}} , { } = 2 while Dsum {{p}} , { , {p}} = 1. The actual world remains the same, therefore Dsum || p||, || p|| = 1, 0 . The explanation of item (3) does not differ from that of item (2) as far as the first component of Dsum is concerned. As to the second component, p being logically stronger than p we have to also shift the actual world from {p} to . Hence, Dsum || p||, || p|| = 1, 1 . In Figure 1 a graphical representation of this item is given. For item (4), p and p have exactly one model, specifically {{p}} for the former and { } for the latter. Thus, Dsum || p||, || p|| = 2, 1 .

Figure 1: Illustration of Example 7, item (3); each box represents a pointed model, with its actual world underlined.

5 Distance-Based Revision Operation for S5 The following definition generalizes Dalal s revision operation from propositional logic to modal logic. Definition 8. A model-based modal revision operation is a function from MFor MFor to Pow(PMod). Let D be a pseudo-distance. We denote by D the model-based modal revision operation such that, φ, µ MFor:

φ D µ = {M ||µ|| : N ||µ||, D(||φ||, M) lex D(||φ||, N)}.

Let us exemplify the above definition with Dsum as D. Example 9. Consider the following revision results (for each of them, Var consists of the atoms appearing in the base and/or input):

(p q) Dsum q = ||p q (p q)|| (p q) Dsum q = ||p q q|| q Dsum q = || q q|| ( q p) Dsum q = ||p q (p q) (p q)||

The outcome of the revision depends on the set Var. For example, p Dsum p is || p|| for Var1 = {p}, while it equals || p ( q q)|| for Var2 = {p, q}. Related to that, Dsum fails to satisfy Parikh s principle of language splitting (Kourousias and Makinson 2007; Parikh 1999), which says that if the variables of φ and ψ are disjoint and the variables of µ are a subset of those of φ then (φ ψ) µ = (φ µ) ψ. This is illustrated by φ = p, ψ = q q, and µ = p: we have (φ ψ) Dsum µ = || p||, (φ Dsum µ) ||ψ|| = || ||. Figure 2 illustrates the distinction between weak and strong revision that we have introduced in Section 3. For the former, the base and the input share a model; hence the distance between them is 0, n for some n 1. Then minimal change means to keep the model and modify the actual world. In the case of strong revision the base and the input do not share any model; hence the minimum distance is n, m for some n 1 and m 0.

Figure 2: Weak revision (left) and strong revision (right); each colored band represents the distance between the pointed models of φ and those µ; the intersection shows the revision result.

Satisfaction of the AGM Postulates To show that D satisfies the AGM postulates we can use the results proved in (Katsuno and Mendelzon 1991) that use the notion of faithful assignment. Given the set PMod, consider a function that assigns to each formula φ MFor a total order φ over PMod. This assignment is said to be faithful if for any M, M PMod the following hold:

1. If M, M ||φ|| then M <φ M does not hold. 2. If M ||φ|| and M < ||φ|| then M <φ M . 3. If φ ψ then φ = ψ.

Let M PMod and M PMod. Then M M is minimal in M under the ordering φ if and only if there exists no other M M such that M is strictly less than M according to φ. The set of minimal elements of M w.r.t. φ is min φ(M). Let D be a pseudo-distance. We now define a faithful assignment by associating to every φ a total order φ such that M φ M if and only if D(||φ||, M) lex D(||φ||, M ). Thus, Definition 8 can as well be formulated as: φ D µ = min φ(||µ||). Since the assignment is faithful, the satisfaction of the AGM postulates can be derived from the results proved in (Katsuno and Mendelzon 1991).

Satisfaction of the Modal Postulates Our main result is a link between the distance axioms and the revision postulates. Loosely speaking, this link is the following: if a set pseudo-distance satisfies certain axioms, then the induced revision operation satisfies (M1-M3). To formally state our main result, we need some technical preliminaries.

Lemma 10. Let D be a pseudo-distance satisfying (A1). Let φ, µ MFor such that φ µ is consistent. Then:

φ D µ = { U, u ||µ|| : V, v ||φ||, U = V and h(u, v) = min(X)},

X = {r N : U , u ||µ||, V , v ||φ||, V = U and r = h(u , v )}.

Definition 11. We denote by hf the function from Val MFor to N0 such that, v Val, φ MFor,

hf(v, φ) = min{r : U, u ||φ||, u U, r = h(v, u )}.

Lemma 12. Let D be a pseudo-distance satisfying (A4) and (A5). Let φ, µ MFor such that µ is propositional and φ µ is inconsistent. Then:

φ D µ = {N ||µ|| : M = U, u ||µ||, O = V, v ||φ||, hs(u, V) = hf(u, φ) and N = V {u}, v }.

Lemma 13. Let D be a pseudo-distance satisfying (A1), (A4) and (A5). Let φ, µ MFor such that µ is propositional and φ µ is inconsistent. Then:

φ D µ = {N ||µ|| : M = U, u ||µ||, O = V, v ||φ||, h(v, u) = hf(u, φ) and N = V {u}, u }.

We are ready to state the main result of the paper:

Proposition 14. Let D be a pseudo-distance.

If D satisfies (A1) then D satisfies (M1). If D satisfies (A4) and (A5) then D satisfies (M2). If D satisfies (A1), (A4), and (A5) then D satisfies (M3).

Proof. We only give the proof of the first item. Let D be any pseudo-distance between sets of valuations satisfying (A1) and let D be the resulting operation. Suppose that µ is consistent with φ. It follows from this that there exists a pair (V, v) and another (U, u) such that (V, v) φ, (U, u) µ and V = U. As D satisfies (A1), D(V, U) = 0; in addition, Dsum ||φ||, ||µ|| = 0, n for some n. But indeed, since V is a S5-model and (V, v) φ, we have that for any u U, (U, u ) φ. Thus φ D µ φ.

Proposition 15. Both Dhaus and Dinj satisfy (M1). Dsum satisfies (M1)-(M3). In addition, both Dhaus and Dinj violate (M2) and (M3).

The following table summarizes the above proposition:

Dhaus Dinj Dsum M1 M2 M3

Table 2: Satisfaction of our new modal postulates.

6 Syntax-Sensitive Revision and Strict Implication One of the most appealing arguments for the use of belief bases is that while {p, q} and {p, p q} are logically equivalent in classical propositional logic, they should however not be revised in the same way: the revision of the former by q should result in {p, q} because p and q are independent. In contrast, the revision of {p, p q} by q should lead to {p q, q}. The latter is logically incomparable with {p, q}, in the sense that neither implies the other. A variant of the argument can be formulated in terms of material equivalence and can be found in the SEP entry for belief revision (Hansson 2022). This variant is based on the fact that the bases are statically equivalent but not dynamically equivalent. The distinction goes beyond belief revision and relates to the debate between coherentists and foundationalists: the former view belief states as having a flat structure where each belief has the same status, while the latter view beliefs as being organized in a web where some beliefs are more basic and support other, less basic beliefs.

A Plea for a Logical Analysis Syntax-sensitive revision operations do not satisfy (R4). They exploit the dynamical non-equivalence of {p, q} and {p, p q} as well as that of {p, q} and {p, p q}, but do not explain it. Indeed, a natural question to ask is whether one can give a logical foundation to that distinction. Intuitively, the material implication p q is too weak to adequately capture the if-then link between p and q; and similarly for the material equivalence p q. Actually, Bob s belief that p q (that Ms. Smith will conform to the party decision) has a dispositional nature: Bob s belief that p q is not only about here and now, that is when it is the

case that the party supports the proposal, but also about the situation where the party does not support the proposal. This leads to the study of logics with a stronger implication connective , such that p q and p (p q) fail to be equivalent: can such logics be equipped with revision operations that satisfy syntax independence? The first candidate is intuitionistic logic, whose implication is stronger than the material implication that of classical logic. However, our two belief bases are logically equivalent there, too. Relevance logics are more interesting: the formulas p q and p (p q) typically fail to be equivalent there. Relevance logics however have a paraconsistent nature: basically any set of formulas is consistent, and a first difficulty is to design a revision operation that avoids collapsing into expansion. Several proposals had been made in the literature (Restall and Slaney 1995; Lakemeyer and Lang 1996); the recent (Schwind, Konieczny, and Pino P erez 2022) considers Priest s Logic of Paradox LP. We here take another research avenue that, as far as we know, has not been tried yet and that we believe to be promising: the logic of strict implication.

Revision with Strict Implication

An operator of strict implication can be defined in modal logic as φ ψ = (φ ψ) (Lewis and Langford 1959; Hughes and Cresswell 1968). Therefore its truth condition is:

(V,v) φ ψ if for every v V: (V,v ) φ implies (V,v ) ψ.

The modal operator of necessity can be defined from strict implication: φ abbreviates φ. For example, the set of pointed models of p (p q) is

||p (p q)|| ={(V,v) : V Pow(Var), v V, p v and for every v V : p v implies q v}.

Hence ||p (p q)|| = {{pq, q, }, {pq, q}, {pq, }, {pq}} for the case Var = {p, q}. The material implication (p (p q)) (p q) and its strict variant (p (p q)) (p q) are both valid. In contrast, neither (p q) (p (p q)) nor (p q) (p (p q)) are valid. It is exactly this non-equivalence of p (p q) and p q that makes the logic of strict implication an interesting basic logic for belief revision. The following example illustrates the above point:

Example 16. Assume Var = {p, q}.

p q Dsum q = ||p q (p q)|| (5) p (p q) Dsum q = || p q p q (p q)|| (6) p (p q) Dsum p = || p q p q (p q)|| (7) p q Dsum q p = ||(p q) (q p)|| (8) p q Dsum p q = ||(p q) (p q)|| (9) p q Dsum (p q) = ||p q ( ( q p) (q p))|| (10)

Items 5 and 6 illustrate that Dsum satisfies the intuitions we have put forward in the introduction. In item 7, unlike the previous item, q should be true in the actual world. Item 8 is implied by the AGM preservation postulate: as q p is consistent with p q, the revision of the former by the latter is equivalent to their conjunction. All the examples in items 5, 6, 7 and 8 are weak revisions. The next two items 9 and 10 showcase strong revision. For Item 9, except for the pointed model {p}, for any other (U, u) ||p q|| there is a pointed model (V, v) ||p q|| such that Dhaus(V, U) = 1. This implies that the set of closest pointed models is determined by the distance between their actual worlds. Hence, the closest actual world after the revision is either {p, q} or . For Item 10, the revision process involves adding a new world that is not present in any model of p q: the world where p q is true, that is, {p}. While the distance between {p} and {q} is 2, the distance between {p} and {pq} is only 1; and the same is the case for the distance between {p} and . Hence, for all models of p q containing one of these worlds we can reduce the lexical distance to its minimum.

7 Related Work

We have already mentioned that there are only relatively few studies of revision operations for modal logics. Probably one reason for that is Fuhrmann s finding that several AGM postulates make little sense when bases are required to satisfy the (Poss) principle (Hansson 1999; Fuhrmann 1989). This principle says that when ψ is consistent with φ then φ ψ. As shown in (Fuhrmann 1989), it is incompatible with the AGM revision postulates (in particular the preservation postulate (R2)). Our approach is immune to that negative result because we do not suppose that belief bases satisfy (Poss). Closest to our work is an approach by Caridroit et al. It is based on the work in (Ågotnes, van der Hoek, and Wooldridge 2012) and also rejects (Poss) (Caridroit et al. 2016). Caridroit et al. take a doxastic perspective where accessible worlds model an agent s belief state. They consider that two pointed models (V,v) and (U,u) agreeing on the actual world (in our terms: v = u) have smaller distance than models disagreeing on the actual world. Our contribution takes the opposite view: agreement on the actual world is less important than agreement on the set of accessible worlds, as embodied in our lexicographic ordering on pointed models lex. As our distance differs from Caridroit et al. s, the resulting revision operation is different from theirs. As far as we know, the only study of revision operations for the logic of strict implication is (Berto 2019). It is not built on a classical propositional logic basis because it assumes hyperintensionality of beliefs. It is therefore difficult to compare it to our approach. In a spirit similar to ours, Konieczny et al. proposed what may be called a logic for syntax-sensitive revision (Konieczny, Lang, and Marquis 2005). They introduce an extension of propositional logic where the belief bases {p, q} and {p q} are not logically equivalent. This is obtained by giving the status of a logical connective to the set comma

and allows them to define an operation where the revision of these bases by q has different outcomes. Finally, belief revision and merging operations under integrity constraints as studied in (Konieczny and Pino P erez 2002) can also be related to our approach: we can identify integrity constraints as formulas prefixed by a modal operator of necessity. However, in the approach of (Konieczny and Pino P erez 2002) integrity constraints cannot be revised, while our approach caters to that: the input can not only be inconsistent with the integrity constraints, but we can also revise by a new integrity constraint. The topic of truthlikeness as studied in philosophy of science can be related to our study of distances between sets of possible worlds. In (Eiter and Mannila 1997), Eiter and Manila propose different definitions of distances based on the arguments given in (Oddie 1978; Niiniluoto and Tuomela 1979). Other distances between sets are suggested in (Fujita 2013; Song, Cai, and Immink 2020).

8 Conclusion

In this paper, we have started a systematic study of belief revision operations for modal logic. Syntactically, we have introduced novel modal postulates that ensure minimal change; semantically, we have proposed a family of lexicographical distances between pointed models that extend the traditional Hamming distance. We have also proposed a specific instance of this distance, yielding the revision operation Dsum. We have shown that it sheds new light on some criticisms of AGM revision that had led to the development of syntax-sensitive revision operations. Our work could be extended in at least three directions. First, we could consider logics other than S5. This requires a careful extension of our lexicographic (pseudo-)distance. It is straightforward for the modal logics KD45 and K45, while it is less obvious for logics such as K and S4. Furthermore, beyond other logics of strict implication, one may view strict implication as a particular conditional operator and exploit that in many conditional logics the formulas p q and p (p q) fail to be equivalent. Precisely, the two formulas are only logically equivalent in those of Lewis s sphere systems (Lewis 1973) satisfying both weak and strong centering, that is, the actual world is the only element of the innermost sphere. Indeed, such models validate the axiom of conditional modus ponens (p (p q)) q and the axiom of conjunctive sufficiency (p q) (p q), and from these two one can prove the logical equivalence of p (p q) and p q. Second, we could move from the Hamming distance to the set inclusion-based ordering underlying Satoh s revision operation (Satoh 1988) and Winslett s update operation (Winslett 1988, 1990). Third, it would be interesting to have a complete set of postulates characterising our operation. This is however certainly not easy to achieve: our operation extends Dalal s belief revision operation, for which as far as we know no characterisation exists in the literature.

Acknowledgements Our work was partially supported by project LIANDA - BBVA Foundation Grants for Scientific Research Projects, Spain.

References Ågotnes, T.; van der Hoek, W.; and Wooldridge, M. J. 2012. Conservative Social Laws. In ECAI, volume 242, 49 54. Alchourr on, C. E.; G ardenfors, P.; and Makinson, D. 1985. On the logic of theory change: Partial meet contraction and revision functions. The journal of symbolic logic, 50(2): 510 530. Ben-Naim, J. 2006. Lack of Finite Characterizations for the Distance-Based Revision. In Doherty, P.; Mylopoulos, J.; and Welty, C. A., eds., Proceedings, Tenth International Conference on Principles of Knowledge Representation and Reasoning, Lake District of the United Kingdom, June 2-5, 2006, 239 248. AAAI Press. ISBN 978-1-57735-271-6. Berto, F. 2019. Simple hyperintensional belief revision. Erkenntnis, 84(3): 559 575. Caridroit, T.; Konieczny, S.; de Lima, T.; and Marquis, P. 2016. On Distances Between KD45n Kripke Models and Their Use for Belief Revision. In Kaminka, G. A.; Fox, M.; Bouquet, P.; H ullermeier, E.; Dignum, V.; Dignum, F.; and van Harmelen, F., eds., ECAI 2016 - 22nd European Conference on Artificial Intelligence, 29 August-2 September 2016, The Hague, The Netherlands - Including Prestigious Applications of Artificial Intelligence (PAIS 2016), volume 285 of Frontiers in Artificial Intelligence and Applications, 1053 1061. IOS Press. ISBN 978-1-61499-671-2. Chellas, B. F. 1980. Modal logic: An introduction. Cambridge University Press. Dalal, M. 1988. Investigations into a Theory of Knowledge Base Revision. In Shrobe, H. E.; Mitchell, T. M.; and Smith, R. G., eds., Proceedings of the 7th National Conference on Artificial Intelligence, St. Paul, MN, USA, August 21-26, 1988, 475 479. AAAI Press / The MIT Press. Eiter, T.; and Mannila, H. 1997. Distance Measures for Point Sets and Their Computation. Acta informatica, 34(2): 109 133. Fuhrmann, A. 1989. Reflective modalities and theory change. Synthese, 81: 115 134. Fujita, O. 2013. Metrics Based on Average Distance between Sets. Japan Journal of Industrial and Applied Mathematics, 30: 1 19. Hansson, S. O. 1999. A textbook of belief dynamics. Kluwer Academic Press. Hansson, S. O. 2022. Logic of Belief Revision. In Zalta, E. N., ed., The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Spring 2022 edition. Hughes, G. E.; and Cresswell, M. J. 1968. An introduction to modal logic. Methuen&Co. Ltd, London. Katsuno, H.; and Mendelzon, A. O. 1991. Propositional Knowledge Base Revision and Minimal Change. Artificial Intelligence, 52(3): 263 294.

Konieczny, S.; Lang, J.; and Marquis, P. 2005. Reasoning under inconsistency: the forgotten connective. In Kaelbling, L. P.; and Saffiotti, A., eds., IJCAI-05, Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, Edinburgh, Scotland, UK, July 30 - August 5, 2005, 484 489. Professional Book Center. ISBN 0938075934. Konieczny, S.; and Pino P erez, R. 2002. Merging information under constraints: a logical framework. Journal of Logic and Computation, 12(5): 773 808. Kourousias, G.; and Makinson, D. 2007. Parallel interpolation, splitting, and relevance in belief change. Journal of Symbolic Logic, 72(3): 994 1002. Lakemeyer, G.; and Lang, W. 1996. Belief Revision in a Nonclassical Logic. In G orz, G.; and H olldobler, S., eds., KI-96: Advances in Artificial Intelligence, number 1137 in LNCS, 199 211. Lehmann, D. J.; Magidor, M.; and Schlechta, K. 2001. Distance Semantics for Belief Revision. J. Symb. Log., 66(1): 295 317. Lewis, C.; and Langford, C. H. 1959. Symbolic Logic. Dover reprint. Orig. published in 1932. Lewis, D. 1973. Counterfactuals. Basil Blackwell, Oxford. Lindstr om, S.; and Rabinowicz, W. 1999. Belief Change for Introspective Agents. In Hulth, N.; de L eon, D.; and Wallin, A., eds., Spinning Ideas, Electronic Essays Dedicated to Peter G ardenfors on His Fiftieth Birthday, Lund University Cognitive Studies Special Edition. Lund University. Niiniluoto, I. 1987. Truthlikeness. Dordrecht: Springer Netherlands. ISBN 978-94-010-8170-2 978-94-009-37390. Niiniluoto, I.; and Tuomela, R., eds. 1979. The Logic and Epistemology of Scientific Change. Amsterdam: North Holland Pub. Co. Oddie, G. 1978. Verisimilitude and Distance in Logical Space. Acta Philosophica Fennica, 30: 227 43. Parikh, R. 1999. Beliefs, belief revision, and splitting languages. In Moss, L.; Ginzburg, J.; and de Rijke, M., eds., Logic, Language, and Computation, volume 2. CSLI Publications. Restall, G.; and Slaney, J. K. 1995. Realistic Belief Revision. In WOCFAI, 367 378. Satoh, K. 1988. Nonmonotonic Reasoning by Minimal Belief Revision. In FGCS, 455 462. Schwind, N.; Konieczny, S.; and Pino P erez, R. 2022. On Paraconsistent Belief Revision in LP. In Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, Thirty Fourth Conference on Innovative Applications of Artificial Intelligence, IAAI 2022, The Twelveth Symposium on Educational Advances in Artificial Intelligence, EAAI 2022 Virtual Event, February 22 - March 1, 2022, 5879 5887. AAAI Press. Song, W.; Cai, K.; and Immink, K. A. S. 2020. Sequencesubset distance and coding for error control in DNA-based data storage. IEEE Transactions on Information Theory, 66(10): 6048 6065.

Winslett, M.-A. 1988. Reasoning about action using a possible models approach. In Proc. 7th Conf. on Artificial Intelligence (AAAI 88), 89 93. St. Paul. Winslett, M.-A. 1990. Updating Logical Databases. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press.