Reasoning about Information Change.
In this paper we introduce Dynamic Epistemic Logic, which is a logic for reasoning about information change in a multi-agent system. The information structures we use are based on non-well-founded sets, and can be conceived as bisimulation classes of Kripke models. On these structures, we define a notion of information change that is inspired by Update Semantics (Veltman, 1996). We give a sound and complete axiomatization of the resulting logic, and we discuss applications to the puzzle of the dirty children, and to knowledge programs.
Introduction
Recently the notions of information and information change have gained a
prominent place in several fields of scientific research, such as philosophy, the
formal semantics of natural language and computer science. The present paper
highlights two of such developments, namely the update semantics of Veltman
(1996), and the analysis of communication in distributed systems, in particular
the approach of Fagin et al. (1995). Our main goal here is to show that tools of
the former may provide useful supplements to the approach of the latter.
Update Semantics
In his influential paper 'Defaults in Update Semantics,' Frank Veltman presents
a dynamic view on meaning. Following the slogan "You know the meaning of
a sentence if you know the change it brings about in the information state of
anyone who accepts the news conveyed by it," the meaning of a sentence is
associated with a function on information states. We will discuss Veltman's
update semantics as a simple example to illustrate the main notions involved.
The language of update semantics is a standard propositional modal language.
Definition 2.1 (Language) Given a set of propositional variables P , the language
LP of update semantics is the smallest set containing P such that if OE
and / are in LP , then OE - /, :OE and 3OE are in LP . 2
As said, we will interpret sentences as functions on information states. The
notion of information state used in update semantics is a very simple one. 1
Definition 2.2 (Information states)
ffl A possible world w assigns to each propositional variable a truth-value; it
is a function 1g.
ffl An information state oe is a set of possible worlds. 2
Veltman introduces more complex notions of information state to model reasoning with
default rules.
Intuitively, if an agent is in information state oe, then oe contains all worlds
that are compatible with the agent's information: for all the agent knows, each
possible world in oe may picture reality correctly. For example, the information
state consisting of the set of all possible worlds represents an information state
of an agent that has no information about the world at all, and the empty set
is an information state in which an agent has contradictory information.
When oe is an information state, and OE a sentence, we will write oe[OE] for
the result of updating oe with the sentence OE. Intuitively, oe[OE] is the state that
results when the agent, being in state oe, gets the information expressed by OE.
Definition 2.3 (Interpretation)
ae
oe if oe[OE]
update of an information state oe with a sentence p results in a state containing
all and only the worlds in oe in which p is true. The result of updating
a state oe with a negated sentence is a state containing all worlds in oe that do
not survive in oe updated with OE. Conjunction is defined as intersection.
A sentence of the form 3OE gets an interpretation roughly corresponding to
the intuitive meaning of 'It might be the case that OE.' An update of oe with
3OE either returns the same information state (when oe updated with OE does
not result in the empty state, i.e. when OE is compatible with the information
contained in oe), or it returns the inconsistent state (when OE is not compatible
with the information contained in oe). This reflects the assumption that an
agent in a state oe already knows what she considers possible and what not,
which means that a sentence of the form 'It might be that.' can never provide
new information; at most, it can be inconsistent with the information contained
in oe.
Definition 2.4 (Acceptance and validity)
ffl A sentence OE is accepted in an information state oe iff
oe k\Gamma\Gamma OE.
ffl A sequence of sentences acceptable iff there is a oe such that
ffl An argument OE updating any information state with
the premises in the order they are given, result in a state in which the
conclusion is accepted:
A sentence is accepted in an information state if an update with OE does not
change the information state. Intuitively, this happens only when the information
that OE is already contained in oe. A sequence of sentences is acceptable
when there is a state in which updating with the sentences in the order they
are given does not result in the inconsistent empty state. An argument is valid
iff updating an information state with the premises in the order they are given,
results in a state in which the conclusion is accepted.
One of the interesting features of update semantics is that the order in
which sentences in a text occur is important. In general, it is not the case that
correctly reflects the fact that changing the order of the
sentences of a text will in general produce a different story, which need not even
be coherent. Consider for example the following two examples:
Someone is knocking at the door.It might be John.It is Mary.
Someone is knocking at the door.It is Mary.It might be John.
The first sequence of sentences is acceptable, while the second is not: once one
knows it is Mary who is knocking at the door, it cannot be John anymore. This
is reflected in update semantics: 3p; :p is acceptable, while :p; 3p is not.
Another feature of update semantics is that updates always imply an increase
of information, in the sense that an update of an information state oe always
results in a state that is a subset of oe. i.e. oe[OE] ' oe. But this does not mean all
sentences that are accepted in the first state are also accepted in the updated
state. A typical case is a state oe containing two worlds w and v, with
and This is a state in which the agent does not know whether p is
true or not. In such a state, 3p is accepted. But as soon as the agent learns
that p is not the case, p is not considered possible anymore: in the state oe[:p],
3p is not accepted.
3 Dynamic Epistemic Semantics
Update semantics is a semantics that models the information change of a single
agent. In this section, we develop a semantics for a language in which it is
possible to express facts about the information and information change of several
agents. 2 The language is the following:
Definition 3.1 (Language of DES)
Let A be a non-empty set of agents, and let P be a set of propositional atoms.
The language L A
P of DES is the smallest set such that P ' L, and if OE and /
are in L A
P , and a 2 A, then :OE; OE - /; 2 a OE and [OE] a / are in L A
2 For an approach that uses a similar language, and employs a notion of constructive update
over partial Kripke models, see Jaspars (1994).
Other logical constants, such as -, ! and 3 a , are defined in the standard way.
We will refer to the part of the language that does not contain the [\Delta] a -operator
as the 'classical fragment of the language'. This is just the language of classical
multi-modal logic.
The intended interpretation of 2 a OE is that agent a has the information that
OE. The intended meaning of [OE] a / is that an update of a's information with OE
results in a situation where / is true. There is an operator [OE] a for each agent a
and each sentence OE in the language, which reflects the idea that any statement
about the system of agents and their beliefs is something which the the agents
may learn. This makes the agents effectively as 'intelligent' as us theoreticians,
i.e. in principle any property of the system we are able to formulate in the
object language may be known or learned by the agents.
To give a semantics for this language, we first need to make a choice as to
how to represent the information of the agents. We believe that a representation
that is based on non-well-founded sets is the most elegant way to do this. 3
Definition 3.2 (Possibilities)
Let A, a set of agents, and P , a set of propositional variables, be given.
ffl A possibility w is a function that assigns to each propositional variable
1g, and to each agent a 2 A an information
state w(a).
ffl An information state oe is a set of possibilities. 2
Clearly, this definition is circular, since possibilities are defined in terms of information
states, and information states are sets of possibilities. In the universe
of non-well-founded sets of Aczel (1988), this circularity is harmless. 4
A possibility w characterizes which propositions are true and which are false
by assigning to each atomic sentence a truth value, and it characterizes the
information of each of the agents by assigning to each agent an information
state. The information of an agent is represented, as it is in update semantics,
as a set of possible ways the world might be, according to that agent. In this
case, this is a set of possibilities.
There is a close relation between these non-well-founded models and Kripke-
structures; to be precise, there is a one-one-relation between possibilities and
bisimulation classes of worlds in Kripke models, that preserves truth of the
classical fragment of the language.
Definition 3.3 Let (R a
A decoration of M is a function that assigns to each w 2 W a function d(w) on
such that
3 See Groeneveld (1995) for a discussion of the semantics of DES using Kripke models and
the knowledge structures of Fagin and Halpern (Fagin et al. 1991).
4 The underlying set-theory is axiomatized by ZFC \Gamma (the Zermelo-Fraenkel axioms minus
the axiom of foundation) plus Aczel's Anti-Foundation Axiom (AFA).
assigns to each propositional variable the
same truth-value as it has in w in the model.
assigns to each agent a the set of
functions associated with worlds reachable from w by R a .
If d is a decoration of M , and w a world in M , we say that d(w) is the solution
of w in M , and (M;w) is a picture of d(w). 2
Proposition 3.4
ffl Each Kripke model M has a unique decoration. This decoration assigns
to each world in M a possibility.
ffl Each possibility has a picture.
ffl w in M and w 0 in M 0 have the same solution iff w and w 0 are bisimilar. 2
This means that possibilities can be seen as representing bisimulation classes of
worlds in Kripke models. Moreover, it implies the Bisimulation Principle (3.5
below) which we will frequently use later. In the following definition, we use the
notation w[B]v, for B a set of agent, to stand for the fact that w and v differ at
most from each other in the information states they assign to agent in B.
Proposition 3.5 (Bisimulation Principle) A bisimulation between possibilities
is any relation B such that wBv iff w[A]v and for each a 2 A, if w
there is a v 0 2 v(a) such that w 0 Bv 0 , and if v 0 2 v(a), then there is a w
such that w 0 Bv 0 .
If B is a bisimulation, then for all possibilities w; v: if wBv then
Properties of possibilities
One of the charms of Kripke semantics is the fact that properties of information
such as positive introspection or consistency correspond to certain simple
properties on frames, such as transitivity and seriality of the accessibility rela-
tions. Here are some examples of constraints on possibilities that correspond to
familiar frame constraints.
Definition 3.6 Call a class of possibilities S closed iff it holds that if w 2 S
1. C, the class of consistent possibilities is the largest closed class such that
2. T , the class of truthful possibilities is the largest closed class such that
3. P , the class of positive introspective possibilities is the largest closed class
such that w 2 P and v 2 w(a) imply v(a) ' w(a)
4. N , the class of negative introspective possibilities is the largest closed class
such that w 2 N and v 2 w(a) imply w(a) ' v(a) 2
Of special interest is the class of fully introspective possibilities P " N (which
is a closed class).
Conscious updates
In update semantics, if an agent updates her information with p she will discard
all possible worlds in which p is false. But if her epistemic alternatives are not
classical possible worlds, but possibilities as we have defined them, there will
be no point in also preserving those options in which p is true but in which the
agent does not have the information that p. Ideally, she will also accommodate
for the fact that she has learned p, and after having learned that p, she will not
only have the information that p, but on top of that have the information that
she has the information that p. And so on. We will refer to such an update as a
'conscious' update: the agent who gets new information is conscious of the fact
that she gets this new information.
Note that this is not an 'eliminative' process. A conscious update is not
one in which one simply discards possibilities to reach a state in which one
has more information. For example, consider a situation in which an agent a
does not know whether p, and knows that she does not know this. This will
be modeled by a possibility w such that the set of possibilities w(a) will only
contain possibilities in which a does not know whether p. Removing all non-p-
possibilities from this information state leaves the agent with a set of possibilities
in which p is true, but in which she does not know whether p.
We use the idea of conscious update for for interpreting sentences of the
form [OE] a /, which will be interpreted as 'after a consciously updates with OE,
/ is true.' To do this, we first have to give a formal definition of conscious
update. We will define for each sentence OE and each a 2 A a function [[OE]] a on
possibilities in such a way that applying this function to a possibility returns a
new possibility that is the result of updating a's information state consciously
with the information that OE. Remember that we use the notation w[a]v as an
abbreviation for the statement that w and v differ at most in the information
state they assign to a.
Definition 3.7 (Conscious updates)
a is that w 0 such that w[a]w 0 and w OEg.
So a conscious update of a's information in a possibility w changes the possibility
w in such a way that only a's information state is changed (i.e. the new
possibility differs from the old one only in the information state that is assigned
to a), and this is done in the following way: all possibilities in which OE is not
true are eliminated from a's information state, and in all remaining possibilities,
a's information state is consciously updated with OE.
That this notion of update is well-defined needs some proof. We will rely on
the Solution Lemma of Aczel (1988), which is standardly used in the set theory
ZFC/AFA for establishing the existence of non-well-founded sets, to prove that
that there is in fact a relation that conforms to definition 3.7. Then, we will
give an argument using the bisimulation principle to show that this relation is
the only relation conforming to the definition.
To prove the existence of the update function, fix an actor a 2 A and
some proposition p (i.e. p is a class of possibilities). For each possibility w,
introduce an indeterminate xw , and consider the class of equations defined by
the stipulations
ag [ f(a; fx
By the Solution Lemma this system has a unique solution, which in this case is a
map - from indeterminates to possibilities. Then define cu(a; p), the conscious
update with p for a by
It is not hard to check that it holds that (w; v) 2 cu(a; p) iff w[a]v and
which shows that cu(a; p) is the
function we were looking for.
To show that the update function is unique for each OE and a, assume that
there are in fact two functions f and f 0 that conform to definition 3.7. Note
that by the definition, both of these functions will be total on the class of all
possibilities. We will show that it holds for each possibility w, that
(w). For define a relation B as:
We claim that B is a bisimulation, from which it follows by the bisimulation
principle that so we need to show that for each w
there is a v 0 2 v(a) such that w 0 Bv 0 , and vice versa. Take any w 0 2 w(a). Then,
there must be a u 0 2 u(a) such that u 0
f 0 is a total function, there must be a v 0 2 v(a) such that f 0
this v 0 it holds that w 0 Bv 0 . The other direction is completely symmetric, which
shows that B is a bisimulation.
Definition 3.8 (Truth)
Technically we have to conceive of definitions 3.7 and 3.8 as one simultaneous
definition, since the definition of update uses the notion of truth and vice versa.
This offers no problems, however, and we have only separated the two for clarity.
All classical logical operators are interpreted classically: a conjunction is true
just in case both conjuncts are, a negation is true iff the negated sentence is not
true, 2 a OE is true just in case OE is true in each possibility in a's information state.
New is the definition for [OE] a /: such a sentence is true in a possibility w exactly
when / is true in the possibility that results from updating a's information state
in w with OE. We define validity in the standard way, i.e. for each
possibility w, and for each set of sentences \Gamma, \Gamma for each possibility w
such that w
Update Semantics
It turns out that validity in update semantics can be expressed in DES by
identifying a US-update with a conscious update in DES in a fully introspective
possibility. The validity of an argument-updating with the premises results in
an information state in which the conclusion is accepted-can then be expressed
in DES by a sentence expressing that after an agent consciously updates with the
premises, then she will accept the conclusion, i.e. she will have the information
that the conclusion holds.
Proposition 3.9 Let for each OE in the language of update semantics, OE 0 be just
like OE, except that each occurrence of 3 is replaced by 3 a . Then:
fully introspective w, w
Group Updates
Common knowledge is a concept that crops up in several places in the literature
on distributed systems in computer science, in the literature on game theory in
philosophy and economics and in the literature on pragmatics in linguistics. The
concept is most easily explained as follows: a sentence OE is common knowledge
between a group of agents B just in case each agent in B knows OE, each agent
knows of each other agent that he knows OE, and so on.
What we will do here is model the effect of a sentence becoming common
knowledge between a certain group of agents, and add operators [OE] B for each
A to express this in the object language. Such an operator may be useful,
for example, to formalize an idea in the theory of discourse that the purpose of
an assertion is to extend the common knowledge of speaker and hearer.
Definition 3.10 (Conscious group update)
B is that w 0 such that w[B]w 0 and w
for each a 2 B.
A group update with OE in a possibility w results in a new possibility in which
only the information of the agents in the group has changed. For each agent in
the group, the new information state consists of all the old possibilities in which
OE is true updated with the information that OE becomes common knowledge
between the agents in the group.
This definition is structurally similar to the definition given for conscious
updates above. In fact, it holds that for each w, w[[OE]] a = w[[OE]] fag . Also,
the proof that definition 3.10 is in fact correct is entirely analogous to the
coinduction argument we gave for definition 3.7, for which reason we won't
repeat the argument.
We can now extend the truth definition of DES with the following clause:
Axiomatization
In this section, we provide an axiomatization of the language of DES with group
updates, and prove that it is sound and complete with respect to the semantics.
Definition 3.11 (Conscious K)
The system CK is defined by the following axioms and rules.
Axioms
is valid in classical propositional logic
A3
is an atom. (independence)
(Generalized Ramsey Axiom)
a OE if a 62 B. (Privacy Axiom)
Rules
Nec2 If ' OE then ' 2 a OE
Nec[\Delta] If ' OE then ' [/] B OE
there is a derivation of OE from assumptions in \Gamma. 2
So, in addition to the rules and axioms of classical model logic, the deduction
system consists axioms describing the interaction between the dynamic operators
and the classical logical constants. Axiom 3 together with the rule Nec[\Delta]
guarantee that the dynamic operators behave as normal modal operators. Axiom
4 expresses that updates are functional: if it is not the case that a certain
sentence is true after an update with a certain sentence, then, since the update
always gives a unique result, it must be the case that the negation of that sentence
is true in the updated possibility. Axiom 5 expresses that the update of
an information state has no effect on the 'real' world; the same propositional
atoms will be true or false before and after an update. Axiom 6 expresses that
if it is the case that after a group update with OE, some agent in the group knows
that /, then that agent already knew that if OE were true, then after a group
update with OE, / would be true, and vice versa. Axiom 7, finally, expresses that
a group update has no effect on the information of agents outside of that group.
Proposition 3.12 (Soundness) If \Gamma 'CK OE then \Gamma
proof: A standard induction; by way of illustration, we show the correctness
of axiom 6, and leave the remaining cases to the reader. We have the following
equivalences, if a 2 B:
Proposition 3.13
proof: We use a variation on the classical Henkin proof for completeness of
modal logic, showing that for each consistent set of sentences there is a possibility
in which these sentences are true.
It is easy to show that each consistent set can be extended to a maximal
consistent set (we will refer to this as 'Lindenbaum's Lemma'). Let, for each
maximal consistent set \Sigma, w \Sigma be that possibility such that w \Sigma
and for each agent b: w \Sigma consistent and if 2 b / 2 \Sigma,
then \Gammag. 5 We prove the usual Truth Lemma, that is, for each sentence
- it holds that - 2 \Sigma iff w \Sigma Completeness then follows by standard
argumentation. The Truth Lemma is proven by an induction on the structure
of -, in which all cases are standard, except the case where - is of the form
5 In the terminology of definition 3.3, this model is the solution of the standard canonical
model for the minimal modal logic K. Alternatively, the existence of the possibilities w \Gamma is
easily proven by defining the appropriate set of equations, and an appeal to the Solution
Lemma.
/. The proof for this case rests on the following idea. Just as membership
in w \Sigma (a) depends on the formulae of the form 2 a OE in \Sigma, the B-update of w \Sigma
with OE depends on the formulae of the form [OE] B / in \Sigma. This is reflected by the
following operation on maximal consistent sets:
\Gammag
The functionality axiom A4 will ensure that will be a maximal consistent
set whenever \Gamma is. The step in the Truth Lemma for formulae of the form [OE] B /
then proceeds as follows:
(by 3.14 and induction hypothesis on OE)
(by induction hypothesis on /)
(by definition of \Sigma ffl B OE)
Which only leaves the next lemma. 2
Lemma 3.14 Let OE be fixed, and assume that for each maximal consistent \Sigma,
proof: Define a relation R on possibilities by
there exists a maximal consistent
set \Sigma such that
We will show that R is a bisimulation. The Bisimulation Principle 3.5 then
implies that R actually is an identity relation, which proves the lemma.
Let wRv, and suppose (the case that
easy). We need to show three things:
1. w[A]v.
(by the semantics) iff p 2 \Sigma (by the definition
of
2. Next we must show that for each b 2 A, if w 0 2 w(b) then there is a
We distinguish two cases: b 2 B, and b 62 B.
Assume that b 62 B. It then follows by axiom 7 that
which implies that w \Sigma (b). But by the definition of
and the fact that b 62 B, we have w \Sigma actually
v(b) in this case, which is certainly sufficient.
For the other case, let b 2 B and take any w (b). Then there
must be a \Sigma 0 that is maximal consistent such that w \Sigma 0
and w \Sigma (b). The latter implies that if 2 b - 2 \Sigma, then - 2 \Sigma 0 .
We want to find a v 0 such that (I) v
the set \Sigma . It is then immediate that (II)
holds. To see that (I) holds, take any 2 b / 2
and hence, by axiom
Because w \Sigma 0 by the main assumption of this lemma that
which means that / 2 \Sigma
was arbitrary, it follows that w \Sigma (b), which is what we wanted
to prove.
3. Finally we must show that for each b 2 A, if v 0 2 v(b) then there is a
If b 62 B, we can use the same argument as in case (2). So assume instead
that b 2 B, and take any w (b).
Consider the set \Sigmag. Below we
show that \Delta is consistent (III). Then \Delta can be extended by Lindenbaum's
Lemma to a maximal consistent set \Sigma 0 , for which it holds, by definition
of \Delta that w \Sigma This implies that w \Sigma 0
it is not hard to see that by definition of \Delta and the
functionality axiom it holds that It then follows that that
To see (III), suppose to the contrary that \Delta is inconsistent. Then there
must be
That means that:
(using A3 and A4)
which means that
by the fact that
contradicting the fact that \Gamma is consistent.Some observations and remarks
Here follows a short list of validities and non-validities.
Proposition 3.15
1. (there is no difference between updating with
updating with / - OE)
2. (updating first with OE and then with / is different
from updating with / first, and after that with OE.)
3. (updates of the information of one
group does not affect updates of the information of a disjoint group)
4. If ' OE (if two sentences have the same truth
conditions, they are also equivalent as updates)
It is possible to combine the notion of conscious update with stronger epistemic
logics. This is unproblematic for the logic of introspection: if we add the
introspection axioms of K45 to the axioms of CK, the resulting logic CK45 is
sound and complete with respect to the class of introspective possibilities. For
other well known epistemic logics such as KD45 or S5, updates will be partial
functions, since conscious updates don't necessarily preserve the properties of
consistency and correctness.
We sketch some details for one special case, S5. We take K to be the class of
truthful and introspective possibilities (positive and negative; see definition 3.6).
The K-update
a is then defined as the restriction of [[OE]] a to possibilities in
K. This will make the updates partial functions. For example, for an atom p this
will have the effect that an agent a can only learn p in a possibility w if w As
for the effect on the axiomatics, we conjecture that the following is complete:
add the axioms of S5 to CK; weaken the functionality axiom to :[OE] a
[OE] a :/; and compensate the loss of the existential part of the functionality
axiom by adding the axiom hOEi a ?
We end this brief discussion by a comment on our choice of operators. We
could have added operators of the form CB to the language, one for each (non-
empty) set of agents B, to express the static concept of OE being common knowledge
between the agents in B. Transferring the definition of Fagin et al. (1995)
to our framework, its definition could be the following:
an OE for each an
The reason we have not added these operators is that we have not yet found
an axiomatization for the language with these operators. We hope to correct
this omission in the near future.
4 An application: Automated Dirty Children
We have developed a language and a semantics for reasoning about information
and information change of several agents, which in turn can reason about their
own information and the information of other agents. We have provided an
axiomatization for this semantics. In this section, we want to show that the
logic developed above can be useful as a tool for analyzing problems concerning
reasoning about information in a multi-agent setting. To show this, we consider
a textbook case, the puzzle of the dirty children. This puzzle occurs under
different guises in the literature: it is a variant of the puzzle of the cheating
husbands (see for example Moses et al., 1986), the wise men puzzle (in e.g.
McCarthy, 1990) and the the Conway-paradox (e.g. van Emde Boaz et al., 1980).
The puzzle
The description of the dirty children puzzle that we give here is adapted from
Barwise (1981).
There are n children playing together. During their play some of the children,
say k of them, get mud on their foreheads. Each can see the mud on others
but not on his own forehead. Along comes a father, who says, "At least one
of you has mud on your head." He then asks the following question, over and
over: "Can any of you prove that you have mud on your head?" Assuming
that all the children are perceptive, intelligent, truthful, and that they answer
simultaneously, what will happen?
There is a "proof" that the first k \Gamma 1 times the father asks the question,
the children will all say "no" but that the k-th time the children that are dirty
will answer "yes."
The proof is by induction on the number of dirty children k. For
result is obvious: the dirty child sees that no one else is muddy, so he must
be the muddy one. If there are two dirty children, say a and b, each answers
"no" the first time, because of the mud on the other. But, when b says "no," a
realizes he must be muddy, for otherwise b would have known the mud was on
his head and answered "yes" the first time. Thus a answers "yes" the second
time. b goes through the same reasoning. Now suppose there are three dirty
children, a, b, c. Child a argues as follows. Assume I don't have mud on my
head. Then, by the both b and c will answer "yes" the second time.
When they don't, he realizes that the assumption was false, that he is muddy,
and so will answer "yes" on the third question. Similarly for b and c.
Formalization
We will show how one can formalize the description of the puzzle, and the
reasoning involved, in dynamic epistemic semantics. The result, that after
answers to the father's question, the children that are dirty know that they are
dirty, will then be a theorem in the logic.
Let A be a set of children playing in the mud. Consider a language that
contains a propositional atom p a for each a 2 A, which we will take to express
that child a is dirty. We start by introducing some convenient abbreviations:
ffl Each child can see the forehead of each of the other children. So, if a
child is dirty, each of the other children knows that she is dirty. This
can be expressed by the conjunction of all sentences of the form (p a !
for each a and b in A such that a 6= b. We
abbreviate this conjunction by vision .
ffl It is common knowledge between all children that each forehead can be
seen by each of the other children, i.e. vision is common knowledge between
all children. We can express this as CA vision.
ffl Before asking the children whether they know if they are dirty or not, the
father announces in face of all children that at least one of them has a dirty
forehead. Let father be the sentence
fp a j a 2 Ag, which expresses that
at least one of the children is dirty.
ffl After the father's announcement, all children answer the question 'Do you
know whether you are dirty or not?' The children answer either `yes' or
'no'. Let no be the sentence
f(:2 a p a -:2 a :p a ) j a 2 Ag, which is the
sentence that expresses that none of the children knows that she is dirty
(i.e. the information expressed by all children answering 'no' at the same
time.)
ffl Finally, we let for each B ' A, dirty(B) abbreviate V
This sentence expresses that all and only the children in B have dirty
foreheads.
We can now express in DES that if exactly m children are dirty and it is commonly
known between all children that they can see each other, then it holds
that after a common update with the father's statement that at least one of
the children is dirty, and commonly updating times with the fact that all
children answer 'no', the resulting state is a situation in which all dirty children
know that they are dirty. Formally expressed, this boils down to the following
statement:
Proposition 4.1 Let B be a set containing exactly m children (m - 1), and
stand for a sequence of updates with OE. Then it holds
for all a 2 B: dirty(B); vision; CA vision
A 2 a p a
proof: We will provide a syntactical proof of this statement. Although we do
not have an axiomatization for the language containing the common knowledge
operators CB , it is easy to see that that following axiom is sound, if b 2 B:
We will make use of this axiom in the proof.
The proof of the proposition is by induction on the number of dirty children
m. Assume first that only one child, say a, is dirty. In classical modal logic, it
holds that if a is the only dirty child, and a can see all other children, then a
knows that if at least one child is dirty, it must be herself:
We use axiom 5 to conclude that (omitting the subscript A from the update
operators for legibility):
whence, by axiom 6
dirty(fag); vision; CA vision ' [father]2 a p a
For the induction step, let B be a set of m+1 children, and a; b 2 B. It holds
by induction hypothesis and the necessitation rule that if B 0 has m elements,
then
Since CAvision ' 2 a (vision - CA vision) and dirty(B); vision ' 2 a (:p a !
dirty(B=fag)), it follows that
from which it follows, using axioms 3 and 5, and the fact that ' no ! :2 b p b ,
that
By axiom 6, then
and using the lemma below, finally,
Lemma 4.2 For each m: 2 a [no] m (no ! p a ) ' [no] m+1 2 a p a
This is proven by induction on m. If a ) is equivalent by
axiom 5 to 2 a (no ! [no]p a ), which is, by axiom 6, equivalent to [no]2 a p a .
For the induction step, assume that:
This implies that
From which it follows by axiom 6 that
[no]2 a [no] m (no ! p a )
whence, by induction hypothesis, that
This completes the proof of proposition 4.1. 6 2
Discussion
The puzzle of the dirty children and related puzzles have been discussed relatively
extensively in the literature, and several formalizations have been given.
Our analysis adds to earlier approaches in an essential way, we believe.
First of all, we have rephrased the informal description of the puzzle in the
object language of an independently motivated logic. Something like that has
not been done before: all earlier formalizations of the puzzle that we know
of consist of a more or less ad hoc model of the information and information
change involved in the puzzle. That means that each variant of the puzzle that
differs from the present one calls for a new analysis and the construction of
a new model. The relatively straightforward way in which the puzzle can be
formalized in DES suggests that similar problems may be formulated in the
same way.
Secondly, the fact that our formalization of the puzzle gives results similar
to Barwise's semi-formal results, shows that the paradoxical flavor of the
puzzle does not stem from a logical mistake. This suggests strongly that the
discrepancy between the ideal situation described in the puzzle and a 'real life'
situation should not be explained as a difference in principles of logic, but as
a result of the complexity of the reasoning involved in the puzzle and the way
it depends on the strong trust they should have in the each other's reasoning
capabilities.
Thirdly, the formalization given above makes the role that the father's announcement
and the children's answers play quite explicit. For example, one
of the 'paradoxical' aspects of the puzzle is that the father's statement seems
superfluous at first sight if there two or more dirty children present. In such a
situation, each of the children already knows that one of the children is dirty
(since everyone can see a dirty child). The formal correlate of this fact is a theo-
rem: father. The point of the father's statement lies in the
assumption that his announcement makes it common knowledge that at least
on child is dirty, which was not the case: p a -p b ; vision; CA vision 6' CAfather.
This observation is not new, but our analysis adds to earlier ones in that it is
now possible to formulate such facts in the object language.
Another puzzling aspect of the puzzle that is highlighted in our analysis is
the fact that the children keep on saying 'no' until `suddenly' some children
6 We have not proven that the children do not know that they are dirty before they have
answered the question times. To show that, one needs an extra assumption that in the
initial possibility, none of the children knows whether she is dirty of not, and that this fact is
common knowledge. A proof can then be given along the lines of the proof given here.
answer yes, suggests that each answer supplies new information, although, 'syn-
tactically', the children say the same thing each time. This is directly reflected
in our semantics: an update with no changes the possibility in a certain fixed
way, resulting in a new possibility in which another update with no may change
the possibility again.
This is an example of the failure in DES of the following principle of Success:
which states that after a group update with a sentence OE, each member in the
group knows that OE. This is not a property of updates in general, and the
example of no suggests that this is right. 7
5 Epistemic propositional dynamic logic
In this section, we use the ideas of dynamic epistemic logic for developing a
logic, which we call EPDL, for 'epistemic propositional dynamic logic'. Besides
update actions this logic will also have send actions and test actions. The main
thrust of this move is very much in the line of our discussion in the previous
section: by incorporating more notions, such as send actions, that are crucial
for understanding communication, into the logical object language, it becomes
possible to formalize processes that otherwise would remain part of the meta-language

The language of EPDL may be used to specify or describe the behavior of a
group of communicating agents, in a very general sense. The phenomena modeled
might be human agents speaking to each other, the behavior of processors
in a distributed network, or the behavior of a knowledge base and a human
agent querying it.
The idea that extensions or variations of epistemic logic may be used to
describe such kind of applications is not new. In computer science, the work
of Fagin et al. (1995) and Shoham (1993) on agent oriented programming are
prime examples. Another example is the work of McCarty (1990). See also de
Rijke (1993).
The basic idea here is to treat the update modalities of the previous sections
as programs, and extend the language with certain program operators familiar
from PDL (cf. Pratt (1976), Goldblatt (1987)). We consider a language in which
there are three kinds of basic programs. Firstly, there are update programs of
the form U(B; OE), that have the effect that OE becomes common knowledge in the
group of agents B. Secondly, a program S(a; B; OE) will stand for the action of
agent a sending the message OE to all agents in B. Thirdly, the local tests ?(a; OE)
stand for the action of agent a testing whether she knows that OE. In addition
7 For this particular example, we even have the surprising fact that there are possibilities
w such that w
to these basic programs, we add the program operators of PDL: composition,
union and iteration.
Definition 5.1 (Epistemic Propositional Dynamic Logic)
Given an atomic vocabulary P and a set of actors A, we define a set of assertions
\Phi and a set of programs \Pi by simultaneous induction:
where a
We will interpret programs as relations on possibilities. Since we have included
union in the language, which is interpreted as choice in our semantics, programs
will be non-deterministic in general: running a particular program may
lead to several different outcomes. That means that, in contrast with the updates
described in the previous sections, not all programs will have functional
interpretations.
Definition 5.2 (Semantics of EPDL)
An interpretation for EPDL is a function I that assigns to each triple consisting
of an actor a, a set of actors B and a formula OE a binary relation between
possibilities. Relative to such a interpretation we define the truth conditions of
assertions and the interpretation of programs inductively by:
truth conditions
program interpretations
w[[-
The interpretation function I plays a role only in the clause for the send actions
OE). The basic idea is that I(a; B; OE) describes the effects of the
sending action. Of course, the real interest in sending a message is to exchange
information. Thus the real burden is to relate send actions to epistemic effects.
This can be achieved in EPDL by formulating extra constraints that relate send
actions to update actions and to the information of the actors. Typically, these
extra constraints will reflect certain properties of the communication channel,
or certain pragmatic rules that the actors follow. For example, the axiom
a sincerity condition for actor a (here h-iOE is the existential dual of
actor a can only send the message OE if he has the information that OE.
As an example of the application of EPDL to communicative situations we
discuss a simple example which is called 'the bit-transmission problem' in Fagin
et al. (1995, pp. 107ff. We consider two agents, a sender s and a receiver
r . The sender has a certain piece of information (for example that the value
of register x is either 0 or 1) which she wants to communicate to the receiver.
We let the proposition p represent the information that x has value 1 (and
:p that the value is 0). We assume the communication line may be faulty;
for simplicity's sake we assume that messages either arrive immediately or are
lost forever. Since s cannot be sure that her message has arrived, she will
continue sending the message p until she has received an acknowledgment from
the receiver that he has gotten her message.
Another way of describing the behavior of s and r is as follows. s will send
the message p to r until she knows that r knows that p. As soon as r knows
that p, he will send a message 'I know that p' to s . Such descriptions that
make use of concept such as 'knowledge' are descriptions that we can fairly
straightforwardly translate into our language.
For capturing the behavior of this system in EPDL we first of all need
to express what the effect of sending a message is. Under the assumptions
we have made, that messages either arrive immediately, or are irredeemably
lost, the effect of sending a message OE to r can be described by the program
's information state is updated with OE, or nothing at
all happens (the test ?(r ; ?) will always succeed). The corresponding interpretation
function I interprets send actions as follows:
where Id is the identity relation over possibilities. This interpretation of send
actions corresponds to the syntactical characterization:
The action of s sending r the value of the bit p is can be described by the
program
While the receiver can be described as performing the following program:
(- r
:p)).
We can now formulate statements about such programs in the object language.
For example, the statement "If the value of x is 1, then the receiver will eventually
(that is, after repeating both programs again and again) know that the x is
1" may be represented by: 2 s
p. In fact, this sentence turns
out to be valid under the interpretation I given above.
Properties of programs
We may consider how EPDL programs behave with respect to the properties
of situations introduced in definition 3.6. In particular, we may ask which
properties are preserved under updating with certain programs.
Definition 5.3 Let S be a class of possibilities, I an interpretation. A program
- is persistent over a class S of possibilities under the interpretation I iff w 2 S
and
The following result claims that if I interprets all send actions as actions that
preserve positive or negative introspection, then all programs will.
Proposition 5.4 If each send action S(a; B; OE) is persistent over P (N ,
respectively) under I, then each program - is persistent over P (N ,
In general, programs are not persistent over the class of truthful situations, nor
over the class of consistent situations. One example is the program - s
above.
In a situation where S knows that r does not know the value of the bit, the
may result in a possibility in which r knows the value, but s still
believes that r does not know it.
Knowledge programs
As observed by Fagin et al. (1995), one way of looking at a problem like the
bit transmission problem is in terms of so called knowledge programs. That is,
we can model the actors as executing a certain set of instructions of the form
OE ) ff, which are read as "if OE then do ff", where OE is a formula of epistemic
logic, and ff is some action. Formally, they define a knowledge program for an
actor a as a set of these instructions g. These
programs are interpreted indeterministically by requiring that a performs one
of the actions ff i for which the test OE i succeeds.
The models they consider consist of 'local states' of agents standing in a
certain relation to each other. These 'local states' are meant to correspond in a
relatively direct way to states that the agents may actually be in. Actions are
interpreted as operations on such representations, while sentences of modal logic
are interpreted in a possible worlds model that is derived from this representa-
tion. In addition to this 'two-level' architecture, the model contains an explicit
representation of time, and a simple logic of time is added to the language.
It is clear that the in EPDL there are programs similar to these knowledge
programs, i.e. programs that make an action conditional on the epistemic state
of the actor. We will make a few remarks about how our framework compares
with the approach adopted by Fagin et al. One of the most salient differences
is that the former has an ontology that is much richer. Although this means
that the model allows for distinctions that cannot be drawn in our model and
that the behavior of a system can be described in much more detail than in our
approach, it also implies, as the authors themselves note, that it is often unclear
what part of the behavior of a system should be modeled by what part of the
semantics.
In the work of Fagin et al., information change on the level of Kripke structures
is a notion that is derived from change in the underlying model. By
contrast, we have given an explicit semantics for the notion of epistemic update
on this level, thereby providing a semantics in which it is much more clear what
is going on. Moreover, this means that we are not restricted to using only S5
models, which in the architecture of the system of Fagin et al. seems unavoid-
able. This is interesting, because it makes it possible to describe situations
in which agents are misinformed about either their environment or about the
information of the other agents.
6 Conclusions
In this paper, we have combined techniques from epistemic and dynamic logic to
arrive at a logic for describing multi-agent information change. The key concept
of dynamic semantics is that the meaning of an assertion is the way in which
the assertion changes the information of the hearer. Thus a dynamic epistemic
semantics consist in a explicit formal definition of the information change potential
of a sentence. We used these ideas to arrive at the system of Dynamic
Epistemic Semantics, which is semantics for a language describing information
change in a multi-agent setting. This semantics proved useful for analyzing
the Muddy Children paradox, and also for giving a semantics for knowledge
programs, since it enabled us to model knowledge change by giving an explicit
semantics to the triggers of the information change (the latter being the assertions
made, or the messages sent). We feel that this is an important extension,
since standard approaches to for example the Muddy Children (e.g. Fagin et al.
generally use static epistemic logics like S5 to describe the situation before
and after a certain epistemic event, leaving the transition between 'before' and
'after' to considerations in the meta-language. 8 In contrast, in dynamic epistemic
logic, epistemic actions like updates are first class citizens of the object
language of DES. For one thing, this opens the possibility of making artificial
agents a bit more intelligent, by giving them an axiomatics for DEL as their
tool for reasoning about knowledge change.
Authors adress:
Department of Philosophy
University of Amsterdam
Nieuwe Doelenstraat 15
The Netherlands
gerbrand@illc.uva.nl
groenev@illc.uva.nl



--R


The Journal of Philosophy
A system of dynamic modal logic.
Reasoning about Knowl- edge
A modeltheoretic analysis of knowledge.
Knowledge in Flux.
Logics of Time and Computation.
Logical Investigations into Dynamic Semantics.
Calculi for Constructive Communication.
On the difference between updating a knowledge base and revising it.
Formalization of two puzzles involving knowedge.
Formalizing Common Sense: Papers by John McCarthy.
Cheating husbands and other stories: A case study of knowledge
Semantical considerations on floyd-hoare logic
Belief revision from the point of view of doxastic logic.
Agent oriented programming.
Peter van Emde Boas
Defaults in update semantics.
--TR

--CTR
Alexandru Baltag , Lawrence S. Moss , Slawomir Solecki, The logic of public announcements, common knowledge, and private suspicions, Proceedings of the 7th conference on Theoretical aspects of rationality and knowledge, July 22-24, 1998, Evanston, Illinois
Fernando R. Velzquez-Quesada , Francisco Hernndez-Quiroz, Some semantics for a logical language for the game of dominoes, Proceedings of the 24th IASTED international conference on Artificial intelligence and applications, p.293-298, February 13-16, 2006, Innsbruck, Austria
Hans P. Van Ditmarsch, Descriptions of Game Actions, Journal of Logic, Language and Information, v.11 n.3, p.349-365, Summer 2002
Jan-Willem Roorda , Wiebe van der Hoek , John-Jules Meyer, Iterated belief change in multi-agent systems, Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 2, July 15-19, 2002, Bologna, Italy
Alexandru Baltag, Logics for insecure communication, Proceedings of the 8th conference on Theoretical aspects of rationality and knowledge, July 08-10, 2001, Siena, Italy
John Cantwell, A Formal Model of Multi-Agent Belief-Interaction, Journal of Logic, Language and Information, v.14 n.4, p.397-422, October   2005
Chitta Baral , Yan Zhang, Knowledge updates: semantics and complexity issues, Artificial Intelligence, v.164 n.1-2, p.209-243, May 2005
H. P. van Ditmarsch , W. van der Hoek , B. P. Kooi, Concurrent dynamic epistemic logic for MAS, Proceedings of the second international joint conference on Autonomous agents and multiagent systems, July 14-18, 2003, Melbourne, Australia
Robert Van Rooy, Quality and Quantity of Information Exchange, Journal of Logic, Language and Information, v.12 n.4, p.423-451, Fall
Barteld P. Kooi, Probabilistic Dynamic Epistemic Logic, Journal of Logic, Language and Information, v.12 n.4, p.381-408, Fall
Andreas Herzig, Modal Probability, Belief, and Actions, Fundamenta Informaticae, v.57 n.2-4, p.323-344, April
Andreas Herzig, Modal probability, belief, and actions, Fundamenta Informaticae, v.57 n.2-4, p.323-344, October
Churn-Jung Liau, A Logical Analysis of the Relationship between Commitment and Obligation, Journal of Logic, Language and Information, v.10 n.2, p.237-261, 2001
Paul Dekker, Meaning and Use of Indefinite Expressions, Journal of Logic, Language and Information, v.11 n.2, p.141-194, Spring 2002
J.-J. Ch. Meyer, Dynamic logic for reasoning about actions and agents, Logic-based artificial intelligence, Kluwer Academic Publishers, Norwell, MA, 2000
Churn-Jung Liau, Belief, information acquisition, and trust in multi-agent systems: a modal logic formulation, Artificial Intelligence, v.149 n.1, p.31-60, September
Barbara Dunin-Keplicz , Rineke Verbrugge, Evolution of Collective Commitment during Teamwork, Fundamenta Informaticae, v.56 n.4, p.329-371, December
dynamic logic;epistemic logic;non-well-founded set theory;information exchange