Forgetting in Multi-Agent Modal Logics

1 Introduction

In the past decades, forgetting has been investigated for many logics and has found many applications in knowledge representation and reasoning (KR). Intuitively, forgetting some symbols from a knowledge base (KB) should result in a weaker KB which entails the same set of sentences that do not mention those symbols.

The seminal paper by Lin and Reiter [1994] studied forgetting in propositional and first-order logics. Over the years, forgetting in propositional logic has been used in abductive reasoning [Lin, 2001], reasoning under inconsistency [Lang and Marquis, 2010], reasoning about knowledge [Su et al., 2009], epistemic planning [Herzig et al., 2003], etc; and forgetting in first-order logic has been applied to progression for basic action theories in the situation calculus [Lin and Reiter, 1997; Liu and Lakemeyer, 2009]. In recent years, forgetting has been generalized to various description logics and applied to ontology reuse [Wang et al., 2009; 2010; Konev et al., 2009; Lutz and Wolter, 2011]. There exist some resolutionbased approaches for forgetting in expressive description logics [Ludwig and Konev, 2014; Koopmann and Schmidt, 2014; 2015]. Forgetting has also been studied for logic programs and used in conflict solving [Zhang and Foo, 2006; Eiter and Wang, 2008; Wang et al., 2014].

Forgetting for modal logics has also been investigated and applied to reasoning about knowledge and belief. Baral and Zhang [2005] studied knowledge update, a special form of update with the effect that the agent becomes ignorant of a propositional formula. Van Ditmarsch et al. [2009] presented a dynamic epistemic logic where the dynamic operator is the action of forgetting a propositional atom. Zhang and Zhou [2009] studied forgetting in propositional S5 logic and its applications in knowledge updates and knowledge games. Liu and Wen [2011] explored forgetting in first-order S5 logic and applied it to progression of knowledge in the situation calculus, which concerns updating the current representation of the world state and agents' epistemic state to reflect the change caused by an ontic or epistemic action. Later, Fang et al. [2015] extended the above results to progression of both knowledge and belief for nondeterministic actions in the single-agent propositional case.

Zhang and Zhou's semantic definition of forgetting coincides with that of existential bisimulation quantifiers. Bisimulation quantifiers were introduced by Ghilardi and Zawadowski [1995] to study uniform interpolation, which is the dual notion of forgetting, in modal logics. A logic has uniform interpolation if for any formula φ and any set S of symbols occurring in φ, there is a formula using only symbols in S such that φ and entail the same set of sentences formulated only in S. The semantics of existential bisimulation quantifiers is as follows: a model M satisfies a formula 9pφ where p is an atom iff there is a model M 0 satisfying φ such that M and M 0 are bisimilar with exception on p. It turns out that any logic that is invariant under bisimulation and closed under bisimulation quantification, that is, closed under elimination of the quantification, has uniform interpolation. It is well-known that K, T and S5 have uniform interpolation [Ghilardi, 1995; B´ılkov´a, 2007; Ghilardi and Zawadowski, 2000]. However, neither K4 or S4 has uniform interpolation [B´ılkov´a, 2007; Ghilardi and Zawadowski, 1995].

In the multi-agent case, D'Agostino and Lenzi [2006] gave a constructive proof that θ-calculus, an extension of Kn with a fixed-point operator, is closed under bisimulation quantification and hence has uniform interpolation. Studer [2009] showed that KC, which is Kn with common knowledge, does not have uniform interpolation, and this also holds for K4C. Pattinson [2013] showed that all modal logics axiomatizable by formulas whose modal depth uniformly equals one, including Kn and Dn, have uniform interpolation. Reasoning about knowledge and belief in the multi-agent case is certainly important from the KR point of view, since higherorder knowledge and belief (i.e., knowledge and belief about other agents' knowledge and belief) play an important role in coordination and interaction. However, to the best of our knowledge, other than the above mentioned works, forgetting in multi-agent modal logics has largely been unexplored, and it remains an open problem whether Tn, K45n, KD45n or S5n have uniform interpolation.

It is well-known that in propositional logic, the result of forgetting atom p from a satisfiable term (i.e., a conjunction of literals) δ can be obtained from δ by substituting any occurrence of literal p or ≻p with >. As every propositional formula can be equivalently transformed into a disjunction of satisfiable terms, and forgetting is distributive over disjunction, propositional logic is closed under forgetting. Interestingly, the idea of literal elimination was used by D'Agostino and Lenzi to prove that θ-calculus is closed under bisimulation quantification.

In this paper, we study forgetting in multi-agent modal logics. We adopt the semantic definition of existential bisimulation quantifiers as that of forgetting. We resort to the normal forms of propositional modal logics, called canonical formulas by Moss [2007], a nice property of which is that an arbitrary modal formula is equivalent to a disjunction of a finite set of satisfiable canonical formulas. Due to the distributive law of forgetting over disjunction, forgetting from arbitrary modal formulas can be reduced to forgetting from satisfiable canonical formulas, which we show can be computed via literal elimination. Hence we show that except K4n and S4n, which do not have uniform interpolation, the other main multi-agent modal systems are closed under forgetting.

2 Preliminaries

In this section, we introduce the background material, i.e., the syntax and semantics of multi-agent modal logics, and the canonical formulas for modal logics as defined by Moss.

2.1 Multi-agent modal logics

We fix a set A of n agents and a countable set of atoms P.

Definition 1 The language LKn is generated by the BNF:

where p 2 P and i 2 A. We use Lpl for the propositional language, i.e., the language without the Ki modality.

We let > and ? represent true and false respectively. We use p and q to range over atoms, φ and to range over formulas, and Φ and to range over sets of formulas. We let P(φ) denote the set of atoms which appear in φ.

Definition 2 A frame is a pair (S↪ R), where

The (modal) depth of a formula φ in LKn , written dep(φ), is the depth of nesting of modal operators in φ. We let ˆKiφ stand for ≻Ki≻φ. We let W Φ (resp. V Φ) denote the disjunction (resp. conjunction) of members of Φ; and we use V ˆKiΦ to represent the conjunction of ˆKiφ where φ 2 Φ.

• ÷ S is a non-empty set of possible worlds;
• ÷ For each agent i 2 A, Ri is a binary relation on S, called the accessibility relation for i.

For s 2 S, we write Ri(s) for ¶t 2 S ♣ sRit♦, and call it the i-children of s.

Different modal systems result from different sets of conditions on the accessibility relations. We say Ri is serial if for any s 2 S, there is s0 2 S s.t. sRis0 ; we say Ri is Euclidean if whenever sRis1 and sRis2, we have s1Ris2.

We list the main modal systems in Table 1. KD45 and S5 are well-accepted as the logics for knowledge and belief, respectively. For each symbol L listed here, we use L for the single agent case, Ln for the case where there are n agents.

Definition 3 A Kripke model is a triple M = hS↪R↪ V i, where (S↪R) is a frame, and V is a valuation map, which maps each s 2 S to a subset of P. A pointed Kripke model is a pair (M↪ s), where M is a Kripke model and s is a world of M, called the actual world.

For simplicity, we often omit the word "pointed".

Definition 4 Let (M↪ s) be a Kripke model where M = hS↪ R↪ V i. We interpret formulas in LKn by induction:

• ÷ M↪ s ♣= p iff p 2 V (s);
• ÷ M↪ s ♣= ≻φ iff M↪ s 6♣= φ;
• ÷ M↪ s ♣= φ ^ iff M↪ s ♣= φ andM↪ s ♣= ;
• ÷ M↪ s ♣= Kiφ iff for all t 2 Ri(s), M↪ t ♣= φ.

We use L to range over modal systems. Consider the context of a modal system L. We say φ is satisfiable, if there exists a model of φ. We say φ entails , written φ ♣= , if for any model (M↪ s), M↪ s ♣= φ implies M↪ s ♣= . We say φ and are equivalent, written φ ⌘ , if φ ♣= and ♣= φ.

D'Agostino and Lenzi [2005] presented another modal language which is based on the cover modality ri:

Definition 5 Let i 2 A, and Φ a finite set of formulas in LKn . We use riΦ to denote the formula Ki(W Φ) ^ (V ˆKiΦ). Note that ri; ⌘ Ki?.

Now, we can get the semantics of the cover modality.

Lemma 1 Let (M↪ s) be a Kripke model where M = hS↪R↪ V i and s 2 S. Then M↪ s ♣= riΦ iff the following conditions hold:

• ÷ for all t 2 Ri(s), there is φ 2 Φ s.t. M↪ t ♣= φ;

Proposition 1 [Janin and Walukiewicz, 1995] Every formula in LKn is equivalent to a formula using only the ri modalities.

• ÷ for all φ 2 Φ, there is t 2 Ri(s) s.t. M↪ t ♣= φ.

2.2 Canonical formulas

We will present our definitions and proofs via canonical formulas of modal logics, as defined by Moss [2007], which capture Kripke models up to a given depth.

Definition 6 (Canonical formulas) Let P ✓ P be finite. We inductively define the set EP k as follows:

• ÷ EP k+1 = ¶δ0 ^ Vi2A riΦi ♣ δ0 2 EP 0 and Φi ✓ EP k ♦.
• ÷ EP 0 = ¶Vp2 ˜ P p ^ Vp2P∩ ˜ P ≻p ♣ ˜ P ✓ P♦;

Let δ = δ0 ^ Vi2A riΦi 2 EP k+1 . We denote δ0 by w(δ), and call it the world of δ; we denote Φi by Ri(δ), and call it the i-children of δ.

Intuitively, when we restrict our attention to the atoms in P , a canonical formula of depth k provides a complete syntactic representation of a Kripke model up to depth k.

The following proposition says that every Kripke model (M↪ s) satisfies a unique canonical formula of a given depth k, which we call the depth k canonical formula of (M↪ s).

Proposition 2 [Moss, 2007] Let (M↪ s) be a model and k 2 N. Let P ✓ P be finite. Then, there exists a unique δ 2 EP k s.t. M↪ s ♣= δ.

We can get the following corollary which means that every modal formula can be equivalently transformed into a disjunction of satisfiable canonical formulas whose depth is not less than that of the original formula.

Proposition 3 Consider the context of a modal system L. Let φ 2 LKn and l 2 N s.t. l ≥ dep(φ). Let P = P(φ). Then there exists a unique set Φ ✓ EP l s.t. φ ⌘ W Φ, and for every δ 2 Φ, δ is satisfiable in L.

Now, we introduce the projection operations on canonical formulas. A canonical formula can be graphically represented as a tree. The operation δ# prunes the leaves of this tree. In δ#l , we perform pruning l times sequentially. We call δ# the 1st-cut of δ, and δ#l the lth-cut of δ.

Definition 7 Let P ✓ P be finite. Let k 2 N and δ 2 EP k . Then, δ# is inductively defined as follows:

Let Φ be a set of canonical formulas. We use Φ# to denote the set ¶φ# ♣ φ 2 Φ♦.

Definition 8 Let P ✓ P be finite. Let k↪ l 2 N s.t. k ≥ l. Let δ 2 EP k . Then, δ#l is inductively defined as follows:

Similarly to Φ# , Φ#l is the set ¶φ#l ♣ φ 2 Φ♦. Obviously, δ ♣= δ#l for all l  dep(δ).

It is easy to prove the following, which intuitively says that the i-children of the lth-cut of a canonical formula is equal to the lth-cut of its i-children, i.e., the two operations are commutative.

Proposition 4 Let δ be a canonical formula. Let l 2 N s.t. l < dep(δ). Then for all i 2 A, we have Ri(δ#l ) = Ri(δ)#l .

Example 1 Let δ = p ^ ri¶≻p ^ri¶p↪ ≻p♦♦. Obviously, the depth of δ is 2. By Definitions 7 and 8, δ#1 = δ# = p ^ ri(¶≻p ^ ri¶p↪ ≻p♦♦)# = p ^ ri¶≻p♦. Similarly, we get Ri(δ#1 ) = ¶≻p♦, Ri(δ) = ¶≻p ^ri¶p↪ ≻p♦♦, and Ri(δ)#1 = ¶≻p♦. Hence Ri(δ#1 ) = Ri(δ)#1 = ¶≻p♦.

3 Forgetting

In this section, we define forgetting in multi-agent modal logics. We first review forgetting in propositional logic.

We use a subset of the atoms to denote a valuation.

Definition 9 Let φ 2 Lpl and p an atom. A formula 2 Lpl s.t. P( ) ✓ P(φ)∩¶p♦ is a result of forgetting p in φ, written pforget(φ↪ p) ⌘ , if for any valuation P, P ♣= φ (meaning P satisfies φ) iff there is a valuation P 0 s.t. P 0 ♣= and P ⇠p P 0 , i.e., P ∩ ¶p♦ = P 0 ∩ ¶p♦.

The definition of forgetting in multi-agent modal logics is analogous to that in propositional logic. For this purpose, we use the well-known concept of bisimulation.

Definition 10 (p-bisimulation) Let (M↪ s) and (M 0 ↪ s0 ) be two Kripke models where M = hS↪R↪ V i and M 0 = hS0 ↪R0 ↪ V 0 i. A p-bisimulation between (M↪ s) and (M 0 ↪ s0 ) is a relation ⇢ ✓ S ⇥ S0 s.t. s⇢s0 , and whenever t⇢t0 , we get:

forth For all i, if tRiu, then there is u0 s.t. t0R0iu0 and u⇢u0 ;

back For all i, if t0R0iu0 , then there is u s.t. tRiu and u⇢u0 .

We say that (M↪ s) and (M 0 ↪ s0 ) are p-bisimilar, written

(M↪ s)$p (M 0 ↪ s0 ), if there is a p-bisimulation between them.

Clearly, $p is an equivalence relation. A nice property of p-bisimilar Kripke models is that they agree on all modal formulas wherein p does not appear.

Proposition 5 Let (M↪ s)$p (M 0 ↪ s0 ). Let φ 2 LKn where p does not appear in φ. Then M↪ s ♣= φ iff M 0 ↪ s0 ♣= φ.

Definition 11 (Forgetting) Consider the context of a modal system L. Let φ 2 LKn and p an atom. A formula s.t. P( ) ✓ P(φ) ∩ ¶p♦ is a result of forgetting p in φ, written kforget(φ↪ p) ⌘ , if for any model (M 0 ↪ s0 ), M 0 ↪ s0 ♣= iff there is a model (M↪ s) of φ s.t. (M↪ s)$p (M 0 ↪ s0 ).

So the semantics of forgetting is that of existential bisimulation quantifiers as presented in the introduction. Clearly, if both 1 and 2 are results of forgetting p in φ, then they are logically equivalent. In this paper, when we prove kforget(φ↪ p) ⌘ , the proof of the if direction of Definition 11 is straightforward by making use of (M↪ s)$p (M 0 ↪ s0 ) and the induction hypothesis if applicable. To save space, we only present the proof of the only-if direction.

We now analyze basic properties of forgetting.

Proposition 6 Consider the context of a modal system L. If kforget(φ↪ p) ⌘ , then φ ♣= ; and for any ⌘ where p does not occur, φ ♣= ⌘ iff ♣= ⌘.

Proposition 7 Consider the context of a modal system L.

1. If φ 2 Lpl and pforget(φ↪ p) ⌘ , then kforget(φ↪ p) ⌘ ;
2. kforget(φ1 _ φ2↪ p) ⌘ kforget(φ1↪ p) _ kforget(φ2↪ p).

Proof: We only prove the only-if direction of Part 1. Let M 0 ↪ s0 ♣= . We let the structure of M be a copy of that of M 0 ; let V expand V 0 s.t. V (s) ♣= φ. Then we have M↪ s ♣= φ and (M↪ s)$p (M 0 ↪ s0 ).

We now relate forgetting to uniform interpolation.

Definition 12 We say that a modal system L is closed under forgetting if for any formula φ and any atom p 2 P(φ), there exists an L formula s.t. kforget(φ↪ p) ⌘ .

Definition 13 We say a modal system L has uniform interpolation if for every formula φ and every P ✓ P(φ), there is a formula such that P( ) ✓ P and such that for any formula ⌘ with P(⌘) ✓ P, we have φ ♣= ⌘ iff ♣= ⌘.

Zhang and Zhou [2009] proposed the forgetting postulates,

which correspond to the definition of uniform interpolation. By Proposition 6, we have

Proposition 8 If a modal system L is closed under forgetting, then L has uniform interpolation.

As mentioned in the introduction, neither K4 nor S4 has uniform interpolation. Because K4 is indeed K41, which is a special case of K4n, K4n does not have uniform interpolation. Similarly, neither has S4n. Hence, we get

Corollary 1 Neither K4n nor S4n is closed under forgetting.

Finally, we propose a syntactical method of forgetting.

Definition 14 (Literal elimination) Let φ 2 LKn and p an atom. We let φp denote the formula obtained from φ by substituting all occurrences of ≻p with > and subsequently substituting all occurrences of p with >.

Merely requiring to replace ≻p and p by > would be ambiguous. Because, should we then replace ≻p by > or by ?? The last would happen if we were to replace the p in ≻p by >. That would be an undesirable outcome. The 'subsequently' in Definition 14 is not ambiguous and avoids that outcome.

Typically, we only apply this substitution to formulas wherein negations only bind atoms. Similarly to Φ# , Φp is the set ¶φp ♣ φ 2 Φ♦.

In the following sections, we will show that when δ is a canonical formula satisfiable in L, kforget L (δ↪ p) ⌘ δp .

4 Forgetting in multi-agent modal logics

In this section, we show that forgetting from satisfiable canonical formulas can be computed via literal elimination in the following multi-agent modal logics: Kn, Dn, Tn, K45n, KD45n and S5n. As an easy corollary, we have that the above logics are closed under forgetting and they have uniform interpolation.

4.1 Forgetting in Kn and Dn

In this subsection, we consider Kn and Dn cases. In fact, these results were first proved by D'Agostino and Lenzi [2006]. As mentioned in the introduction, they gave a constructive proof that θ-calculus is closed under bisimulation quantification. The core result they proved is the following:

Theorem [D'Agostino and Lenzi, 2006] Let φ be a cover disjunctive formula for θ-calculus. Then 9pφ ⌘ φp .

In the theorem, a cover disjunctive formula is a generalization of the notion of a disjunction of canonicial formulas that we use in this paper.

Here 9p is the bisimulation quantifier we defined in the introduction. Their proof is via an automata approach. Here we present an easy inductive proof, which serves as the basis for the proofs of all the forgetting results in this paper.

Theorem 1 (The basic theorem) Let L be Kn or Dn, and δ an L-satisfiable canonical formula. Then kforget L (δ↪ p) ⌘ δp .

Proof: We prove by induction on dep(δ). The base case, i.e., δ 2 EP 0 , follows from Proposition 7. We prove the only-if direction of the induction case, i.e., δ 2 EP k where k ≥ 1. Let M 0 ↪ s0 ♣= δp . We constructM and define a relation ⇢ between the worlds of M and M 0 as follows. Figure 1 illustrates the construction.

1. Create a new world s, let s⇢s0 , and V (s) ♣= w(δ).
2. For all i 2 A, t0 2 R0i (s0 ), and ⌘ 2 Ri(δ), if M 0 ↪ t0 ♣= ⌘p , by the induction hypothesis, there exist (Mt0 ↪⌘↪ tt0 ↪⌘) and ⇢t0 ↪⌘ s.t. Mt0 ↪⌘↪ tt0 ↪⌘ ♣= ⌘ and ⇢t0 ↪⌘ : (Mt0 ↪⌘↪ tt0 ↪⌘)$p (M 0 ↪ t0 ). Add a new copy of Mt0 ↪⌘ intoM, let sRitt0 ↪⌘, and expand ⇢ with ⇢t0 ↪⌘.

It is easy to show that ⇢ : (M↪ s)$p (M 0 ↪ s0 ) and M↪ s ♣= δ. In the case of Dn, it is obvious from the above construction that if M 0 satisfies seriality, so does M.

As a corollary of Propositions 3, 7 and Theorem 1, we get Corollary 2 Kn and Dn are closed under forgetting.

Example 3 Let φ be ˆKip^ ˆKi≻p, meaning that agent i is ignorant about p. Intuitively, after forgetting p, the agent should still have consistent belief. We convert φ into a disjunction of two canonical formulas δ1 and δ2 where δ1 = p ^ ri¶p↪ ≻p♦ and δ2 = ≻p^ri¶p↪ ≻p♦. Then δp 1 = δp 2 = >^ri¶>♦. The disjunction of them is equivalent to ˆKi>.

4.2 Forgetting in Tn

In this subsection, we analyze properties of Tn satisfiable canonical formulas, and show that forgetting via literal elimination applies to them.

We begin with a simple example which shows that Theorem 1 does not hold for unsatisfiable canonical formulas.

Example 4 Let δ = ≻p ^ ri¶p♦. Clearly, δ is a canonical formula, and it is equivalent to ? in Tn. However, δp = >^ri¶>♦ which is equivalent to >.

The reason that forgetting via literal elimination does not work on δ is that δ is unsatisfiable in Tn. This motivates us to consider only satisfiable canonical formulas.

The following proposition says that any Tn satisfiable canonical formula δ has the reflexive property: for any agent i and any 1  l  dep(δ), the lth-cut of δ is an i-child of its (l - 1)th-cut.

Proposition 9 Let δ be a Tn satisfiable canonical formula where dep(δ) ≥ 1. Let l 2 N s.t. 1  l  dep(δ). Then, for all i 2 A, we have δ#l 2 Ri(δ#l-1 ).

Proof: Here, we only prove the base case, i.e., δ# 2 Ri(δ). Let k = dep(δ) and M↪ s ♣= δ. Obviously, M↪ s ♣= δ# . Since M is reflexive, s 2 Ri(s). By the semantics of the ri modality, there exists δi 2 Ri(δ) s.t. M↪ s ♣= δi. So both δ# and δi are the depth k - 1 canonical formula of (M↪ s) (cf. Proposition 2). Hence δ# = δi 2 Ri(δ).

Example 4 Cont'd We have δ# = ≻p and Ri(δ) = ¶p♦. Obviously, δ# ◁2 Ri(δ). So δ is not satisfiable in Tn.

Example 5 Let δ = p ^ q ^ ri¶p ^ q↪ p ^≻q♦. It is a Tn satisfiable canonical formula. Then, δ# = p^q, and Ri(δ) = ¶p ^ q↪ p ^ ≻q♦. Obviously, δ# 2 Ri(δ).

Theorem 2 (The Tn theorem) Let δ be a Tn satisfiable canonical formula. Then kforget Tn (δ↪ p) ⌘ δp .

Proof: The proof is the same as that of the basic theorem except the following. In the induction case, we get (M↪ s)$p (M 0 ↪ s0 ) and M↪ s ♣= δ. Let k = dep(δ). Then for any l  k, M↪ s ♣= δ#l . We now let sRis for each agent i. It is obvious that (M↪ s) is a Tn model. It is easy to see that (M↪ s)$p (M 0 ↪ s0 ) still holds. It remains to show that M↪ s ♣= δ still holds. We prove by induction on k - l that for any l  k, M↪ s ♣= δ#l still holds. Base case. M↪ s ♣= w(δ), which is δ#k . Induction case. Suppose that M↪ s ♣= δ#l . To show that M↪ s ♣= δ#l-1 , it suffices to show that for each i 2 A, there exists ⌘ 2 Ri(δ#l-1 ) s.t. M↪ s ♣= ⌘. By Proposition 9, δ#l 2 Ri(δ#l-1 ). Hence δ#l is the desired ⌘.

4.3 Multi-pointed Kripke models

In the next subsection, we show that forgetting via literal elimination applies to satisfiable canonical formulas of K45n, KD45n and S5n. The proof for the basic theorem does not immediately carry forward to these cases, because the model constructed in the proof may not be transitive or Euclidean. Also, we cannot simply fix the problem by adding edges as we do in the proof of the Tn theorem. We will overcome the problem via multi-pointed Kripke models which offers flexibility in the construction of required models. In this subsection, we introduce the basic concepts regarding multi-pointed models.

Definition 15 A multi-pointed Kripke model is a pair (M↪ T ) where M is a Kripke model, and T is a possibly empty set of worlds of M.

Throughout this paper, we use (M↪ s) to denote a singlepointed model, and (M↪ T ) a multi-pointed model.

Given a single-pointed model (M↪ s) and i 2 A, we can naturally obtain a multi-pointed model (M↪ T) where T = Ri(s), i.e., the i-children of s.

Similarly to the semantics of the cover modality, we have:

Definition 16 Let Φ be a set of formulas. We say a multipointed model (M↪ T) is Φ-complete if the following hold:

• ÷ for every t 2 T , there exists φ 2 Φ s.t. M↪ t ♣= φ;
• ÷ for every φ 2 Φ, there exists t 2 T s.t. M↪ t ♣= φ.

Obviously, M↪ s ♣= riΦ iff (M↪ Ri(s)) is Φ-complete.

Then, we can extend Proposition 2 to multi-pointed models: we have that a multi-pointed model (M↪ T) corresponds to a unique set of canonical formulas of a given depth k, which we call the depth k canonical formula set of (M↪ T).

Proposition 10 Let (M↪ T) be a multi-pointed model, and k 2 N. Let P ✓ P be finite. Then, there exists a unique set Φ ✓ EP k s.t. (M↪ T) is Φ-complete.

We now extend the concept of bisimulation to multipointed models.

Definition 17 Let (M↪ T) and (M 0 ↪ T 0 ) be two Kripke models. A p-bisimulation between (M↪ T ) and (M 0 ↪ T 0 ) is a relation ⇢ between the worlds of M and M 0 s.t.

• ÷ for every t 2 T, there exists t0 2 T 0 s.t. t⇢t0 ;
• ÷ for every t0 2 T 0 , there exists t 2 T s.t. t⇢t0 ;
• ÷ whenever u⇢u0 , the atoms, forth and back conditions in Definition 10 hold.

We end with a constraint on multi-pointed models, which is crucial for constructing transitive and Euclidean models.

Definition 18 Let (M↪ T) be a Kripke model and i 2 A. We say that (M↪ T) is i-equivalent if for all t1↪ t2 2 T, we have t1Rit2, and for every s 2 S, if there exists t 2 T s.t. sRit or tRis, then s 2 T .

4.4 Forgetting in K45n, KD45n and S5n

In this subsection, we generalize the forgetting results for satisfiable canonical formulas to K45n, KD45n and S5n.

The following proposition says that any K45n satisfiable canonical formula δ has the identical-children property: for any agent i and any i-child δi of δ, the lth-cut of δ's i-children is equal to the i-children of the (l - 1)th-cut of δi.

Proof: Let k = dep(δ), M↪ s ♣= δ, i 2 A and δi 2 Ri(δ). Here, we only prove the base case, i.e., (Ri(δ))# = Ri(δi). Then there exists t 2 Ri(s) s.t. M↪ t ♣= δi. Since M is transitive and Euclidean, Ri(s) = Ri(t). Obviously, (M↪ Ri(s)) is (Ri(δ))# -complete and (M↪Ri(t)) is Ri(δi)-complete. So (M↪Ri(s)) is also Ri(δi)-complete. So both (Ri(δ))# and Ri(δi) are the depth k-2 canonical formula set of (M↪ Ri(s)) (cf. Proposition 10). Hence (Ri(δ))# = Ri(δi).

Proposition 11 Let δ be a K45n satisfiable canonical formula where dep(δ) ≥ 2. Let l 2 N s.t. 1  l < dep(δ). Then, for all i 2 A and δi 2 Ri(δ), (Ri(δ))#l = Ri(δ#l-1 i ).

Now, we prove an important lemma, which is the multipointed extension of the only-if direction of the version of the basic theorem for K45n.

Lemma 2 (The K45n lemma) Let δ be a K45n satisfiable canonical formula where dep(δ) ≥ 1. Let (M 0 ↪ s0 ) be a K45n model of δp . Then for all i 2 A, there exists a multi-pointed K45n model (M↪ T) that is i-equivalent, Ri(δ)-complete and (M↪ T )$p (M 0 ↪ R0i (s0 )).

Proof: We prove by induction on dep(δ).

Base case, i.e., Ri(δ) is a set of propositional formulas. We construct (M↪ T ) and define the p-bisimulation ⇢ between (M↪ T) and (M 0 ↪R0i (s0 )) as follows. Figure 2 illustrates the construction. We initialize S = ; and ⇢ = ;.

1. For all t0 2 R0i (s0 ) and δi 2 Ri(δ), if M 0 ↪ t0 ♣= δp i , we create a world t s.t. V (t) ♣= w(δi). Then we add it into S and T, and let t⇢t0 .
2. For all t1↪ t2 2 T, we let t1Rit2.

It is easy to verify (M↪ T) satisfies the requirements.

1. For t 2 T and j 6= i, we make a copy of (M 0 ↪R0j (t0 )), denoted by (Mt↪j↪ Tt↪j) where t0 is the original world of t. We connect t to all worlds of Tt↪j via j-edges, i.e., let tRju for u 2 Tt↪j . We let u⇢u0 when u is the copy of u0 .

Induction step. The construction of (M↪ T) is similar to that of the base case except the following. In Step 3, since M 0 ↪ t0 ♣= δp i , by the induction hypothesis, there exist (Mt↪j↪ Tt↪j) that is j-equivalent and Rj(δi)-complete and ⇢t↪j: (Mt↪j↪ Tt↪j)$p (M 0 ↪R0j (t0 )). We expand ⇢ with ⇢t↪j. Obviously, (M↪ T) is transitive, Euclidean and i-equivalent, and (M↪ T )$p (M 0 ↪ R0i (s0 )).

It remains to verify that (M↪ T) is Ri(δ)-complete. Let dep(δ) = k. We prove by induction on k - l that for all 0  l < k, (M↪ T) is Ri(δ)#l -complete. Base case: l = k - 1, and Ri(δ)#l is a set of propositional formulas. By Step 1, (M↪ T) is Ri(δ)#l -complete. Induction step. Suppose that (M↪ T) is Ri(δ)#l -complete. We prove that it is also (Ri(δ))#l-1 -complete. Let t 2 T. By the construction, there exists δi 2 Ri(δ) s.t. M↪ t ♣= w(δi). It suffices to show that M↪ t ♣= δ#l-1 i . Since w(δ#l-1 i ) = w(δi), M↪ t ♣= w(δ#l-1 i ). By the identical-children property (Proposition 11), (Ri(δ))#l = Ri(δ#l-1 i ). By the induction hypothesis, (M↪ T) is Ri(δ#l-1 i )-complete, so M↪ t ♣= riRi(δ#l-1 i ). For j 6= i, because (Mt↪j↪ Tt↪j) is Rj(δi)- complete and Rj(t) = Tt↪j , M↪ t ♣= rjRj(δi), hence M↪ t ♣= rjRj(δi)#l-1 . By Proposition 4, Rj(δi)#l-1 = Rj(δ#l-1 i ), soM↪ t ♣=rjRj(δ#l-1 i ).

Now, we get the following theorem via Lemma 2.

Theorem 3 (The K45n theorem) Let δ be a K45n satisfiable canonical formula. Then kforget K45n (δ↪ p) ⌘ δp .

Proof: The proof is the same as that of the basic theorem except Step 2 of the induction case. By the K45n lemma, for every i 2 A, there exist (Mi↪ Ti) and ⇢i : (Mi↪ Ti)$p (M 0 ↪R0i (s0 )). Add a new copy of Mi into M, let sRit for all t 2 Ti, and expand ⇢ with ⇢i.

From the construction of the K45n lemma and the K45n theorem, if the given model M 0 is a KD45n model, then we can acquire a KD45n model M. Hence we can get

Theorem 4 Let δ be a KD45n satisfiable canonical formula. Then kforget KD45n (δ↪ p) ⌘ δp .

We proceed to S5n. The models constructed in the proofs of the K45n lemma and the K45n theoremmay not be reflexive. We can fix it via adding edges as follows: for all i 2 A,

1. for all t 2 S, we let tRit; (reflexive edges)
2. for all t↪ u 2 S, if tRiu, we let uRit. (symmetric edges) It is easy to verify that the new models are S5n models.

Example 6 In Figure 3, given a model (M↪ T) shown in Figure 2, we add blue edges so that it is an S5n model. Note that it is not necessary to add edges for four submodels (Mt1↪j↪ Tt1↪j), (Mt1↪k↪ Tt1↪k), (Mt2↪j↪ Tt2↪j) and

(Mt2↪k↪ Tt2↪k). All of them are S5n models since they are acquired by the induction hypothesis. We just add the edges as follows:

1. Let t1Rjt1, t1Rkt1, t2Rjt2 and t2Rkt2;
2. For u 2 Tt1↪j (resp. Tt1↪k), let uRjt1 (resp. uRkt1).
3. For u 2 Tt2↪j (resp. Tt2↪k), let uRjt2 (resp. uRkt2).

All that remains now is to prove that the constructed models satisfy the original formulas. Since the logic S5n is both K45n and Tn logics, any S5n satisfiable canonical formula has the reflexive and identical-children properties (Propositions 9 and 11). Hence, we get

Theorem 5 (The S5n theorem) Let δ be an S5n satisfiable canonical formula. Then kforget S5n (δ↪ p) ⌘ δp .

Proof: Let k = dep(δ). Here, we only verify that M↪ s ♣= δ when k ≥ 1. We prove by induction on k - l that for any l  k, M↪ s ♣= δ#l still holds. Base case. M↪ s ♣= w(δ), which is δ#k . Induction case. Suppose that M↪ s ♣= δ#l . To show that M↪ s ♣= δ#l-1 , it suffices to show that for each i 2 A, M↪ s ♣= riRi(δ#l-1 ), i.e., (M↪Ri(s)) is Ri(δ#l-1 )- complete. Here, we only prove that for every t 2 Ri(s), there exists ⌘ 2 Ri(δ#l-1 ) s.t. M↪ t ♣= ⌘. The other direction can be similarly proved.

Suppose that t = s. By the reflexive property, δ#l 2 Ri(δ#l-1 ). Let ⌘ = δ#l . This, together with the hypothesis, imply that M↪ s ♣= ⌘ where ⌘ 2 Ri(δ#l-1 ).

Suppose that t 2 S ∩ ¶s♦. Before adding the edges, by construction, there exists δi 2 Ri(δ) s.t. M↪ t ♣= δi. Let ⌘ = δ#l-1 i . After adding the edges, that M↪ t ♣= w(⌘)^Vj2A∩¶i♦ rjRj(⌘) holds. Now, we prove that M↪ t ♣= riRi(⌘), i.e., (M↪Ri(t)) is Ri(⌘)-complete. By transitive and Euclidean properties, we get Ri(t) = Ri(s). By the identical children property, Ri(⌘) = Ri(δ#l ). These, together with the hypothesis, imply that M↪ t ♣= riRi(⌘).

As a corollary of Theorems 2-5, we get Corollary 3 Tn, K45n, KD45n and S5n are closed under forgetting.

By Proposition 8 and Corollary 3, we can get the next corollary which settles the open problems regarding uniform interpolation in multi-agent modal logics.

Corollary 4 Tn, K45n, KD45n and S5n do have uniform interpolation.

5 Conclusions

In this paper, we have studied forgetting in multi-agent modal logics. We adopted the semantic definition of existential bisimulation quantifiers as that of forgetting. We showed that except the two modal systems K4n and S4n, which have been shown lack of uniform interpolation, the other main multiagent modal systems, namely Kn, Dn, Tn, K45n, KD45n, and S5n, are closed under forgetting.

To achieve the above results, we presented a syntactical method of forgetting: to forget an atom from an arbitrary modal formula, first transform the formula to a disjunction of canonical formulas, then remove all the unsatisfiable ones, and lastly substitute any literal of the atom with >. To prove that this syntactical method of forgetting produces the desired result, given a model satisfying the formula obtained from a satisfiable canonical formula via literal elimination, we construct a model satisfying the original formula and p-similar to the given model. To this end, we analyze properties of satisfiable canonical formulas in different logics, and use multipointed models to gain flexibility in model construction.

In multi-agent systems, background information is formalized as common knowledge of propositional formulas. We have also shown that the extensions of the above logics with propositional common knowledge are closed under forgetting. These results were omitted for lack of space.

It is well-known that the size of a canonical formula is nonelementary. So the proposed syntactic method of forgetting is obviously an unpractical one. Thus one topic for future research is to investigate more efficient approaches for computing forgetting. Yet another one is to explore forgetting for distributed knowledge and more general cases of common knowledge. It would also be interesting to apply forgetting to progression and abductive reasoning of knowledge and belief in multi-agent systems.

Acknowledgments

Liangda Fang and Yongmei Liu acknowledge support from the Natural Science Foundation of China under Grant Nos. 61572535 and 61573386. Hans van Ditmarsch acknowledges support from ERC project EPS313360. He is also affiliated to IMSc (Institute of Mathematical Sciences), Chennai, India, and to Zhejiang University, China.