A Model-Theoretic Analysis of Monotonic Knowledge

1. Introduction

Planning sequences of actions and reasoning about their effects is one of the most thoroughly studied areas in AI. Realistic planning requires, however, not only the ability to reason about the real world, but also the ability of the planning agent to reason about the infor­ mation it has about the real world. In other words, intelligent agents need to be able to reason about their own knowledge as well as other agents' knowledge. (Planning, in fact , requires a theory of knowledge and action. See [Mo80], [Mo84).)

A theory of knowledge requires a robust mathematical model of knowledge. Starting with Hintikka [Hi62], knowledge was tradition­ ally modelled by Kripke structures [Kr63) (e.g. , [Mo80, Mo84, MSHI78, Sa76)). More recently, however, the adequacy of Kripke structures to model propositional attitudes, and in particular epistemic attitudes, has been questioned on several grounds [FHV84,FV84). Fagin et a!. introduced modal structures [FV841, called knowledge structures when applied to knowledge [FHV84 , which captures Hintikka's possible worlds semantics in a set-theoretic way, rather then a graph-theoretic way as in Kripke structures. It turns out that modal structures not only a fortiori justify the use of Kripke structures to model possible worlds, but they also enable a much more refined analysis of several notions [FHV84,FV84). We shall use modal structure in our model-theoretic analysis of knowledge.

It is well known that there is not really such a thing as the con­ cept of knowledge, but rather a whole continuum of "concepts of knowledge" (cf. [Le78,0C68)) . Fagin et a!. [FHV84) chose to use a notion of knowledge where the agents are logically omniscient, i.e., they know all the consequences of their knowledge, and are fully introspective , they are both positively introspective (aware of their knowledge) and negatively introspective (aware of their ignorance). One way to explain the logical omniscience of these agents is to view their knowledge as implicit, i.e., the agents implicitly know every­ thing that logically follows from their explicit knowledge [HM84a,Le84,RP85). From this point of view, however, it is hard to justify the assumption that the agents have negative introspection.

The above argument motivates a model-theoretic study of a notion of positively introspective knowledge, where the agents are introspective of their knowledge but not of their ignorance. Such a concept of knowledge was advocated, on other grounds, by Hintikka [Hi62) and Moore [Mo84). A fully introspective knowledge is non­ monotonic, since ignorance leads to knowledge (by introspection). This lead to several difficulties in trying to circumscribe this kind of knowledge ( cf. [HM84b,Pa84,St81)). In contrast, the concept of knowledge studied here is monotonic. In terms of modal logic, fully introspective knowledge correspond to the modal logic S5, while posi­ tively introspective knowledge correspond to the modal logic S4.

Our treatment here of positively introspective knowledge closely resemble the treatment of fully introspective knowledge in [FHV84). Nevertheless, there are several significant differences, upon which we elaborate in the paper. The most important point is that

A MODEL-THEORETIC ANALYSIS OF MONOTONIC KNOWLEDGE

Moshe Y. Vardi

CSLI, Ventura Hall Stanford University Stanford, CA 94305, USA

in our framework we can study comparative knowledge and cir­ cumscribed knowledge. Our framework enables us to assign precise meaning to the notion of "to know more", which in turn enables us to circumscribe knowledge, i.e., to assign precise meaning to the notion of "all one knows".

2. Knowledge Structures

We now define knowledge structures that capture the essence of Hintikka's [Hi62) possible worlds approach towards modelling knowledge.

Before we formally define knowledge structures, let us discuss them informally. The basic idea underlying knowledge structures is that there are different levels of knowledge. Consider the following example, taken from [FHV84). Assume there are two agents, Alice and Bob, and that there is only one atomic proposition p. At the Oth level ("nature"), assume that p is true. The 1st level tells each player's knowledge about nature. For example, Alice's knowledge at the 1st level could be "I (Alice) don't know whether p is true or false" and Bob's could be "I (Bob) know that pis true". The 2nd level 'tells each player's knowledge about the other player's knowledge about nature. For example, Alice's knowledge at the 2nd level could be "I know that I don't know about p, but I know that Bob knows whether p is true or false" , and Bob's could be "I know that I know p, but I don't know whether Alice knows p". Thus, Alice knows that either p is true and Bob knows it, or else p is false and Bob knows it . At the 3rd level, Alice's knowledge could be "I know that Bob does not know whether I know about p". This can continue for arbitrarily many levels.

We assume a fixed finite set P of atomic propositions, and a fixed finite set A of agents. Intuitively, a knowledge structure has various levels, where the Oth level is a truth assignment to the atomic propositions, and where the kth level contains a set of "possible" /c­ ary worlds for each agent. Formally, we define a Oth-order assign­ ment, f 0 , to be a truth assignment to the atomic propositions. We call <fo> a 1-ary world (since its "length" is 1). Assume induc­ tively that /c-ary worlds <fo, ... ,!,._1> have been defined. Let Wk be the set of all k-ary worlds. A kth-order assignment is a function fk:A-+PowerSet( Wk) · Intuitively, fk associates with each agent a set of "possible" /c-ary worlds. There is a "compatibility" restriction on fk's, which we shall discuss shortly . We call <fo, ... ,fk> a ( k+ 1 )-ary world. An infinite sequence <f0,fl,h, ... > is called a knowledge structure if each prefix <f0, ··· ,/,._1> is a /c-ary world for each k.

Before we list the restriction that we mentioned, let us recon­ sider the above example. In that exam£Le, fo is the truth assignment that makes p true. Also, fi(Alice)={p,p} (where by p (respectively, ii} we mean the 1-ary world <fo> where fo is the truth assignment that makes e._ true (respectively, false)), and fi(Bob)={p} . Saying f 1 (Alice)={p,p} means that Alice does not know whether pis true or false. We can write the 2-ary world <fo,h> ss <p, (Alice-+{p,P}, Bob-+{p})>. _l,et us denote this 2-a!1 world by w1. Let w 2 b~ the 2-ary world <p, (Alice-+{p,P},Bob-+{p})>, Jet W:! be <p,_i.Alice-+{cl,Bob .. {p})> , Jet W4 be <P. (Alice-+{p},Bob-+{ii})>. In the example above h{Alice)={ w1,~.w3,w4}, since Alice thinks bot~ w1 (where p is tr~e, Bob knows it, but she does not), w2 (where p 1s false, Bob knows 1t, but she does not), w 3 (where p is true, Bob knows it, and she knows it), and w 4 (where p is false, Bob knows it, and she knows it), are possible worlds. Similarly, h(Bob)={wl>UJ:!} , since Bob thinks both w 1 (where p is true, he knows it, but Alice does not know it) and W:! (where pis true, he knows it, and Alice knows it) are possible worlds.

The restriction that we mentioned earlier, is:

(Kl) <go, ... ,g,...2>Ek..1(a) iff there is a (k- 1)st-order assignment g,_1 such that <go, ... ,gk_2,g,...1>Ef,(a), for aEA and I<k.

This restriction says that the (k-1)-ary worlds that agent a thinks are possible are prefixes of the k-ary worlds that a thinks are possible. That is, a's higher-order knowledge extends a's lower-order knowledge.

Restriction K1 is not really particular to knowledge and actu­ ally applies to any normal modality [FV84]. Indeed, the structures that we have defined so far are exactly the modal structures of Fagin and Vardi [FV84]. Since we are trying to model knowledge, we have to impose certain semantic restrictions on these structures in order to

capture the properties of knowledge that we have in mind. The pro­ perties of knowledge in which we are interested are those relevant to planning and acting.

The first property that we are trying to capture is that knowledge is always correct, i.e. , anything that someone knows is true. While it is possible to have false beliefs, it is impossible to have false knowledge. The reason that this distinction is important to planning and acting is simply that, for an agent to achieve her goals, the beliefs on which she bases her actions must generally be true. To capture this property we impose the following restriction on worlds [FHV84]:

(K2) </0, ... ,/,...1> E/,( a), for aEA and k;::: 1.

That is, the real k-ary world is one of the possibilities for each agent .

The second property of knowledge that is important to plan­ ning is that, if an agent knows something, then she knows that she knows it. That is, the agents are aware of their knowledge. We call this positive introspection. This property is important for reasoning about plans that requires gathering information or plans that consists of several actions [Mo84]. To capture this property we impose the following restriction on worlds:

(K3) If <g0, . · ,g,...1>Eg,(a), then gk_ 1(a)~J,...1 (a), for aEA and k>l.

Let us see why this captures positive introspection. Knowledge is captured in our model by sets of possibilities. The more possibilities an agent has, the less she knows. Since an agent knows what she knows but does not necessarily know what she does not know, it is conceivable to her that she knows more than she is aware of. Thus if w=<fo, ... ,/,...1> represents the actual state of knowledge, then vJ =< g 0 , ·.. ,g,_ 1 > is a conceivable possibility for a with respect tow only if g,_1(a)~/,_1(a) . Thus if vJ =<g0, .. . ,g,...1> is one of a's possibile worlds, then vJ must be conceivable to her with respect to w, i.e., gk_1( a)~fk-1( a).

The last property of knowledge that we consider is that if an agent does not know something, then she knows that she does not know it. That is, the agents are aware of their ignorance. We call this negative introspection. This property is philosophically contr­ oversial (see [Le78]), and was rejected by Hintikka [Hi62] and Moore [Mo84]. We also reject it here but on different grounds.

In every model of knowledge in which knowledge is captured by a set of possibilities, the agent turns out to be logically omniscient [Hi75J. This is because these models satisfy the following formula, where K.¢> means that a knows ¢>:

K.pf\K.(p"Jq)"JK.q

Namely, the agents know all the consequences of their knowledge. This is of course unrealistic, not only for humans but for any physi­ cal agent. One way to explain the logical omniscience of these agents is to view their knowledge as implicit rather than explicit, i.e., an agents implicitly knows all the consequences of her explicit knowledge [HM84a, Le84, Re74, RP85]. The following analysis shows that an agent is implicitly aware of her implict knowledge: Suppose she explicitly knows p and p"J q, so she implicitly knows q. Then she explicitly knows that she knows p and she explicitly knows that she knows p"J q, and therefore she implicitly knows that she knows q. On the other hand, there is no reason to accept that an agent is implictly aware of her ignorance. Thus we also reject negative introspection.

We note that another approach to the logical omniscience prob­ lem is to consider the agents as idealized [Mo84]. In that case, we believe that it does make sense to accept negative introspection. Indeed, Fagin et a!. [FHV84] did accept negative introspection, and they captured full introspection by the following restriction:

(K3') If <g 0 , ·· ,g,... 1 >Eg,(a), then g,_1(a)=/,...1(a), for aEA and k>l.

That is, in all the worlds that an agent thinks possible she has exactly the same knowledge as in the real world.

Notice that the only difference between K3 and K3' is that the inclusion is replaced by an equality. As we shall see later this subtle difference carries substantial implication. We call knowledge struc­ tures that satisfy K3' fully introspective knowledge structures.

A natural question that one may ask is whether worlds can be viewed as partial specifications of structures. This would be very desirable since worlds are finite while structures are infinite. McCarthy [Mc84] posed essentially this question as an open problem in 1975. It turns out surprisingly, that not every world can be extended to a knowledge structures. The following theorem charac­ terizes the extendible worlds.

Theorem 1. A world </0, ... Jk> is a prefix of some knowledge structure if and only if either k-:;, 1 or whenever <go, ... ,g,...1> E/,{ a) and < ho, ... ,h,...2> Eg,...1( a) , then there is a (k- 1)st-order assignment h,_1 such that <ho, .. . ,h,_1>E/,(a) and h,_,( aK g,_1( a).

We note that, in the context of fully introspective structures, every world is a prefix of some structure.

The intuition behind the condition of the theorem will be explained in the full paper. From now on, we deal only with worlds that satisfy the condition of Theorem 1.

3. Syntax and Semantics

The set of formulas is the smallest set that contains the atomic propositions, is closed under Boolean connectives and contains K.¢> if it contains ¢>. The depth of a formula ¢> is the depth of nesting of the K.'s in¢>:

• depth(p)=O, if p is atomic propositions.
• depth(·t/>)=depth(¢>).
• depth(¢>/\ 1/J)= max{ depth(t/>),depth(,P)}.
• depth(K.(t/>))=l+depth(¢>).

We are almost ready to define what it means for a knowledge structure to satisfy a formula. We begin by defining what it means for an ( r+ 1 )-ary world </0, ... Jr> to satisfy formula ¢> , written <fo, ... Jr>f=¢>, if r;::depth(¢>).

• </0, .. . Jr> f=p, where p is a primitive proposition , if p is true under the truth assignment f0.
• <fo, · · · Jr>f=·¢> if </o, · · · Jr>'fltf>.
• <fo, ... Jr> f=<PJ/\t/>2 if both </o, ... Jr> F¢>1 and <fo, · · · Jr> FtP2·
• <fo, · .. Jr>f=K.¢> if <go, ... ,gr-l>f=¢> for each <go,· · · ,g,.._J>E/~·).

Note that we do not define satisfaction of "deep" formulas in "short" worlds. The actual arity of the world does not quite matter, as long as it is "long" enough .

Lemma 2: Assume that depth(t/>)=k and r;::: k. Then <fo, · · · Jr> f=¢> iff </o, ... ,fk> f=¢>.

We say that the knowledge structure f= <f0,1J, · · · > satisfies ¢>, written ff=¢>, if </o, ... Jk>f=¢>, where k=depth(¢>). This is a reasonable definition, since if w=<fo, .. . Jr> is an arbitrary prefix off such that r;::: k, then it then follows from Lemma 2 that fpt/> iff wf=¢>.

A formula ¢> is valid if it is satisfied by all knowledge structures. From Theorem 1 and Lemma 2 it follows that if depth(tf>)=k, then it suffices to check that ¢> is satisfied in all ( k+ 1 )-ary worlds.

Theorem 3: The validity problem for knowledge structures is decid­ able.

We can axiomatize validity in the following way:

Theorem 4: The following formal system if sound and complete for validity in knowledge structure:

(A1) All substitution instances of propositional tautologies.

{A2) K.¢>/\K.(t/>"JI/J)"JK.,P.

{A3) K.t/>"JK.K.¢>.

(R1) From¢> and t/>"JI/J infer 1/J.

(R2) From ¢> infer K.¢>.

Thus the logic of knowledge structures is the generalization of the modal logic S4 [Ch80J to include multiple modalities. We note that to axiomatize validity in fully introspective knowledge structure one has to. add the axiom ·K.tf>"JK.·K.¢> [FHV84]. That is, the logic of fully mtrospect1ve knowledge structures is a generalization of the modal logic S5.

4. Comparative Knowledge

In this section we want to compare the knowledge state of the same agent in two different knowledge structures. We want to give precise meaning to informal statements such as "I know today more than I knew yesterday". The basic idea, which we have already mentioned in the previous sections, is that, since knowledge is cap­ tured in our model by sets of possibilities, the more possibilities an agents has, the less she knows. Thus if f=</0,/t, · · · > and g= < g0,g" · · · > , then a knows in g at least as much as she knows in r , denoted r~. g , if gk( a)~fk( a), for all k:2: 1, that is if a has in rat least all the possibilities she has in g and possibly more. IC we have both f~ · g and g ~ · f, then we say that a knows the same in f and g , denoted f:= · g. Note that f:= · g if fk( a)= gk( a) for all k:2: 1.

Lemma 5: ~ · is a reflexive and transitive relation. = · is an equivalence relation.

The interpretation that we want to give to "knowing at least as much" is that if a knows in g at least as much as she knows in f, then g is a possible state for her in f. The following theorem justifies this interpretation.

Theorem 6:

• {1) r~.g if and only if <g0, ... ,g~>-1 >E/Ma) for all k:2:1.
• {2) ff=K.,t/J if and only if gf=</> whenever f~ · g .

Thus, a knows </> precisely when </> holds in all knowledge structures that a thinks are possible. Theorem 6 shows the equivalence of two notions of truth. The first notion of truth is "internal", this truth is determined by looking inside the structure. The second notion of truth is "external", this truth is determined by considering an infinitude of possible structures. The reader should compare Theorem 6 with Theorem 2.6 in [FHV84[.

Now that we have justified our notion of "knowing at least as much", we show that this notion makes sense only for partially introspective agents:

Theorem 7: Let f and g be fully introspective knowledge structure. Then f~ · g if and only if g:= · f.

Thus for fully introspective agents "knowing at least as much" is equivalent to "knowing the same". The intuition behind it is that when an agent does not know something, she knows that she does not know. Therefore, her ignorance gains her knowledge. Conse­ quently, no two distinct states of knowledge are comparable (cr. [HM84J).

Previous attempts {cf. [Mo80, Mo84, MSHI78, Sa76]) to provide a semantic foundation for reasoning about knowledge have made use of K ripke structures [Kr63]. We describe Kripke structures for posi­ tively introspective knowledge and explore the relationship between them and knowledge structures.

A Kripke structure for positively introspective knowledge is tuple M=( W,II ,R), where W is a set of possible states, II : P--+PowerSet( W) assigns meaning to the atomic propositions, and R:A--+ w'2 assigns to every agent a reflexive and transitive relation on W. Intuitively, (s,t)ER(a) if tis a possible state for a in I. We now define what it means for a formula </> to be satisfied at a state s of M, written M,sf=</>.

• M,sf=p, where p is an atomic proposition, if sEil(p).
• M,sf=-.4> if M,s'r=/4.
• M,sf=</>1\.P if M,sf=</> and M,sf=I/J.
• M,sf=K.<i> if M,tf=</> for all t such that (s,t)ER(a).

It is not hard to show that with Kripke semantics, the modality K. has all the properties discussed in Section 2 [HM85], but that seems to us less than satisfying, since it leaves to many notions unex­ plained. Bo.th the notion ~f a state a.nd ~he notion of possibility are left as pnm1tlve not10ns w1th no exphcat10n. The following theorem clarifies these issues by providing an exact correspondence between knowledge structures and states in Kripke structures.

Theorem 8 :

1. To every Kripke structure M for positively introspective knowledge and every state s in M, there corresponds a knowledge structure fM.· such that M,sf=</> if and only if fM.,f=.P, for every formula o;P; and if sand tare states in M such that (s,t)ER(a) then rM., ~. fM,t·
2. M-..,=( W,II,R), where W is the set of all knowledge struc­ tures, II(p)={f : ff=p}, and R(a)={(f,g): r~. g}, is a Kripke structure for positively introspective knowledge. Moreover M,ff=o;P if and only if fpo;P, for every formula o;P. '

Theorem 8 shows that knowledge structures and Kripke struc­ tures have the same theory (as we already know from Theorem 3 and the results in [HM85] about axiomatization of validity in Kripke structures), but its implications are deeper. It shows that knowledge structures and Kripke structures complement each other in modelling knowledge: knowledge structures model states of knowledge, and Kripke structures model collections of knowledge states. In particu­ lar a state t is possible for a in a state s if a knows in t at least as much as it knows in s. Correspondence between fully introspective knowledge structures and Kripke structures for fully introspective knowledge was shown in [FHV84].

5. Circumscribed Knowledge

In principle there is no difference between positive information, the facts that are stated to be true, and negative information, the facts that are stated to be false . Indeed, in logic, a truth-assignment is a function from the set of atomic propositions to the set {true,/alse}, and the roles of true and false are completely symmetric. In common sense reasoning, however, we tend to use mostly the posi­ tive facts while ignoring a whole plethora of unstated negative facts. Circumscription [MeSO] is a formal tool to capture this paradigm of common sense reasoning. Our goal in this section is to circumscribe knowledge, that is, we want to give precise meaning to informal statements such as "I know that o;P, and this is all I know".

We start by analyzing a simple case. Suppose that we are given a k-ary world w as a description of the agents' state of knowledge, and we are told that this is all the agents know. For example, suppose that we are told about Alice and Bob in Section 2 that this is all they know. Strictly speaking, this cannot be true. Since Bob knows p, he knows that he knows p, he knows that he knows that he knows p, etc . ad infinitum. What we want to find is some knowledge structure f , such that w is a prefix of f , i.e., w=</0, ·· . J~>--1 > , and such that the knowledge contained in w is circumscribed, i.e., there is no knowledge in r unless it follows, in some sense, from the knowledge in w.

The answer to that problem depends in part on the underlying model of knowledge acquisition. For example, is it possible for Alice to know that Bob knows about p without being told so by Bob, say by tapping into Bob's database? We consider here the most "permis­ sive" situation, where agents have no knowledge about how other agents acquire knowledge. In this case fk( a) should include all the k­ ary worlds that are possible for a in w, i.e. , all the k-ary worlds where a knows at least as much as he knows in w.

This leads to the following definition, where we use the convention that /o( a) is the empty set: fk( a) is the no-information extension

~/ 1~>--l(a) if /k(a)={ <go, ... ,g~>--1>: gl>-1(a)~/i>-1(a)}. The no­ an[orr_nallon eztenston of the k-ary world w=<fo, ... J~>-- 1 >, denoted w , IS the sequence <!o, ... Ji>-1,/k, ... >, where /,.(a) is the no­ information extension of /,_1( a) for m> k Cor each agent aEA.

Intuitively, the no-information extension of f~>-1(a) describes what a knows at level k+1, given that she has no information besides t~at already described at /i>-1( a) and given the underlying "permis­ Sive" model of knowledge acquisition described above.

To justify our definition of the no-information extension we have firs~ t? prove that w· is indeed a knowledge structure (which is not a pr10n clear), and then we have to show that the knowledge in w is indeed circumscribed in w·.

Theorem II : Let w be a k-ary world. Then

1. w· is a knowledge structure, and
2. if r is a knowledge structure such that w is a prefix of r, then w·~ · f, for all aEA.

Consider now a k-ary world w=<fo, ... J~>-- 1> . In such a world the agents have knowledge of depth k-1. Thus in w· we would expect the agents to have knowledge of depth k-1 and no more. Now we have to be careful how we define depth of knowledge. IC a knows p, then she knows that she knows p, she knows that she knows that she knows p, etc . This does not seem, however, as genuinely deep knowledge. IC, on the other hand, a knows that b knows that a kn~ws p, then it seems that a does have deep knowledge. We charac­ teme depth of knowledge by the following definitions.

An a-formula, where a is an agent, is a formula that describes the knowledge of a. Formally,

• K.,t/J is an a-formula.
• IC o;6 is an a-formula and .P is an arbitrary formula, then ;o;P, .PI\ ,P, and t/J/\<;6 are a-formulas.

We can now define the depth. of a formula, which is the depth of a's knowledge described by the formula.

• depth.(p)=O if p is atomic propositions.
• depth.(-,¢)= depthJ<I> ).
• depth.(¢/\.P)=max{ depth.(tP) ,depthJ, ,P)}.
• depth.(K.(¢))=1+max{ depthb{¢) : b=fa and ¢ is a ~formula}. Otherwise depth.(K .¢ )= depthJ ¢ ).

Theorem 10: Let w be a k-ary world and let a be an agent. Then w')=¢, where depth.(¢)=k if and only if¢ is a valid formula.

Corollary. Let w be a 1-ary world and let a be an agent. Then w')=K.¢ if and only if ¢ is a valid formula.

That is, 1-ary worlds consists only of a description of "nature" and they contain no knowledge.

The no-information extension was defined in [FHV84J for fully introspective knowledge. In that context, however, it is not true that w' has the minimum amount of knowledge among all extensions of w, since, as we have argued before, ignorance leads to knowledge by negative introspection. In particular, even no information extensions of 1-ary worlds contain arbitrarily deep knowledge [FHV84J . Thus the only justification for the definition in [FHV84J is the intuition that lead to the definition in the first place.

We now consider statements of the form "all a knows is ¢". The first observation is that such statements need not necessarily make sense even if ¢ is a consistent formul a [HM84bJ. Consider the formula K.p\1 K.q. The statement "all a knows is that either she knows p or she knows q" does not make sense. Either a knows p, and then she knows that she knows p, or she knows q, and then she knows that she knows q. It just cannot be the case that all she knows is that that either she knows p or either she knows q. In the terminology of [Mc80J, K.¢ does not have a unique circumscript ion. When does the statement "all a knows is ¢" make sense? Only when there is a unique way to circumscribe K.¢.

This motivates the following definition. A knowledge structure f is an a-minimal model for a formula ¢ if fF=¢ and f~ · g for all knowledge structures g such that gp¢. A formula ¢ is a-honest if K.¢ has an a-minimal model. The following theorem shows that a­ minimal models for K.¢ indeed circumscribe the knowledge expressed by ¢ (just as minimal predicate circumscribe predicates in [Mc80]).

Theorem 11: Let f be an a-minimal model for K 4 ¢. Then fpK · .P if and only if K.¢~.P is a valid formula.

We can now answer the question "what does a knows if all she knows is ¢?". The answer is that a knows exactly all the logical conse­ quences of K.¢. Note that this is not the case for fully introspective knowledge. There, if all that a knows is p, then a does not know q, so she knows that she does not know q, even though K.p~K.-,K.q is not a valid formula for fully introspective knowledge [HM84bJ . Indeed , the issue of circumscription for fully introspective knowledge is less clear and less intuitive than it is for positively introspective knowledge (cf. [Ha84, HM84b , Pa84J, St81J).

Our treatment here is closely related to Konolige's "cir­ cumscriptive ignorance" [Ko82J . Konolige introduced circumscriptive modalities [¢J, where ¢ is a formula. Roughly speaking, [K.¢Jt/J holds if a knows .P when all she knows is ¢. Konolige's treatment is com­ pletely axiomatic; he adds the inference rule:

(R3) From ¢1-t/J (in the system {A1-3,R1-2}) infer -,[¢J.p.

Since Konolige had no semantics, we view our treatment (Theorem ll) here is as an a fortiori justification for his axiomatic approach.

We want to show now that we can test effectively for honesty of formulas . To do this we extend our definition of ~ · from struc­ tures to worlds in the natural way: <fo, ... J·> :=; · <go, . .. ,g·> if g.( aKt.( a).

Theorem 12: A formula¢, such that depth(¢)=k is a-honest if and only if there is a (k+2)-ary world w such that wpK.¢, and if ul is a (k+2)-ary world such that ul pK.¢, then w :=;. ul

Corollary: Honesty is decidable.

6. Concluding Remarks

We have defined a model-theoretic framework for positively introspective knowledge, which we argue is the right model for impli­ cit knowledge. This framework provides precise means to compare knowledge states, which enabled us to define the notion of a minimal model. We have shown that using the notion of minimal models we can circumscribe knowledge.

Acknowledgements. The research reported here was supported by gift from the System Development Foundation. Much of the work was completed on computer equipment provided by the Xerox Cor­ poration. I'd like to thank R. Fa~in , Y.O. Moses, J .Y. Halpern, _and the anonymous reviewers for theu helpful comments on a prevwus draft of this paper.