7.2 Modal Epistemic Logic


7.2 Modal Epistemic Logic

I now move beyond propositional logic to a logic that allows reasoning about uncertainty within the logic. Perhaps the simplest kind of reasoning about uncertainty involves reasoning about whether certain situations are possible or impossible. I start with a logic of knowledge that allows just this kind of reasoning.

7.2.1 Syntax and Semantics

The syntax of propositional epistemic logic is just a slight extension of that for propositional logic. As an example, consider a propositional modal logic for reasoning about the knowledge of n agents. As in the case of propositional logic, we start with a nonempty set Φ of primitive propositions, but now there are also modal operators K1, , Kn, one for each agent. Formulas are formed by starting with primitive propositions and closing off under negation and conjunction (as in propositional logic) and the application of modal operators, so that if φ is a formula, so is Kiφ. Although Kiφ is typically read "agent i knows φ," in some contexts it may be more appropriate to read it as "agent i believes φ." Let Kn (Φ) be the language consisting of all formulas that can be built up this way; for notational convenience, I often suppress the Φ. The subscript n denotes that there are n agents; I typically omit the subscript if n = 1. I also make use of abbreviations such as , , and , just as in propositional logic.

Quite complicated statements can be expressed in a straightforward way in this language. For example, the formula

says that agent 1 knows that agent 2 knows p, but agent 2 does not know that agent 1 knows that agent 2 knows p. More colloquially, if I am agent 1 and you are agent 2, this can be read as "I know that you know p, but you don't know that I know that you know it."

Notice that possibility is the dual of knowledge. Agent i considers φ possible exactly if he does not know φ. This situation can be described by the formula Ki φ. A statement such as "Alice does not know whether it is sunny in San Francisco" means that Alice considers possible both that it is sunny in San Francisco and that it is not sunny in San Francisco. This can be expressed by formula KA p KA ( p), if p stands for "it is sunny in San Francisco."

When is a formula in modal logic true? Truth will be defined relative to a possible world in an epistemic frame. The truth conditions for conjunction and negation are the same as in propositional logic. The interesting case is a formula of the form Kiφ. Recall that an agent is said to know an event U in an epistemic frame if every world that the agent considers possible is in U. This intuition is also used to define the truth of Kiφ. The idea is to associate an event [[φ]] with the formula φ—the event consisting of the set of worlds where φ is true. Then Kiφ is true at a world w if i (w) [[φ]]. Roughly speaking, this says that Kiφ is true if φ is true at every world that agent i considers possible.

To get this definition off the ground, there must be some way of deciding at which worlds the primitive propositions are true. This is done by adding one more component to an epistemic frame. An epistemic structure (sometimes called a Kripke structure) for n agents is a tuple (W, 1,, n, π), where (W, 1, , n) is an epistemic frame, and π is an interpretation, a function that associates with each world in W a truth assignment to the primitive propositions. That is, π(w)(p) {true, false} for each primitive proposition p Φ and world w W. There may be two worlds associated with the same truth assignment; that is, it is possible that π(w) (w) for w w. This amounts to saying that there may be more to a world than what can be described by the primitive propositions.

In propositional logic, a formula is true or false given a truth assignment. In modal logic, of which this is an example, the truth of a formula depends on the world. A primitive proposition such as p may be true in one world and false in another. I now define under what circumstances a formula φ is true at world w in structure M = (W, 1,, n, π), written (M, w) φ. The definition proceeds by induction on the structure of formulas.

The first three clauses are the same as the corresponding clauses for propositional logic; the last clause captures the intuition that agent i knows φ if φ is true in all the worlds that i considers possible.

Recall that a system can be viewed as an epistemic frame. To reason about knowledge in a system using epistemic logic, an interpretation is needed. A pair J = (, π) consisting of a system and an interpretation π is called an interpreted system. Just as a system can be viewed as an epistemic frame, an interpreted system can be viewed as an epistemic structure. Satisfiability () can then be defined in interpreted systems in the obvious way. In particular,

7.2.2 Properties of Knowledge

One way to assess the reasonableness of the semantics for knowledge given in Section 7.2.1 is to try to characterize its properties. A formula φ is valid in an epistemic structure M, denoted M φ, if (M, w) φ for all w in M. (Of course, a world w is in M = (W, ) if w W.) A formula φ is satisfiable in M if (M, w) φ for some world w in M. If is a class of structures (e.g., the class of all epistemic structures, or the class of all epistemic structures where the i relations are equivalence relations), then φ is valid in (or with respect to) , denoted , if φ is valid in every structure in .

One important property of the definition of knowledge is that each agent knows all the logical consequences of his knowledge. If an agent knows φ and knows that φ implies ψ, then both φ and φ ψ are true at all worlds he considers possible. Thus ψ must be true at all worlds that the agent considers possible, so he must also know ψ. It follows that

is valid in epistemic structures. This property is called the Distribution Axiom since it allows the Ki operator to distribute over implication. It suggests that the definition of Ki assumes that agents are quite powerful reasoners.

Further evidence of this comes from the fact that agents know all the formulas that are valid in a given structure. If φ is true at all the possible worlds of structure M, then φ must be true at all the worlds that an agent considers possible in any given world in M, so it must be the case that Kiφ is true at all possible worlds of M. More formally, the following Rule of Knowledge Generalization holds:

Note that from this it follows that if φ is valid, then so is Kiφ. This rule is very different from the formula φ Kiφ, which says that if φ is true then agent i knows it. An agent does not necessarily know all things that are true. In Example 6.1.1, agent 1 may hold card A without agent 2 knowing it. However, agents do know all valid formulas. Intuitively, these are the formulas that are necessarily true, as opposed to the formulas that just happen to be true at a given world. It requires a rather powerful reasoner to know all necessarily true facts.

Additional properties of knowledge hold if the i relations satisfy additional properties. For example, if the i relation is transitive, then

turns out to be valid, while if the i relation is Euclidean, then

is valid. Imagine that an agent has the collection of all facts that he knows written in a database. Then the first of these properties, called the Positive Introspection Axiom, says that the agent can look at this database and see what facts are written there, so that if he knows φ, then he knows that he knows it (and thus the fact that he knows is also written in his database). The second property, called the Negative Introspection Axiom, says that he can also look over his database to see what he doesn't know. Thus, if he doesn't know φ, so that φ is not written in his database, he knows that φ is not written there, so that he knows that he doesn't know φ.

It is possible for Kifalse to hold at a world w in an epistemic structure, but only if it holds vacuously because i(w) is empty; that is, agent i does not consider any worlds possible at world w. If i is serial (so that i(w) is nonempty for all w), then Kifalse is valid.

If i is reflexive (which certainly implies that it is serial), then an even stronger property holds: what an agent knows to be true is in fact true; more precisely, Kiφ φ is valid in reliable structures. This property, occasionally called the Knowledge Axiom or the veridicality property (since "veridical" means "truthful"), has been taken by philosophers to be the major one distinguishing knowledge from belief. Although you may have false beliefs, you cannot know something that is false.

This discussion is summarized in the following theorem:

Theorem 7.2.1

start example

Suppose that M = (W, 1, , n, π) is an epistemic structure. Then for all agents i,

  1. M (Kiφ Ki(φ ψ)) Kiψ;

  2. if M φ then M Kiφ;

  3. if i is transitive, then M Kiφ KiKiφ;

  4. if i is Euclidean, then M Kiφ Ki Kiφ;

  5. if i is serial, then M Ki false;

  6. if i is reflexive, then M Kiφ φ.

end example

Proof

  1. If (M, w) Kiφ Ki(φ ψ), then (M, w) φ and (M, w) φ ψ for all worlds w i(w). It follows from the definition of that (M, w) ψ for all w i(w). Therefore, (M, w) Kiψ. Thus, (M, w) (Kiφ Ki(Φ ψ)) Kiψ. Since this is true for all w W, it follows that M (Kiφ Ki(Φ ψ)) Kiψ. (I omit the analogue of these last two sentences in parts (c), (d), and (f) and in all future proofs.)

  2. If M φ then (M, w) φ for all worlds w W. It immediately follows that (M, w) Kiφ for all w W (since i (w) W).

  3. Suppose that (M, w) Kiφ. Then (M, w) φ for all w i(w). Let w i(w). Since i is transitive, it follows that i(w) i(w). Thus, (M, w) φ for all w i(w), and so (M, w) Kiφ. Since this is true for all w i(w), it follows that (M, w) KiKiφ.

  4. Suppose that (M, w) Kiφ. Then (M, w′′) φ for some w i(w). Let w i(w). Since i is Euclidean, it follows that w i(w). Thus, (M, w) Kiφ. Since this is true for all w i(w), it follows that (M, w) Ki Kiφ.

  5. Choose w W. Since i is serial, there is some world w i(w). Clearly, (M, w) false. Thus, (M, w) Kifalse.

  6. If (M, w) Kiφ, then (M, w) φ for all w i(w). Since i is reflexive, w i(w). Thus, (M, w) φ.

Notice that the proof of part (a) did not start by assuming M Kiφ Ki(Φ ψ) and then go on to show that M Kiψ. M Kiφ means that (M, w) Kiφ for all w W ; this cannot be assumed in the proof of part (a). Showing that M (Kiφ Ki(Φ ψ)) Kiψ requires showing that (M, w) (Kiφ Ki(Φ ψ)) Kiψ for all W. This means that only (M, w) Kiφ Ki(Φ ψ) can be assumed. By way of contrast, note that the proof of part (b) shows that if M φ, then M Kiφ. It does not follow that M φ Kiφ. Just because φ is true, the agent does not necessarily know it!

Theorem 7.2.1 makes it clear how certain properties of knowledge are related to properties of the possibility relation. However, note that there are two properties that follow from the possible worlds approach, no matter what assumptions are made about the possibility relation: the Distribution Axiom and the Rule of Knowledge Generalization. To the extent that knowledge is viewed as something acquired by agents through some reasoning process, these properties suggest that this notion of knowledge is appropriate only for idealized agents who can do perfect reasoning. Clearly, this is not always reasonable. In the multi-agent systems model introduced in Section 6.3, knowledge is ascribed to agents in a multi-agent system based on their current information, as encoded in their local state. This notion of knowledge explicitly does not take computation into account. While it is useful in many contexts, not surprisingly, it is not adequate for modeling agents who must compute what they know.

7.2.3 Axiomatizing Knowledge

Are there other important properties of the possible-worlds definition of knowledge that I have not yet mentioned? In a precise sense, the answer is no. All the properties of knowledge (at least, in the propositional case) follow from those already discussed. This can be formalized using the notions of provability and sound and complete axiomatization.

An axiom system AX consists of a collection of axioms and inference rules. An axiom is just a formula, while a rule of inference has the form "from φ1, , φk infer ψ," where φ1, , φk, ψ are formulas. An inference rule can be viewed as a method for inferring new formulas from old ones. A proof in AX consists of a sequence of steps, each of which is either an instance of an axiom in AX, or follows from previous steps by an application of an inference rule. More precisely, if "from φ1, , φk infer ψ" is an inference rule, and the formulas φ1, , φk have appeared earlier in the proof, then ψ follows by an application of this inference rule. A proof is a proof of the formula φ if the last step of the proof is φ. A formula φ is provable in AX, denoted AX φ, if there is a proof of φ in AX.

Suppose that is a class of structures and is a language such that a notion of validity is defined for the formulas in with respect to the structures in . For example, if = Prop, then could consist of all truth assignments; if = Kn, then could be the class of epistemic structures. An axiom system AX is sound for with respect to if every formula of that is provable in AX is valid in every structure in . AX is complete for with respect to if every formula in that is valid in every structure in is provable in AX. AX can be viewed as characterizing the class if it provides a sound and complete axiomatization of that class; notationally, this amounts to saying that AX φ iff θ for all formulas φ. Soundness and completeness provide a connection between the syntactic notion of provability and the semantic notion of validity.

There are well-known sound and complete axiomatizations for propositional logic (see the notes to this chapter). Here I want to focus on axioms for knowledge, so I just take for granted that all the tautologies of propositional logic are available. Consider the following collection of axioms and inference rules:

  • Prop. All substitution instances of tautologies of propositional logic.

  • K1. (Kiφ Ki(φ ψ)) Kiψ (Distribution Axiom).

  • K2. Kiφ φ (Knowledge Axiom).

  • K3. Ki false (Consistency Axiom).

  • K4. Kiφ KiKiφ (Positive Introspection Axiom).

  • K5. Kiφ Ki Kiφ (Negative Introspection Axiom).

  • MP. From φ and φ ψ infer ψ (Modus Ponens).

  • Gen. From φ infer Kiφ (Knowledge Generalization).

Technically, Prop and K1–5 are axiom schemes, rather than single axioms. K1, for example, holds for all formulas φ and ψ and all agents i = 1, , n. Prop gives access to all propositional tautologies "for free." Prop could be replaced by the axioms for propositional logic given in the notes to this chapter. Note that a formula such as K1q K1q is an instance of Prop (since it is a substitution instance of the propositional tautology p p, obtained by substituting K1q for p).

Historically, axiom K1 has been called K, K2 has been called T, K3 has been called D, K4 has been called 4, and K5 has been called 5. Different modal logics can be obtained by considering various subsets of these axioms. One approach to naming these logics is to name them after the significant axioms used. In the case of one agent, the system with axioms and rules Prop, K (i.e., K1), MP, and Gen has been called K. The axiom system KD45 is the result of combining the axioms K, D, 4, and 5 with Prop, MP, and Gen; KT4 is the result of combining the axioms K, T, and 4 with Prop, MP, and Gen. Some of the axiom systems are commonly called by other names as well. The K is quite often omitted, so that KT becomes T, KD becomes D, and so on; KT4 has traditionally been called S4 and KT45 has been called S5. I stick with the traditional names here for those logics that have them, since they are in common usage, except that I use the subscript n to emphasize the fact that these are systems with n agents rather than only one agent. I occasionally omit the subscript if n = 1, in line with more traditional notation. In this book I focus mainly on S5n and KD45n.

Philosophers have spent years arguing which of these axioms, if any, best captures the knowledge of an agent. I do not believe that there is one "true" notion of knowledge; rather, the appropriate notion depends on the application. For many applications, the axioms of S5 seem most appropriate (see Chapter 6), although philosophers have argued quite vociferously against them, particularly axiom K5. Rather than justify these axioms further, I focus here on the relationship between these axioms and the properties of the relation.

Theorem 7.2.1 suggests that there is a connection between K4 and transitivity of i, K5 and the Euclidean property, K3 and seriality, and K2 and reflexivity. This connection is a rather close one. To formalize it, let n consist of all structures for n agents, and let rn (resp., rtn; rstn; eltn; etn) be the class of all structures for n agents where the possibility relations are reflexive (resp., reflexive and transitive; reflexive, symmetric, and transitive; Euclidean, serial, and transitive; Euclidean and transitive).

Theorem 7.2.2

start example

For the language K,

  1. Kn is a sound and complete axiomatization with respect to n

  2. Tn is a sound and complete axiomatization with respect to rn

  3. S4n is a sound and complete axiomatization with respect to rtn

  4. K45n is a sound and complete axiomatization with respect to etn

  5. KD45n is a sound and complete axiomatization with respect to eltn

  6. S5n is a sound and complete axiomatization with respect to rstn

end example

Proof Soundness follows immediately from Theorem 7.2.1. The proof of completeness is beyond the scope of this book. (See the notes to this chapter for references.)

This theorem says, for example, that the axiom system S5n completely characterizes propositional modal reasoning in rstn. There are no "extra" properties (beyond those that can be proved from S5n) that are valid in structures in rstn.

7.2.4 A Digression: The Role of Syntax

I have presented logic here using the standard logician's approach (which is also common in the philosophy and AI communities): starting with a language and assigning formulas in the language truth values in a semantic structure. In other communities (such as the statistics and economics communities), it is more standard to dispense with language and work directly with what can be viewed as frames. For example, as I already observed in Section 6.2, a probability space can be viewed as a simple probability frame. Economists quite often use epistemic frames, where the is are equivalence relations or even epistemic probability frames (typically satisfying SDP).

It is not possible to give formulas a truth value in an epistemic frame. There is no interpretation π to even give a truth value to primitive propositions. Nevertheless, economists still want to talk about knowledge. To do this, they use a knowledge operator that works directly on sets of possible worlds. To understand how this is done, it is best to start with the propositional operators, and . Each of these can be associated with an operation on sets of worlds. The operator corresponding to is intersection, and the operator corresponding to is complementation. The correspondence is easy to explain. Given an epistemic structure M = (W, 1, , n, π), let [[φ]]M ={w : (M, w) φ}. Thus, [[φ]]M, called the intension of φ, is the event corresponding to φ, namely, the set of worlds where φ is true. Then it is easy to see that [[φ ψ]]M = [[φ]]M [[ψ]]M—that is, the event corresponding to φ ψ is the intersection of the events corresponding to φ and to ψ. Similarly, [[ φ]]M = [[φ]]M. The semantic analogue of Ki turns out to be the operator Ki on sets, which is defined so that Ki(U) = {w : i(w) (U). I was essentially thinking in terms of the Ki operator when I defined knowledge in Section 6.1. The following proposition makes precise the sense in which Ki is the analogue of i:

Proposition 7.2.3

start example

For all formulas φ and ψ,

  1. [[φ ψ]]M = [[φ]]M [[ψ]]M,

  2. [[ φ]]M = [[φ]]M,

  3. [[Kiφ]]M = Ki([[φ]]M).

end example

Proof See Exercise 7.5.

Not surprisingly, Ki satisfies many properties analogous to Ki.

Proposition 7.2.4

start example

For all epistemic frames F = (W, 1, , n), the following properties hold for all U, V W and all agents i:

  1. Ki(U V) = Ki(U) Ki(V),

  2. if i is reflexive, then Ki(U) U,

  3. if i is transitive, then Ki(U) Ki(Ki(U)),

  4. if i is Euclidean, then Ki(U) Ki(Ki(U)).

end example

Proof See Exercise 7.6.

Part (a) is the semantic analogue of Ki(Φ ψ) (Kiφ Kiψ), which is easily seen to be valid in all epistemic structures (Exercise 7.7). Parts (b), (c), and (d) are the semantic analogues of axioms K2, K4, and K5, respectively.

For reasoning about a fixed situation, there is certainly an advantage in working with a frame rather than a structure. There is no need to define an interpretation π and a satisfiability relation ; it is easier to work directly with sets (events) rather than formulas.

So why bother with the overhead of syntax? Having a language has a number of advantages; I discuss three of them here.

  • There are times when it is useful to distinguish logically equivalent formulas. For example, in any given structure, it is not hard to check that the events corresponding to the formulas Kitrue and Ki((p q) (q p)) are logically equivalent, since (p q) (q p) is a tautology. However, a computationally bounded agent may not recognize that (p q) (q p) is a tautology, and thus may not know it. Although all the semantics for modal logic that I consider in this book have the property that they do not distinguish logically equivalent formulas, it is possible to give semantics where such formulas are distinguished. (See the notes to this chapter for some pointers to the literature.) This clearly would not be possible with a set-based approach.

  • The structure of the syntax provides ways to reason and carry out proofs. For example, many technical results proceed by induction on the structure of formulas. Similarly, formal axiomatic reasoning typically takes advantage of the syntactic structure of formulas.

  • Using formulas allows certain notions to be formulated in a structure-independent way. For example, economists are interested in notions of rationality and would like to express rationality in terms of knowledge and belief. Rationality is a complicated notion, and there is certainly no agreement on exactly how it should be defined. Suppose for now though that the definition of what it means to be rational is a formula involving knowledge (and perhaps other operators; see the references in the notes for some discussion). The formula can then be used to identify corresponding events (such as "agent 1 is rational") in two different structures.

Similarly, formulas can be used to compare two or more structures that, intuitively, are "about" the same basic phenomena. For a simple example, consider the following two epistemic structures. In M1, both agents know the true situation. There are two worlds in M1: in one, p is true, both agents know it, know that they know it, and so on; in the other, p is false, both agents know it, know that they know it, and so on. In M2, agent 1 knows the true situation, although agent 2 does not. There are also two worlds in M2: in one, p is true and agent 1 knows it; in the other, p is false and agent 1 knows that it is false; agent 2 cannot distinguish these two worlds. Figure 7.1 (where self-loops are omitted) illustrates the situation:

click to expand
Figure 7.1: Two related epistemic structures.

Notice that K1p K1 p holds in every state of both M1 and M2, while K2p K2 p holds in both states of M1, but not in both states of M2. Using formulas makes it possible to relate M1 and M2 in a way that cannot be done using events. Formulas such as p and K1p are represented by totally different sets in M1 and M2. That is, the set of worlds where p is true in M1 bears no relationship to the set of worlds where p is true in M2, and similarly for K1p. Nevertheless, it seems reasonable to say that these sets correspond in some way. There is no obvious way to do that without invoking a language.




Reasoning About Uncertainty
Reasoning about Uncertainty
ISBN: 0262582597
EAN: 2147483647
Year: 2005
Pages: 140

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net