Belief, Awareness, and Limited Reasoning: Preliminary Report

1. Introduction

As has been frequently pointed out in the liter­ ature (see, for example, [Hi]), possible-worlds se­ mantics for knowledge and belief do not seem ap­ propriate for modelling human reasoning since they suffer from the problem of what Hintikka calls logical omniscience. In particular, this means that agents are assumed to be so intelligent that they must know all valid formulas, and that their knowl­ edge is closed under implication, so that if an agent knows p, and knows that p implies q, then the agent

must also know q.

Unfortunately, in real life people are certainly not omniscient! Indeed, possible-world advocates have always stressed that this style of semantics assumes an "ideal" rational reasoner, with infinite computational powers. But for many applications, one would like a logic that provides a more realistic representation of human reasoning.

does not know that it knows exactly because it is (presumably) not aware of its knowledge. Similarly, a sentence such as "You're so dumb, you don't even that you don't know p!" is perhaps best understood as saying "You're not even aware that you don't know p".

1. People are resource-bounded: they simply lack the computational resources to deduce all the logical consequences of their knowledge (we still don't know whether Fermat's last theorem is true) .
2. People don't always know the relevant rules. As pointed out by Konolige [Ko], a student may not know which value of x satisfies the equation x +a= b simply because he doesn't know the rule of subtracting equal quantities from both sides.
3. People don't focus on all issues simultaneously. Thus, when we say "a believes p", we more properly mean that in a certain frame of mind (when a is focussing on the issues that involve p), it is the case that a believes p. Even if a does yerfect reasoning with respect to the limited number of issues on whic:':l he is focussing in any given frame of mind, he may not put his conclusions together. Indeed, although in each frame of mind person a may be consistent, the conclusions a draws in different frames of mind may be inconsistent.

In this paper we present a number of different approaches to modelling lack of logical omniscience. These approaches can be viewed as attempting to model different causes for the lack of omniscience, as suggested by the discussion above. Our first approach is essentially an extension of Levesque's [Levl] to the multi-agent case, which in addition avoids some of the problems we see in Levesque's approach. This approach is one that attempts to deal with awareness ((1) above) . Our second ap­ proach combines the possible-worlds framework with a syntactic awareness function; it seems to be more appropriate for dealing with resource-bounded rea­ soning, which has a strongly syntactic component. By adding time into the picture, we can extend the second approach to one that can capture how knowl­ edge is acquired over time, perhaps through the use of a particular (possibly incomplete) set of deduction rules as in [Ko]. Finally, we present an approach that could be called the society-of-minds approach [Mi,BI,Do], which attempts to capture the type of local reasoning discussed in (4) above (a similar idea has been independently suggested by a number of authors, including Levesque [Lev2], Stalnaker [St], and Zadrozny [Za]). The second and third approaches can easily be combined to give a semantics which captures both awareness and local reasoning.

2. Levesque's Logic of Implicit and Explicit Belief

Before we describe our models for knowledge and belief, we briefly review Levesque's logic of implicit and explicit belief, and discuss our criticisms of it. (We take the liberty of slightly changing Levesque's notation, to make it more consistent with our later development.)

The formulas of the language considered by Levesque are formed in the obvious way from a set <I> of primitive propositions, using the standard con­ nectives - and /\, as well as two modal operators B and L (standing for explicit belief and implicit belief respectively; an agent's implicit beliefs include all the logical consequences of his explicit beliefs) . However, Levesque restricts the language so that no B or L appears within the scope of another. Thus if cp and y, are formulas, then so are -cp and cp 1\ Y,; if cp is propositional (does not contain B or L) then Bcp and Lcp are also .formulas. Of course, Boolean connectives such as Y and => are defined in terms of - and 1\ as usual.

A model of implicit and explicit belief is a tuple M = (S, 98, T, F), where S is a set of (primitive) situations, 98 is a subset of S (the situations that could be the actual ones according to what is be­ lieved), and T and F are functions from <I> (the set of primitive propositions) to subsets of S. Intuitively, T(p) consists of all situations that support the truth of p, while F(p) consists of all situations that support the falsity of p.

An incoherent situation s is one that is an element of T(p) n F(p) for some primitive proposition p . Thus an incoherent situation supports both the truth and falsity of some primitive proposition. A complete situation (called a possible world in [Levl]) is one that supports either the truth or falsity of every primitive proposition and is not incoherent (i.e., s is a member of exactly one of T(p) and F(p) for each primitive proposition p) . A situation s is com­ potible with a situation s' if s and s' agree wherever s is defined; i.e. if s € T(p) then s' € T(p), and if s € F(p) then s' € F(p), for each primitive proposition p . Let !111" consist of all complete situations in S compatible with some situation in 98.

We can now define the support relations F=r and PF between situations and formulas. Intuitively, M,s F=r cp when situations in model M supports the truth of cp, while M, s F= F cp when s supports the falsity of cp. The definition is:

M,s F=r p, where p is a primitive proposition, if s € T(p) .

M,s f=F p, where p is a primitive proposition, if s € F(p).

M,s F=r -cp if M,s PF cp .

M,s FF -r:p if M,s FT r:p . M,s FT r;p, 1\ r:p2 if M,s FT r:pl and M,s FT r:{l2· M,s FF r;p, 1\ r:p2 if M,s FF r:pl or M,s FF r:{l2· M,s FrBr:p if M.t Frr:p for all tE SIJ. M,s FF Br:p if M,s lfrBr:p. M,s FrLr:p if M,t FT r:p for all t E $' . M,s ppLr:p if M,s lfrLr:p.

We say that the formula r:p is true, or is satisfied, at situation s if M, s F T r:p holds. Levesque defines a formula r:p to be valid, written pr;p, if r:p is true at s for all models M = (S, SIJ, T, F), and all complete situations s E S.

As Levesque points out, it is easy to see that with this semantics p(Br:p ~ Lr:p), i.e., explicit belief implies implicit belief. It is also easy to see that implicit belief is closed under implication and that all valid formulas are implicitly believed. Thus we have

If : · -p (where r:p is propositional), then pLr:p, and p(Lr:p 1\ L(r:p ~ ~jt)) ~Lijt

Explicit belief does not seem to suffer from the problems of logical omniscience. Before we go on, Jet us discuss what we mean by "logical omniscience". An agent is logically omniscient if when ever he believes all of the formulas in a set ~. and ~ logically implies the formula r:p, then the agent also believes r;p . There are three cases of special interest: (1) what we have been calling closure under implication (namely, when­ ever both r:p and r:p ~ 1Jt are believed, then ljt is be­ lieved), (2) closure under valid implication (if r:p ~ 1/t is valid, and if r:p is believed, then ljt is believed), and (3) belief of valid formulas (if r:p is valid, then r:p is believed) . Now explicit belief has none of these three properties. Thus, explicit beliefs are not closed under implication (for example, Bp 1\ B(p ~ q) 1\ -Bq is satisfiable), nor under valid implication (although p~ (pi\ (qV-q)) is valid, Bpi\ -B(p/\ (qV-q)) is sat­ isfiable), and valid formulas are not necessarily be­ lieved (-B(pV-p) is satisfiable). Moreover, it is also possible to explicitly believe unsatisfiable state­ ments (Bp 1\ B-p is satisfiable, as, for that matter, is B(p 1\ -p)) .

A closer examination of Levesque's semantics shows that the lack of closure under implication and the possibility of believing unsatisfiable state­ ments both stem from the presence of incoherent situations. Indeed, as Levesque points out in [Lev2], while

Br:p/\B(r:p~ljt)~BI/t is not a valid formula, it is easy to check that

Br:p 1\B(r:p ~ 1/t) ~ B(ljtV(r:p 1\ -r:p)) is valid. Thus, either the agent's knowledge is closed under implication, or else some situation he believes possible is incoherent. Similarly, since Br:p/\B(-r:p):=B(r:p/\-r:p), inconsistent beliefs are only possible if every situation the agent believes possible is incoherent. However, to the extent that EflJ is viewed as the set of situations that the agent considers possible, it seems unreasonable to allow incoherent situations. It is hard to imagine an agent that would consider an incoherent situation possible. As Levesque notes in [Lev2] , there is a big difference between believing both p and -p, and believing p 1\ -p.

On the other hand, an agent's lack of knowledge of valid formulas is not due to incoherent situations, but is rather due to the lack of "awareness" on the part of the agent of some primitive propositions; similar reasons hold for the Jack of closure under valid implication. Let us say that an agent is aware of a primitive proposition p, which we abbreviate Ap, if B(pV-p) holds. In some of the following discussion, we shall use the word "aware" both in the precise mathematical sense just defined, and in the more usual English sense, since our mathematical notion of "awareness" does seem to model fairly well the English notion. We shall later mention other possible interpretations for the notion of aware­ ness. Although not every valid sentence is believed,

we do have the following:

Proposition 2.1. Let r:p be a valid propositional formula, and let PI· .. . , Pk be all the primitive propositions that appear in r:p. Then p(A(P!) 1\ ... 1\A(pk)) ~B(r:p) .

Intuitively, Proposition 2.1 says that you believe a valid formula provided that you are aware of all primitive propositions that appear in it. This sug­ gests that Levesque's semantics may be appropriate for capturing the lack of logical omniscience that arises through lack of awareness, but not for cap­ turing the type that arises due to Jack of computa­ tional resources. There may well be a very compli­ cated formula whose truth is hard to figure out, even if you are aware of all the primitive propositions that appear in it.

We have a number of other criticisms, both phil­ osophical and technical, of Levesque's logic:

1. Although truth (i.e. the Fr relation) is defined for all situations, only complete situations are considered when checking for validity. This means that there are "valid" formulas r:p of Levesque's logic (for example, pV-p) such that M, s If T r:p for some situation s. While restricting to complete situations ensures that all propositionally valid formulas continue to be valid in Levesque's logic, it seems inconsistent with the philosophy of looking at situations.
2. As usual with non-classical worlds, while the intuitions behind F seem fairly clear for prim­
3. itive propositions, they are not so clear for the

propositional connectives. For example, suppose that the agent is unaware of the primitive prop­ osition p, so that neither M, s F r p norM, s F F p hold. Thus, by the semantic definitions given above, M,s Fr(p=p) does not hold either. Yet we can still imagine an agent that is unaware of p yet but is aware of some propositional tautologies, in particular ones like p = p . It is interesting to note that in the classical three­ valued logic of Lukasiewicz [Lu], => is usually taken to be a primitive along with t\ and -. and the semantics is defined so that p = p is a tautology, even though pY-p is not. Even though Levesque's semantics could be redefined in this way, the question of motivating the semantics of the connectives still remains.

1. As Vardi observes [Va], although an agent in Levesque's model does not know all the logical consequences of his beliefs (if we understand "logical consequence" to mean consequence of classical propositional logic), it follows from Levesque's results [Levl] that agents in Levesque's logic are perfect reasoners in rele­ vance logic [AB]. Unfortunately, it seems no more clear that people can do perfect reasoning in relevance logic than that they can do perfect reasoning in classical logic!

Besides the criticisms mentioned above, the cur­ rent presentation of Levesque's logic suffers from another serious drawback: namely, it deals with only depth-one formulas and with only one agent. But a viable logic of knowledge or belief should be able to capture - within the logic! - meta-reasoning about one's own beliefs and reasoning about other agents' beliefs. Meta-reasoning is crucial for planning and goal-directed behavior, since one has to reason about the knowledge that one has and needs to acquire. And a knowledge representation utility that does not have certain information may need to reason about where that information is located, and thus about the knowledge of other systems. Such rea­ soning can quickly get quite complicated, and it is not immediately obvious how to e~tend Levesque's model to deal with it.

In the next three sections we present three other approaches to dealing with the problem of logical omniscience, each of which attempts to solve aspects of the problem. All of them deal with the multi-agent case, and are presented in a Kripke-style possible­ worlds framework. Kripke-style structures were chosen because of their familiarity to most readers; we could just as well have used the modal structures framework of [FHV,FV].

A relation R is transitive if (s, u) · R whenever (s. 1) · R and (1, u) · R: R is Euclidean if (1, u) · R whenever (s, 1) · R and (s, u) · R : R is serial if for each s · S there is some 1 · S such that (s,l) · R. Intuitively, (s,l) · 98, if player i in states believes that state 1 is possible. It is well known (see [Ch,HM] for discussion and motivation) that by malting the 98; relations transitive, Euclidean, and serial we capture the axioms associated with belief. In particular, the fact that 98, is transitive ensures the soundness of the axiom L,cp + L,L;cp. the fact that it is Euclidean ensures the soundness of - L,cp +L;-L;cp, while the fact that it is serial ensures the soundness of - L;(false) . Note that the fact that 98; is Euclidean means that for any given states. the relation 98, restricted to the worlds possible relative to s (i.e., {II (s,l) · 98,}) is an equivalence relation (i.e., it is reflexive, symmetric, and transitive): the fact that 98; is serial means that there is always some world possible relative to s. Knowledge differs from belief in that you cannot know false facts (although you may believe them). This amounts to requiring the additional axiom K;cp + cp (note we use K, to denote "player i knows". In order to capture knowledge, instead of assuming that each 98, is transitive, Euclidean, and serial. we would make the stronger assumption that each 98; is an equivalence relation on S.

3. A logic of awareness

The first logic we consider, a logic to reason about awareness, is essentially an ·extension of Levesque's logic (to allow multiple agents and nested beliefs) that dispenses with both partial and inco­ herent situations. Formally, we proceed as follows. Since we wish to deal with many agents, we fix a set of agents (or players) 1, .. . , n and instead of a single Band L, we allow operators B~o ... ,Bn, L~o ... ,Ln. We allow arbitrary nesting of the B;'s and L/s in formulas. A Kripke structure for awareness is a tuple M=(S,'IT,.41, ... , .4n,81'11, ... ,81'1n). where Sis a set of states, '"(s, ·) is a truth assignment to the primitive propositions for each state s E S (i.e., 'IT(s,p) E {true, false} for each p E <t>), .4; associates with each state s a set of primitive propositions (intuitively, these are the primitive propositions of which player i is aware at state s), and 81'1; is a binary relation over S which is transitive, Euclidean, and serial, for each player i. 1 For convenience, we also assume that false is a special primitive propo­ sition, and that 'IT(s.[alse) =false and false E .4;(s) for all states s.

Note that a state corresponds to a complete sit­ uation or possible world. There are no partial states. However, as we shall see, the awareness functions make each state partial from the point of view of player i. Of course, in a given state, player i and player j will not necessarily be aware of the same formulas.

In order to define truth of formulas in this logic with many players, we have support relations Ff and F j for each set 'I' of primitive propositions. Intuitively, the effect of t=t and t=i is to restrict every state to a partial situation where only the primitive propositions in 'I' are defined. We also have a standard two-valued notion of truth defined via F· We proceed as follows:

M,s Ff p, where p is a primitive proposition, if TT(s,p) =true and p e 'I'.

M, s F= j p, where p is a primitive proposition, if TT(s,p) =false and p e 'I'.

M,s F= p, where p is a primitive proposition, if TT(s,p) =true.

M,s t=i -cp if M,s t=~ rp.

M,s FF -cp if M,s FT rp.

M,s F= -rp if M,s IF rp.

.M,s F~ 'PI/\ 'P2 if M,s t=i 'PI and M,s Ff 'P2·

M,s FF rp1/\rp2 if M,s FF 'PI or M,s F=i 'P2·

M,s F= 'PI/\ 'P2 if M,s F= 'PI and M,s F= 'P2·

M,s F=f B;rp if M,t F=fn...t,(s)'P for all t such that (s , t) e SIJ;.

M,s F=i B;rp if M,t F=tn...t;(s)'P for some t such that (s, t) e SB;.

M,s F= B;rp if M,s F=~B;rp, where ci> is the set of all primitive propositions.

M,s F=f L;rp if M, t F=~ rp for all t such that (s, t) e f¥1;.

M,s t=i L;rp if M,t F=i rp for some t such that (s, t) e SB;.

M, s F= L;rp if M, t F= rp for all t such that (s, t) e fXl;. We note a number of properties of this definition. Proposition 3.1.

1. F= is complete, i.e., for each M, s, rp, either M, s F= rp or M,s F= -rp.
2. a. If 'Irs; 'I'' and if M,s f=~rp, then M,s t=~:rp.
3. If 'Irs; 'I'' and if M,s f=prp, then M,s FF rp.
4. a. For each set 'I' of primitive propositions, if '¥ M,s FT rp then M,s F rp.
5. For each set 'I' of primitive propositions, if '¥ M,s FF rp then M,s F= _-rp.

Proof. The proof in each case is a straightforward induction on the structure of rp. ·

From the definitions, it also follows that B;rp is true relative to 'I' at state s (i.e., M,s F=f B;rp) iff 'P is true relative to 'I' n .4;(s) at all the states that player i thinks possible (in state s). In particular, this means that B;rp is true at states (i.e., M, s F= B;rp, that is, M,s F=~B;rp , where ci> is the set of all prim­ itive propositions) iff rp is true relative to .4;(s) (the primitive propositions of which i is aware at state s) at all the states player i thinks possible. By way of contrast, since L;rp depends only on player i's implicit belief, and not his awareness, L;rp is true at states if in all states that player i thinks possible, rp is true (irrespective of whether i is aware of rp) . It can easily be shown (using parts 2(a) and 3(a) of Proposition 3.1) that just as in Levesque's logic, we have f=(B;rp~L;rp) : if player i explicitly believes rp, then he also implicitly believes rp. Note that we also have f=(B;L;rp = B;rp), so that player i explicitly believes that he implicitly believes rp exactly if he explicitly believes rp. Thus, our semantics extends to nested formulas in a reasonable way.

Our logic of awareness shares a number of prop­ erties with Levesque's. As before, player i implicitly believes all valid formulas and all the logical con­ sequences of his beliefs. Not all valid formulas are necessarily explicitly believed; in particular, -B,(pY-p) is still satisfiable. Neither are a player's explicit beliefs closed under valid implications; for example, B;pl\ -B;(pl\ (qY-q)) is satisfiable. And Proposition 2.1 still holds, indicating that we also have a logic of awareness. Indeed, all of the axioms of Levesque's logic are still sound in our system. (A complete axiomatization of our logic will appear in the full paper.) However, because we do not have incoherent situations, our notion of explicit belief differs from Levesque's in that (a) for us, an agent's set of explicit beliefs is closed under impli­ cation, and (b) in our system, an agent cannot hold inconsistent beliefs; thus, a formula such as B;(pl\ -p) is not satisfiable.

The careful reader will have also noticed one more difference between our logic and Levesque's: namely, the treatment of F=i for formulas of the form B;rp and L;rp. For Levesque, M, s F= F Brp iff M, s !Fr Brp, so that a situation supports the falsity of explicit belief exactly if it does not ~port its truth. For us, M,s F=i B;rp if M,t F=i ,(s)'P for some t such that (s, t) e SB;. Thus, for us, a situation supports the falsity of B;rp exactly if there is a situation that agent i believes possible that supports the falsity of rp. It turns out (hat this change has no effect on the valid depth one formulas (which is why we did not mention it above), but does affect nested formulas. Our formulation allows a formula such as -B;(B 1 pY-B 1 p) to be satisfiable (for example, if i is not aware of p) .

We close this section with one final observation on the relationship between implicit and explicit belief in our logic. It is easy to check that

B;(pYq) =

[(A;pl\ L;p)V(A;q 1\L;q)Y(A;p/\A;q 1\ L;(pYq))] .

Similarly, we can show that, for example, B;B 1 p:: (A;pi\L;(A 1 pi\L 1 p)) . Note that in both these cases explicit belief was replaced by a combination of implicit belief and awareness (recall that A;p is an abbreviation for B;(pY-p) . This can be done in general. In fact we have the following proposition, whose proof is given in the full paper:

Proposition 3.2. Given a formula rp, ~ can effectively find a formula rp 1 such that rp = rp 1 and B; occurs in rp 1 only in the context B;(pY-p), where pis a primitive prop­ osition.

We remark that rp' is in general exponential in the size of rp, so that such a representation may not be very succinct. However, this result does show that in a strong sense explicit belief in this logic is generated by awareness of primitive propositions.

4. A logic of general awareness

The logic defined in the previous section limits awareness to primitive propositions. This prevents it from capturing general resource-bounded reason­ ing. We now present a logic that gives us more fine-grained control over a player's awareness. In particular, in this logic, an agent's knowledge is not closed under implication. The main new feature of this logic is a somewhat syntactic awareness operator. Thus, in addition to the modal operators B; and L; of the previous logic, we also have a modal operator A; for each player i. We can give the formula A;(Jl a number of interpretations: "i is aware of <p", "i is able to figure out the truth of qJ", or even (when reasoning about knowledge bases) "i is able to com­ pute the truth of <p within time T'.

A Kripke structure for general awareness is a tuple M=(S,'IT,.41> ... ,.4n,$1, ... ,$n), where, as before, S is a set of states, '"(s, ·) is a truth assignment for each state s e S, and $; is a transitive, Euclidean, and serial binary relation on S for each player i. 2 However, now we take .4;(s) to be an arbitrary set of formulas (not just primitive formulas), where again we add the restrictions that false e .4;(s) for all s. Note that we have not (yet) placed any restrictions on .4;(s) . In particular, it is possible for both <p and -<p to be in .4;(s), and it is possible that, for example, <p 1\ If is in .4;(s) but If 1\ <p is not in .4;(s). The formulas in .4;(s) are those that the agent is "aware of", not necessarily those he believes.

We have not yet discussed exactly what "aware­ ness" really is, and indeed, we do not in tend to do so at all here! The precise interpretation we give to the notion of awareness will depend on the in­ tended application of the logic. By placing various restrictions on the awareness function, we can cap­ ture a number of interesting distinct notions. We shall discuss some interesting restrictions below.

This logic does not have support relations, just a standard two-valued truth relation 1=. defined inductively as follows :

M, s I= p, where p is a primitive proposition, if 'IT(s,p) =true.

M,s 1=-qJ if M,s jF<p. M,s I= <JJ1/\ <Jl2 if M,s I= (JJ 1 and M,s I= <p2.

M,s I=A;<p if <p e .4;(s).

2 Again, to capture knowledge rather than belief, we would take 98 1 to be an equivalence relation on s.

As was pointed out to us by Peter van Emde Boas, without this latter restriction the "pragmatically paradoxical" sentence B 1 (JJ I\ -B,p) ("Agent i simultaneously believes that p is true and that he doesn't believe it") is satisfiable in the logic (at a state s where p i\ -B;p · .-;(s), but p ~ .-,(s)).

M, s I= B;<p if <p e .4;(s) and M, t I= <p for all t such that (s, t) E $;.

M,s I= L;<p if M,t I= <p for all t such that (s,t) e $;.

Note that with this logic, player i explicitly be­ lieves <p iff (a) player i implicitly believes qJ (i.e., <p is true in all the worlds he considers possible) and (b) player i is aware of qJ; thus B;<p = L;<p 1\ A; (Jl . You cannot have explicit beliefs about formulas you are not aware of! It is easy to see that L; acts like the classical belief operator; if we assume that play­ ers are aware of all formulas, this logic reduces to the classical logic of belief, known as KD45 or weak SS (cf. [Ch,HM]).

Just as for our previous logic, agents still do not explicitly believe all valid formulas ; for example, -B;(pV-p) is satisfiable because the agent might not be aware of the formula pV-p. However, unlike the previous logic, an agent's explicit beliefs are not necessarily closed under implication ; B;p 1\ B;(p-::> q) 1\ -B;q· is satisfiable since i might not be aware of q. Since awareness is essentially a syntactic operator, this approach does suffer from all the shortcomings of the syntactic approach men­ tioned by Levesque [Levl] . For example, there is no reason to suppose that B;(<JJ 1\ !f)= B;(l/t 1\ <p), since A;(<p 1\ !f) might hold without A;(l/t 1\ <p) holding. But in fact, people do not necessarily identify for­ mulas such as If 1\ <p and <p 1\ If. Order of presentation does seem to matter. And a computer program that can compute the truth of qJ 1\ If in time T might not be able to compute the truth of If 1\ <p in time T.

On the other hand, as memtoned above, depending on the intended application, we may want to add some restrictions to the awareness function to cap­ ture certain properties of "awareness". These in­ clude:

1. Awareness could be closed under subformulas; i.e., if <p e .4;(s) and If is a subformula of <p, then If E .4;(s) . Note that this makes sense if we are reasoning about a knowledge base that will never compute the truth of a formula unless it has computed the truth of all its subformulas. But it is also easy to imagine a program that knows that <pV-<p is true without needing to compute the truth of <p. Perhaps a more rea­ sonable restriction is simply to require that if qJ 1\ If e .4;(s) then both qJ, If e .4;(s) .l
2. If order of presentation of conjuncts is irrelevant, we could have <p 1\ If e .4;(s) iff If 1\ qJ e .4;(s). Similarly, we could decide that an agent is aware

• of a formula iff he is aware of its negation, so that cp E Jll;(s) iff ~cp € .J;(s).
• Agent i might only be aware of a certain subset of the primitive propositions, say 'I'. In this case we could take .J;(s) to consist of exactly those formulas which only mention primitive propositions that appear in '1'. This type of awareness function gives a logic in somewhat the same spirit as Levesque's logic or the logic of awareness presented in Section 3, but there are some crucial differences. For example, in the awareness logic, the formula B;cp =;. B;(cpV'f) is valid, whether or not i is aware of of; but this formula is not valid in the logic we have just described.
• We can allow awareness of players as well as formulas, so, for example, player j might not be aware of any formula that mentioned player i.
• A self-reflective agent will be aware of what he is aware of. Semantically, this means that if cp E Jll;(s), then A;cp E Jll;(s) . This corresponds to the axiom A;cp =;.A;A;cp.
• Similarly, an agent might know what formulas he is aware of. Semantically, this means that if (s, t) E /XJ; then .J;(s) = Jll;(t) . This corre­ sponds to the axiom A;cp =;. L;A;cp. This restriction seems particularly appropriate when awareness is generated by a subset of primitive propositions or a subset of players, as discussed above.
• The elements of .J;(s) could be exactly those formulas whose truth can be computed in some specified time or space bound by a given pro­ gram or set of programs. This type of "aware­ ness" could provide a tool for formalizing the recent advances in cryptography theory. Here the problem is in making sense out of what it means that an adversary does not know how to read a message which is encoded using a public­ key cryptosystem (cf. [RSA,Me,GMR]). Such a system is completely insecure from an information-theoretic point of view, but is deemed to be difficult to break in a reasonable amount of time for complexity-theoretic reasons. We remark that knowledge seems more appro­ priate than belief when trying to capture rea­ soning about cryptographic protocols.

The message that the reader should get from these examples is that the ability to place conditions on the awareness function provides a flexible tool for modelling various situations. Even greater flexibility can be attained once we incorporate time into the

language; this is the subject of the next section.

5. Incorporating time We can further extend this logic (and in fact all the other logics we have been discussing) by adding a relation, and a corresponding modal operator, to capture time. Formally, a model would now be a tuple M = (S,rr, Jilt ·.. . , Jlln, lXlt ·... , lXln, ~. where 8 is a deterministic, serial relation; i.e. for all s E S, there is a unique t E S such that (s, t) E 8 . Intuitively, (s, t) € 8 if t describes the state of the world at the "next" time instant after s. 4 We also add unary modal operators o and 0 into the language, where Ocp is true if cp is true at the next time instant (or "tomorrow"), and Ocp is true if cp is eventually true. We define 5'" to be the reflexive, transitive closure of /Y, that is, the binary relation on S defined by (s,t) € g'" iff there exist States SQ, .. . ,Sk SUCh that s=s0 , t=sk, and (s;,s;+t) E /Y for i<k. More formally, we have:

4 Thus we have taken time to be linear rather than branching, discrete rather than continuous, and with no endpoint. However, easy modifications can be made to the model presented above to allow us to deal with all of the possibilities (cf. [HC]).

M,s F Ocp if M,t F cp for (the unique) t such that

(s,t)€8.

M.s F Ocp if M, t F cp for some t € 5'" . As usual in the literature, we define 0 to be the dual of 0. so that Ocp is ~O~cp. Thus Ocp is true if cp is true now and forever in the future.

Once we have time in the picture, we can con­ sider investigating what happens when we impose a number of additional constraints on the relationship between belief (or knowledge), time, and awareness. When considering knowledge rather than belief, in some treatments (for example [Sa,Lehl]), an addi­ tional requirement is placed on the interaction be­ tween knowledge and time, which, roughly speaking, captures "not forgetting' The intuition is that the set of worlds an agent thinks possible should decrease over time, as the agent acquires more information. In particular, this means that at a given time, the set of worlds that an agent now thinks could possibly describe the situation of tomorrow is a superset of the set of worlds that he actually thinks possible tomorrow. Syntactically this corresponds to the ax­

iom

• (*) K;(Ocp) =;. OK;cp;

if agent i knows (today) that cp will be true tomor­ row, then tomorrow he will know cp (where we use K; since we are dealing with knowledge rather than belief) . Semantically, this corresponds to the follow­ ing restriction (where /XJ; is an equivalence relation, since we are dealing with knowledge):

If for some states s, t, u we have (s, t) E 8 and (!, u) E lXJ,, then there exists a state (**) w such that (s, w) E /XJ; and (w, u) E 8; i.e. fYo/XJ;<;;,/XJ;o8.

It is easy to check that axiom (*) holds in all models that obey the restriction (**) (although it is still an open question whether(*) characterizes such models). As pointed out to us by Elias Thijsse, (*) is not immediately applicable to belief. For example, I may believe now that I may finish writing this paper by tomorrow, but tomorrow I may realize that this belief is false, and no longer believe it. But even with regards to knowledge, (*) is not often not a realistic assumption. People certainly forget! And (**) seems to have rather unpleasant consequences for the decision procedure of the resulting logic (see Section 7).

Recall that one interpretation we gave the aware­ ness function in the previous section was in terms of the formulas whose truth could be computed within a certain amount of time. Since we are dealing with a decidable language, we can imagine a program that will eventually be able to compute the truth value of every formula. We can capture this very easily in our present framework by simply requiring that the awareness functions satisfy the following constraints:

• (t) if (s,t) e g- then .4;(s)<;.4;(t) and
• (:1:) for all s e S and all formulas r:p, there is SOme t With (s, t) E g"* and r:p E .4;(t).

Intuitively, constraint (t) says that agent i's aware­ ness never decreases over time, while (t) says that i is eventually aware of every formula. In a model satisfying these constraints, we have the following sound inference rule: from r:p infer ()B;r:p. Thus, all valid formulas are eventually believed. Moreover, the obvious weakening of closure under implication also holds. As long as r:p and r:p => Y, are stable formulas (once true, they remain true), then if r:p and r:p => Y, are believed, it follows that eventually y, will be believed too. Thus, if r:p and r:p => Y, are stable, then we have

Other variations on these restrictions are also possible. For example, we may want to drop (:j:) while retaining (t), so that while an agent's awareness increases, he might not be eventually aware of every formula. We may also want to impose conditions on how awareness increases, say by allowing appli­ cation of a particular deduction rule at every step, where the deduction rule applied might depend on current knowledge or past history (this was suggested to us by Kurt Konolige) . There is clearly room for further work here.

5 If we wish to capture knowledge rather than belief, then we need to add the further restriction that s is a member of every member of W;(s) .

6. A logic of local reasoning

Although the logic of general awareness discussed in the previous two sections is quite flexible, it still has the property that an agent cannot hold incon­ sistent beliefs. In this section we present a logic in which agents can hold inconsistent beliefs, but without making use of incoherent situations.

Our key observation is that one reason that peo­ ple hold inconsistent beliefs is that beliefs tend to come in non-interacting clusters. We can almost view an agent as a society of minds, each with its own set (or cluster) of beliefs, which may contradict each other.

This phenomenon seems to occur even in science. The physicist Eugene Wigner [Wi] notes that the two great theories physicists reason with are the theory of quantum phenomena and the theory of relativity. However [RB, p. 166], Wigner thinks that the two theories may well be incompatible!

In our previous logics, given a states, we viewed {t I (s, t) e .'B;} as the set of states that agent i thought possible in state s. In our next logic, there is not necessarily one set of states that an agent thinks possible, but rather a number of sets, each one corresponding to a different cluster of beliefs. Al­ ternatively, as discussed in the introduction, we can view these sets as representing the worlds the agent thinks are possible in a given frame of mind, when he is focussing on a certain set of issues.

More formally, a Kripke model for local reasoning (or a cluster mode{) is a tuple M = (S, '"· <&t ·. .. , <&n) where Sis a set of states, 'IT(s, ·) is a truth assignment to the primitive propositions for each state s e S, and <&;(s) is a nonempty set of nonempty subsets of S, with the restriction that if s' e T e <&;(s), then T e <&;(s 1 ). It turns out that this restriction ensures that if an agent believes a fact, then he believes that he believes it (i.e., B;r:p => B;B;r:p) . 5 Intuitively, if <&; (s) = { T1, ... , Tkl, then in states player i sometimes (depending perhaps on his state of mind or the issues on which he is focussing) believes that the set of possible states is precisely T1; sometimes he believes that the set of possible states is precisely T2, etc. Or we could view each of these sets as representing precisely the worlds that some member of the society in agent i's mind thinks possible. If <&;(s) is just a singleton set for each state s, say {1":,}, then this model is equivalent to the models of the previous section, where we interpret (s, t) e .'B; exactly if t e 1:,.

An interesting special case of these models is one where in each frame of mind, an agent refuses to admit that he may occasionally be in another frame of mind. This phenomenon can be observed with people. Semantically, we can capture this by requir­ ing that if s' e T e ~;(s), then ~;(s') is the singleton set {n. 6 We call a cluster model satisfying this restriction a narrow-minded cluster model.

With this semantics we are not really trying to capture implicit and explicit belief. Rather, we are trying to capture weak and strong belief, where a weak belief is one that is true of some frame of mind (i.e. all the states in some cluster), while a strong belief is one that is true in all frames of mind. Accordingly, we now interpret B;rp as player i weakly believes rp, and use the new modal operator S; to denote strong belief, so that S;cp means player i strongly believes cp. We define I= for cluster models

as follows :

M, s I= p, where p is a primitive proposition, if 'IT(s,p) =true.

M, s I= -cp if M,s IF cp.

M,s l=cp1/\cp2 if M,s Fflll and M,s Ffl'2·

M,s I= B;cp if there is some Te ~;(s) such that M, t l=cp for all te T.

M, s I= S;cp if M, t I= rp for every T e ~;(s) and ev­ ery te T.

It is easy to see from the semantic definitions given that weak belief is not closed under implication, but in this case the reason has nothing to do with awareness. B;p 1\ B;(p~ q) 1\ -B;q is satisfiable sim­ ply because in one frame of mind agent i might believe p, in another he might believe p~ q, but he might never be in a frame of mind where he puts these facts together to conclude q.

More importantly for our purposes, note that an agent may now hold inconsistent (weak) beliefs: B ;P 1\ B;-p is satisfiable, since in one frame of mind agent i might believe p, while in another he might believe -p. On the other hand, B;(p 1\ -p) is im­ possible: agents do not believe in incoherent worlds.

Of course, S;p 1\ S;-p is also unsatisfiable.

In the narrow-minded cluster model, an agent will believe he is consistent (even if he is not) since in a given frame of mind he refuses to recognize that he may have other frames of mind. Thus, B;( ~(B;p 1\ B;-p)) is valid in this case. Indeed, since an agent can do perfect reasoning within a given frame of mind, a "narrow-minded" agent will also believe he is a perfect reasoner: in the narrow-minded cluster model, B;(B;p/\B;(p~q)~B;q) is also valid.

6 Note that this restriction is not possible in general when dealing with knowledge rather than belief. You cannot refuse to know the truth, although you can refuse to Jxli~ve it!

7 The proof in the case of one knower is a modification of the techniques of [Lehl]. In that paper, Lehmann also claims a double-exponential decision procedure for the logic of knowledge and time with many knowers, but his proof techniques seem to fail [Leh2).

Note that in both the general and narrow-minded cluster model an agent's beliefs are closed under valid implication and agents believe all valid formu­ las. This is because we have assumed that agents can do perfect reasoning within each cluster. We can easily combine the ideas of the cluster model with those of the general awareness model to get a model where agents do not necessarily believe all valid formulas. The details are straightforward and

left to the reader.

7. Decision procedures and complete axiomatizations

In the case of the classical logics of belief and knowledge, S5 and KD45, it is known that the problem of deciding whether a formula is satisfiable is NP complete in the case of one player, and PSPACE complete if there is more than one player (see [HM] for a discussion of these results) . Despite the apparent extra machinery we have introduced in our models, we can show that the decision pro­ cedures get no harder.

Theorem 7.1. For Levesque's model of implicit and explicit belief, and the one-knower version of the logics of awareness, the logic of general awareness, and the narrow­ minded version of the logic of local reasoning, the problem of deciding satisf~ability of formulas is NP complete (and hence the problem of deciding validity is co-NP complete). For the many-knower versions of all these logics, the one­ knower and many-knower versions of the logic of general awareness with time, and the unrestricted version of the logic of local reasonir;, the problem of deciding satisflability and validity of fon,,u/as is PSPACE complete.

We remark that once we add condition ( .. ) to the semantics of knowledge and time, things seem to get much worse. There the best-known results are a double-exponential decision procedure in the case of one knower; the problem for many knowers is still open. 7

Using standard techniques of modal logic, we can also provide complete axiomatizations for all the logics we have discussed. We discuss a complete axiomatization for the logic of general awareness here to show how the usual axioms of belief must be modified. Axiomatizations for the other logics we have discussed and further details of proofs will appear in the full paper.

Recall that in this logic we have B;cp = L;cp 1\A;rp,

and L; acts like the classical belief operator. It is well-known (cf. [Ch,FV,HM]) that belief can be axiomatized as follows:

1. All substitution instances of propositional tautologies.
2. L;rp::;. L;L;rp ("Introspection of positive belief").
3. -L;rp::;. L;-L;rp ("Introspection of negative be­ lief").
4. L;rpl 1\ L;(rp,::;. fP2)::;. L;rp2 ("What player i be­ lieves is closed under modus ponens").
5. -L;(false) ("Player i does not believe a contradiction").

There are two inference rules: (1) from rp1 and fPI ::;. fP2 infer rp2 (modus ponens) and (2) from rp infer L;rp ("belief of tautologies") . 8

If we simply add to this collection of axioms two more axioms, namely A;(false) ("player i is aware of the formula false") and B;rp = L;rp 1\A;rp ("explicit belief is equivalent to implicit belief plus awareness"), then we get a complete axiomatization of the logic of general awareness.

Theorem 7 .2. The axiom system described above is a sound and complete axiomatization of the logic of general awareness.

Even more insight into the logic is obtained if we consider the fragment of the logic where we can only discuss explicit belief, and not implicit belief (i.e, if we consider the language without the L; operators) . Consider the following axioms schemas and rules of inference.

1. All substitution instances of propositional tautologies.
2. B;rp 1\ A;B;rp::;. B;B;rp
3. -B;rp 1\A;(-B;rp)::;. B;-B;rp
4. B;rp! 1\B;(rp,::;. fP2) /\A;rp2::;.B;rp2
5. -B;(false)
6. A;(jalse) .
7. B;rp:;.A;rp

There are three inference rules: (1) from rp and rp::;. 1/1 infer 1/1, (2) from 1/1 infer A;l/1::;. B;l/1, and (3) from B;rp! 1\ ... 1\ B;rpn 1\ fPl 1\ ... 1\ fPn::;. 1/1 infer B;rpl 1\ ... B;rpn/\A;I/I*B;I/1. (We can view (2) as a special case of (3) with n = 0.) Both (2) and (3) can be viewed as rules of "limited beliefs of tautologies".

Note how the crucial differences between implicit and explicit belief are reflected in the axiom system, particularly axioms 2, 3, and 4 and the rules of limited belief of tautologies. In all these cases an agent must be aware of the relevant formula before he believes it. Of course, similar remarks hold if we replace belief by knowledge. Note that axiom

8 Note that in the case of knowledge, rather than belief, we replace L, by K, , and replace the axiom -L,(Jalse) by K;<p +<p ("Whatever player i knows is true") .

2 indicates how, according to de Chardin, an animal may know, but not know that it knows, while axiom 3 indicates how an agent may be "so dumb that he doesn't even know that he doesn't know p".

Theorem 7.3. The axiom system above is a sound and complete axiomatization for the language of general aware­ ness without the implicit belief operator.

It is also straightforward to axiomatize some of the restrictions on awareness mentioned in Section 4. For example, if the order of presentation of the conjuncts does not matter, we have A;(rp 1\ 1/1) =A;( I/! 1\ rp); if an agent is always simulta­ neously aware of a formula and its negation, we have A;rp = A;-rp. If we take awareness to be closed under subformulas, then this can be captured axio­ matically by adding the axiom schemas A;( -rp)::;. A;rp,

A;(rp/\I/I)::;.A;rp/\A;I/1, A;(B 1 rp)::;.A;rp, A;(L 1 rp)::;.A;rp, and A;(A 1 rp) ::;.A;rp. With these additional axioms, it can be shown that . an agent's beliefs are closed under implication (that is, whenever both rp and rp::;. 1/1 are believed, then 1/1 is believed), although agents still do not believe all valid formulas. By changing ::;. to = in these axioms, we can capture a notion of awareness generated by a set of primitive propositions. We note that in the case of awareness generated by a set of primitive propositions, a num­ ber of the axioms and rules simplify. In particular, we can omit the clauses involving awareness in axioms 2, 3, and 4, and omit rule of inference (3) altogether. Further details can be found in the full paper.

8. Conclusions

We have examined a number of logics, each of which captures different aspects of the problem of lack of logical omniscience, including lack of aware­ ness and local reasoning (within a cluster of beliefs). We expect that other logics can be designed to capture other aspects of this issue.

We are currently investigating quantified versions of these logics. Here some very interesting technical and philosophical questions arise. For example, since we would like to be able to capture sentences such as "He is aware of something that I am not aware of", we seem to be forced into allowing states with different domains, and dealing with all the technical complications that arise there. We hope to report on these issues in a future paper.

9. Acknowledgements

We would like to thank Elias Thijsse for his detailed reading of the paper and numerous pertinent comments and criticisms. We would like to thank Kurt Konolige, Hector Levesque, Yoram Moses, Pe­ ter van Emde Boas, Moshe Vardi, and Ed Wimmers, for their helpful remarks.

10. References

• [AB) A R. Anderson and N. D. Belnap, EnJai/ment, the Logic of Relevance and Necessity, Princeton University Press (1975).
• [BI] A Borgida and T. Imielinski, Decision mak­ ing in committees - a framework for dealing with inconsistency and non-monotonicity, Proc. Nonmonotonic Reasoning Workshop, (1984) .
• [Ch] B. F. Chellas, Modal Logic, Cambridge Uni­ versity Press (1980) .
• [Cr] M. J. Cresswell, Logics and Languages, Methuen and Co. (1973) .
• [Do] J. Doyle, A society of mind, Proc.Jntemationa/ Joint Conference on Artificial Intelligence (JJCAJ), 1983.
• [Eb] R. A Eberle, A logic of believing, knowing and inferring, Syruhese 26 (1974), pp. 356-382.
• [FHV] R. Fagin, J. Y. Halpern, and M. Y. Vardi, A model-theoretic analysis of knowledge, Proc. 25th IEEE Symposium on Foundations of Computer Science, West Palm Beach, Florida (1984), pp. 268-278.
• [FV] R. Fagin and M. Y. Vardi, An internal semantics for modal logic, Proc. of the 17th Symposium on Theory of Computing (1985), pp. 305-315.
• [GMR) S. Goldwasser, S. Micali, and C. Rackoff, The knowledge complexity of interactive proof-systems, Proc. of the 17th Symposium on Theory of Computing (1985), pp. 291-304.
• [HM) J. Y. Halpern and Y. 0 . Moses, A guide to the modal logics of knowledge and belief, to appear as an IBM Research Report (1985) .
• [Hi] J. Hintikka, Impossible possible worlds vin­ dicated, J. Philosophical Logic 4 (1975), pp. 475-484.
• [HC] G.E. Hughes and M.J. Cresswell, An Intro­ duction to Modal Logic, Methuen, London (1968) .
• [Ko] K. Konolige, Belief and incompleteness, SRI Artificial Intelligence Note 319, SRI Inter­ national, Menlo Park (1984) . pp. 377-381.
• [Kr] S. Kripke, Semantical analysis of modal logic, Zeitschrift fur Mathematische Logik und
• Grundlagen der Mathematik 9 (1963), pp. 67-96.
• [Lehl) D.J. Lehmann, Knowledge, common knowl­ edge, and related puzzles, in "Proceedings of the Third Annual ACM Conference on Principles of Distributed Computing", 1984, pp. 62-67.
• [Leh2] D.J. Lehmann, private correspondence.
• [Lev1] H. J. Levesque, A logic of implicit and explicit belief, Proc. Na.-'1 Conf on Artificial Intelligence (1984), pp. 198-202; a revised and expanded version appears as FLAIR Technical Report #32, (1984) .
• [Lev2] H. J. Levesque, Global and local consistency and completeness of beliefs, in preparation.
• [Lu] J. Lukasiewicz, 0 logice trojwartosciowej (On three-valued logic), Ruch Filozoficzny S (1920), pp. 169-171.
• [Me] M. J. Merritt, Cryptographic protocols, Ph.D. Thesis, Georgia Institute of Technol­ ogy, 1983.
• [Mi] M. Minsky, Plain talk about neurodevelopmental epistemology, Proc. 5th Int. Joint Conf on AI (1977), pp. 1083-1092.
• [MH] R. C. Moore and G. Hendrix, Computational models of beliefs and the semantics of belief sentences, Technical Note 187, SRI Inter­ national, Menlo Park (1979) .
• [Raj V. Rantala, Impossible worlds semantics and logical omniscience, Acta Philosophica Fennica 35 (1982), pp. 106-115.
• [RB] N. Rescher and R. Brandom, The Logic of Inconsistency, Rowman and Littlefield (1979).
• [RSA] R. Rivest, A Shamir, and L. Adleman, A method for obtaining digital signatures and public-key cryptosystems, Comm. of the ACM, 21:2 (1978), pp. 120-126.
• [Sa] M. Sato, A study of Kripke-style methods of some modal logics by Gentzen's sequential method, Publications of the Research Institute for Mathematical Sciences, Kyoto University, 13:2, 1977.
• [Se] K. Seger berg, An essay on classical modal logic, Uppsala, Philosophical Studies (1972) .
• [St] R. Stalnaker, Inquiry, M.I.T. Press, 1985.
• [Va] M. Y. Vardi, On epistemic logic and logical omniscience, unpublished manuscript.
• [Wi] Eugene P. Wigner, The unreasonable effec­ tiveness of mathematics in the natural sci­ ences, Comm. on Pure and Applied Math. 13 (1960), pp. 1-14.
• [Za] W. Zadrozny, Explicit and implicit beliefs, a solution of a problem of H. Levesque, unpublished manuscript, 1985.