Knowing More - From Global to Local Correspondence

1 Introduction

Since the seminal work of Hintikka [1962], modal logic is important in knowledge representation, witnessed by e.g. its key role as epistemic logic ([Fagin et al., 1995]).

Adding specific axioms to such a modal logic allows one to specify that the knowing agent is, e.g., veridical (Kaϕ→ϕ). Dynamic Epistemic Logic ([van Ditmarsch et al., 2007b]) provides a modal logical basis to the area of belief revision, thereby enabling multi-agent belief revision, giving an account of the change of higher order information, and capturing this all in one and the same object language. And since the 1960's, the role of modal logic has well expanded from Knowledge Representation to AI in general: Since the pioneering work [Moore, 1977] on knowledge and action, agent theories like BDI ([Rao and Georgeff, 1991]) use modal logic

∗ also Computer Science, University of Otago, New Zealand

Barteld Kooi

Faculty of Philosophy University of Groningen B.P.Kooi@rug.nl

(the modalities representing time, information, or action) to analyse interactions between modalities, like perfect recall, no-learning, realism, or notions of commitment.

The flexibility to express such attitudes and their interactions in modal logic is one of the key explanations for its popularity. More often than not, adding a specific syntactic schematic requirement to an axiomatic system corresponds with a condition on the frames of the semantics . The systematics of this is known as correspondence theory, which, since [van Benthem, 1976] studies which classes of axioms do guarantee to correspond to a semantic requirement. As a simple example , consider the following: For all ϕ, formula Kaϕ → Kbϕ, is true in a frame iff ∀s, t(Rbst ⇒ Rast) in that frame. In words: agent b knows at least what a knows in state s, iff a considers at least possible what b does. Correspondence is a powerful notion, since it allows us to quantify over all instances ϕ.

However, adding a scheme ϕ to a modal logic of which one knows it corresponds to some property Φ on Kripke models, also has as an effect that ϕ becomes a global property. Expanding our example, suppose one adds the scheme Kaϕ → Kbϕ as an axiom to a modal epistemic logic, ensuring that one may assume Rb ⊆ Ra. If the logic is about a set of agents A, then it becomes common knowledge among A that b knows at least what a knows. And if there is a notion of time in our model, we have that it will always be the case that b knows at least what a knows, and, when having modalities for actions, it follows that no action can make it come about that a holds a secret for b.

Now, wouldn't it be useful to be able to say that in the current state, b knows at least what a knows, but that in another state of the current model this may be different; or that agent c knows that b is at least as knowledgeable as a, but d does not know this? At first sight, one might think this is not possible in modal logic, because it would mean quantifying over infinitely many formulas, but only in one state at a time. We demonstrate in this paper that it is possible, though, by adding an appropriate inference rule to a standard modal epistemic logic. In Section 2, we introduce a language of Comparative Modal Logic, for which we provide an axiomatization in Section 3. In Section 4, we demonstrate that the idea can be straightforwardly applied to obtain a Comparative Epistemic Logic. In Section 5 we argue how this approach can be generalized, and we conclude.

2 Language and semantics

We introduce Comparative Modal Logic (CML), which has a simple modal language.

Definition 1 (language of CML) Let a set of indices A and a set of atomic variables P be given. The language L(A, P) is defined by the following BNF:

where a, b ∈ A and p ∈ P. When A, P or both are clear from context, we also write L(P), L(A) and L, respectively. ♦aϕ is shorthand for ¬□a¬ϕ.

Here, □a is just a modal operator, which will be written Ka from Section 4 on, when it is supposed to mean 'a knows that . . . '. The idea of a ⪰ b is that it should, locally, correspond to 'for all ϕ, (□aϕ → □bϕ)'. Under an epistemic interpretation for instance, a ⪰ b means 'in state s, agent a considers at least possible what b considers possible', which, locally, should then correspond to 'in s, agent b knows at least what a knows'. However, non-epistemic interpretations are interesting as well. If □aϕ models 'a desires ϕ' or a has ϕ as a goal [Rao and Georgeff, 1991], then a ⪰ b would read 'every state desired by b is desired by a', which, locally, should correspond to 'b wants at least what a wants'. Next, □aϕ might mean 'when following the social norm a, it will always be the case that ϕ [ ˚Agotnes et al., 2007]. The formula a ⪰ b would then read 'norm a is at least as liberal as b', which, locally, should correspond to 'what is allowed under norm a is also allowed under norm b'. As a final example, in Dynamic Logic [Harel et al., 2000] one could use a ⪰ b ∧ β ⪰ α to express equivalence of programs a and b. The language is interpreted in multi-modal Kripke models.

Definition 2 (CML models) Let a finite set of indices A and a countable set of propositional variables P be given. A CML model M is a tuple M = (W, R, V ) such that

• W is a nonempty set of possible worlds,
• R : A → ℘(W ×W) assigns a relation to each a ∈ A,
• V : P →℘(W) is a valuation.

As mentioned about the language, although our main interest is in epistemic logic, we will look at the general modal case first. Hence we do not require that accessibility relations are equivalence relations.

Definition 3 (semantics)

M, w |= p iff w ∈ V (p) M,w |= ¬ϕ iff M,w ̸|= ϕ M,w |= ϕ∧ψ iff M,w |= ϕ and M,w |= ψ M,w |= □aϕ iff for all v if Rawv, then M, v |= ϕ M,w |= a ⪰ b iff for all v if Rbwv , then Rawv

We can now become a bit more precise about what it means that □aϕ → □bϕ should, locally, correspond to a ⪰ b. Let Γ be {□aϕ → □bϕ | ϕ ∈ L}. Then we would like to have for any M,w, that M,w |= Γ iff M,w |= a ⪰ b. However, this correspondence will not be that tight: It is well possible that Γ holds in M, w, but a ⪰ b does not:

Example 4 Take the following model: W = {w, u, v}, Ra = {(w, u)} and Rb = {(w, u), (w, v)} and, finally, u ∈ Vp iff v ∈ Vp, for all p. In this model, we have M, u |= ϕ iff M, v |= ϕ for all ϕ, and hence we have M, w |= □aϕ → □bϕ, and yet we do not have Rb(w) ⊆ Ra(w), i.e.

To further emphasize the non-standard behavior of our modal language, we state two more negative results. First let us briefly revisit some modal semantic notions.

Definition 5 Given two models M = 〈W, R, V 〉 and M ′ = 〈W ′ , R′ , V ′ , 〉, a relation R ⊆ W ×W ′ is called a bisimulation if the following holds: ('atomic') for all p ∈ P, if Rww′ then w ∈ V (p) iff w′ ∈ V ′ (p) ('forth') if Rww′ and if for some v ∈ W and some a ∈ A one has Rawv, there there is a v′ ∈ W ′ such that R′aw′ v′ and Rvv′ and, finally ('back') if Rww′ and if for some v′ ∈ W ′ and some a ∈ A one has R′aw′ v′ , there there is a v ∈ W such that Rawv and Rvv′ . If there is a bisimulation between M and M ′ with Rww', we write M, w ∼= M ′ , w′ .

A special case of a bisimulation is obtained by unraveling a model M,w into a model M ′ ,w as follows. Given W and a set of agents A let W ′ be all the finite paths in M from w, i.e., states w′ in W ′ are of the form w′ = 〈w1, a1,w2, a2, . . . ,wn, anwn+1〉 such that w1 = w and for all i ≤ n, in M one has Rai wiwi+1. Let lst(w′ ) = lst(〈w1, a1, w2, a2, . . . , wn, an, wn+1〉) = wn+1. Put w′ ∈ V ′ (p) iff lst(w′ ) ∈ V (p), and R′aw′ v′ if v′ = 〈w1, a1, w2, a2, . . . , wn, anwn+1, a, u〉 for some u ∈ W.

With a classical modal language CL(A, P) we mean L(A, P) without the a ⪰ b formulas.

Lemma 6 We have the following.

1. ([Blackburn et al., 2001, page 66]) IfM,w ∼=M ′ ,w′ then for all ϕ ∈ CL(A, P): M,w |= ϕ iff M ′ ,w′ |= ϕ.
2. ([Blackburn et al., 2001, page 63]) If M ′ ,w is an unraveling of M,w then for all ϕ ∈ CL(A, P): M,w |= ϕ iff M ′ , w |= ϕ.
3. Bisimulations do not preserve L(A, P), i.e., item 1 above does not hold for the modal language that includes ⪰.
4. Unravelings do not preserve L(A, P), i.e., item 2 above does not hold for the modal language that includes ⪰.

Proof () We only show item 3 and 4. Take the model M ′ = 〈W ′ ,R′ , V ′ 〉 such that W ′ = {w′ , z′ } and R′a = R′b = {(w′ , z′ )}. Take M from Example 4, and define w′ ∈ V ′ p if w ∈ Vp and z′ ∈ V ′ p iff u ∈ Vp. It is not hard to verify that M,w ∼= M ′ ,w′ , yet M ′ ,w′ |= (a ⪰ b) while M,w |= ¬(a ⪰ b). For item 4, consider the unraveling M ′′ = 〈W ′′ ,R′′ , V ′′ 〉 of M ′ , where W ′′ = {w′ , 〈w′ , a, z′ 〉, 〈w′ , b, z′ 〉}. It is easily verified that M ′ ,w′ |= (a ⪰ b) ∧ (b ⪰ a) while M ′′ ,w′ |= ¬(a ⪰ b) ∧ ¬(b ⪰ a). □

To show that L(A, P) is not completely unbehaved, we show that there are modified kinds of bisimulation and unraveling that do preserve the language. The idea is simple: instead of looking at individual steps we look at sets of indices for which two states are accessible.

Definition 7 Let for C ⊆ A, relation RC be such that RCwv iff for all i ∈ A: (Riwv iff i ∈ C). Note the second occurrence of 'iff' in this definition, it follows that for every w and v there is exactly one set C ⊆ A for which RCwv.

Given two models M = 〈W,R, V 〉 and M ′ = 〈W ′ , R′ , V ′ , 〉, a relation R ⊆ W×W ′ is called a coalitional bisimulation if the following holds: ('atomic') for all p ∈ P, if Rww′ then w ∈ V (p) iff w′ ∈ V ′ (p) ('forth') if Rww′ and if for some v ∈ W and some C ⊆ A (C ̸= ∅) one has RCwv, there there is a v′ ∈ W ′ such that R′C w′ v′ and Rvv′ and, finally ('back') if Rww′ and if for some v′ ∈ W ′ and some C ∈ A one has R′C w′ v′ , there there is a v ∈ W such that RCwv and Rvv′ . If there is a coalitional bisimulation between M and M ′ with Rww', we write M, w ∼=coal M ′ , w′ . Let M, w with M = 〈W, R, V 〉 be given. A coalitional unraveling of M is a model M ′ , w with M ′ = 〈W ′ , R, V ′ 〉, where W ′ consists of all paths 〈w1,C1,w2, . . . ,wn,Cn,wn+1〉 such that w1 = w and for all i ≤ n, one has RCwiwi+1. V ′ is defined as in the case for (ordinary) unravelings, and R′C w′ v′ if v′ = 〈w1,C1,w2,C2, . . . ,wn,Cnwn+1,C, u〉 for some u ∈ W and C ⊆ A.

Coalitional unravelings M ′ ,w of M,w respect access for coalitions of indices. The following theorem is a straightforward extension of items 1 and 2 of Lemma 6:

Theorem 8 (Preservation) 1. If M,w ∼=coal M ′ ,w′ then for all ϕ ∈ L(A, P): M,w |= ϕ iff M ′ ,w′ |= ϕ.

2. If M ′ ,w is an coalitional unraveling of M,w then for all ϕ ∈ L(A, P ): M, w |= ϕ iff M ′ , w |= ϕ.

3 Axiomatization

Let us reflect upon what the properties of ⪰ should be. First of all, it should be possible to derive, from a ⪰ b, that □aϕ → □bϕ. This is facilitated by Axiom Ax⪰ of our logic (Definition 10). How about the other direction, i.e., when can we derive that a ⪰ b? As we know from example 4, it is not sufficient to have □aϕ → □bϕ not even if we would have this for all ϕ. Instead, let us consider the following rule R, where the atom p does not occur in θ.

To see that it is sound, note that its contrapositive says that from the non-derivability of θ → (a ⪰ b), one can infer the non-derivability of (□ap ∧ ¬□bp) → ¬θ. So suppose that θ → (a ⪰ b) is not valid, i.e., θ ∧ ¬(a ⪰ b) is satisfiable, and assume p does not occur in θ. It follows that for some model M = 〈W,R, V 〉 and state s, we have M, s |= θ ∧ ¬(a ⪰ b). The second conjunct means that there is some t for which Rbst but not Rast. Since p does not occur in θ, we can change the valuation without changing θ. Take V ′ p = {t | Rast}. We obviously have 〈M, R, V ′ 〉, s |= (□ap∧¬□bp) ∧ θ, i.e., (□ap ∧¬□bp) →¬θ is not valid.

So, semantically, we have just proven that if θ ∧ (a ⪰ b) is satisfiable, then so is θ ∧ (□ap ∧ ¬□bp). But we need something stronger: namely if θ ∧ (a ⪰ b) is satisfiable in some state reachable from s following a specific path, then so is θ ∧ (□ap ∧ ¬□bp). Such a path can be indicated through ♦a1 (θ1∧♦a2 (θ2∧. . . ♦an (θn∧(a ⪰ b)) . . .)): if that formula is satisfiable, then so should ♦a1 (θ1 ∧ ♦a2 (θ2 ∧ . . . ♦an (θn ∧ (□ap∧¬□bp)) . . .)) be. Therefore, we will introduce pseudo modalities, which will eventually be used in our rule R⪰ which generalizes R. They are the dual of a notion introduced in [Renardel de Lavalette et al., 2002].

Definition 9 (pseudo modalities) We define the following pseudo modalities, which are (possibly empty) sequences s = () or s = (s1, . . . , sn), where each si is a formula or an agent. The formula 〈s〉ϕ is defined as follows:

We define [s]ϕ as ¬〈s〉¬ϕ. If p is an atom, we say that p does not occur in s if p does not occur in any formula si in s.

Definition 10 (proof system) The following comprises the axioms and inference rules of the logic CML

Prop All instances of propositional tautologies

MP From ϕ → ψ and ϕ, infer ψ

Nec From ϕ, infer □aϕ

• R⪰ From 〈s〉(□ap ∧ ¬□bp) → θ, infer 〈s〉¬(a ⪰ b) → θ, where p does not occur in θ or s.

Lemma 11

1. Let p be an atom not occurring in ϕ. Then the rule R is an instance of R⪰ obtained with s = (). Moreover, R⪰ is equivalent to R1 : R1 If 〈s〉¬(a ⪰ b) ∧ θ is consistent, then so is 〈s〉(□ap ∧ ♦b¬p) ∧ θ

1. The following are derivable in CML
2. (a) ⊢ a ⪰ a
3. (b) ⊢ a ⪰ b ∧ b ⪰ c → a ⪰ c

Theorem 12 (Soundness) For all ϕ ∈ L, if ⊢ ϕ then |= ϕ.

3.1 Completeness Our completeness proof is in structure inspired by the proof of a modal logic with a D-operator in [de Rijke, 1993]. However, there the emphasis is on a 'classical' modal logic with a 'non-classical' operator, in this paper, the emphasis is on the transition from 'global axiom' to 'local rule'.

Definition 13 A theory Γ is a set of formulas. Γ is a P -theory if all propositional atoms in Γ are from P. Γ is a witnessed P-theory if for every 〈s〉¬(a ⪰ b) ∈ Γ, there is an atom p such that 〈s〉(□ap ∧ ¬□bp) ∈ Γ. If Γ is not witnessed, then a formula 〈s〉¬(a ⪰ b) for which there is no 〈s〉(□ap ∧ ¬□bp) ∈ Γ, is called a defect for the theory Γ.

Lemma 14 (Extension Lemma) Let Γ be a CML-consistent P-theory. Let P ′ ⊆ P be an extension of P by a countable set of propositional variables. Then there is a maximal CMLconsistent, witnessed P ′ -theory Γ′ extending Γ.

Proof (Sketch) Let P 0 = {p0, p1, . . .} be a set of fresh atomic variables. Let Pn = P ∪ {pi | i ≤ n}. Define Ln to be L(A, Pn), and let Lω be L(A, P ′ ). A theory Δ ⊆ Σ is called an approximation if for some n it is a consistent Pn-theory. For such a theory, the atom pn+1 is the new atomic symbol for Δ if n is the least number such that Δ is a Pn-theory. Assume an enumeration of ψ0, ψ1, . . . of all formulas of the form 〈s〉¬(a ⪰ b). Define

Clearly, by Ax⪰, the set Δ+ is consistent when Δ is and hence, if Δ is an approximation, so is Δ+. To define the extension Σ′ of Σ, assume ϕ0, ϕ1, . . . to be an enumeration of the formulas in Lω, and define Σ0 = Σ, and

Finally, put Σ′ = ⋃n∈ω Σn. By construction, Σ′ is a maximal consistent, witnessed P ′ -theory extending Σ. □

Definition 15 (canonical model) We define the canonical model M = (W, R, V )

• W = {Γ | Γ is a maximal Lω-consistent witnessed P ′ - theory}
• ΓRaΔ iff for all ϕ ∈ Lω it holds that if □aϕ ∈ Γ, then ϕ ∈ Δ
• Vp = {Γ | p ∈ Γ}

Lemma 16 (Successor Lemma) Assume that Γ is a maximal Lω-consistent witnessed theory. Then, if ¬(a ⪰ b) ∈ Γ, there is some Δ ∈ W such that RbΓΔ, but not RaΓΔ.

Lemma 17 (Coincidence Lemma) Let M be as defined in Definition 15. Then

Theorem 18 The logic CML is sound and complete with respect to the semantics of Definition 3.

4 Adding Knowledge: CEL

Let CEL, Comparative Epistemic Logic, be the logic that is obtained from CML by writing Ka for □a and Ma for ♦a (where a ∈ A, and A is a set of agents) adding the following three knowledge-axioms (where ϕ is an arbitrary formula):

• T Kaϕ → ϕ
• 4 Kaϕ→KaKaϕ
• 5 ¬Kaϕ→Ka¬Kaϕ

We will write ⊢CEL for derivability in CEL. Models for CEL will be ordinary multi-agent S5-models.

Theorem 19 The logic CEL is sound and complete with respect to S5 models.

Proof () We harvest from the work in the previous section: the Extension Lemma goes through for CEL-consistent theories, and by definition, the canonical model is such that each Ra is an equivalence relation. □

An obvious question is whether adding knowledge properties to the logic 'induces' new properties. Surprisingly, it does. First consider the following instance of R⪰, here p is fresh for θ:

Theorem 20 Let ϕ be an arbitrary formula, and a, and b agents. Then

Theorem 20 may at first sight seem surprising. It states that it is impossible that one agent knows at least as much as another, without the first agent knowing this. Likewise, it is impossible that one agent considers a state possible that a second agent does not consider possible, without the first agent knowing this. This applies for instance to a game-like setting, where one agent b knows more than another agent a: this cannot go unnoticed by b, in the sense that b knows that he is at least as knowledgeable as a. In particular, two agents cannot know the same without both knowing this!

The technical results in the previous sections suggest that the infinite scheme

is captured by the formula a ⪰ b. However, we have also seen that, would we allow for infinite conjunctions, then although we would have ⊢ (a ⪰ b) → ∧ϕ∈L(Kaϕ → Kbϕ), this implication can only be reversed on models that are 'minimal', or 'bisimilar contractions' or 'strongly extensional' [Blackburn et al., 2001]. Intuitively, a model is strongly extensional if it cannot contain fewer worlds without changing its information content, i.e.: removing a state would mean changing the truth of some formula in some other state. Related to this, it is worth noting that the notion of 'knowing more than' cannot be captured in the language of CEL. Although one might suspect that 'b knows more than a' is captured by (a ⪰ b) ∧ ¬(b ⪰ a), but the latter only says that a considers more states to be possible than b. However, these states can all be bisimilar to states that both agents consider possible, in which case both agents would know the same.

Proof (of Theorem 20)

Ax⪰pos We first derive Mb(Kap∧¬Kbp)∧(a ⪰ b) → ⊥, as follows (note that in S5, the 'inner modalities always win', i.e. XiYiϕ ↔ Yiϕ, for X, Y ∈ {K,M} cf.[Meyer and van der Hoek, 1995]).

• 1 (a ⪰ b) assumption
• 2 Mb(Kap ∧Mb¬p) assumption
• 3 Ma(Kap ∧Mb¬p) from 1, 2,Ax⪰
• 4 MbMb¬p from 2
• 5 MaKap from 3
• 6 Kap ∧Mb¬p from 4, 5, S5
• 7 ¬(a ⪰ b) 6, Ax⪰

From this it follows that Mb(Kap∧¬Kbp) → ¬(a ⪰ b), and, by using (2), we have Mb¬(a ⪰ b) → ¬(a ⪰ b), which is equivalent to (a ⪰ b) → Kb(a ⪰ b).

Ax⪰neg We know from the previous item that Mb(a ⪰ b) → MbKb(a ⪰ b). But in S5 we have MbKbϕ → Kbϕ and Kbϕ → ϕ, hence we obtain Mb(a ⪰ b) → (a ⪰ b), which is the contrapositive of what we need to show. □

We now discuss some virtues of CEL

1. Note that it is satisfiable that Kc(a ⪰ b) ∧ ¬Kd(a ⪰ b): indeed, knowing more is now a local property, which does not need to be common knowledge. We also have that (a ⪰ b)∧¬Ka(a ⪰ b) is satisfiable, and ¬(a ⪰ b)∧¬Ka¬(a ⪰ b).
2. Consider the formula: ¬Kaϕ ∧ ∧i∈A((a ≻ i) → Kiϕ). This expresses that a does not know ϕ, but anybody who would know even a little bit more would know it.
3. Combined with a notion of linear time (with ♦ expressing 'eventually'), we are able to reason about properties like ♦(a ⪰ b), expressing that eventually, b will know at least what a knows.
4. In dynamic epistemic logic, CEL would enable to communicate what in standard DEL would require an infinite amount of communication. The public announcement a ⪰ b has the effect that the local property that b knows at least what a knows becomes a global property: after an announcement with a ⪰ b the model behaves 'as if' Rb ⊆ Ra.
5. The notion of 'knowing at least as' for individuals has at least two extensions to that of groups. Let C and D to be two coalitions. We can interpret C ⪰∩ D in w as ⋂c∈C Rc(w) ⊇ ⋂d∈D Rd(w) and C ⪰∪ D in w as ⋃c∈C Rc(w) ⊇ ⋃d∈D Rd(w). Then, C ⪰∩ D would mean: 'the distributed knowledge of D is at least that of C (in w)', and C ⪰∪ D would mean 'what everybody in D knows is at least what everybody in C knows (in w)'. For instance, the sentence 'Steve knows at least what his parents know' would have the following three interpretations: (p1 ⪰ s) ∧ (p2 ⪰ s) ('Steve knows at least what each of his parents know') and {p1, p2} ⪰∪ {s} ('Steve knows at least what both of his parents know') and {p1, p2} ⪰∩ {s} ('Steve knows at least what his parents distributively know').
6. For notions of group knowledge, many other options present themselves. It is well known that common knowledge of a coalition D, written CD, semantically corresponds to the transitive closure R∗D of the union of the individual relations [Fagin et al., 1995] Ri(i ∈ D). So one could add primitives like D∗ ⪰ F ∗ indicating that the common knowledge of coalition D is a subset of the common knowledge of group F. And the notion of group knowledge on both sides of ⪰ do not have to coincide either: D∗ ⪰ F E for instance might read: 'currently, all what is common knowledge in coalition D, is known by everybody in F'.
7. On contraction-minimal models, the fact that a knows something that b does not know, is expressed by ¬(b ⪰ a). Note that it is possible that both agents know something that the other does not know: ¬(a ⪰ b) ∧ ¬(b ⪰ a) is satisfiable.
8. There is a rich literature on 'only knowing' also in the multi-agent context [Halpern and Lakemeyer, 1996]. Although related to the issues that CEL addresses, there are also differences: in only knowing, one tries to characterize the minimal amount of knowledge of an agent, given he knows a certain fact ϕ. In CEL, the emphasis in on comparing one agent's knowledge to an other agent's.
9. A Case Study Consider a sender and a receiver attempt to communicate a secret to each other without an eavesdropper learning it. A very powerful eavesdropper is one that intercepts all communications. This creates the setting where sender, receiver, and eavesdropper are three agents that can be modelled in a multi-S5 system and where all communications are so-called public announcements by sender and receiver. One specific example of such a setting is known as the Russian Cards Problem [van Ditmarsch, 2003]. The setting is one where a pack of different cards are distributed over the three 'players', where every player only knows his own cards. Anne and Bill are sender and receiver, Cath the eavesdropper:

From a pack of seven known cards 0, 1, 2, 3, 4, 5, 6 Anne and Bill each draw three cards and Cath gets the remaining card. How can Anne and Bill openly (publicly) inform each other about their cards, without Cath learning from any of their cards who holds it?

The S5 model M describing this setting consists of all possible card deals (valuations) where Anne and Bill hold three cards and Cath one. In M an epistemic class for an agent can be identified with the hand of cards of that agent. E.g., given that Anne holds {0, 1, 2}, she cannot distinguish the four deals-we use some suggestive notation-012.345.6, 012.346.5, 012.356.4, and 012.456.3 from one another.

To exchange the secret, Anne and Bill execute a protocol, where a protocol is a function from local states of agents (their hands of cards, therefore) to nondeterministic choice between announcements. If Anne in fact holds 0, 1, and 2, and Bill holds 3, 4, and 5 (so that Cath holds 6, let us call this deal d), the execution of one such protocol consists of

Anne says α: "My hand of cards is one of 012, 034, 056, 135, 246" after which Bill says β: "Cath has card 6."

We follow [van Ditmarsch et al., 2007a] and model the effect of the two announcements above by using temporal operators ❣α and ❣β. In the case of public announcements, our model is a set N of trees with states N, s, t, where s is a deal, and (s, t) represents a contraction-minimal S5 model representing the knowledge given deal s and 'time point' t.

Given the initial situation where Anne and Bill know 'somewhat more' than Cath, execution of the protocol brings us in a situation where they both are equally knowledgeable and also in fact know more than Cath. This can now be elegantly expressed. In the initial state N, d, s0, all players have different knowledge about the card deal: they only know their own hand of cards, and all three hands are of course different, as one card cannot be held by more than one player, giving

After the first announcement, Bill is informed about the card deal and now knows more than Cath, but Anne does not:

After Bill's announcement, both Anne and Bill know the card deal (in fact both have identity access on the resulting model 'after α; β'; so they know the same). Therefore

In this case it is known by the players who knows more than who, and we also have that N, d, s0 |= ❣αKc¬(c ⪰ a) and N, d, s0 |= ❣α ❣βKc(c ≻ b), etc. But there are more complex executions of such protocols where the duration of the protocol is (finite but) uncertain, and where Anne can inform Bill but Cath remains uncertain about this. Under these circumstances we can reach truly local knowledgeability; i.e., scenarios α1; α2, . . . αn exist after which c ≻ b is true, and Anne knows that but not Cath, so we get :

5 Conclusion

We have put the first steps on a path to 'local correspondence theory'. There is no reason our analysis would have to stop at looking at 'knowing at least as'. For instance, consider, in a doxastic setting, the property that Baϕ → ϕ. It belongs to the modal logic folklore that if one wants this property globally to hold, the access for Ba should be reflexive: ∀sRass. However, like in the case for knowing at least as, this would then be enforced globally, and the fact that agent a's beliefs are correct would be common knowledge. How about a local notion, in which we can express that 'in the current state, agent a's beliefs are correct'? Such a local property would be obtained as follows. Let r(a) be true in state s if Raww holds, let p a new atom, not occurring in θ or s and let r be

It is not hard to see (given Section 3) that if one takes a multiagent logic for belief, say KD45, and adds the rule r to it, one obtains a logic for belief in which one can express that locally, agent a's beliefs are truthful. In fact, we think our procedure can be generalized along the following lines.

Take a multi-modal scheme ϕ(⃗a, ⃗ p)., where ⃗a and ⃗ p are sequences of agents and atoms, respectively. Suppose this scheme corresponds with the first order property Φ(⃗a). Introduce a symbol in the modal object language φ which is true at s iff is ϕ holds at s. Then consider the following rule ρ, where p is free for s and θ.

Conjecture 21 Suppose the modal logic X is sound and complete wrt. a semantics X. Then adding the rule ρ together with the axiom φ(⃗a) → ϕ(⃗a, ⃗ p) to X gives a logic that is sound and complete wrt. X , where φ(⃗a) can be 'locally interpreted as guaranteeing' ϕ(⃗a, ⃗ p).

As an example, in CEL, take ϕ(⃗a, ⃗ p) = Ka1 p → Ka2 p; ϕ(⃗a) = ∀s, t(Ra2 st → Ra1 st), and φ = a1 ⪰ a2. Similarly for veridicality and rule r. The formulation of Conjecture 21 is admittedly a bit vague, let alone it comes with a proof. But we think our result contributes to a general methodology, if not result, in achieving more 'local correspondence' properties.

One area in which Comparative Logic might be further explored is that of Dynamic Logic. There, the interpretation of a ⪰ b, where a and b are atomic programs, may be similar to the one given in the paper, but it would be interesting to investigate on top of that a calculus that predicts how this ⪰ can be lifted to a general comparison α ⪰ β between programs.