A Guide to the Modal Logics of Knowledge and Belief: Preliminary Draft

1. Introduction

Reasoning about knowledge and belief has long been an issue of concern in philosophy and artificial intelligence (cf. [Hi1],[MH],[Mo]). Recently we have argued that reasoning about knowledge is also cru­ cial in understanding and reasoning about protocols in distributed systems, since messages can be viewed as changing the state of knowledge of a system [HM]; knowledge also seems to be of vital importance in cryp­ tography theory [Me] and database theory.

In order to formally reason about knowledge, we need a good semantic model. Part of the difficulty in providing such a model is that there is no agreement on exactly what the properties of knowledge are or should be. For example, is it the case that you know what facts you know? Do you know what you don't know? Do you know only true things, or can something you "know" actually be false?

* This author's work was supported in part by DARPA contract N00039-82-C-0250.

Possible-worlds semantics provide a good formal tool for "customizing" a logic so that, by making mi­ nor changes in the semantics, we can capture different sets of axioms. The idea, first formalized by Hintikka [Hi1], is that in each state of the world, an agent (or knower or player: we use all these words interchange­ ably) has other states or worlds that he considers pos­ sible. An agent knows p exactly if p is true in all the worlds that he considers possible. As K.ripke pointed out [Kr], by imposing various conditions on this possi­ bility relation, we can capture a number of interesting axioms. For example, if we require that the real world always be one of the possible worlds (which amounts to saying that the possibility relation is reflexive), then it follows that you can't know anything false. Similarly, we can show that if the relation is transitive, then you know what you know. If the relation is transitive and symmetric, then you also know what you don't know. (The one-knower models where the possibility relation is reflexive corresponds to the classical modal logic T , while the reflexive and transitive case corresponds to S4, and the reflexive, symmetric and transitive case corresponds to S5.)

Once we have a general framework for modelling knowledge, a reasonable question to ask is how hard it is to reason about knowledge. In particular, how hard is it to decide if a given formula is valid or satis­ fiable? The answer to this question depends crucially on the choice of axioms. For example, in the one­ knower case, Ladner [La] has shown that for T and S4 the problem of deciding satisfiability is complete in polynomial space, while for S5 it is NP-complete, and thus no harder than the satisfiability problem for propositional logic.

Our aim in this paper is to reexamine the possible­ worlds framework for knowledge and belief with four particular points of emphasis: (1) we show how general techniques for finding decision procedures and com­ plete axiomatizations apply to models for knowledge and belief, {2) we show how sensitive the difficulty of the decision procedure is to such issues as the choice of modal operators and the axiom system, {3) we discuss how notions of common knowledge and implicit knowl­ edge among a group of agents fit into the possible­ worlds framework, and, finally, {4) we consider to what extent the possible-worlds approach is a viable one for modelling knowledge and belief.

We begin in Section 2 by reviewing possible-world semantics in detail, and proving that the many-knower versions of T, S4, and S5 do indeed capture some of the more common axiomatizations of knowledge. In Section 3 we turn to complexity-theoretic issues. We review some standard notions from complexity theory, and then reprove and extend Ladn.er's results to show that the decision procedures for the many-knower ver­ sions ofT, S4, and S5 are all complete in polynomial space. · This suggests that for S5, reasoning about many agents' knowledge is qualitatively harder· than just reasoning about one agent's knowledge of the real world and of his own knowledge.

In Section 4 we turn our attention to modifying the model so that it can deal with belief rather than knowledge, where one can believe something that is false. This turns out to be somewhat more compli­ cated than dropping the assumption of reflexivity, but it can still be done in the possible-worlds framework. Results about decision procedures and complete ax­ iomatizations for belief parallel those for knowledge.

In Section 5 we consider what happens when op­ erators for common knowledge and implicit knowledge are added to the language. A group has common knowledge of a fact p exactly when everyone knows that everyone knows that everyone knows . . . that p is true. (Common knowledge is essentially what Mc­ Carthy's "fool" knows; cf. [MSHI].) A group has im­ plicit knowledge of p if, roughly speaking, when the agents pool their knowledge together they can deduce p. (Note our usage of the notion of "implicit knowl­ edge" here differs slightly from the way it is used in [Lev2] and [FH].) As shown in [HM1], common knowl­ edge is an essential state for reaching agreements and coordinating action. For very similar reasons, common knowledge also seems to play an important role in hu­ man understanding of speech acts {cf. [CM]). The no­ tion of implicit knowledge arises when reasoning about what states of knowledge a group can attain through communication, and thus is also crucial when reason­ ing about the efficacy of speech acts and about com­ munication protocols in distributed systems.

· A problem is said to be complete with respect to a complexity class if, roughly speaking, it is the hardest problem in that class (see Section 3 for more details).

It turns out that adding an implicit knowledge op­ erator to the language does not substantially change the complexity of deciding the satisfiability of formu­ las in the language, but this is not the case for com­ mon knowledge. Using standard techniques from PDL (Propositional Dynamic Logic; cf. [FL],[Pr]), we can show that when we add common knowledge to the language, the satisfiability problem for the resulting logic (whether it is based on T, S4, or S5) is complete in deterministic exponential time, as long as there at least two knowers. Thus, adding a common knowledge operator renders the decision procedure qualitatively more complex. {Common knowledge does not seem to be of much interest in the in the case of one knower. In fact, in the case of S4 and S5, if there is only one knower, knowledge and common knowledge are iden­ tical.)

We conclude in Section 6 with some discussion of the appropriateness of the possible-worlds approach for capturing knowledge and belief, particularly in light of our results on computational complexity.

Detailed proofs of the theorems stated here, as well as further discussion of these results, can be found in the full paper ([HM2]).

2. Logics of knowledge

2.1 Syntax: A logic of any kind needs a language. Although we consider a number of different logics here, the syntax for all of them is essentially the same. We wish to reason about a world consisting of a propo­ sitional reality ("nature") and m agents, creatively named 1, ... , m. Given a set of primitive proposi­ tions ~ = { P, Q, R, ... } and a set of m agents, we define .Cm(~) to be the least set of formulas contain­ ing ~ , closed under -. , 1\ , and the modal operators K1, ... , Km. Thus, if p and q are formulas of .Cm(<P), then so are -.p, p 1\ q, and K,p, fori = 1, ... , m (where K,p is read "player i knows p"). We use the standard abbreviations p V q for-.( -.p 1\ -.q) and p :::> q for -.(p 1\ ·q). The size of a formula pin .Cm(~), denoted IPI, is its length over the alphabet ~U{ -.,I\,(,), K1, ... , Km}·

2.2 Possible-worlds semantics: Following Hin­ tikka [Hi1], Sato [Sa], Moore [Mo], and others, we use a possible-worlds semantics to model knowledge. This provides us with a general framework for our seman­ tical investigations of knowledge and belief. (Every­ thing we say about "knowledge" in this subsection ap­ plies equally well to belief.) The essential idea behind possible-worlds semantics is that an agent's state of knowledge corresponds to the extent to which he can determine what world he is in. In a given world, we can associate with each agent the set of worlds that, according to the agent's knowledge, could possibly be the real world. An agent is then said to know a fact p exactly if p is true in all the worlds in this set; he does not know p if there is at least one world that he considers possible where p does not hold.

Kripke [Kr] introduced Kripke structures as a for­ mal model for a possible-worlds semantics for the modal logic of necessity and possibility. A Kripke structure M is a tuple (S, 1!" 1 P1, ... , Pm), where Sis a set of states, 1r( s) is a truth assignment to the primitive propositions of 4> for each state s E S (i.e., 1r(s, P) E {true, false} for each primitive proposition P E 4> and states E S), and Pi is a binary relation on the states of S, for i = 1, ... , m. A Kripke world (or just world) w is a pair (M, s), where M = (S, .. . ) is a Kripke structure and s E S. p, is intended to capture the possibility relation according to player i: (s, t) E P1 if, in world (M, s), player i considers (M, t) a possible world.

One of the advantages of Kripke-style semantics is that we can view a Kripke structure as a labelled directed graph, where the nodes are the states of S, and there is an edge from s to t labelled i exactly if (s, t) E Po. This graph-theoretic viewpoint will turn out to be particularly useful in our decision procedures (see Section 3).

We now formally define the notion of a formula being true at a world via the relation f= , a binary relation between worlds and formulas, where w f= pis read "p is true at w" or "w satisfies p":

The last clause in this definition captures the in­ tuition that player i knows p in world (M, s) exactly if p is true in all worlds that i considers possible.

A formula p is said to be valid (resp. satisfiable) if w f= p for all worlds w (resp. some world w). We write f= p if p is valid. Note that p is satisfiable iff -.p is not valid.

The following well-known theorem captures some of the formal properties of our f= :

Theorem 1:

• (a) All instances of propositional tautologies are valid.
• (b) For all formulas p, q E .Cm(4>) and i = 1, ... , m, the formula [K,p 1\ Ki(p :::> q)] :::> K,q is valid.
• (c) For all formulas p, q E .Cm(4>), iff= p and f= p :::> q, then f= q.

2.3 Axiom systems for knowledge: Theorem 1 tells us that by subscribing to Kripke semantics we are forced to accept a number of constraints on the type of notions of knowledge that we can model.* We now show that in a precise sense these are the only con­ straints that we are forced to accept by using Kripke semantics. We do so by defining an axiom system K<ml corresponding to the above constraints, and then prov­ ing that these axioms characterize Kripke worlds.** Such results are well known (cf. [HC,Sa,Ch]). Were­ prove them here (using techniques originally due to Makinson [Ma]) in order to show the close correspon­ dence between the axioms and a particular Kripke structure which we call the canonical structure.

K<m> consists of two axiom schemas:

Al. All tautologies of the propositional calculus

Rl. From 1- p and 1- p :::> q infer 1- q (Modus ponens) R2. From 1- p infer 1- K,p (Generalization)

A formula p is said to be K<mJ-provable, denoted K<ml 1- p, if pis an instance of one of the axiom schemas, or if p follows from provable formulas by one of the in­ ference rules R1 and R2 (we omit the qualifier K<ml if it is clear from context). A formula p is consistent if -.p is not provable. A finite set of formulas {Pl> ... , Pk} is consistent exactly if p1 1\ ··· 1\ Pk is consistent, and an infinite set of formulas is consistent exactly if all of its finite subsets are consistent. Of course, a formula or set of formulas is said to be inconsistent exactly if it is not consistent. A set F of formulas is a maximal con­ sistent set if it is consistent and for all p E ( .Cm ( 4>) \F), the set F U {p} is inconsistent.

· We discuss the ramifications of this point in Section 6.

** The name K<m> is inspired by the fact that for one knower, the system reduces to the well-known modal logic K.

Using standard techniques of propositional rea­ soning, we can show

Lemma 2: In any axiom system that includes A1 and R1:

• (a) every consistent set F can be extended to a max­ imal consistent set,
• (b) if F is a maximal consistent set, then for all for­ mulas p, q:
• (i) either p E For --,p E F,
• (ii) p 1\ q E F iff p E F and q E F,
• (iii) if p E F and p :J q E F, then q E F,
• (iv) if p is a valid formula then p E F.

1><1

An axiom system S is sound with respect to a set of worlds .M if every formula provable from S is valid in .M (i.e., is true in every world in .M). S is complete with respect to .M if every formula that is valid in .M is provable from S. We think of an axiom system as characterizing a set of worlds exactly if it provides a sound and complete axiomatization of that set.

Theorem 3: K<m> is a sound and complete axioma­ tization for Kripke worlds.

Proof: Theorem 1 implies that K<m> is sound with respect to Kripke worlds. In order to prove complete­ ness, it suffices to show that every consistent formula is satisfiable. We will do so by constructing a Kripke structure Me, which we call the canonical Kripke struc­ ture for K<m>, containing a state sv for each maximal K<m>-consistent set V in such a way that (Me, sv) f= p for all p E V. Since, by Lemma 2, every consistent set of formulas is contained in some maximal consistent set, this suffices. We proceed as follows. Given a set V of formulas, define VI K, = {pI K,p E V}. Let Me= (S, 1r, P1, ... , Pm), where

We now show, by induction on the structure of p, that for all V we have (Me, sv) f= p iff p E V. More precisely, assuming that the claim holds for all subfor­ mulas of p, we will also show that it holds for p. H p is a primitive proposition P, this is immediate from the definition of 1r(sv, P) above. The cases where p is a conjunction or a negation are simple and left to the reader. Assume that pis of the form K,q and that p E V. Then q E VI K, and, by definition of P,, if (sv, sw) E P,, then q E W. By the induction hypoth­ esis, (Me, sw) f= q for all W such that (sv, sw) E Po. By the definition off=, it follows that (Me, sv) f= K,q.

For the other direction, assume (Me, sv) f= K,q. It follows that the set (VI K,)u--,q is inconsistent. Sup­ pose not. Then by Lemma 2 it would have a max­ imal consistent extension W, and, by construction, we would have (sv, sw) E Po. By the induction hy­ pothesis we have (Me, sw) f= ...,q, and so (Me, sv) f= ...,K,q, contradicting our original assumption. Since (VI K,) U ...,q is inconsistent, some finite subset, say Pl, ... , p,., ...,q, must be inconsistent. Thus, by propo­ sitional reasoning, we have

By R2, we have

Since a maximal consistent set contains all tautologies, we must have

And since Pl· ... , Pk E VI K,, we must also have

Now, by repeated applications of axiom A2 and Lemma 2(b)(iii), we can easily show that K1q E V, as desired. 1><1

In the philosophical literature, one finds a great deal of discussion as to which axioms truly character­ ize knowledge (see !Len] for a discussion and review). Some of the ones more commonly considered include:

the knowledge axiom, which states that only true facts can be known (this is usually taken as the essential property distinguishing knowledge from belief),

the positive introspection axiom, which states that an agent knows what he knows, and

the negative introspection axiom, which says that an agent knows what he does not know.

In the case of a single agent, the system K+A3 is classically known as T, T+A4 is known as 84, while S4+A5 is known as 85. In the case of m agents, m > 1, we will call these systems T<m>· S4<m>· and S5(m) respectively.

Philosophers have spent years trying to determine which of these systems (if any) best captures knowl­ edge (again, see !Len]). In view of Theorem 1, the best that can be said is that we are modelling a rather ide­ alized reasoner, who knows all tautologies and all the logical consequences of his knowledge. If we take the classical interpretation of knowledge as true, justified belief, then an axiom such as A3 seems to be neces­ sary. On the other hand, philosophers have shown that axiom A5 does not hold with respect to this interpre­ tation ([Len]). However, the S5 axioms do capture an interesting interpretation of knowledge appropriate for reasoning about distributed systems (see [HMl] and Section 6). We continue here with our investigation of all these logics, deferring further comments on their appropriateness to Section 6.

Theorem 3 implies that the provable formulas of K<ml correspond precisely to the formulas that are valid for Kripke worlds. As Kripke showed [Kr], there are simple conditions that we can impose on the pos­ sibility relations P, so that the valid formulas of the resulting worlds are exactly the provable formulas of T(ml, S4<ml, and S5(m) respectively. We will try to motivate these conditions, but first we need a few def­ initions.

We say that a binary relation P on a set S is re­ flexive if ( s, s) E P for all s E S; P is transitive if, for all s,t,u E S, if (s,t) E P and (t,u) E P, then (s,u) E P; P is symmetric if, for all s, t E S, whenever (s, t) E P then (t, s) E P; P is Euclidean if, for all s, t, u E S, whenever (s, t) E P and (s, u) E P, then (t, u) E P; finally, P is serial if, for all s E S, there is some t such that ( s, t) E P. A relation that is reflexive, symmetric, and transitive, is also commonly called an equivalence relation . Some of the relationships between these no­ tions are described by the following lemma ( cf. [ Ch]):

Lemma 4:

• (a) If P is symmetric and transitive, then P is Eu­ clidean.
• (b) P is symmetric, transitive, and serial iff P is re­ flexive and Euclidean iff P is reflexive, symmetric, and transitive. 1><1

We say a world (M, s) is reflexive (resp. symmetric, transitive, Euclidean, rt, rst, serial) exactly if all the possibility relations in M are reflexive (resp. sym­ metric, transitive, Euclidean, reflexive and transitive, reflexive, symmetric, and transitive, serial).

To see the relationship between these notions and the axioms described above, consider the canonical Kripke structure Me defined in Theorem 2. Recall that (sv, sw) E P, in Me exactly if VI K, ~ W, where VI K, = {pI K,p E V}. Now suppose that all instances of A3 are true at sv . Then it is easy to see that ( sv , sv) E P,, since VI K, ~ V. This suggests that A3 corresponds to reflexivity. Indeed, it is easy to check that A3 is sound in all reflexive worlds. In terms of the possible worlds, if P, is reflexive, then in world w, player i always considers w to be one of his possible worlds. Thus, if in world w player i knows p, then p must be true in w; i.e., K,p :J p.

A4 forces the possibility relations in the canonical structure to be transitive. To see this, suppose that (sv,sw),(sw,sx) E P, and that all instances of A4 are true at sv. Then if K,p E V, by A4 we have K, K,p E V, and by the construction of Me, we have K,p E Wand p EX. Thus VIK· ~X and (sv,sx) E P, as desired. In terms of possible worlds, a transitive possibility relation says that if in world w, player i considers w' possible, and if in w' player i considers w" possible, then in world w player i will already consider w" possible.

Similar reasoning shows that axiom A5 forces the possibility relation in the canonical structure to be Euclidean. Note that the possibility relation in the canonical structure is forced to be symmetric by the axiom

which can be shown to be a consequence of A3 and A5. This corresponds to the observation of Lemma 4(b) that a relation that is both reflexive and Euclidean is also symmetric.·

Arguments essentially identical to those of Theo­ rem 3 can now be used to show:

Theorem 5:

• (a) T<m> is a sound and complete axiomatization for reflexive worlds.
• (b) S4(m) is a sound and complete axiomatization for rt worlds.
• (c) S5<m> is a sound and complete axiomatization for rst worlds. 1><1

We close this section with some remarks on Kripke structures for S5 (i.e., the case of one agent). We de­ fine two worlds ( M, s) and ( M', s') to be equivalent, written (M, s) = (M', s'), if, for all formulas p, we have (M, s) f= p iff (M', s') f= p.

· Since Lemma 4(b) says that a relation that is both reflexive and Euclidean must also be transitive, the reader may suspect that axiom A4 is redundant in S5. This indeed is the case.

Proposition 6: Suppose M = (S, 1r, P), where P is an equivalence relation (so that M is a model of S5), and s E S. Then (M, s) = (M', s), where M' = (S', 1r 1 , P') and S' = {t I (s, t) E P} (so S' is the equivalence class of s), 1r 1 is 1r restricted to S', and P' = {(t, t') It, t' E S'}.

Proof: By a straightforward induction on the struc­ ture of formulas. 1><1

Proposition 6 intuitively says that in determin­ ing the truth of an S5 formula at a given state s, we can restrict our attention to states that are considered possible at s. It follows that we can assume without loss of generality that models of S5 have a particularly simple form: M = (S, 1r, P), where for all s, t E S, we have (s, t) E P (and in particular, S5 is a sound and complete axiomatization for worlds (M, s) where M has this form). Note that for such models, we do not even have to mention the P relation; we can simply assume that all states are related to each other via P. However, these remarks do not hold for S5<ml if m > 1.

3. Deciding the satisfiability of formulas

In this section we examine the inherent difficulty of determining whether a formula in a given logic is satisfiable. Of course, the problem of determining va­ lidity is a closely related one, since p is valid iff ...,p is not satisfiable. We consider this problem using tools from the computational complexity. We briefly review the necessary notions here; the reader should consult [HU] for further details.

The cost of solving a given problem is usually measured by the amount of ·time and or space (mem­ ory) required to compute the solution, as a function of the input size. Since the inputs we consider in this section are formulas, we will typically be interested in how difficult it is to determine if a formula p is satisfi­ able or valid as a function of IPI· We are usually most interested in deterministic computations, where at any point in the computation, the next step of a compu­ tation is uniquely determined. However, thinking in terms nondeterministic computations - ones where the program may "guess" which of a finite number of steps to take - has been very helpful in classifying the intrinsic difficulty of a number of problems. The complexity classes we will be most concerned with here are P, PSPAOE, EXP, and NP: the problems that are solvable in deterministic polynomial time, determinis­ tic polynomial space, deterministic exponential time, and nondeterministic polynomial time, respectively. It is not hard to show that P s;;; NP s;;; PSPAOE s;;; EXP; it is also known that P =I EXP. While it is conjectured that all the other subset relations are strict, proving this remains elusive. The P = NP problem is cur­ rently considered the most important open problem in the field of computational complexity.

Roughly speaking, a problem A is said to be hard with respect to a complexity class C (eg. NP-hard, PSPAO.&hard, etc.) if every problem inC can beef­ fectively reduced to A; i.e., for any problem Bin C, an algorithm for B can be easily obtained from an algo­ rithm for A. A problem is complete with respect to a complexity class C if it is in C and is C-hard. A well­ known result due to Cook [Co] shows that the problem of determining whether a formula of propositional logic is satisfiable is NP-complete. In particular, this means that if we could find a polynomial-time algorithm for deciding satisfiability for propositional logic, we would also have polynomial-time algorithms for all other NP problems. This is considered highly unlikely.

Since propositional logic is a sublanguage of all the logics we have considered, the satisfiability prob­ lem for all of them is NP-hard. Ladner showed that, at least for S5, it is no harder.

Theorem '1 ([La]): The problem of deciding S5-satis­ fiability is NP-complete.

The key step in the proof of Theorem 7 lies in showing that satisfiable S5 formulas can be satisfied in very small worlds:

Proposition 8 ([La]): An S5 formula pis satisfiable iff it is satisfiable in a world (M, s) where M has less than IPI states.

Proof: Assume that p is satisfiable, and let ( M, s) f= p. By Proposition 6 and the remarks following it, we can assume that M = (S, 1r, P), where (t, t') E P for all t, t' E S. Let F be the set of subformulas of p of the form Kq for which (M, s) f= ...,Kq; i.e., F is the set of subformulas of p that have the form K q and are false at state s. For each formula Kq E F, there must be a state Sq E S such that (M, Sq) f= ...,q. Let M' = (S', 11"', P'), where S' = {s} U {sq I q E F}, 11"' is the restriction of 1r to S', and P' = {(t, t') It, t' E S'}. Note that IS'I ~ IPI· We now show that for all states s' E S' and for all subformulas q of p (including p itself), (M, s') f= q iff (M', s') f= q. As usual, we proceed by induction on the structure of q. The only nontrivial case is when q is of the form K q'. Sup­ pose s' E S'. If (M, s') f= K q', then (M, t) f= q' for all t E S, so, in particular, (M, t) f= q' for all t E S'. By induction hypothesis, (M', t) f= q' for all t E .S', so (M',s') f= Kq'. And if (M,s') ~ Kq', then (M, s') f= -,K q'. Since M is a model of S5, we have (M, s') f= K-,Kq', so that (M, s) f= -,Kq' (since (s', s) E P by assumption). But then it fol­ lows that K q' E F, and ( M, Sq·) f= ...,q'. By construetion, Sq· E S', and by induction hypothesis, we also have (M' 1 8q·) f= -.q'. Since (8 1 1 8q·) E P', we have (M', 8 1 ) f= -.Kq', and so (M', 8 1 ) ~ Kq' as desired. Since s E S' and (M, 8) f= p by assumption, we also have (M', 8) f= p. IXl Proof of Theorem 7: Because the propositional calculus is part of S5, Cook's Theorem implies that deciding S5 satisfiability is NP-hard. We now give an NP algorithm for deciding S5 satisfiability. Intu­ itively, given a formula p, we simply guess a world (M, 8) where M has at most jpjstates, and verify that this world does satisfy p. More formally, we proceed as follows.

Given a formula p, where !PI = n, we nondeter­ ministically guess a Kripke structure M = (S, 11" 1 P), where S is a set of k :5 n states, (8, t) E P for all 8 1 t E S, and for all 8 E S and primitive propositions P not appearing in p, 1r(8, P) =true. (Note that the only "guessing" that enters here is in the choice of k, and the truth value 1r(8, P) for primitive propositions P that appear in p in the k states in S.) Since at most n primitive propositions appear in p, guessing such a Kripke structure can be done in nondeterministic time O(n 2 ) (i.e., :5 cn 2 for some constant c). Next, we check whether p is satisfied at some state 8 E S . This can easily be done deterministically in time O(n 2 ) by simply computing, by induction on structure, whether (M, 8) f= q for each state 8 E S and each subformula q of p. We leave details to the reader. By Proposi­ tion 8, if p is satisfiable, one of our guesses is bound to be right . (Of course, if pis not satisfiable, no guess will be right.) Thus we have a nondeterministic O(n 2 ) algorithm for deciding if p is satisfiable. IX1

As the following result shows, this technique will not work for deciding satisfiability for the other logics we have been considering.

Proposition 9: There is a constant c > 0 such that for all n > 1, there is a formula Pn with IPn I = n that is S5<w (resp. S4-, T-, K-) satisfiable such that Pn is Satisfiable Only in WOrlds With ~ zy'C'n' (resp. ~ zen I ~ zy'C'n', ~ zy'C'n') states. IX1

In fact, as Ladner shows:

Theorem 10 ([La]): The problem of deciding the satisfiability of formulas for the logics K, T, and S4 is PSPAO.E-complete. IX1

It is easy to extend Ladner's techniques to show that for all m, K(ml 1 T (ml 1 and S4(ml are PSPAO.E­ complete. Interestingly, although S5 is NP-complete, we can show that S5<ml , for m ~ 2, is also PSPAO.E­ complete. Thus, for S5, having more than one knower bumps the complexity of deciding satisfiability up from NP-complete to PSPAO.E-complete. The upper bound for S5<mJ is proved using techniques similar to Lad­ ner's. The lower bound follows from the following ob­ servation (which is also used in the proof of Proposi­ tion 9):

Lemma 11: Let p E .C<1>(4>) (i.e., only one modal operator, K, appears in p). Let r(p) be the .C<2>(4>) formula that results from replacing all occurrences of K in p by K1K2. Then p is T-satisfiable iff r(p) 1s S5<wsatisfiable (iff r(p) is S4<wsatisfiable).

As a consequence, we have:

Theorem 12: The problem of deciding the satisfia­ bility of formulas in K( m) I T ( m) I and S4( m) is PSPA 0.& complete. The problem of deciding the satisfiability of formulas in S5<rn> form ~ 2 is also PSPAO.E-complete. IX1

The algorithms that prove that the logics are all in PSPAOE are based on tableau techniques and de­ pend crucially on the following observation. Define a structure M = (S, 11" 1 P1 , ··· , .Pm) to be treelike if its graph forms a tree, with no backedges. The r-clo8ure of M is the structure that results when the possibil­ ity relations .P1, ... , .Pm are replaced by their reO.exive closures. We can similarly define the rt-clo8ure and rst-closure of a structure M.

Proposition 13: A K(mJ (resp. T(rnJ· S4(rnJ· S5(rnJ) formula p is satisfiable iff it is satisfiable in a world (M, 8) where M is a treelike structure (respectively, the r-closure, rt-closure, rst-closure of a treelike struc­ ture) of depth :5 jpj. 1X1

Using Proposition 13, we construct an algorithm that checks if p is satisfiable by constructing the appro­ priate treelike structure for p depth first, in a space­ efficient manner. See [HM2] for details.

4. Belief

A number of recent papers (for example [Lev1]) have pointed out that the knowledge represented in a knowledge base is typically not required to be true. Thus the propositional attitude that philosophers have called belief seems more appropriate than knowledge for formalizing the reasoning and deduction of a knowl­ edge base. Since knowledge bases typically are as­ sumed to have introspective powers, and so know what they know and do not know, this amounts to dropping A3 from the S5 axioms. However, since it is also as­ sumed that knowledge bases do not have inconsistent beliefs, we must add:

(Note that A6 follows from A3 by propositional rea­ soning, but is independent of the rest of the axioms if we drop A3.) A6 is also called the axiom D, and the system consisting of Al, A2, A4, AS, A6, Rl, and R2 is called KD45(m) (cf. [Ch]) or weak SS<m>.

It now remains to find a model for KD45(m)· In terms of possible worlds, the semantic impact of A6 is simply to say that the possibility relations must be se­ rial. Since we have already argued that A3 corresponds to reflexivity, it would seem that we can get a model of KD45<m> simply by considering worlds where the possi­ bility relation(s) are symmetric, transitive, and serial, although not necessarily reflexive. Unfortunately, this won't work; as Lemma 4 shows, any binary relation which is symmetric, transitive, and serial, must also be reflexive.

In the case of one knower, there are well-known ways to get around this problem: we consider a struc­ ture where one distinguished state describes what is true in the "real" world, and a set of states corre­ sponds to the worlds that the agent thinks possible (cf. [Levl]). This is analogous to the case for S5, where as observed in the remarks after Proposition 6, we can, without loss of generality, take a model to be a set of states (all related to each other by the possibility rela­ tion P), one of which will be the real world. Thus, in the case of one knower, the difference between knowl­ edge and belief is that, in the case of belief, the real world is not necessarily one of the worlds the agent considers possible. But this approach does not extend to the many-knower case in any obvious way.

The solution to our problem is already implicit in our discussion in Section 2. Recall that axiom AS corresponds to the possibility relation being Euclidean rather than symmetric. To understand the intuition behind Euclidean relations, observe that for a given state s, if P is Euclidean then the restricton of P to {t I (s, t) E P} is reflexive, symmetric, and transitive, i.e., an equivalence relation. Thus, for a Euclidean relation, the worlds that an agent thinks are possible form an equivalence relation, but do not necessarily include the real world. The fact that the relation is serial means that an agent always thinks some worlds are possible. Applying exactly the same techniques as those used in Theorem 5 we can now show (cf. [FV]):

Theorem 14: KD45(m) is a sound and complete ax­ iomatization for Euclidean, transitive, and serial worlds.

Similarly, using the same techniques as in Theo­ rems 7 and 12, we can show:

Theorem 15: The problem of deciding the satisfia­ bility of KD45 formulas is NP-complete. For m ~ 2, the problem of deciding the satisfiability of KD45<m> formulas is PSPAO.E-complete.

5. Incorporating Common Knowledge and Implicit Knowledge

In a number of situations it is useful to be able to reason about the state of knowledge of a group of agents, not just that of an individual agent. For ex­ ample, we may want to reason about facts that are part of a group's "culture": not only does everyone know them, but everyone knows that everyone knows them, and everyone knows that everyone knows that everyone knows, and so on. These facts are said to be common knowledge . Put another way, these are es­ sentially the facts that "any fool knows" (cf. [MSHI]).

To capture these notions, we extend the language ..Cm(~) by adding two new operators: E and 0. Thus, if pis a formula, then so are Ep ("everyone knows p") and Op ( "p is common knowledge"). We view Ep as an abbreviation for K1pA .. . AKmp, while Op is intended to represent the infinite conjunction EpA EEp A .... Note that if m = 1 then Ep = Kp; thus common knowledge becomes interesting only if there are at least two agents.

We can capture the intended meaning of these constructs quite straightforwardly in our semantics. Given a structure M = (S, 11" 1 P1, ... , Pm), we define a state t to be reachable from s if there is some sequence uo, ... ,un of states in S such that s = uo, t = un, and for all i = 1, ... , n- 1, there is some j such that (u,, Ui+l) E P;. Then we have

Somewhat surprisingly, even though 0 is an "in­ finitary" operator, we can give a complete axiomati­ zation for it. Consider the following set of axioms (cf. [MSHI,Sa,Leh]):

and the rule of inference

Let KC(ml (resp. TC(ml· S4C(m) 1 S5C(m)) be the system that results from adding A7-All and R3 to the axioms for K<ml (resp. T<m>· S4<m>· S5<m1).

Theorem 16: For the language of common knowl­ edge, KC(ml (resp. TC(ml· S4C(mJ· S5C(m)) is a sound and complete axiomatization for Kripke worlds (resp. reflexive worlds, rt worlds, rst worlds). l><l

The common knowledge operator 0 adds a great deal of expressive power to the language. We can now make universal statements about what is true at all reachable worlds in the structure. One of the conse­ quences of this is that the analogues to Theorem 12 and Proposition 13 no longer hold. In fact we have:

Proposition 1 '1: There is a constant c > 0 such that for all n > 2, there is a formula Pn with IPn I = n that is KC- (resp. TC-, S4C<W· S5C<w) satisfiable, but is not satisfiable in any world (M, s) where M is a treelike structure (resp. reflexive closure, rt closure, rst closure of a treelike structure) of depth < 2Fn. l><l

Theorem 18: For m 2:: 2, the problem of decid­ ing the satisfiability of KC(ml (resp. TC(ml 1 S4C(ml 1 S5C(mJ) formulas is complete for exponential time. l><l

The proof of the exponential-time lower bound follows from techniques similar to those used in [FL] to prove a similar bound for PDL. The upper bound can be obtained using techniques of [Prj or [EH]. In fact, the techniques of [EH] allow us to combine the proof of the correctness of the algorithm with a proof of the completeness of the appropriate axiom system. Further details can be found in [HM2].

Besides the knowledge common to a group of agents, it is also often desirable to be able to reason about the knowledge that is implicit in the group, i.e., what someone who could combine the knowledge of all of the agents in the group would know.· Thus, for exam­ ple, if Alice knows p and Bob knows p ::::> q, then to­ gether they have implicit knowledge of q, even though it might be the case that neither of them individually knows q. Whereas common knowledge, in McCarthy's analogy, essentially corresponds to what "any fool" knows, implicit knowledge corresponds to what a (fic­ titious) "wise man" (one that knows exactly what each individual agent knows) would know. Implicit knowl­ edge is a useful notion in describing the total knowl­ edge available to a group of agents in a distributed environment (cf. [HM1]). Intuitively, a. group has im­ plicit knowledge of a fact if the knowledge of that fact is distributed among the members of a group. In a closed system, a group of cooperating agents cannot come to know a fact if it is not already implicit knowl­ edge In order to capture the notion of implicit knowl­ edge in our language, we add a new modal opera­ tor I that stands for "implicit knowledge". We can then capture implicit knowledge semantically as fol­ lows. Given a Kripke structure M = (S,1r, P11 ... , Pm) , we define

· Note that Levesque [Lev2] uses the term "implicit be­ lief" in a somewhat different sense than we do here. In his case, an agent's "explicit" beliefs are not de­ ductively closed, and the agent's "implicit" beliefs are roughly the deductive closure of his explicit beliefs.

The intuition behind this definition is that if all the agents could "put their knowledge together", the only worlds they would consider possible are precisely those in the intersection of the sets of worlds that each one individually considers possible. Put another way, if some agent knows that a world t is not the real world, then the "wise man" should know this too. Thus the wise man would only consider possible the worlds that all agents consider possible. Note that in the case of a single agent (i.e., m = 1), we have Ip = Kp; implicit knowledge just reduces to knowledge.

How can we be sure that this definition really does capture our intuitions regarding implicit knowledge? One way is to find a complete axiomatization. If we view I p as saying "the wise man knows p" , one axiom that suggests itself is

this axiom is easily seen to be sound with respect to the semantics given for I. We also expect the I operator to act like a knowledge operator, and indeed it is easy to see that it satisfies the axiom schema A2:

Moreover, if the P, relations are reflexive, so that knowl­ edge satisfies A3, then so does implicit knowledge; sim­ ilar remarks hold for A4 and A5. Let Kl<ml (resp. Tl(mJ· S41(mJ· S51(ml) be the system that results from adding axiom A12 to the axiom system K(mJ (resp. T(mJ· S4(ml· S5(ml) and assuming that I also satisfies axiom schemas A2, A3, A4, and A5 (where applica­ ble). Then we have

Theorem 19: For the language of implicit knowl­ edge with m 2:: 2 knowers, Kl(mJ (resp. Tl(mJ, S41(mJ, S51(ml) is a sound and complete axiomatization for Kripke worlds (resp. reflexive worlds, rt worlds, rst worlds). l><l We remark that if m = 1, we can get a com­ plete axiomatization for implicit knowledge simply by adding the axiom schema I p = K p to the axioms for knowledge.

In the discussion above, we also viewed implicit knowledge as the knowledge the agents would have by pooling their individual knowledge together. This sug­ gests the following rule of inference:

Again, this inference rule is easily seen to be sound with respect to the semantics for I given above. Intu­ itively it says that if q = q1 1\ ... 1\ qm implies p, and if each of the agents knows a "part" of q (in particu­ lar, agent i knows qi), then together they have implicit knowledge of q, and thus implicit knowledge of p.

It is easy to check that this inference rule is deriv­ able from axiom A2, A12, and propositional reasoning. Conversely, A12 is derivable from R4 and the other ax­ ioms for knowledge. Thus, we can replace A12 by R4 and get another complete axiomatization for implicit knowledge. We omit details here. Finally, we observe that the addition of the I operator does not essentially affect the complexity of the language. We can extend the techniques of Theorem 12 to show:

Theorem 20: For m ?: 2, the problem of deciding the satisfiability of KI(m) (resp. TI(m), S41(m), S5l(m)) formulas is PSPACE.complete.

6. Conclusions

We have investigated various classical modal log­ ics of knowledge and belief. It is reasonable at this point to consider to what extent these logics really do capture our intuitive notions. Our feeling in this re­ gard is that there are several useful notions of knowl­ edge and belief; some of them are captured by these logics, others are not. For example, consider a proces­ sor in a given distributed system that has received a certain set of messages (or a robot that has observed a certain set of facts). There are a number of global states of the system ("possible worlds") that are con­ sistent with the processor having received these mes­ sages (or the robot having made these observations). We can say that the processor knows p in this case if pis true in all these global states. Note that this is an "external" interpretation of knowledge, that does not require a processor to perform any reasoning to obtain knowledge, or even to be "aware" of this knowledge. This interpretation of knowledge precisely satisfies the S5<ml axioms, and turns out to be quite useful in prac­ tice (see [HM1] for further discussion).

When it comes to formalizing the reasoning of a knowledge base or of humans, computational complex­ ity must be taken into account. We cannot expect a program to carry out exponential-time algorithms, much less a human! On the other hand, we must be careful in interpreting the lower bounds on complexity we have presented in the previous sections. These are worst-case results, and there is no reason to believe that most cases of interest should act like the worst case. Indeed, the evidence suggests that just the op­ posite is true. The complexity of deciding formulas that humans are interested in tends to be much better than the worst-case analysis would indicate. We have noted that for one-knower S5 and KD45, the decision procedure for satisfiability offormulas is NP-complete, just as it is for propositional logic. Resolution methods have proved to be quite efficient in practice for propo­ sitional logic, and it seems that similar techniques can also be applied successfully to S5 and KD45. And the fact that there are successful practical theorem-provers for linear-time temporal logic, a modal logic whose sat­ isfiability problem is PSPACE.complete, suggests that this is a feasible task even for the many-knower ver­ sions of the logics we have been considering.

These observations suggest that the logics we have been considering may provide reasonable approxima­ tions to the reasoning carried out by a knowledge base, but they still do not seem realistic models for hu­ man reasoning. Humans simply do not seem to be logically omniscient [Hi2], in the sense of Theorem 1: they do not know all tautologies, nor is their knowl­ edge closed under deduction (i.e., it does not satisfy [K1p 1\ K1(p :::> q)] :::> K,q). A number of attempts have been made to modify the possible-worlds frame­ work to provide a more realistic semantic model of hu­ man reasoning. Most of these attempts have involved either allowing non-classical "impossible" worlds in ad­ dition to the regular possible worlds [Cr,Ra], using a non-classical truth assignment [Lev2,FH] or enriching the possible worlds with a syntactic "awareness" func­ tion [FH]. While none of these attempts appears as yet to provide the definitive solution, they do suggest that there is sufficient flexibility in the possible-worlds approach to make it worth pursuing.

Acknowledgements: We would like to thank Ron Fagin, Bob Moore, Nils Nilsson, and Moshe Vardi, for their helpful comments and criticisms. The first au­ thor would also like to thank the students of Stanford course CS400B for numerous interesting discussions on implicit knowledge.