From Hypersets to Kripke Models in Logics of Announcements

Lawrence S. Moss

Abstract

This note discusses two semantics for a logic of group announcements and verifies that the two have the appropriate relation. The first semantics is the hyperset semantics of Gerbrandy [4, 5] and Gerbrandy and Groeneveld [6]. The second is the Kripke model semantics of Baltag, Moss and Solecki [2]. The relation between the two semantics was noted without proof in [2]. A proof does appear in Gerbrandy [5]. The presentation here is more algebraic in that it uses coalgebras and final coalgebra maps to give the semantics of [4, 5, 6], and the equivalence of the two semantics is shown without bisimulation.

Contents

1 Introduction 2

2 The hyperset update 4

1 Introduction

This note is concerned with two semantics for the logic of group-level updates. Such logics were first proposed by Plaza [8], and independently in Gerbrandy [4, 5] and Gerbrandy and Groeneveld [6]. The idea is to start with multi-agent modal logic and add propositional operators having to do with conscious announcement of propositions to groups of agents.

Syntax We fix a set AtProp of atomic propositions and a set A of agents. Then the usual multi-modal logic L over AtProp and A is generated in the following way:

sentences φ p ∈ AtProp | ¬φ | φ ∧ ψ | □_{A}φ (A ∈ A)

We extend L to the language L(□^{∗}) by adding the common knowledge operators □_{B}^{∗}, for all non-empty B ⊆ A; to L([ ]) by adding the binary announcement operators [φ]_{B}ψ for all non-empty B ⊆ A, and to L([ ], □^{∗}) by adding both constructs.

The key construct is the announcement operation, taking two propositions φ and ψ, and also a set B of agents, and returning the proposition [φ]_{B}ψ. The intended meaning of this is if we take the group B and announce φ to this group in such a way that everyone in B is aware of the announcement and everyone outside of B is ignorant of it, then ψ holds. Of course, at this point we have not given a formal semantics. But this is the idea.

Our point This note does not discuss the uses of this logic and related variations. What we are interested in here are two semantics. The first semantics proposed uses hypersets, or non-wellfounded sets (see Aczel [1]). The second uses Kripke models. This second semantics is more general as we shall explain below. We will reverse the historical development and discuss the Kripke model semantics first because it requires less background to understand.

An example of an announcement To see what the subject is about, consider the case of a set A of three agents, say A, B, and C; two atomic sentences, p and q, and a Kripke model with four worlds w, x, y, and z depicted below. We have written out the accessibility relations in tabular form. In other notation, we have w →_{A} w, w →_{A} x, x →_{C} z, w ⊧ p, etc. We have some standard semantic facts, such as w ⊧ ¬□_{B}p (in w, B does not know p, since p is false in y), and w ⊧ □_{A}¬□_{B}p, etc.

Now suppose someone comes to each world v ∈ W where p holds, takes A and B off to the side, and tells them (together) that indeed, p holds there. We want to update the worlds so that A and B’s accessibility relations only include worlds where p is true. On the other hand, C was excluded from the announcement (and in fact at this point, we want to assume that C did not even know about it.) So C’s accessibility relation should not change. We want to represent the updated version v′ in a way that captures the epistemic alternatives available to each of the agents. Our proposal is that the worlds

\begin{aligned}w \\ p & A : w, x \\ q & B : w, y, z \\ & C : w, y \end{aligned} \begin{aligned}x \\ p & A : w, x \\ ¬q & B : x \\ & C : x, z \end{aligned} \begin{aligned}y \\ ¬p & A : y, z \\ q & B : w, y, z \\ & C : w, y \end{aligned} \begin{aligned}z \\ p & A : y, z \\ ¬q & B : w, y, z \\ & C : x, z \end{aligned}

Figure 1: The Kripke model W

below represent the updated versions of the corresponding worlds above. Note first that in the updated worlds, we have kept C’s accessibility relations the way they were, since C was not party to the communication.

\begin{aligned}w′ \\ p & A : w′, x′ \\ q & B : w′, z′ \\ & C : w, y \end{aligned} \begin{aligned}x′ \\ p & A : w′, x′ \\ ¬q & B : x′ \\ & C : x, z \end{aligned} \begin{aligned}z′ \\ p & A : z′ \\ ¬q & B : w′, z′ \\ & C : x, z \end{aligned}

Figure 2: The updated model W′ adds worlds w′, x′, and z′ to W

Further, consider the update of w, and focus on the worlds accessible to B. Before the update, B used to think that w, y, and z were possible. It should be clear why there is no trace of y in the worlds accessible to B after the update of w. So we need to update w to some new world; this is why w′ is needed. And w′ should have the same propositional content, since announcements do not change facts. The main question might be: why in w′ do A’s accessibility relations point to w′ and x′ (and not w and x)? And why do B’s point to w′ and z′ (and not w and z)? The reason is that announcing p to A and B should mean that not only do A and B think ¬p is impossible, but also that ¬p should be impossible from all the worlds they think possible, etc.

The main justification for our proposal on how to model actions comes from looking at semantic facts that hold in the updated worlds. For example, ⟨W′, w′⟩ ⊧ □_{{A,B}}^{∗}p. That is, in W′ at the world in w′, it is common knowledge among A and B that p holds. (We use the standard modeling of common knowledge via infinite iteration.) On the other hand, one can check that the updates do not change any knowledge facts for C: for all v ∈ W, ⟨W, v⟩ ⊧ □_{C}φ iff ⟨W′, v′⟩ ⊧ □_{C}φ. Both of these consequences seem right.

These considerations lead to what we call the Kripke model semantics for L([ ]). We interpret our languages on an arbitrary ⟨W, w⟩, where W is a multiagent Kripke model with accessibilities →_{A} for each A ∈ A, and w is a world of W. (We call such ⟨W, w⟩ model-world pairs.) However, to do this, we need to define ⟨W, w⟩ ⊧ φ in terms of semantic facts about model-world pairs ⟨V, v⟩, where V differs from W. (This contrasts with the standard semantics of modal logic where W alone suffices.) Here are the main clauses in the definition:

⟨W, w⟩ ⊧ p  if w ⊧ p in W in the usual way
⟨W, w⟩ ⊧ □_{A}φ if for all v ∈ W such that w →_{A} v, ⟨W, v⟩ ⊧ φ
⟨W, w⟩ ⊧ □_{B}^{∗}φ if ⟨W, w⟩ ⊧ □_{A_{1}} ⋯ □_{A_{n}}φ for all sequences ⟨A_{1}, …, A_{n}⟩

from B^{∗}, including the empty sequence

⟨W, w⟩ ⊧ [ψ]_{B}φ if ⟨W ⊕^{ψ,B} W, new(w)⟩ ⊧ φ,

where W ⊕^{ψ,B} W and new are defined below

The worlds of W ⊕^{ψ,B} W are the elements of the disjoint sum W + W. (We take W + W to be a set such as ({0} × W) ∪ ({1} × W).) We indicate the left injection of W into W + W (the function taking w to ⟨0, w⟩) by new, and the right injection by old. We make this into a Kripke model W ⊕^{ψ,B} W as follows, using the structure of W:

new(v) →_{A} new(u) if v →_{A} u, A ∈ B, and u ⊧ ψ
new(v) →_{A} old(u) if v →_{A} u and A ∉ B
old(v) →_{A} new(u) never holds

old(v) →_{A} old(u) if v →_{A} u
new(v) ⊧ p  if v ⊧ p
old(v) ⊧ p  if v ⊧ p

This completes the definition of W ⊕^{ψ,B} W. So we have specified the semantics of our languages.

Once again, the idea is that ⟨W, w⟩ ⊧ [ψ]_{B}φ means that after all of the agents A ∈ B learn ψ via a public announcement in the world w, φ holds. The effect of this announcement in the semantics is that agents A ∈ B should discard all worlds where ψ fails; they are no longer “possible worlds.” For A ∉ B, there is no effect of the announcement. Here is how this gets formalized in our two copies: The left copy is the updated copy and the right side is the “old world.” It is clear that the right copy is isomorphic to the original W since no arrows depart from it. In the left copy, the agents not in B are not aware of the update, and so all of their possibilities are in the old world. But agents in B are restricted: if A ∈ B, and v →_{A} u, then new(u) is not a successor of new(v) in W ⊕^{ψ,B} W iff u |̸=_{A} ψ.

2 The hyperset update

The main point of this note is to compare the Kripke model update which we just studied with another one which we introduce now. This is the semantics via hypersets studied in Gerbrandy [4, 5] and in Gerbrandy and Groeneveld [6]. However, we are not going to work with the original formulations, since they involved some machinery from Barwise and Moss [3], especially the Corecursion Theorem. To understand the Corecursion Theorem from first principles would take some work, since it critically uses a set theory based on urelements. This would be new for practically everyone. It seems to me that it might be easier for some, and perhaps most, people who have an interest in these matters to see a different development.

So another goal of this paper is to give a new formulation of the hyperset semantics based on ideas coming from coalgebra. I believe that the importance of coalgebras for the study of transition systems is due to Aczel [1] (the same book which introduced non-wellfounded sets to a wide audience); of course there may be earlier references that I do not know of. There is some overhead to either view: one either has to learn some non-standard set theory (especially involving urelements), or some basic definitions from category theory. Part of the purpose of this note is to put down enough details so that someone familiar with the definitions of category and functor could understand our reformulation. A related purpose is to show that in order to work with the hyperset update, it is not really necessary to invoke even the concept of a bisimulation(!). One can get all of the needed results out of final coalgebra maps and their properties.

Here are a series of general definitions and remarks, in preparation for our formulation of the hyperset update:

Some general points of notation For any sets A and B, A + B denotes the disjoint union of A and B. The exact definition of this set is irrelevant, but it brings along injections of A and B into it. We will write these as new_{A+B} : A → A + B and old_{A+B} : B → A + B. We usually drop the subscripts. (It is more common to name these by something like inl and inr. We name them “old” and “new” to fit better with the metaphor of updating worlds.) If f : A → C and g : B → C, then ⟨f, g⟩ : A + B → C is the unique map such that f = ⟨f, g⟩ ∘ new and g = ⟨f, g⟩ ∘ old. Also, if f : A → B and g : C → D, then f + g : A + C → B + D is ⟨new_{B+D} ∘ f, old_{B+D} ∘ g⟩.

Re-packaging multi-modal Kripke structures as coalgebras A Kripke model W can be re-packaged as a coalgebra for the following functor F on sets or classes a and functions f : a → b:

\begin{aligned}F (a) & = & P(AtProp) × A → P(a) \\ F (f) & = & ⟨S, α⟩ ↦ ⟨S, f[α(A)]⟩ \end{aligned}

An F -coalgebra is a pair ⟨A, e⟩, where A is a set or class and e : A → F (A). We drop the F since it is the only functor in the paper. To see that coalgebras correspond to Kripke structures, in one direction we take a model W to ⟨W, f⟩, where

f(w) = ⟨AtProp(w), A ↦ {v : w →_{A} v}⟩

Here AtProp(w) is the set of atomic propositions true at w in W. In the other direction, a coalgebra ⟨E, e⟩ gives a Kripke model: the worlds are the elements x ∈ E; the atomic propositions true at x are the elements of π_{1}(e(x)), and x →_{A} y iff y ∈ (π_{2}(e(x))(A).

Continuing the correspondence, a morphism of coalgebras ⟨A, e⟩ and ⟨B, f⟩ is a map k : A → B so that f ∘ k = F (k) ∘ e. Modulo re-packaging, this is a p-morphism of Kripke models.

A final coalgebra is a coalgebra ⟨C, c⟩ such that for all ⟨A, e⟩ there is a unique coalgebra morphism k : C → e. The map k is called the final coalgebra map for ⟨A, e⟩. Concerning the functor F of this paper, there exists a final coalgebra ⟨C, c⟩. Assuming the Antifoundation Axiom, we can take C to be the greatest fixed point of F, considered as a monotone operator on sets. AFA also allows us to assume that c is the identity on C. To compare the two approaches, we therefore assume AFA and the consequences just noted.

A fact worth noting is that if we have a morphism k : A → B as above, and if the final coalgebra maps are f : A → C and g : B → C, then f = k ∘ g. To see this, one checks that k ∘g is a morphism of coalgebras. So by the uniqueness part of finality, it must be identical to f.

Returning to hyperset update This is the map g = g_{ψ,B} defined on C in a few steps as follows: First, one considers f : C → C + C given by

f(c) = ⟨π_{1}(c),
A ∈ B ↦ {new(b) : b ∈ π_{2}(c)(A) & b ⊧_{C} ψ}
A ∉ B ↦ {old(b) : b ∈ π_{2}(c)(A)}
⟩

Next, let q : C → F (C + C) be F old ∘ c. (Recall that c : C → F (C) is the identity.) Then ⟨f, q⟩ : C + C → F (C + C) is a coalgebra. Notice that F old ∘ c = q = ⟨f, q⟩ ∘ old, so old : C → C + C is a coalgebra morphism from ⟨C, c⟩ to ⟨C + C, ⟨f, q⟩⟩. The final coalgebra map for c is of course id_{C}. Let s : C + C → C be the final coalgebra map. We define the final coalgebra update g to be s ∘ new. Note that the notation does not mention ψ and B, but to remind ourselves of them we could write g_{ψ,B}.

Remark In order to connect this more closely to the original formulations, it is probably useful to note the following result:

Proposition 2.1 For any set or class A and any map k : A → F (A+C) there is a unique h : A → C such that c ∘ h = F (⟨h, id_{C}⟩).

In fact, h is obtained by the same kind of construction which we used in defining g above: considering a bigger coalgebra and using its final coalgebra map. Proposition 2.1 is from [7]. That paper also contains other results along these lines and some applications.

Now, Proposition 2.1 is closely related to the ideas behind the original formulations from [4, 5, 6]. The idea is that we take A = C and k = f. That is, we take an element c of C and return the pair consisting of the atomic propositions true at c, and also a function. That function takes an agent A ∉ B to set contains either elements of C accessible via A (the “old worlds” accessible from a by →_{A}), and these worlds are especially tagged as such. The function also takes A ∈ B to the set of elements of C accessible via A which are modified by this very operation; again, these worlds are tagged as “new” so that they aren’t confused with the old ones. The circularity in this formulation is a central ideological feature of the approach, and we won’t discuss the reasons for it here. But we will mention that work on hypersets and coalgebras can clarify circular characterizations of this kind.

The model-world update Re-packaging W ⊕_{ψ,B} W from earlier gives a coalgebra k : W + W → F (W + W). In more detail,

k(new(w)) = ⟨ AtProp(w),

A ∈ B ↦ {new(v) : w →_{A} v & v ⊧_{W} ψ}

A ∉ B ↦ {old(v) : w →_{A} v}
⟩
k(old(w))  = ⟨ AtProp(w), A ↦ {old(v) : w →_{A} v}
⟩

We let d_{W +W} : W + W → C be the final coalgebra map.

Proposition 2.2 Assume that ψ is preserved under final coalgebra maps. Then

d_{W +W} ∘ new = g_{ψ,B} ∘ d_{W} .

This is the central result of this note. It is based on the following claim:

Claim d_{W} + d_{W} is a coalgebra morphism from ⟨W + W, k⟩ to ⟨C + C, ⟨f, q⟩⟩.

This is the heart of the proof, we will go into the details. Consider some old(w) ∈ W + W. Applying k gives ⟨AtProp(w), A ↦ {old(v) : w →_{A} v}⟩. Now applying F (d_{w} + d_{w}) to this gives

⟨AtProp(w), A ↦ {old(d_{w}((v)) : w →_{A} v}⟩.

Going the other way, (d_{W} + d_{W})(old(w)) = old_{C}(d_{W} (w)). Then applying ⟨f, q⟩ to this gives q(d_{W} (w)) = F old ∘ c(d_{W} (w)). Now

c(d_{W} (w)) = d_{W} (w) = ⟨AtProp(d_{W} (w)), A ↦ {d_{W} (v) : w →_{A} v}⟩,

so that

F old ∘ c(d_{W} (w)) = ⟨AtProp(d_{W} (w)), A ↦ {old(d_{W} (v)) : w →_{A} v}⟩.

Our proof in this case is completed by noticing that AtProp(w) = AtProp(d_{W} (w)). And this holds because coalgebra morphisms preserve the AtProp function, in view of the way such morphisms work.

The remaining case is some new(w) ∈ W +W. Now (F (d_{W} +d_{W}))(k(new(w))) is

⟨ AtProp(w),
A ∈ B ↦ {new(d_{W} (v)) : w →_{A} v & v ⊧_{W} ψ}
A ∉ B ↦ {old(d_{W} (v)) : w →_{A} v}
⟩

And also ⟨f, q⟩(d_{W} + d_{W} (new(w)) = f(d_{W} (w)). And

f(d_{W} (w)) =  ⟨π_{1}(d_{W} (w)),

A ∈ B ↦ {new(b) : b ∈ π_{2}(d_{W} (w))(A) & b ⊧_{C} ψ}

A ∉ B ↦ {old(b) : b ∈ π_{2}(d_{W} (w))(A)}
⟩

These two expressions are equal: this involves tracing through our definitions. It is exactly here that we use the assumption that ψ is preserved under final coalgebra maps.

So now we verified the claim that d_{W} + d_{W} is a coalgebra morphism from ⟨W + W, k⟩ to ⟨C + C, ⟨f, q⟩⟩. Recall that s is the final coalgebra map for W + W. It follows that d_{W +W} = s ∘ (d_{W} + d_{W}) = (g ∘ d_{W}) + d_{W}. Hence d_{W +W} ∘ new = g ∘ d_{W}. This completes the proof of Proposition 2.2.

Proposition 2.3 Every φ is preserved under final coalgebra maps.

Proof By induction on φ. The only interesting step is when we assume that both ψ and φ are preserved under final coalgebra maps, and prove the same thing for [ψ]φ. Note that for all ⟨W, w⟩,

w ⊧_{W} [ψ]φ iff new(w) ⊧_{W ⊕^{ψ,B}W} φ
iff ((d_{W} + d_{W}) ∘ new)(w) ⊧_{C} φ ind. hyp. on φ
iff (g_{ψ,B} ∘ d_{W})(w) ⊧_{C} φ  ind. hyp. on ψ and Prop. 2.2
iff d_{W} (w) ⊧_{C} [ψ]φ
⊣

It follows that for all ψ and B, d_{W +W} ∘ new = g_{ψ,B} ∘ d_{W}. This is the sense in which the two semantics for updates agree.

Conclusion The modest point of this note has been to give a coalgebraic formulation of the hyperset semantics, and to prove the equivalence of that semantics with the Kripke semantics. For more on both semantics, and on the area of announcement logics as a whole, one should see the papers [2, 4, 5, 6, 8].

References

[1] Peter Aczel, Non-Well-Founded Sets, CSLI Lecture Notes Number 14, CSLI Publications, 1988.

[2] Alexandru Baltag, Lawrence S. Moss, and Sławomir Solecki, Logics of Public Announcements, Common Knowledge, and Private Suspicions, to appear. Preliminary version in the Proceedings of TARK-VII , 1998.

[3] Jon Barwise and Lawrence Moss, Vicious Circles. CSLI Lecture Notes Number 60, CSLI Publications, Stanford, 1996.

[4] Jelle Gerbrandy, Dynamic Epistemic Logic, in Logic, Language, and Information, vol. III, CSLI, to appear 1999.

[5] Jelle Gerbrandy, Bisimulations on Planet Kripke, Ph.D. Dissertation, University of Amsterdam, 1999.

[6] Jelle Gerbrandy and Willem Groeneveld, Reasoning about information change, Journal of Logic, Language, and Information 6 (1997) (Special issue on Cognitive Actions in Focus (TARK 1996), edited by Johan van Benthem and Yoav Shoham), 147–169.

[7] Lawrence S. Moss, “Parametric Corecursion,” to appear in Theoretical Computer Science.

[8] Jan Plaza, Logics of Public Communications, Proceedings, 4^{th} International Symposium on Methodologies for Intelligent Systems, 1989.