Multi-Agent Only Knowing on Planet Kripke

1 Introduction

Suppose a modeler were to provide a collection of logical sentences � as a knowledge base to characterize an agent. One would expect that the beliefs of the agent would be exactly those that follow from � : 1 However, in classical epistemic logic [Fagin et al., 1995], K� does not preclude K(� ^ �) from holding in general. So unless � carefully includes both the beliefs and non-beliefs of the agent, it is not the case the K� can succinctly characterize all the beliefs of the agent.

In this regard, the idea of only knowing is a natural and intuitive notion to precisely capture the beliefs of a knowledge base. First introduced by Levesque [1990], it enriches classical epistemic logic with a new operator O, the idea being Op holds precisely when the worlds considered possible by the agent are all and only those where p holds. So, Op � Kp and more interestingly, Op � :Kq. For knowledge-based agents,

� Partially funded by the FWO project on Data Cleaning and KU Leuven's GOA on Declarative Modeling for Mining and Learning.

1 In this work, we do not di�erentiate between "knowledge" and "belief", and use these terms interchangeably.

Vaishak Belle �

Dept. of Computer Science KU Leuven Leuven, Belgium vaishak@cs.kuleuven.be

in particular, this seems like the right kind of modality to include in our language. And indeed, it is very closely related to important concepts such as minimal knowledge [Halpern and Moses, 1984]. The main di�erence being that the logic of only knowing includes the O modality in the language, whereas in [Halpern and Moses, 1984], knowledge minimization is purely a meta-theoretic concept; so, only knowing has some advantages.

Somewhat surprisingly, extending only knowing's simple semantics to the many agent case has been far from straightforward. Independently, Halpern [1993] and Lakemeyer [1993] attempted extensions, but these were shown to exhibit unintuitive properties [Halpern and Lakemeyer, 2001]. In later work, Halpern and Lakemeyer [2001] do manage to capture only knowing, but by appealing to prooftheoretic constructs such as canonical models in the semantics. (Canonical models, moreover, which are based on sets of maximally consistent sets of formulas, are also perhaps not realizable in practice.) The approach of Waaler and Solhaug [2005] was based on model-theoretic constraints, which as the authors admit, "is complex and hard to penetrate". Finally, in more recent work, Belle and Lakemeyer [2010] show how the proof-theoretic construction of [Halpern and Lakemeyer, 2001] can be avoided to naturally capture multi-agent only knowing, but at the cost of introducing a semantics that significantly deviates from the classical (that is, Kripke) account.

The purpose of this paper is to revisit the notion of multiagent only knowing, but to phrase the truth conditions in terms of the usual Kripke framework in a natural way, that is, by avoiding canonical models and other proof-theoretic machinery. There are several reasons why this is being attempted. Formulating the account in a more familiar truth theory has the advantage that deep results known in other areas of modal logic can finally be put in the context of only knowing. Indeed, as one would observe, the basis for our reconstruction is Moss' investigation into normal forms [Moss, 2007], which itself is inspired by and builds on the seminal work of Fine [1975]. Second, we show how the multi-agent only knowing modality developed here can be expressed in terms of the cover modality [D'Agostino and Lenzi, 2005], which is intimately connected to co-algebras and their role in central results on modal logic, such as interpolation and Beth definability. In the longer term, a multi-agent only knowing framework in classical modal logic would be more accessible for dynamic epistemic logic based knowledge representation languages [Demolombe, 2003; Herzig et al., 2000; van Ditmarsch et al., 2011]. In sum, only knowing is arguably an essential companion to the classical knowledge operator in AI applications, and the work considered here would allow modal logicians to use it more readily.

The paper is organized as follows. In Section 2, we recall the essentials of epistemic logic and characteristic formulas, as introduced by Moss, together with some related results used in the sequel. Then, in Section 3, we define our logic with our specific truth conditions for the multi-agent only knowing connectives which use the characteristic formulas. In Section 4, we compare and relate formally our logic and our definition of multi-agent only knowing with the recent approach proposed by Belle and Lakemeyer [2010]. In Section 5, we present the cover modality and establish formally its connection with our multi-agent only knowing modality. This allows us in Section 6 to axiomatize the validities of our logic once it is extended with the cover modality. We discuss other related e�orts in Section 7 before concluding.

2 Preliminaries

In this section, we first recall the basics of epistemic logic. Then, we introduce the characteristic formulas for modal logic as defined by Moss and recall a number of results about these formulas that will be used in the rest of the article.

2.1 Epistemic Logic

In the rest of the paper, P is a set of propositional letters called atomic facts and A is a finite set whose elements are called agents.

Definition 1 (Language L). We define the language L inductively as follows.

where G � A, j 2 A and p 2 P. In the sequel, we use the following abbreviations:

Let ' 2 L. The modal depth of ', denoted d('), is defined inductively as follows: d(p) = 0; d(' ^ ) = maxfd('); d( )g; d(:') = d('); d(Kj') = d(') + 1 and d(CG') = d(') + 1. The set of propositional letters appearing in ' is denoted P(').

The formula Kj' reads as "agent j Knows '". Dually, the formula b Kj' reads as "agent j considers it possible that ' holds". The formula EG' reads as "everybody in group G knows that ' holds". Common knowledge of ' means that everybody knows that ' but also that everybody knows that everybody knows ', that everybody knows that everybody knows that everybody knows ', and so on ad infinitum. Formally, this corresponds to the following formula CG' := EG'^EGEG'^EGEGEG'^ : : : ; and is infinitary in nature. But as we do not allow infinite conjunction, the common knowledge operator is introduced as a primitive connective in our language.

PL Axioms and Inference Rules of Prop. Logic

Figure 1: Proof System L for L

A (pointed) epistemic model (M; w) represents how the actual world represented by w is perceived by the agents. Atomic facts are used to state properties of this actual world.

Definition 2 (Epistemic model). An epistemic model is a tuple M = (W; R; V) where:

• � W is a non-empty set of possible worlds,
• � R : G ! 2 W�W is a function assigning to each agent j 2 G an accessibility relation on W,
• � V : � ! 2 W is a function assigning to each propositional letter of � a subset of W. V is called a valuation.

We write w 2 M for w 2 W, and (M; w) is called a pointed epistemic model (w often represents the actual world). If w; v 2 W, we write wRjv for R( j)(w; v). Finally, we write

Intuitively, in the definition above, v 2 Rj(w) means that at w; the agent j believes that v might be the real world.

The truth conditions of Kj' are defined in such a way that Kj' holds in a possible world when ' holds in all the worlds agent j considers possible.

Definition 3 (Truth conditions). Let M be an epistemic model, w 2 M and ' 2 L. Then, M; w j= ' is defined inductively as follows:

M; w j= p i� w 2 V(p)

M; w j= :' i� M; w6 j= '

M; w j= ' ^ i� M; w j= ' and M; w j=

M; w j= Kj' i� for all v 2 Rj(w); we have M; v j= '

M; w j= CG' i� for all v 2 RG(w); we have M; v j= '

We write M j= ' when M; w j= ' for all w 2 M, and j= ' when for all epistemic models M, M j= '. In that latter case, we say that ' is L-valid.

The following theorem shows that the set of validities of L can be axiomatized by the proof system L.

Theorem 1. The proof system L for L defined in Figure 1 is sound and strongly complete for L w.r.t. the class of epistemic models.

2.2 Characteristic Formulas

We will resort in our definitions and proofs to particular kinds of modal formulas which capture the structure of epistemic models (modulo bisimulation) up to a given modal depth. These formulas were defined by Moss [2007] and are very similar to the normal forms for modal logic as introduced by Fine [1975]. 2

In what follows, we use S and E, possibly decorated with superscripts and subscripts, to denote sets of formulas. The subscripts refer to constructions using inductive definitions. When the superscript is an agent index j or the group G; it means that the formulas in the set are in the context of Kj and CG respectively.

Definition 4. [Moss, 2007] Let P � P be finite. We inductively define the sets E P n as follows:

An element � of E P n with n > 0 will often be written as follows (note that the S j n are replaced by R j(�) and the S G n are replaced by RG(�)):

Basically, a characteristic formula �n+1 provides a complete syntactic representation of a pointed epistemic model up to modal depth n + 1. So, intuitively, if we view a characteristic formula �n+1 of E P n+1 as the syntactic representation up to modal depth n + 1 of a possible world w where it holds, a formula �n of S j n can also be viewed as a syntactic representation up to modal depth n of a possible world accessible by R j from w.

The following proposition not only tells us that a formula �n completely characterizes the structure up to modal depth n of any pointed epistemic model where it holds (first item), but also that the structure of any epistemic model up to modal depth n can be characterized by such a �n (second item).

Proposition 1. [Moss, 2007] Let P � P be finite, let n 2 N and let � 2 E P n . Let ' 2 L such that d(') � n and P(') � P.

2 Halpern and Lakemeyer [2001] discuss a similar normal form in the context of only knowing.

Then, the following hold:

The following corollary is also used in the sequel. It states that any formula can be reduced to a disjunction of �s. (Thus, they are referred to as normal forms.) The decomposition of a formula ' into �s syntactically (and precisely) captures the relevant structure of the set of pointed epistemic models which make ' true. Put di�erently, each � can be seen as a syntactic description of the modal structure (up to depth n and modulo bisimulation) of a pointed epistemic model which makes ' true.

Corollary 1. Let ' 2 L and let k 2 N. Let P := P(') and let n = d(') + k. Then, there is S ' n = f� 1 n ; : : : ; � m n g � E P n such that

Moreover, for each n, this set S ' n is unique.

3 DefiningMulti-Agent Only Knowing

We define our logic for multi-agent only knowing in two steps. First, we define a language where we cannot nest the multi-agent only knowing connectives. Then, we generalize it to allow for an arbitrary nesting of these connectives.

3.1 AConstrained Logic

The class of models for our first logic is the class of epistemic models. Only the syntax of the logical language and the truth conditions change, because the language is extended with only knowing operators. Our first language is in fact an extension of the language ONL � n of Belle and Lakemeyer [2010], in the sense that no connector O k j or O k G may occur in the scope of a Kj, a O k j or a O k G .

Definition 5 (Language L O G� ). We define the languages L O G� inductively as follows.

where 2 L, k 2 N, G � Agt, j 2 A, and p 2 P. The formulas Oj' and OG' are abbreviations for O 0 j ' and O 0 G ' respectively.

The formula O k j reads "the agent j only believes (knows) up to degree k" and the formula O k G reads "the group of agents G only believes (knows) up to degree k".

Definition 6 (Truth conditions for L O G� ). The satisfaction relation j= between pointed epistemic models and formulas of L O G� is defined inductively as follows. The basic case as well as the cases for the connectives :; ^; Kj and CG are defined like in Definition 3. We only define the cases for O k j and O k G . Let M be an epistemic model, w 2 M and let 2 L. Let n = k + d( ) and let X 2 A[ 2 A . Then,

We recall that the finite set S n = f�1; : : : ; �mg � E P n (where P = P( )) is such that j= $ _ �2S n �.

Let ' 2 L O G� . We write M j= ' when M; w j= ' for all w 2 M, and j= ' when for all epistemic models M, M j= '.

The intuition underlying our definition of the truth condition for our multi-agent only knowing operator can be explained as follows. As noted in the previous section, each � of S n can be seen as a syntactic description of the modal structure (up to depth n and modulo bisimulation) of a pointed epistemic model which makes true. So, the agent (or the group of agents) only knows if she considers possible all and only the possible worlds that make true, disregarding the structure of these worlds after a certain depth k: the bigger k is, the more entrenched this knowledge will be. Note that if we restrict our setting to the propositional case with a single agent, then we recover the original definition of only knowing as defined by Levesque [1990].

Importantly, note that we do not need to resort to an operator Nj' like in the usual definitions of multi-agent only knowing. Instead, we refer in the semantics to characteristic formulas and our only knowing operator is introduced here as a primitive connective.

Example 1. One would think that this constrained language is little more than the single agent version, that is, formulas such as Oi p � :Kiq are the only interesting valid sentences in this logic. In fact, this language can be used to capture multiagent autoepistemic defaults [Lakemeyer, 1993]. 3 Suppose p denotes a secret, and consider the default assumption that if i has no knowledge of j knowing the secret, then it is the case that j does not know it. Let � = :KiKj p � :Kj p:

It can now be shown that if � is the only formula that i only knows, then, Oi� � Ki:Kj p is a valid sentence. That is, i actually believes that j does not know p: Note, for example, adding objective knowledge to i's knowledge does not change his conclusion, that is, j= Oi(p ^ �) � Ki:Kj p. Of course, if i where to believe that j indeed knows p, this conclusion is now retracted: j= Oi(p ^ � ^ Kj p) � KiKj p.

3.2 A Logic of Multi-Agent Only Knowing

As in the logic of the previous section, the class of models is again the class of (pointed) epistemic models. Only the syntax of the logical language changes, the satisfaction relation and the class of models remains the same as before. The syntax of this full language is, in fact, an extension of the language ONLn of Belle and Lakemeyer [2010]. Like for ONLn, we also allow an arbitrary nesting of the connectors Kj, O k j and O k G .

3 Levesque [1990] had previously shown that only knowing a subjective formula can capture such defaults in the single agent case.

Definition 7 (Languages L O G and L O ). The language L O G is defined inductively as follows.

where k 2 N, G � Agt, j 2 A and p 2 P. The formulas Oj' and OG' are abbreviations for O 0 j ' and O 0 G ' respectively. We define the language L O as the language L O G without the group connectives CG and O k G .

Proposition 2. Let k 2 N and 2 L. Let P := P( ) and n = d( )+k. Then by Corollary 1, there is S n = f� 1 n ; : : : ; � m n g � E P n such that j= $ _ �n2S n �n. Then, we have that the following

holds:

and

Proof. It follows straightforwardly from the truth conditions for O k j and O k G . qed

Corollary 2. Let k 2 N and ' 2 L O G . Let P := P(') and n = d(') + k. Then, there is S ' n = f� 1 n ; : : : ; � m n g � E P n such that

Moreover, for each n, this set S ' n is unique.

Proof. The proof is by induction on the nesting depth n of operators O k j and O k G . The base case n = 0 holds trivially by definition. The induction step is proved by applying Proposition 2: the right-hand sides of Expressions (1) and (2) do not contain operators O k j and O k G . qed

Definition 8 (Truth conditions for L O G ). The truth conditions are exactly the same as in Definition 6. When j= ' holds for some ' 2 L O G , we say that ' is L O -valid.

Example 2. With the enriched language, we can handle entailments of the sort:

That is, if i believes p and also believes j to only know q, he not only knows that j knows q (as in classical epistemic logic) but also knows that j does not know p (a property of only knowing).

As an extension to our previous example, suppose � says that if i does not believe p is the only thing that j knows then it is the case that j knows more. That is,

We can then show that Oi� � Ki:Oj p is a valid sentence, that is, i believes that j knows more than p:

Given the reading of our graded multi-agent only knowing operator, we have the following expected result, which is the counterpart of [Belle and Lakemeyer, 2010, Theorem 5]: if an agent (or a group of agents) only knows that ' holds up to a certain degree, then she also only knows it up to a lower degree.

Proposition 3. Let m; n 2 N such that n � m and let ' 2 L O G . Let j 2 A and G � A. Then, the following holds:

Proof. The proof follows the same lines as the proof of [Belle and Lakemeyer, 2010, Theorem 5]. Let (M; v) be a pointed epistemic model. First, one should observe that for all �m 2 E P m , there is �n 2 S �m n such that M; v j= �n if, and only if, M; v j= �m (this �n depends on the structure of (M; v) beyond modal depth m). Vice versa, for all �n 2 E P n , there is �m 2 E P m such that M; v j= �n if, and only if, M; v j= �m (this �n does not depend on the structure of (M; v) beyond modal depth m). From this observation and by examining the truth conditions of Definition 6, we conclude easily that our two implications hold. qed

However, the reverse implications in Proposition 3 do not hold necessarily, because of the dependence on the structure of (M; v) in the first case. We now explore the relation to the Belle and Lakemeyer scheme in more detail in the next section.

4 Relation to Belle and Lakemeyer

First, we recall the essentials of the approach of Belle and Lakemeyer [2010]. They do not consider only knowing operators dealing with groups of agents and do not consider degrees of only knowing as we do. Moreover, and without loss of generality, we assume that there are only two agents: A := fa; bg, as in [Belle and Lakemeyer, 2010]. Then, we consider the fragment ONL O n of the language L O G defined as follows:

Definition 9 (Languages ONLn and ONL O n ). The language ONLn is defined inductively as follows:

where p 2 P and j 2 A. The formula Oj' is an abbreviation for Kj' ^ Nj:'. The language with the connectives :; ^; Kj and Oj (instead of Nj) is denoted ONL O n .

The semantics of Belle and Lakemeyer [2010] is based on the notion of k-structures. We consider a non-empty set of possible worlds W which simply consists of all the propositional valuations for the propositional letters in P. A kstructure (k � 1), say e k , for an agent is defined inductively as follows:

• � e 1 �W� ffgg,
• � e k �W� E k�1 , where E m is the set of all m-structures.

A e 1 for a, denoted as e 1 a , is intended to represent a set of worlds f(w; fg); : : :g. A e 2 is of the form f(w; e 1 b ); (w 0 ; e 01 b ); : : :g, and it is to be read as "at w, a believes b considers worlds from e 1 b possible but at w 0 , a believes b to consider worlds from e 01 b possible". This conveys the idea that a has only partial information about b, and so at di�erent worlds, a believes di�erent things about b.

We define a e k for a, a e j for b and a world w 2 W as a (k; j)-model (e k a ; e j b ; w). Only formulas of a maximal a-depth of k, and a maximal b-depth of j are interpreted w.r.t. a (k; j)- model. (See [Belle and Lakemeyer, 2010] for more details on these notions; definitions are not reproduced here.) The truth conditions are defined as follows:

With these definitions and our abbreviations, we have that

We say that a formula ' 2 ONL O n is BL-valid when it is valid in the sense of Belle and Lakemeyer [2010], that is when it is true in all (k; j)-models, if ' is of a-depth k and b-depth j.

We now show that the set of BL-validities for the language ONL O n is the same as the set of validities in our logic L O .

Lemma 1. Let ' 2 ONL O n be a formula of a-depth k and of b-depth j. Then, for all (k; j)-models (e k a ; e j b ; w), there is a pointed epistemic model (M; w) such that e k a ; e j b ; w j= ' if, and only if, M; w j= '. Vice versa, for all pointed epistemic models (M; w), there is a (k; j)-model (e k a ; e j b ; w) such that e k a ; e j b ; w j= ' if, and only if, M; w j= '.

Proof. For the first part, the worlds of M are w and all the k 0 - structures and the j 0 -structures present in e k a and e j b . The valuations and the accessibility relations for these worlds are defined canonically. For the second part, we unravel the pointed epistemic model (M; w) up to modal depth k for the worlds accessible from w by a and up to modal depth j for the worlds accessible fromw by b (see [Blackburn et al., 2001]). qed

Theorem2. A formula ' 2 ONL O n is L O -valid if, and only if, it is BL-valid.

Proof. It follows from the previous Lemma 1. qed

Note that, unlike the approach of Belle and Lakemeyer [2010], we can simultaneously satisfy an infinite set of sentences of unbounded modal depth.

5 The Cover Modality

The cover modality r has been used as a syntactic primitive in modal logics [D'Agostino and Lenzi, 2005]. It has recently been axiomatized [Bılkov´a et al., 2008]. Here, we define a multi-modal version of this cover logic.

Definition 10 (Language Lr). The language Lr is defined inductively as follows.

where j 2 A and p 2 P. Moreover, we use the following abbreviations: Kj' := rj; _ rjf'g.

Definition 11 (Truth conditions for Lr). The satisfaction relation j= is defined like in Definition 6 for the base case and for the connectives : and ^. For the cover modalities, the truth conditions are defined as follows:

for all v 2 Rj(w) there is i 2 f1; : : : ;mg such that M; v j= 'i ; and for all i 2 f1; : : : ;mg there is v 2 Rj(w)

such that M; v j= 'i :

Note that j= b Kj' $ rjf>; 'g. Likewise, we can define our multi-agent only knowing modalities O k j with the cover modality as follows.

Proposition 4 (Expressiveness of the cover modality). Let ' 2 L O G and k 2 N. Let P := P(') and n = d(') + k. Then for all pointed epistemic model (M; w), we have that the following holds: for any j 2 A,

Proof. It follows straightforwardly from the truth conditions of the multi-agent only knowing operators O k j and O k G given in Definition 6. qed

The above proposition shows that Lr is at least as expressive as L O on the class of epistemic models. Therefore:

Theorem 3 (Decidability of L O ). Let ' 2 L O . The problem of determining whether ' is L O -valid is decidable.

Proof. The proof follows from the fact that Lr is at least as expressive as L O on the class of epistemic models by Proposition 4 and the fact that the validity problem of Lr is decidable, as shown by Bılkov´a et al. [2008]. qed

6 Proof System

To define the proof system for Lr, we need to introduce some further notations. Typically, formulas of Lr are denoted '; ; : : :, finite sets of formulas are denoted �; �; : : : and sets of sets of formulas are denoted A; B; : : :

We define the (power set) lifting of the relation 2� Lr�2 Lr as the relation 2 � 2 Lr � 2 2 Lr given by �2A if, and only if, for all ' 2 �, there is � 2 A such that ' 2 �, and for all � 2 A, there is ' 2 � such that ' 2 �.

Let E be a non-empty set. An object A 2 2 2 E is a redistribution of a set B 2 2 2 E if �2A for all � 2 B (hence in particular [ B � [ A). We call such a redistribution slim if moreover [ B = [ A. The set of all slim redistributions of A is denoted by S RD(A).

• (r0) Axioms and Inference Rules of Prop. Logic
• (r1) If 8' 2 �; 9 2 � such that ' ! ; and 8 2 �; 9' 2 � such that ' !
• then r j� ! r j�

Figure 2: Proof System Lr for Lr

Theorem 4. [Bılkov´a et al., 2008] The proof system Lr defined in Figure 2 is sound and strongly complete for Lr w.r.t. the class of epistemic models.

We are going to extend the language of Lr in order to include explicitly the only knowing operator that we introduced in Section 3. Since this modality is definable in terms of the cover modality by Proposition 4, we straightforwardly obtain an axiomatization of this extended language.

Definition 12 (Language L O r ). The language L O r is defined inductively as follows.

where 2 L O , k 2 N, j 2 A and p 2 P. Moreover, we use the following abbreviation: Kj' := rj; _ rjf'g.

The truth conditions are defined like in Definition 3 for the base case and for the connectives : and ^. For the cover modalities, the truth conditions are defined like in Definition 11, and for the multi-agent only knowing modality the truth conditions are defined like in Definition 6.

Theorem 5. The proof system L O r is the proof system Lr of Figure 2 to which we add the following inference rule: for all j 2 A, for all ' 2 L O , for all k 2 N,

where n := d(') + k and P := P(').

Then, the proof system L O r is sound and strongly complete for L O r w.r.t. the class of epistemic models.

Proof. The proof of soundness is standard. Completeness is obtained by observing that Theorem 4 gives us completeness for the language Lr without the multi-agent only knowing modality. Then, we obtain completeness for the full language L O r because the multi-agent only knowing modality is definable in terms of the cover modality by Proposition 4 and this definition corresponds in fact to our inference rule (O k j ). qed

The language L O r is an extension of the language L O of Section 3 with the cover modality. From Theorem 5, we obtain a soundness and completeness result for this restricted language L O :

Corollary 3. Let ' 2 L O . Then, ' is derivable in the proof system L O r if, and only if, ' is L O -valid.

7 Other RelatedWork

Besides the immediately relevant work already discussed above, let us note the following related e�orts.

Minimal knowledge approaches have also enjoyed multiagent extensions [Hoek and Thijsse, 2002]. While minimal knowledge is related to only knowing, it di�ers in the sort of conclusions one can draw. We refer readers to [Levesque and Lakemeyer, 2001] for discussions. A related proposal is that of total knowledge [Pratt-Hartmann, 2000], where knowledge is required to be true. So defaults, for example, would lead to an inconsistency.

Although defaults are not the focus of this paper, there are also proposals that study the interaction between knowledge and defaults in a multi-agent setting, such as [Morgenstern, 1990]. In terms of proof theory, Bonatti and Olivetti [2002], among others, have developed proof systems for such defaults. The relation between concepts like only knowing and this work, however, remains to be explored.

Finally, there are numerous modal logics for multi-agent systems for concepts such as beliefs, dynamics, and desires, which we do not review here. See [van der Hoek and Wooldridge, 2012; Fagin et al., 1995] and references therein. Only knowing is not considered by these, however.

8 Conclusion

We investigated a new version of multi-agent only knowing in the classical Kripke setting, while putting it in context of existing proposals on this topic. This comes with a number of benefits - for example, the definability with the cover modality, a group version of multi-agent only knowing, and an operator for assessing the epistemic entrenchment of what an agent or a group only knows - while avoiding proof-theoretic constructions.

At this point, the development of this paper could lead to dynamic logic based representation formalisms such as [van Ditmarsch et al., 2011] finally embracing the only knowing modality in a multi-agent and dynamic setting. These formalisms are also based on a Kripke semantics.