Paper deep dive
Resolving Asynchronous Distributed Knowledge
Philippe Balbiani, Hans van Ditmarsch, Clara Lerouvillois
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 95%
Last extracted: 7/5/2026, 1:36:23 AM
Summary
The paper introduces a new logic for 'Resolving Asynchronous Distributed Knowledge,' which generalizes the existing synchronous logic of Resolving Distributed Knowledge by Ågotnes and Wang. While the synchronous version assumes a global clock and common awareness of updates, the proposed asynchronous logic uses a history-based semantics where agents are unaware of resolutions involving groups they are not part of. This leads to a more complex axiomatization where synchronous axioms relating resolution to distributed knowledge are no longer valid. The paper defines a resolution relation and a 'view' for agents to track their knowledge relative to a history of prior resolutions.
Entities (9)
Relation Signals (3)
Ågotnes and Wang → authored → Resolving Distributed Knowledge
confidence 100% · One of those is the logic of Resolving Distributed Knowledge, by Agotnes and Wang.
Resolving Asynchronous Distributed Knowledge → generalizes → Resolving Distributed Knowledge
confidence 100% · It is an asynchronous generalization of the synchronous logic of resolving distributed knowledge.
Resolving Asynchronous Distributed Knowledge → uses → History-based Semantics
confidence 100% · The logical semantics is history-based: truth is not only with respect to a given world in a model, but also with respect to a given history of prior resolutions
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:There are by now various epistemic modal logics with intersection modalities for distributed knowledge and intersection update modalities for dynamic phenomena like agents sharing (all their) information, agents receiving information from other agents, and full information protocols. One of those is the logic of Resolving Distributed Knowledge, by Agotnes and Wang. It has distributed knowledge modalities for arbitrary subsets of the set of all agents and it also has so-called resolution modalities for arbitrary subsets of agents sharing their knowledge. In that logic, the agents not involved in the knowledge sharing are aware of the agents sharing knowledge, agents are memory-less, and the kind of dynamics represents synchronous updates, where there is common awareness of the global clock. In contrast, in this contribution we present a logic for Resolving Asynchronous Distributed Knowledge. It is an asynchronous generalization of the synchronous logic of resolving distributed knowledge. The logical semantics is history-based: truth is not only with respect to a given world in a model, but also with respect to a given history of prior resolutions, of which each individual agent can only observe a part. In particular, an agent is unaware of resolutions for groups of agents not including her. As is to be expected, this comes with many technical complications, for example concerning the axiomatization. The synchronous axioms relating resolution to distributed knowledge are now invalid. The modelling advantages of such an asynchronous novel logic, for distributed computing and similar areas, are however substantial and a major asset.
Tags
Links
- Source: https://arxiv.org/abs/2606.31855v1
- Canonical: https://arxiv.org/abs/2606.31855v1
Trouble viewing inline? Open PDF directly →
Full Text
56,970 characters extracted from source content.
Expand or collapse full text
M. Bílková, M. Gattinger, I. van der Giessen, M. Girlando, Y. Wang (Eds.): Advances in Modal Logic 2026 (AiML 2026) EPTCS 447, 2026, p. 75–92, doi:10.4204/EPTCS.447.5 © Philippe Balbiani et al. This work is licensed under the Creative Commons Attribution License. Resolving Asynchronous Distributed Knowledge Philippe Balbiani IRIT, CNRS—INPT—UT philippe.balbiani@irit.fr Hans van Ditmarsch IRIT, CNRS—INPT—UT hansvanditmarsch@gmail.com Clara Lerouvillois IRIT, CNRS—INPT—UT IHPST, Paris 1 Panthéon Sorbonne clara.lerouvillois@irit.fr There are by now various epistemic modal logics with intersection modalities for distributed knowl- edge and intersection update modalities for dynamic phenomena like agents sharing (all their) infor- mation, agents receiving information from other agents, and full information protocols. One of those is the logic ofResolving Distributed Knowledge, by Ågotnes and Wang. It hasdistributed knowledge modalities for arbitrary subsets of the set of all agents and it also has so-calledresolutionmodali- ties for arbitrary subsets of agents sharing their knowledge. In that logic, the agents not involved in the knowledge sharing are aware of the agents sharing knowledge, agents are memory-less, and the kind of dynamics represents synchronous updates, where there is common awareness of the global clock. In contrast, in this contribution we present a logic forResolving Asynchronous Distributed Knowledge. It is an asynchronous generalization of the synchronous logic of resolving distributed knowledge. The logical semantics is history-based: truth is not only with respect to a given world in a model, but also with respect to a given history of prior resolutions, of which each individual agent can only observe a part. In particular, an agent is unaware of resolutions for groups of agents not including her. As is to be expected, this comes with many technical complications, for example concerning the axiomatization. The synchronous axioms relating resolution to distributed knowl- edge are now invalid. The modelling advantages of such an asynchronous novel logic, for distributed computing and similar areas, are however substantial and a major asset. 1 Introduction If Anne (a) knowspand Bill (b) knowsp→qthen neither knowsqbut they still havedistributed knowledgeofq. If they were tosharetheir information, they would both knowq. Distributed knowledge modalities areintersection modalities:pis distributed knowledge foraandbin a worldw, iffpis true in all worldsvwhich are indistinguishable fora andforbfrom the actual worldw. In this case, distributed knowledge ofpbecomes common knowledge ofpby sharing. However, as is well known, propositions may be distributed knowledge even when the agents cannot share this information. For another scenario, ifpis true butadoes not know this, andbknows that, thenaandbhave distributed knowledge of the former, as it is true in all worlds which are indistinguishable foraand forb. But whenbinformsaof p, or even ofpand that she does not knowp, agentalearns thatpwhich makes her ignorance false. Modalities for sharing information areintersection updates(intersection update modalities): in a world wpropositionqis true afteraandbshare their knowledge iffqis true in the model wherein we have replaced the indistinguishability relations foraandbby the intersection of these two relations. Let now Cath (c) enter the scene and let us replay the first of the above scenarios, where all three agentsa,b,c are initially aware thataknowspandbknowsp→q. Again Anne and Bill share their knowledge. What does Cath learn from this? That depends. If we assume synchrony, then Cath learns that Anne and Bill share their knowledge, so afterwards Cath knows that Anne and Bill now both knowq. Also, Anne and Bill know that Cath knows this. But if we assume asynchrony, Anne and Bill may have shared their knowledge without Cath learning that. In which case Cath still considers it possible that Anne 76Resolving Asynchronous Distributed Knowledge does not knowq. But also Anne and Bill now face more uncertainty. For example, if after Anne and Bill share their knowledge, Anne and Cath share their knowledge, Cath now knows that Anne knowsp. But Bill, who was not involved in the second sharing, does not know that. And so on. Various logics have been proposed to formalize distributed knowledge and sharing knowledge and their interaction, and that should be seen as incorporating synchrony. Instead, we propose an asynchronous logic to formalize distributed knowledge and sharing knowledge and their interaction. The remainder of this introduction is a succinct survey of modal logics with intersection modalities, modal logics with intersection updates, and modal logical approaches to asynchrony. Intersection modalities.If we consider a modal language with modalities□ a and□ b , interpreted on Kripke models with binary relationsR a andR b , resp., the problem of intersection modalities boils down to the observation that adding a novel modality (suggestively named)□ a∪b pis true in a worldw iffpis true in all worldsvwhich areR a -accessibleor R b -accessible does not create problems. This is so because in such a case,R a∪b =R a ∪R b and one simply has that□ a∪b pis equivalent to□ a p∧□ b p. Whereas adding a modality□ a∩b such that□ a∩b pis true in a worldwiffpis true in all worldsv which areR a -accessibleand R b -accessible creates problems. One now has thatR a∩b =R a ∩R b and we can no longer define□ a∩b pwith the other modalities, the canonical model is not of the right kind. One way to address this is to expand the logical language withnominals[46, 47] which led to the development ofhybrid logics[13, 4] and related logics [29, 30, 49]. Another way to address this led to the development of modal logics with intersection modalities, where we highlight Propositional Dynamic Logic (PDL) with intersection [19, 33], and epistemic logics with distributed knowledge [24, 32, 2], although there are many further approaches such as Boolean Modal Logic [26, 27], and knowledge representation logics [43, 51]. Propositional dynamic logic.InPDLwe generalize from modalities□ a to modalities□ α whereα is a program and that are interpreted in models with recursively defined relationsR α , with the same basic programsa,b, . . .as above but apart from∪operations of sequential execution and arbitrary iteration, as well as another basic program called test [34]. By also adding intersectionα∩βof programs to PDL, we obtainIPDL[19, 33]. Here,α∩βrepresents parallel execution of programsαandβas R α∩β =R α ∩R β , so again, similar toR a ∩R b above. Various works involving the complexity [38, 39, 40] and axiomatization [6] ofIPDLhave appeared. Distributed knowledge.The notion ofdistributed knowledgeis rooted in sociology, economics, and philosophy [35, 36, 50] under different terms; [35] is an admirable pamphlet against centralized planning and in favour of distributed planning (and authority), [36] calls it ‘impersonal knowledge’, and [50] ‘undiscovered public knowledge’. The earliest epistemic logical source is [31] (the later journal version [32] also gives a logical semantics), wherein the notion was called ‘implicit knowledge’, followed on the heals by [44] who proposes an axiomatization (without claiming completeness) in a temporal epistemic logic. In fact their non-temporal fragment is the, yet somewhat later, complete axiomatization of [24, 37], where these publications achieved completeness by different methods. All such works interpret modalies □ a not on models with arbitrary relationsR a but on models with equivalence relations. Among the many issues of further interest concerning distributed knowledge, particularly in view of representing multiple agents sharing knowledge given uncertainty about their own and each other’s knowledge, is a certain discrepancy between syntactic and semantic intuitions of distributed knowledge, and what sharing knowledge actually means. Such issues were already discussed in the original [24, 37] and continue to be investigated in more recent times [25]. Intersection updates.After the history of intersection modalities we now proceed with the history of intersection updates, the history ofsharinginformation. Given a Kripke model with two (typically) equivalence relationsR a andR b , theintersection update modality□ update a∩b is such that□ update a∩b pis true Philippe Balbiani et al.77 in a worldwof a modelMiffpis true in the same worldwbut in theupdatedmodelM a∩b wherein the relationsR a andR b are replaced by the relationR a ∩R b . That is all. Note that when we interpret the intersection modality we (may)change the point of evaluationin a given model but wedo not change the modelwherein we evaluate the formula bound by the modality, whereas if we interpret the intersection update modality wedo not change the point of evaluationbut we (may)change the modelwherein we evaluate the formula bound by the modality. Intersection update modalities are therefore interpreted as updates of Kripke models and they can indeed be seen as a further development indynamic epistemic logics, such as public announcement logic [48] and action model logic [8] (for references see [22, 42]), although these are updates with very different properties. The first paper involving the intersection update to our knowledge was [12], in a mixed setting of epistemic and inquisitive logic. The intersection update here is theresolveaction, encoding the answer to a question thus resolving an issue (intersecting an epistemic relation with an issue relation). On the heals of [12] were a number of related publications [9, 15, 14, 28, 7]. Here, [9] introduces intersection updates on plausibility structures whereas [7] further generalizes the inquisitive and epistemic setting of [12]. Independently, slightly later again, [1] focuses on intersection updates (calledresolution) and distributed knowledge for arbitrary sets of agents and their interaction. Further developments introduce uncertainty even among agents who have shared information [10, 11], which also relates to a different strand of research coming out of distributed computing, and intersection updates incarnate the execution ofcommunication graphsorcommunication patterns[54, 16, 17, 52, 53]. The operation of pooling or basic intersection in [18] corresponds to a intersection (update) modality similar to what we call resolu- tion here; this updates models with plausibility relations. An attempt to combine distributed knowledge and intersection updates into a single modality forsharing knowledgeis [5]. Asynchrony.Intersection modalities like distributed knowledge and intersection updates such as resolution and communication patterns assume synchrony (and even so in distributed computing, were aroundof asynchronous events represents a snapshot recording time). Things become more complex with (full) asynchrony, in the absence of a global clock. This was already addressed in [32], and ‘full information protocols’ in distributed computing [41] correspond to intersection updates. In dynamic epistemic logics such asynchrony requires a history-based semantics [45, 20]. Even with more restricted information exchange such as in gossip protocols this leads to far more challenging axiomatizations (and higher complexities) [23, 21, 3]. Overview of content.In Section 2 we review the logic of resolving (synchronous) distributed knowl- edge. In Section 3 we introduce the logic of resolving asynchronous distributed knowledge, and compare it to the logic of synchronous distributed knowledge. In Section 4 we define an infinitary axiomatization for the logic of resolving asynchronous distributed knowledge and prove its completeness. Section 5 lists further research, on redundant resolutions, derivable rules, expressivity, and common knowledge. 2 Resolving distributed knowledge We briefly present Ågotnes and Wang’s logic for resolving distributed knowledge [1]. LetAbe a finite non-empty set ofagents, andPa countable set of propositional variables (atoms). The languageL DR is defined byφ::=p|⊤|(φ∧φ)|¬φ|D B φ|R B φ, wherep∈PandB⊆A. The sublanguageL D with only modalitiesD B φis the language of distributed knowledge. For□ a we now writeK a , and it is defined by abbreviation asD a . FormulaR B φis read as ‘after resolution for group of agentsB,φ(is true)’. The structures are multi-agentepistemic models(W,∼,V)for the setAof agents (where(W,∼)is a multi-agentframe). We can see∼as a set∼ a a∈A of binaryindistinguishability relations(or as a 78Resolving Asynchronous Distributed Knowledge (taut)all instantiations of propositional tautologies (K D )D B (φ→ψ)→(D B φ→D B ψ) (T D )D B φ→φ (5 D )¬D B φ→D B ¬D B φ (DG)D B φ→D C φifB⊆C (RA)R B p↔p (RN)R B ¬φ↔¬R B φ (RC)R B (φ∧ψ)↔(R B φ∧R B ψ) (RD1)R B D C φ↔D B∪C R B φwhenB∩C̸=/0 (RD2)R B D C φ↔D C R B φwhenB∩C=/0 (NecD)Fromφ, inferD B φ (NecR)Fromφ, inferR B φ (MP)Fromφandφ→ψ, inferψ Table 1: AxiomatisationRDfor the logic of resolving distributed knowledge function mapping each agent to such a relation∼ a ). ValuationVis a function from the set of atoms to the powerset ofWmapping each atom to the subset of worlds where it is true. We write∼ B := T a∈B ∼ a for the epistemic relation of a groupB(so that∼ /0 =W×W). IfM= (W,∼,V)andB⊆Athenupdated model M B := (W,∼ B ,V)is the result of resolution for groupB, where∼ B a := T b∈B ∼ b ifa∈Band∼ B a :=∼ a otherwise. In updated modelM B the relations for the agentsa∈Bhave been updated from∼ a to∼ B . Hence, inM B we have that∼ B B =∼ B a for alla∈B, unlike inM. Given these notations, we have that∼ B C =∼ C ifB∩C=/0 and that∼ B C =∼ B∪C ifB∩C̸=/0. Note thatM a =Mand thatM /0 =M. ForM a 1 ,...,a n we writeM a 1 ...a n , and for(M B ) C we writeM B.C . Let a vector ⃗ Grepresent a sequenceB 1 . . .B n , whereB i ⊆Afor 1≤i≤n—the empty sequence isε. By| ⃗ G|we denote the length of ⃗ G, anda/∈ ⃗ Gmeans thata/∈Bfor anyB⊆Asuch thatBoccurs in ⃗ G. We write∼ ⃗ G a for the accessibility relation of an agentainM ⃗ G . We now present the semantics. The satisfaction relation|=is defined by induction onφ∈L DR , wherep∈PandG⊆A. M,w|=piffw∈V(p) M,w|=⊤ifftrue M,w|=¬φiffM,w̸|=φ M,w|=φ∧ψiffM,w|=φandM,w|=ψ M,w|=D B φiffM,v|=φfor allv∈Wsuch thatw∼ B v M,w|=R B φiffM B ,w|=φ A formulaφ∈L DR isvalidiff for all modelsM= (W,∼,V)and for allw∈W,M,w|=φ. The axiomatizationRDfor the logic of resolving distributed knowledge in Table 1 extends that of the logic of distributed knowledge with reduction axioms for resolution and a derivation rule for necessitation of resolution. Completeness of this axiomatization is shown by reducingL DR -formulas to L D -formulas, by which we mean that any formula with resolution and distributed knowledge modalities is provably (and semantically) equivalent to a formula without resolution modalities. It can be shown thatReplacement of Equivalents(RE: fromφ↔ψderiveχ[p/φ]↔χ[p/ψ], whereχ[p/φ]is uniform substitution ofpinχbyφ) is derivable inRD. This is needed to reduce formulas of formR G R H φwhere G̸=H, as there is no axiom of shapeR G R H φ↔. . . Philippe Balbiani et al.79 3 Resolving asynchronous distributed knowledge We now propose a logical framework for resolvingasynchronousdistributed knowledge. The logical languageL DR is the same, whereas accessibility relations are now encoding asynchronous distributed knowledge. Given asynchrony, we propose a history-based semantics. That is, instead of interpreting formulasφin pointed models(M,w), where such anMcould be an updatedM ⃗ G , we now wish to interpret formulas in pointed models(M,w, ⃗ G), where the resolution sequence explicitly remains at our disposition. This is necessary, because what an agent knows now may be different when she was involved in the last resolution in ⃗ Gthan from when she was not. In order to compare pairs(w, ⃗ G)and(v, ⃗ H)we not only need the indistinguishability relation∼ a between worldswandvbut also a novelresolution relation ≈ a between resolution sequences ⃗ Gand ⃗ H. Connecting both relations is theviewby agentaof sequence ⃗ G, denotedsee a ( ⃗ G), that is the set of agentsBwith whomahas shared the equivalence relations (e.g., recalling the introduction, after resolutionab, she has shared it withbas the new∼ a is now∼ a∩b ). The setsee a ( ⃗ G)determines the knowledge gained by agentaafter history ⃗ G—or after any other history ⃗ H that she cannot distinguish from ⃗ G. Let us begin by defining the resolution relation and the view, and show some relevant results relating them. Resolution relation.Leta∈A, and ⃗ G, ⃗ H∈P(A) ∗ be given. Theresolution relation≈ a between resolution sequences is the equivalence closure of: ε≈ a εiff true ⃗ G.B≈ a ⃗ Hiff ⃗ G≈ a ⃗ Hwhena/∈B ⃗ G.B≈ a ⃗ H.Biff ⃗ G≈ b ⃗ Hfor allb∈Bwhena∈B We further define≈ B := T a∈B ≈ a . Note that≈ /0 is the universal relation. View.Theviewsee a ( ⃗ G)of agentaof a resolution sequence ⃗ Gis the setB⊆Aof agents such that given any modelM= (W,∼,V), agenta’s current relation∼ ⃗ G a is∩ b∈B ∼ b . LetB⊆A, then: •see B (ε):=B; •see B ( ⃗ G.C):=see B∪C ( ⃗ G)whenB∩C̸=/0; •see B ( ⃗ G.C):=see B ( ⃗ G)whenB∩C=/0. Forsee a ( ⃗ G)we writesee a ( ⃗ G). Note thatsee B ( ⃗ G) =Cdoes not mean that the view of all agents inBis C, but only that the union of the views of all agents inBisC. It is easy to see thatsee B ( ⃗ G) = S b∈B see b ( ⃗ G) (induction on the length of ⃗ G). Before proceeding with the definition of the semantics, we state some properties of the resolution relation and the view, that will later prove useful. Straightforward proofs have been omitted. Lemma 3.1.If a/∈ ⃗ I, then ⃗ G≈ a ⃗ H. ⃗ I if, and only if, ⃗ G≈ a ⃗ H. Similarly, if ⃗ I∈P(A ) ∗ , then ⃗ G≈ B ⃗ H. ⃗ Iif, and only if, ⃗ G≈ B ⃗ H. Lemma 3.2.ε≈ B ⃗ G if, and only if, ⃗ G∈P(A ) ∗ . Consequently, we also have as a corollary that wheneverB∩C=/0, thenC≈ B ⃗ Giff ⃗ G∈P(A ) ∗ . Lemma 3.3.If a∈B, then ⃗ G.B≈ a ⃗ H iff there are ⃗ H 1 , ⃗ H 2 ∈P(A) ∗ such that ⃗ H= ⃗ H 1 .B. ⃗ H 2 with ⃗ G≈ B ⃗ H 1 and a/∈ ⃗ H 2 . Lemma 3.4.If B∩C̸=/0, then C≈ B ⃗ H iff there are ⃗ H 1 , ⃗ H 2 ∈P(A) ∗ such that ⃗ H= ⃗ H 1 .C. ⃗ H 2 with ⃗ H 1 ∈P(A\(B∪C)) ∗ and ⃗ H 2 ∈P(A ) ∗ . 80Resolving Asynchronous Distributed Knowledge Lemma 3.5.If ⃗ G≈ see B ( ⃗ H) ⃗ I and ⃗ H≈ B ⃗ J, then ⃗ G. ⃗ H≈ B ⃗ I. ⃗ J. Proof.The proof proceeds by induction on the length of ⃗ H. If ⃗ H=ε, suppose ⃗ G≈ B ⃗ I(becausesee B (ε) = B) andε≈ B ⃗ J. by Lemma 3.1,ε≈ B ⃗ J⇒ ⃗ J∈P(A )and then ⃗ G≈ B ⃗ Iimpliesε. ⃗ G= ⃗ G≈ B ⃗ I. ⃗ J. If ⃗ H= ⃗ H ′ .C, suppose ⃗ G≈ see B ( ⃗ H ′ .C) ⃗ Iand ⃗ H ′ .C≈ B ⃗ J. We now distinguish caseB∩C=/0 from caseB∩C̸=/0. • IfB∩C=/0,see B ( ⃗ H ′ .C) =see B ( ⃗ H ′ )and ⃗ H ′ .C≈ B ⃗ J⇒ ⃗ H ′ ≈ B ⃗ J(Corollary 3.1) so, by inductive hypothesis, ⃗ G. ⃗ H ′ ≈ B ⃗ I. ⃗ J. Hence ⃗ G. ⃗ H ′ .C≈ B ⃗ I. ⃗ Jby Corollary 3.1 again. • IfB∩C̸=/0, thensee B ( ⃗ H ′ .C) =see B∪C ( ⃗ H ′ ). Note that sinceB⊆B∪C, ⃗ G≈ see B∪C ( ⃗ H ′ ) ⃗ Iimplies ⃗ G≈ see B ( ⃗ H ′ ) ⃗ I(and respectively forC). Leta∈B∩C. By Lemma 3.3, ⃗ H ′ .C≈ a ⃗ Jimplies ⃗ J= ⃗ J 1 .C. ⃗ J 2 where ⃗ H ′ ≈ C ⃗ J 1 anda/∈ ⃗ J 2 . Then, we have ⃗ G≈ see C ( ⃗ H ′ ) ⃗ Iand ⃗ H ′ ≈ C ⃗ J 1 so, by induction hypothesis, ⃗ G. ⃗ H ′ ≈ C ⃗ I. ⃗ J 1 . Hence ⃗ G. ⃗ H ′ .C≈ a ⃗ I. ⃗ J 1 .C. ⃗ J 2 = ⃗ I. ⃗ J. Let nowa∈B . Then, ⃗ H ′ .C≈ a ⃗ Jiff ⃗ H ′ ≈ a ⃗ J, and we have ⃗ G≈ see a ( ⃗ H ′ ) ⃗ I(forsee a ( ⃗ H ′ .C) =see a ( ⃗ H ′ )). So, by induction hypothesis, ⃗ G. ⃗ H ′ ≈ a ⃗ I. ⃗ J and hence ⃗ G. ⃗ H ′ .C≈ a ⃗ I. ⃗ J. Therefore ⃗ G. ⃗ H ′ .C≈ B ⃗ I. ⃗ J Lemma 3.6. ⃗ G≈ a ⃗ H impliessee a ( ⃗ G) =see a ( ⃗ H). Proof.The proof is by induction on the length of ⃗ G. Base case. We have:ε≈ a ⃗ Himpliesa/∈ ⃗ H(Lemma 3.2) sosee a (ε) =a=see a ( ⃗ H). Induction case. Now consider ⃗ G.B. We distinguisha/∈Bfroma∈B. Ifa/∈Bwe have: ⃗ G.B≈ a ⃗ H iff (by definition) ⃗ G≈ a ⃗ H, which implies (induction)see a ( ⃗ G) =see a ( ⃗ H), sosee a ( ⃗ G.B) =see a ( ⃗ H). If nowa∈Bthe resolution sequence compared with must have shape ⃗ H.B. ⃗ Iwherea/∈ ⃗ I(Lemma 3.3) so that: ⃗ G.B≈ a ⃗ H.B. ⃗ Iiff ⃗ G.B≈ a ⃗ H.B(Lemma 3.1), which implies ⃗ G≈ b ⃗ Hfor allb∈B. This implies (in- duction)see b ( ⃗ G) =see b ( ⃗ H)for allb∈B, which implies S b∈B see b ( ⃗ G) = S b∈B see b ( ⃗ H)so (by definition) see a ( ⃗ G.B) =see a ( ⃗ H.B) =see a ( ⃗ H.B. ⃗ I). Consequently, we also have that ⃗ G≈ B ⃗ Himpliessee B ( ⃗ G) =see B ( ⃗ H). From [5] we further recall that for all modelsM= (S,∼,V),∼ ⃗ G B =∼ see B ( ⃗ G) . In other words, we might as well have stated that ⃗ G≈ B ⃗ H implies∼ ⃗ G B =∼ ⃗ H B , or that ⃗ G≈ B ⃗ Himplies∼ see B ( ⃗ G) =∼ see B ( ⃗ H) , and will quote Lemma 3.6 in such cases. However,see a ( ⃗ G) =see a ( ⃗ H)does not imply ⃗ G≈ a ⃗ H. Typical counterexamples are thatsee a ( ⃗ G.a) = see a ( ⃗ G)whereas ⃗ G.a̸≈ a ⃗ Gandsee a (ab.ab) =see a (ab)whereasab.ab̸≈ a ab. We proceed to define the semantics. Definition 3.7(Semantics).By induction onφ∈L DR , wherep∈P,B⊆Aand ⃗ G∈P(A) ∗ . M,w, ⃗ G|=piffw∈V(p) M,w, ⃗ G|=⊤iff true M,w, ⃗ G|=¬φiffM,w, ⃗ G̸|=φ M,w, ⃗ G|=φ∧ψiffM,w, ⃗ G|=φandM,w, ⃗ G|=ψ M,w, ⃗ G|=D B φiffM,v, ⃗ H|=φfor allv∈W, ⃗ H∈P(A) ∗ such thatw∼ ⃗ G B vand ⃗ G≈ B ⃗ H M,w, ⃗ G|=R B φiffM,w, ⃗ G.B|=φ As not uncommon in history-based semantics, two notions of validity emerge. A formulaφ∈L DR is ε-validifM,w,ε|=φfor all modelsM= (W,∼,V)and for allw∈W. A formulaφ∈L DR is∗-valid(or Philippe Balbiani et al.81 always valid) ifM,w, ⃗ G|=φfor allM= (W,∼,V),w∈W, and all ⃗ G∈P(A) ∗ . We should acknowledge that we are uncertain ifε-validity and∗-validity correspond. This is a question left for future research. This asynchronous semantics looks very much like the synchronous semantics of the previous sec- tion, except for the clause for distributed knowledge. Let us be explicit about some differences and correspondences. First, Example 3.8 shows thatM,w, ⃗ G|=φis not equivalent to (in the synchronous semantics)M ⃗ G ,w|=φ. So there is a real difference. Example 3.8.Consider three agentsa,b,cand modelMand updatedM ab as in Figure 3.8. Instead of naming worlds byw,v, etcetera, we name them with their valuation, where pdenotes¬p. Reflexive arrows are omitted. We also assume symmetry and transitivity. pq pq pq pq pq pq pq pq b abc a abc Figure 1: An epistemic modelM(on the left) and its updateM ab (on the right) with three agents. We now have thatM ab ,pq,ε|=K c K a pbut not thatM,pq,ab̸|=K c K a p. Agentcis unaware of agents aandbresolving their knowledge in modelM: resolutionabis indistinguishable from the empty se- quenceεfor her. She therefore does not know agentahas learnt the truth aboutpas a consequence of this resolution. SinceM,pq,ε̸|=K a pandab≈ c ε, thereforeM,pq,ab̸|=K c K a p. And therefore alsoM,pq,ε̸|=R ab K c K a p. Now consider the prior synchronous semantics. ThenM ab ,pq|=K c K a pand thereforeM,pq|=R ab K c K a p. But we can also look at this in another way, rather illustrating a correspondence. Let us for a vanish- ing moment consider asynchronousdistributed knowledge modalityD D D B φ, interpreted as follows on our history-based models, wherein we only have replaced ⃗ G≈ B ⃗ Hby ⃗ G= ⃗ H. M,w, ⃗ G|=D D D B φiffM,v, ⃗ H|=φfor allv∈W, ⃗ H∈P(A) ∗ such thatw∼ ⃗ G B vand ⃗ G= ⃗ H Now writeM,w, ⃗ G|=φanywhere for the synchronousM ⃗ G ,w|=φ(while replacing allD B byD D D B ). This embeds the synchronous semantics into the asynchronous semantics. So, with respect to the above example, indeed,M,pq,ab̸|=K c K a p, but on the other hand we now haveM,pq,ab|=K K K c K K K a p, which after all corresponds toM ab ,pq|=K c K a p. Isn’t that neat? However, let us now go back to one language and two different semantics again. A further maybe somewhat curious observation is that resolutionR B has the same semantics either way, only the interpre- tation of distributed knowledgeD B is different synchronously and asynchronously. Despite the identical semantics, with asynchrony, resolutionR B encodespartial synchronizationfor group of agentsB without any agents not inBbeing aware of that, whereas, with synchrony, resolutionR B encodesfull synchro- nizationfor all agents however with aspects ofpartial observation: group of agentsBjointly learn (all) each other’s knowledge whereas all agents not inBlearn that, but not what the agents inBlearn. The agents not inBonly partially observed the resolution. Preparing the ground for the asynchronous axiomatization presented in the next section, let us review what parts of the synchronous axiomatization remain valid and what are now invalid. It is fairly simple. 82Resolving Asynchronous Distributed Knowledge All axioms and rules ofRDremain valid (or validity preserving), except (RD1) and (RD2); and maybe (NecR). Ifε-valid and∗-valid were the same (the open question), then we would have necessitation of resolution. (It is easy to see why: assume|=φand (NecR). Given arbitrary(M,w), from the first we get thatM,w,ε|=φ, and from that and the secondM,w,ε|=R B φ, so thatM,w,B|=φ. We therefore easily show thatφis∗-valid by induction on the length of resolution sequences.) Example 3.9.ModelMin Figure 3.9 provides a counterexample to (RD1), and modelM ′ below provides a counterexample to (RD2), where we have again named worlds with valuations of atoms. pq pq pq pq d d abc pq pq pq pq b b b bc Figure 2: Epistemic modelsM(on the left) andM ′ (on the right) with four agents. We have thatM,pq,ε|=D abc R ab ¬K a qbutM,pq,ε̸|=R ab D bc ¬K a q—after resolutionab, agentsb andccan imagineahas further shared knowledge withd, thereby learning thatq. Therefore (RD1) is invalid. Looking atM ′ , we have thatM ′ ,pq,ε|=K a R bc K b pbutM ′ ,pq,ε̸|=R bc K a K b pbecauseais not aware ofbandcsharing their knowledge so she does not knowbhas learnt thatp. Therefore (RD2) is invalid. On the other hand, there are now novel validities involving distributed knowledge and resolution. Lemma 3.10. (1)If B∩C̸=/0, then|=R B D C φ→D B∪C R B. ⃗ I φfor all ⃗ I∈P(A ) ∗ . (2)If B∩C̸=/0, then|=D B∪C R B. ⃗ I φfor all ⃗ I∈P(A ) ∗ implies|=R B D C φ. (3)If B∩C=/0, then|=R B D C φ↔D C φ. We recall once more, comparing to the first and second items jointly, (RD1)|=R B D C φ↔D B∪C R B φ whenB∩C̸=/0, and, comparing to the third item (RD2)|=R B D C φ↔D C R B φwhenB∩C=/0. The proofs of the above are fairly straightforward but are omitted, as we will present a complete axiomatizationRAD in the next section. Then, the third item is (in one direction) an instantiation of the later axiom (RD) for the case that ⃗ G=Band ⃗ H=ε, whereas for the first item we have ⃗ G=Bas well as ⃗ H=B. ⃗ I. The second item instantiates derivation rule (RDI) ofRAD. Even for fairly simple (‘small’) models given a set of agentsA, and even when everyone’s view isA(for alla,see a ( ⃗ G) =A) there is no bound to uncertainty caused by asynchrony (see the example below). This is different from synchrony, where once everyone’s view isA, this is commonly known. Two notes: with synchrony, we can also have arbitrary higher-order uncertainty, but at the price of large models (with enchained equivalence classes for different agents); and with asynchrony, we can also have common knowledge that everyone’s view isA, namely after resolution withA(full synchronization). Example 3.11.Let|A|≥3. Consider a resolution sequence ⃗ Gwithout /0 and without singleton sets (irrelevant), and withoutA. Suppose towards a contradiction that there is bound to the length| ⃗ G|of ⃗ G after which a further resolution is no longer informative. LetI⊆Awith 1<|I|<|A|. Below we define a (unique) modelMand a (unique) formulaψ∈L DR that distinguishes ⃗ Gfrom ⃗ G.I. Consider the formula Philippe Balbiani et al.83 φ:= V a∈A K a p∧ b K a V b∈A\a ¬(K b p∨K b ¬p) and a modelMconsisting of 2n+1 states namelys 1 ∪s 2 a |a∈A∪t 2 a |a∈A, where the relations ∼ a are the reflexive closure of the conditions: for alla,b∈Awitha̸=b,s 2 a ∼ b t 2 a , and for alla∈A, s 2 a ∼ a s 1 , and where valuationV(p) =s 1 ∪s 2 a |a∈A. We now have thatM,s 1 ,ε|=φ(namely, already in standard epistemic logic,M,s 1 |=φ). LetΣbe the sequence of length| ⃗ G|of agentsa∈Asuch that the last is a member ofIbut not ofBprecedingI, the before last is a member ofBbut not ofB ′ precedingB, and so on. Let the firstBin ⃗ G.Iapart from the selected memberainΣalso contain an agent b̸=a. Now consider ψ:=K Σ (K a K b p∧K b K a p) whereK Σ abbreviates the stackK x . . .K y listing all the members ofΣ. ThenM,s 1 , ⃗ G̸|=ψwhereas M,s 1 , ⃗ G.I|=ψ. For four agentsa,b,c,d, (so-called ‘windmill’) modelMis depicted in Figure 3. In such a model we have that, for example,M,s 1 ,ab.bc|=K c (K a K b p∧K b K a p)butM,s 1 ,ab̸|=K c (K a K b p∧K b K a p). For an example where everyone’s view isAbut uncertainty still remains, consider the sequence of resolutionsabc.bcd.abdafter which all four agents have accessibility relation∼ A . We however have M,s 1 ,abc.bcd.abd̸|=K c K a K d p, but nowM,s 1 ,abc.bcd.abd.abc|=K c K a K d p. p(s 1 ) p a ¬p bcd p b ¬p acd p c ¬p abd p d ¬p abc Figure 3: ‘Windmill’ modelMwith four agents. 4 Axiomatization In this section we show soundness and completeness of the axiomatizationRAD, that is composed of the axioms and rules given in Table 2. Thatφ∈L DR is derivable inRADis denoted⊢φ. Axiomatization RADcontains an infinitary derivation rule (RDI) using admissible forms, defined below. As we have an infinitary derivation rule, in the completeness part of the proof we proceed by maximal consistent theories, also defined below, instead of the usual maximal consistent sets. Showing completeness in- volves ‘unravelling’ a canonical model, in order to get it into the right shape. Before we proceed, let us comment on the differences between axiomatizationsRDandRAD. First, asR ε φisφby definition, the RDaxioms (K D ) . . . (DG) involving distributed knowledge are derivable from (in fact, instantiations of) theRADaxioms (RK D ) . . . (RDG). Second, as resolutionsR ⃗ G for a singleton sequence ⃗ Gare simplyR B for someB⊆A, we can also equate theRDaxioms (RA), (RN) and (RC) with the similarly namedRAD axioms (where theRADaxiom R⊤is derivable inRDusing (NecR)). So the only difference is that the RDaxioms (RD1) and (RD2) are missing (and they are not theorems, because we have shown through 84Resolving Asynchronous Distributed Knowledge (taut)all instantiations of propositional tautologies (RK D )R ⃗ G D B (φ→ψ)→R ⃗ G (D B φ→D B ψ) (RT D )R ⃗ G D B φ→R ⃗ G φ (R5 D )R ⃗ G ¬D B φ→R ⃗ G D B ¬D B φ (RDG)R ⃗ G D B φ→R ⃗ G D C φifB⊆C (RA)R ⃗ G p↔p (R⊤)R ⃗ G ⊤ (RN)R ⃗ G ¬φ↔¬R ⃗ G φ (RC)R ⃗ G (φ∧ψ)↔(R ⃗ G φ∧R ⃗ G ψ) (RD)R ⃗ G D B φ→D see B ( ⃗ G) R ⃗ H φfor all ⃗ H≈ B ⃗ G (NecD)Fromφ, inferD B φ (MP)Fromφandφ→ψ, inferψ (RDI)Fromα(D see B ( ⃗ G) R ⃗ H φ)for all ⃗ H≈ B ⃗ G, inferα(R ⃗ G D B φ) Table 2: AxiomatizationRADfor the logic of resolving asynchronous distributed knowledge counterexample that they are invalid), instead of which we now have axiom (RD) and rule (RDI) (that allow to derive the validities listed in Lemma 3.10). Finally,RDhas (NecR) but notRAD, where an open question is whether (NecR) is derivable inRAD. Let us now proceed. Anadmissible formαis defined byα::=♯|(φ→α)|D B αwhereφ∈L DR andB⊆A. The set of admissible forms is denotedAForm. An admissible form contains a unique occurrence of♯. For α∈AFormandφ∈L DR ,α(φ)is the formula obtained by replacing♯inαbyφ. Lemma 4.1.If⊢φ→ψ, then⊢α(φ)→α(ψ). Proof.The proof proceeds by straightforward induction onα. Theorem 4.2(Soundness).If⊢φthen|=φ. Proof.It needs to be shown that all axioms are valid and all rules preserve validity. As for the axioms, their validity is obvious, except for (RD). Let us then show|=R ⃗ G D B φ→D see B ( ⃗ G) R ⃗ H φfor all ⃗ H∈P(A) ∗ such that ⃗ G≈ B ⃗ H. Suppose there are ⃗ G, ⃗ H,BandM= (W,∼,V),w∈Wsuch thatM,w,ε|=R ⃗ G D B φand M,w,ε̸|=D see B ( ⃗ G) R ⃗ H φ, where ⃗ G≈ B ⃗ H. Then, there arev∈Wand ⃗ I∈P(A) ∗ such thatw∼ see B ( ⃗ G) v i.e. w∼ ⃗ G B v,ε≈ see B ( ⃗ G) ⃗ IandM,v, ⃗ I̸|=R ⃗ H φ, sov, ⃗ I. ⃗ H̸|=φ. Sinceε≈ see B ( ⃗ G) ⃗ Iand ⃗ G≈ B ⃗ H, by Lemma 3.5, ε. ⃗ G= ⃗ G≈ B ⃗ I. ⃗ H. Hence fromM,v, ⃗ I. ⃗ H̸|=φwe can concludeM,w, ⃗ G̸|=D B φi.e. M,w,ε̸|=R ⃗ G D B φ. This contradicts the hypothesis. We now turn to the rules. That (MP) and (Nec) preserve validity can be standardly shown. Let us consider (RDI). For clarity, we only consider the case whereα=♯, whilst others can be treated similarly. Suppose|=D see B ( ⃗ G) R ⃗ H φfor all ⃗ H∈P(A) ∗ such that ⃗ G≈ B ⃗ H. Suppose also, towards a contradiction, ̸|=R ⃗ G D B φ. Then there areM= (W,∼,V),w∈Wsuch thatM,w,ε̸|=R ⃗ G D B φ,i.e. M,w, ⃗ G̸|=D B φ. Hence, there arev∈W, ⃗ H∈P(A) ∗ such thatw∼ ⃗ G B v, ⃗ G≈ B ⃗ HandM,v, ⃗ H̸|=φ, soM,v,ε̸|=R ⃗ H φ. But now, sincew∼ ⃗ G B v, alsow∼ see B ( ⃗ G) v. Moreover,ε≈ see B ( ⃗ G) εby definition. Hence, fromM,v,ε̸|=R ⃗ H φwe getM,w,ε̸|=D see B ( ⃗ G) R ⃗ H φ, where ⃗ G≈ B ⃗ H. This contradicts the hypothesis. Therefore,|=R ⃗ G D B φ. Standard frames and semi-standard frames.Instead of models wherein∼ B is equal to∩ b∈B ∼ b (and even by definition) we need models wherein∼ B may be a proper subset of∩ b∈B ∼ b . The first we Philippe Balbiani et al.85 namestandard models, based onstandard frames, whereas the second aresemi-standard modelsbased semi-standard frames. More precisely, a semi-standard frame is a structure(W,∼)whereWis a non- empty set and, for allB⊆A,∼ B is an equivalence relation onWsuch that for allB,C⊆A, ifB⊆C then∼ C ⊆∼ B . The completeness proofs involving distributed knowledge often involve ‘unravelling’ a canonical model based on a semi-standard frame into one that is based on a standard frame with the same information content [24, 1]. In our completeness proof we employ the results relating standard and semi-standard frames obtained in [5, Section 6] and in particular [5, Proposition 6.10] that the validities on standard frames and semi-standard frames correspond. Here, we merely adapt this to our setting, where the result to use is that from any modelM= (W,∼,V)based on a semi-standard frame we can construct a modelM ′ = (W ′ ,∼ ′ ,V ′ )based on a standard frame; inM ′ the worlds consist of pairs(w,f) wherew∈Wandfis a function of the setFof such functions of typeP(A)×A→P(W). One can then show that (i) if(w,f)∼ ′ ⃗ G B (v,g), thenw∼ ⃗ G B v, and that (i) ifw∼ ⃗ G B v, then there isg∈Fsuch that (w,f)∼ ′ ⃗ G B (v,g), for all ⃗ G∈P(A) ∗ . Providing a procedure to transform each model based on a semi-standard frame into another modally equivalent model that is based on a standard frame requires the following notions. For allB⊆Aand for all w∈W,[w] B is the equivalence class ofwmodulo∼ B . For allX,Y∈P(W), letX+Y= (X )∪(Y ) 1 . We recall thatFis the set of all functions of typef:P(A)×A−→P(W). Let nowM= (W,∼,V)be a model based on a semi-standard frame. We define the modelM ′ = (W ′ ,∼ ′ ,V ′ )byW ′ :=W×F,(w,f)∈V ′ (p)iffw∈V(p)and for allB⊆A,∼ ′ B is the binary relation onW ′ such that for all(w,f),(v,g)∈W ′ ,(w,f)∼ ′ B (v,g)iff, for allC⊆A, the two following conditions hold: −[w] C +Σ a∈C f(C,a) = [v] C +Σ a∈C g(C,a) −ifa∈B∩C,thenf(C,a) =g(C,a)for alla∈A. Obviously, all∼ ′ B are equivalence relations, so(W ′ ,∼ ′ )is a frame. We now show that it is a standard frame. Lemma 4.3.The frame(W ′ ,∼ ′ )is semi-standard. Proof.LetB,B ′ ⊆A. SupposeB⊆B ′ . Suppose∼ ′ B ′ ̸⊆∼ ′ B . Hence, there exist(w,f),(v,g)∈W ′ such that(w,f)∼ ′ B ′ (w,g)and(w,f)̸∼ ′ B (v,g). Thus, either there existsC⊆Asuch that[w] C +Σ a∈C f(C,a)̸= [v] C +Σ a∈C g(C,a), or there existC⊆Aanda∈B∩Csuch thatf(C,a)̸=g(C,a). In the former case, since(w,f)∼ ′ B ′ (v,g), therefore[w] C +Σ a∈C f(C,a) = [v] C +Σ a∈C g(C,a): a contradiction. In the latter case, sinceB⊆B ′ , alsoa∈B ′ ∩C. Since(w,f)∼ ′ B ′ (v,g), thereforef(C,a) =g(C,a): a contradiction. Therefore∼ ′ B ′ ⊆∼ ′ B . Lemma 4.4.The semi-standard frame(W ′ ,∼ ′ )is standard. Proof.LetB,B ′ ⊆A. Suppose∼ ′ B∪B ′ ̸⊇ ∼ ′ B ∩ ∼ ′ B ′ . Hence, there exist(w,f),(v,g)∈W ′ such that (w,f)̸∼ ′ B∪B ′ (v,g),(w,f)∼ ′ B (v,g)and(w,f)∼ ′ B ′ (v,g). Thus, for allC⊆A,[w] C +Σ b∈C f(C,b) = [v] C + Σ b∈C g(C,b). Moreover, for allC⊆Aand for allb∈B∩C,f(C,b) =g(C,b)and for allC⊆Aand for all b∈B ′ ∩C,f(C,b) =g(C,b). Since(w,f)̸∼ ′ B∪B ′ (v,g), there existE⊆Aanda∈(B∪B ′ )∩Esuch that f(E,a)̸=g(E,a). But, sincea∈B∪B ′ , eithera∈B, ora∈B ′ . In the former case, since for allC⊆A and for allb∈B∩C,f(C,b) =g(C,b), thereforef(E,a) =g(E,a): a contradiction. In the latter case, since for allC⊆Aand for allb∈B ′ ∩C,f(C,b) =g(C,b), thereforef(E,a) =g(E,a): a contradiction. Therefore∼ ′ B∪B ′ ⊇∼ ′ B ∩∼ ′ B ′ . 1 Note that(P(W),/0,W,+,∩)is a Boolean ring. 86Resolving Asynchronous Distributed Knowledge Lemma 4.5.For all w,v∈W,f,g∈Fand B⊆A, if(w,f)∼ ′ B (v,g), then w∼ B v. Proof.LetB⊆Aand(w,f),(v,g)∈W ′ be such that(w,f)∼ ′ B (v,g). Hence, for allC⊆A,[w] C + Σ a∈C f(C,a) = [v] C +Σ a∈C g(C,a). Moreover, for alla∈B∩C,f(C,a) =g(C,a). Thus, forC=Bwe get[w] B +Σ a∈B f(B,a) = [v] B +Σ a∈B g(B,a). Moreover, for alla∈B,f(B,a) =g(B,a). Consequently, [w] B = [v] B . Hence,w∼ B v. Corollary 4.6.For all w,v∈W,f,g∈Fand ⃗ G∈P(A) ∗ ,B⊆A, if(w,f)∼ ′ ⃗ G B (v,g), then w∼ ⃗ G B v. Lemma 4.7.For all w,v∈W,f∈Fand B⊆A, if w∼ B v, then there is g∈Fsuch that(w,f)∼ ′ B (v,g). Proof.Letw,v∈W. Supposew∼ B v,i.e.[w] B = [v] B . Since(W ′ ,∼ ′ )is semi-standard, for allC⊆A, ifC⊆B, thenw∼ C vand[w] C = [v] C . To constructg:P(A)×A−→P(W), consider an enumeration a 1 ,a 2 , . . . ,a k of the agents inA. For allC⊆Aand for alla∈A, we defineg(C,a)as follows: −ifa∈B∩Ctheng(C,a):=f(C,a) −ifa∈C , let 1≤i≤kbe such thata=a i . Now, ifi=min1≤j≤k|a j ∈C , then g(C,a):= [w] C +[v] C + ∑ b∈C f(C,b); otherwiseg(C,a):=/0. −ifa/∈Ctheng(C,a):=/0. The reader may easily verify that(w,f)∼ ′ B (v,g). Corollary 4.8.For all w,v∈W,f∈Fand ⃗ G∈P(A) ∗ ,B⊆A, if w∼ ⃗ G B v, then there is g∈Fsuch that (w,f)∼ ′ ⃗ G B (v,g). We can now prove the following lemma that allows one to transform any semi-standard model into a standard model while preserving the satisfaction relation. Lemma 4.9.Let semi-standard M= (W,∼,V)be given and standard M ′ = (W ′ ,∼ ′ ,V ′ )be constructed from M as above. For allφ∈L DR , w∈W , f∈Fand ⃗ G∈P(A) ∗ : M,w, ⃗ G|=φiff M ′ ,(w,f), ⃗ G|=φ. Proof.The proof proceeds by induction onφ. Letw∈W,f∈Fand ⃗ G∈P(A) ∗ . • Ifφ=p, then obviouslyM,w, ⃗ G|=p⇔M ′ ,(w,f), ⃗ G|=p. • Ifφ=⊤, then obviouslyM,w, ⃗ G|=⊤andM ′ ,(w,f), ⃗ G|=⊤. • Ifφ=¬ψ,φ=ψ∧ψorφ=R B ψ, we conclude by applying the inductive hypothesis. This is straightforward. • Ifφ=D B ψ, supposeM,w, ⃗ G|=D B ψandM ′ ,(w,f), ⃗ G̸|=D B ψ. Then, there are(v,g)∈W ′ and ⃗ H∈P(A) ∗ such that(w,f)∼ ′ ⃗ G B (v,g), ⃗ G≈ B ⃗ HandM ′ ,(v,g), ⃗ H̸|=ψ. By induction hypothesis, thenM,v, ⃗ H̸|=ψ. Since(w,f)∼ ′ ⃗ G B (v,g), by Corollary 4.6,w∼ ⃗ G B v. Moreover, ⃗ G≈ B ⃗ H. Therefore M,w, ⃗ G̸|=D B φ. This contradicts the hypothesis. Suppose nowM,w, ⃗ G̸|=D B φandM ′ ,(w,f), ⃗ G|=D B ψ. Then, there arev∈W, ⃗ H∈P(A) ∗ such thatw∼ ⃗ G B v, ⃗ G≈ B ⃗ HandM,v, ⃗ H̸|=ψ. Now, by Corollary 4.8, there isg∈Fsuch that(w,f)∼ ′ ⃗ G B (v,g). By induction hypothesis, fromM,v, ⃗ H̸|=ψwe getM ′ ,(v,g), ⃗ H̸|=ψ, where(w,f)∼ ′ ⃗ G B (v,g) and ⃗ G≈ B ⃗ H. HenceM ′ ,(w,f), ⃗ G̸|=D B ψ: a contradiction. Proposition 4.10.For allφ∈L DR , ifφis valid on standard frames thenφis valid on semi-standard frames. Philippe Balbiani et al.87 Proof.By Lemma 4.9. We now move to the proof of the completeness ofRAD. This requires further terminology. Atheory Tis a set of formulasφ∈L DR such thatTcontains all formulas derivable inRAD;T is closed under (MP) andTis closed under (RDI). A theoryTisconsistentif it does not contain⊥. Furthermore,Tismaximal consistentifTis consistent and, for all theoriesT ′ , ifT⊊T ′ , thenT ′ is not consistent. Note that the only inconsistent theory is the theory containing all formulas. ForTa theory, χ∈L DR andB⊆Awe defineT+χ:=φ|χ→φ∈TandD B T:=φ|D B φ∈T. Lemma 4.11.Let T be a theory,χ∈L DR and B⊆A. Then, T+χand D B T are also theories. Moreover, T⊆T+χandχ∈T+χ. Finally, if¬χ/∈T , T+χis consistent, and ifχ/∈T , T+¬χis consistent. Proof.This is standard. Lemma 4.12.Let ⃗ G∈P(A) ∗ ,B⊆A andφ∈L DR . If T is a theory andα(R ⃗ G D B φ)/∈T , then there is ⃗ H∈P(A)such that ⃗ G≈ B ⃗ H andα(D see B ( ⃗ G) R ⃗ H φ)/∈T . Proof.This is straightforward, sinceTis closed under (RDI). Lemma 4.13(Lindenbaum’s Lemma).If T is a consistent theory, then there is a maximal consistent theoryΣsuch that T⊆Σ. Proof.LetTbe a consistent theory andφ 0 ,φ 1 ,·an enumeration of formulas inL DR . For allk∈N, we define the theoryT k as follows (from the construction and Lemma 4.11 it follows that theseT k are theories, becauseTis a theory): T 0 :=T T k+1 := T k if¬φ k ∈T k T k +φ k if¬φ k /∈T k andφ k does not have the shape¬α(R ⃗ G D B ψ) T k +¬α(D see B ( ⃗ G) R ⃗ H ψ)if¬φ k /∈T k andφ k does have the shape¬α(R ⃗ G D B ψ), for some ⃗ H≈ B ⃗ Gsuch thatα(D see B ( ⃗ G) R ⃗ H ψ)/∈T k Note that in the third case of the inductive step, such a sequence ⃗ His known to exist by Lemma 4.12. Let nowΣ:= S k≥0 T k . It needs to be shown thatΣis a maximal consistent theory. First note that, by construction, for allφ∈L DR , eitherφ∈Σor¬φ∈Σ. We first show thatΣis a theory. ThatΣcontainsRADand is closed by modus ponens is straightfor- ward. Suppose now there are ⃗ G∈P(A) ∗ ,B∈P(A),φ∈L DR andα∈AFormsuch thatα(D see B ( ⃗ G) R ⃗ H φ)∈ Σfor all ⃗ H≈ B ⃗ G. Suppose alsoR ⃗ G D B φ/∈Σ. Then¬R ⃗ G D B φ∈Σ. Letk∈Nsuch thatφ k =¬R ⃗ G D B φ. Then, sinceφ k ∈Σ,¬φ k /∈Σso in particular¬φ k /∈T k . SinceT k is a theory andR ⃗ G D B φ/∈T k , by Lemma 4.12, there is ⃗ H≈ B ⃗ Gsuch thatα(D see B ( ⃗ G) R ⃗ H φ)/∈T k . Hence, by construction,T k+1 =T k + ¬α(D see B ( ⃗ G) R ⃗ H φ). Thereforeα(D see B ( ⃗ G) R ⃗ H φ)/∈Σ, which contradicts the hypothesis. Furthermore,Σis consistent because so is eachT k . We now show thatΣis maximal consistent. Let ∆be a theory strictly containingΣ. Then, there isφ k ∈L DR such thatφ k /∈Σandφ k ∈∆. Sinceφ k /∈Σ, ¬φ k ∈Σ⊂∆. Hence,¬φ k ∈∆, so∆is not consistent. We now (re)introduce the relation∼ B . LetΣ,∆be two maximal consistent theories,B⊆A. Then Σ∼ B ∆iffD B Σ⊆∆. Note that by definition∼ B∪C ⊆∼ B ∩∼ C , but equality is not guaranteed. 88Resolving Asynchronous Distributed Knowledge Lemma 4.14(Existence Lemma).LetΣbe a maximal consistent theory, B⊆A,φ∈L DR . If ˆ D B φ∈Σ, then there is a maximal consistent theory∆such thatΣ∼ B ∆andφ∈∆. Proof.Suppose ˆ D B φ∈Σ. Then¬D B ¬φ∈ΣsoD B ¬φ/∈Σ. Hence¬φ/∈D B Σ. So, by Lemma 4.11, D B Σ+φis consistent. Now, by Lindenbaum’s Lemma, we can extendD B Σ+φto a maximal consistent theory∆such thatD B Σ+φ⊆∆. By Lemma 4.11 again,D B Σ⊆D B Σ+φsoD B Σ⊆∆. HenceΣ∼ B ∆. Moreover,φ∈D B Σ+φ, soφ∈∆. Definition 4.15(Canonical model).Thecanonical model M= (W,∼ B B⊆A ,V)is defined by −W=Σ|Σis a maximal consistent theory; −Σ∼ B ∆if, and only if,D B Σ⊆∆; −V(p) =Σ∈W|p∈Σ. Notice the canonical model is defined on a semi-standard frame. Lemma 4.16(Truth Lemma).For allφ∈L DR , ⃗ G∈P(A) ∗ andΣ∈W : R ⃗ G φ∈ΣiffΣ, ⃗ G|=φ. Proof.The proof proceeds by induction onφ. • Ifφ=p: by (RA) we get:R ⃗ G p∈Σ⇔p∈Σ⇔Σ, ⃗ G|=p. • Ifφ=⊤:Σ, ⃗ G|=⊤and, by (R⊤),R ⃗ G ⊤∈Σ. • Ifφ=¬ψ: by (RN) we get:R ⃗ G ¬ψ∈Σ⇔¬R ⃗ G ψ∈Σ⇔R ⃗ G ψ/∈Σ (IH) ⇔Σ, ⃗ G̸|=ψ⇔Σ, ⃗ G|=¬ψ. • Ifφ=ψ∧χ: by (RC) we getR ⃗ G (ψ∧χ)∈Σ⇔R ⃗ G ψ∧R ⃗ G χ∈Σ⇔R ⃗ G ψ∈ΣandR ⃗ G χ∈Σ (IH) ⇔ Σ, ⃗ G|=ψandΣ, ⃗ G|=χ⇔Σ, ⃗ G|=ψ∧χ. • Ifφ=R B ψ:R ⃗ G R B ψ∈Σ⇔R ⃗ G.B ψ∈Σ (IH) ⇔Σ, ⃗ G.B|=ψ⇔Σ, ⃗ G|=R B ψ. • Ifφ=D B ψ: suppose firstR ⃗ G D B ψ∈ΣandΣ, ⃗ G̸|=D B ψ. Then there are∆, ⃗ Hsuch thatΣ∼ ⃗ G B ∆, ⃗ G≈ B ⃗ Hand∆, ⃗ H̸|=ψ. By induction hypothesis, then,R ⃗ H ψ/∈∆. Now, sinceR ⃗ G D B φ∈Σand, by (RD)R ⃗ G D B ψ→D see B ( ⃗ G) R ⃗ H ψ∈Σ(because ⃗ G≈ B ⃗ H), soD see B ( ⃗ G) R ⃗ H ψ∈Σ. Moreover, since Σ∼ ⃗ G B ∆, alsoΣ∼ see B ( ⃗ G) ∆, soD see B ( ⃗ G) Σ⊆∆. ThenR ⃗ H ψ∈∆, which contradictsR ⃗ H ψ/∈∆. Suppose nowR ⃗ G D B ψ/∈ΣandΣ, ⃗ G|=D B ψ. SinceR ⃗ G D B ψ/∈ΣandΣis closed under (RDI), there is ⃗ H∈P(A) ∗ such that ⃗ G≈ B ⃗ HandD see B ( ⃗ G) R ⃗ H ψ/∈Σ. Then,¬D see B ( ⃗ G) R ⃗ H ψ∈Σ, so ˆ D see B ( ⃗ G) ¬R ⃗ H ψ∈ Σ. By the Existence Lemma, there is a maximal consistent theory∆such thatΣ∼ see B ( ⃗ G) ∆and ¬R ⃗ H ψ∈∆, soR ⃗ H ψ/∈∆. By induction hypothesis then,∆, ⃗ H̸|=ψ. But sinceΣ∼ see B ( ⃗ G) ∆, also Σ∼ ⃗ G B ∆and ⃗ G≈ B ⃗ H, so∆, ⃗ H̸|=ψimpliesΣ, ⃗ G̸|=D B ψ, which contradicts the hypothesis. Theorem 4.17(Completeness).For allφ∈L DR , if|=φ, then⊢φ. Proof.Letφ∈L DR . We show the contrapositive: if̸⊢φ, then̸|=φ. Suppose then̸⊢φ. Thenφ/∈RAD soRAD+¬φis consistent: we extend it to a maximal consistent theoryΣ, by Lindenbaum’s Lemma. Therefore,¬φ=R ε ¬φ∈Σ. By the Truth Lemma,Σ,ε|=¬φsoΣ,ε̸|=φ. Henceφis not valid on semi-standard frames. By Proposition 4.10, then,φis not valid on standard frames. Therefore̸|=φ. Philippe Balbiani et al.89 5 Conclusion and further research We presented a logic of resolving asynchronous distributed knowledge, compared it to the logic of re- solving (synchronous) distributed knowledge known from the literature, and provided an infinitary ax- iomatization for our asynchronous logic. There are a fair number of open questions about this novel logic. (i) We defined two notions of validity, with respect to the empty resolution sequence and with respect to arbitrary resolution sequences, but we do not know whether these define the same set of validi- ties. (i) We gave an infinitary axiomatization, but we have no proof that a finitary axiomatization does not exist. (i) Is necessitation of resolution validity preserving (resp. an admissible derivation rule)? (iv) Is satisfiability decidable, and if so, what is the complexity? (v) Given the embedding of the syn- chronous into the asynchronous semantics, what is the expressivity hierarchy comparing the language fragments with synchronous and with asynchronous distributed knowledge, and with or without resolu- tion? It seems fairly straightforward to show that resolving asynchronous distributed knowledge is more expressive than resolving synchronous distributed knowledge, or at least on the level of so-called update expressivity that describes relations between pointed epistemic models instead of properties of pointed epistemic models in the case of formula expressivity. Concerning the latter, clearly, a sequence of two resolutionsab.bcdoes not correspond to a single resolutionBfor someB⊆A, wherein all agents inB are equally well informed. A more interesting question is whether resolving asynchronous distributed knowledge is more expressive than logical semantics of synchronous distributed knowledge with more involved dynamics than resolution, such as [10, 11, 16]. For example, a sequence of resolutionsab.bc corresponds to a single communication graph (as in [16]) namely werebandcreceive information from a,b,cwhereasaonly receives information froma,b, and, for a more involved example, the uncertainty of an agentdbetween resolutionsabandab.bccan be simulated as non-public information exchange as in [11]. We wish to investigate that in the future. (vi) Can we determine when a resolution in a given sequence is redundant (because uninformative), such as (immediately) repeating the same resolution? (vii) We wish to extend the language and semantics with common knowledge. Acknowledgements.We thank the referees for their reviews: their useful suggestions have been es- sential for improving the readability of a preliminary version of this paper. References [1] T. Ågotnes & Y.N. Wáng (2017):Resolving distributed knowledge.Artif. Intell.252, p. 1–21, doi:10.1016/j.artint.2017.07.002. [2] N. Alechina, P. Balbiani & D. Shkatov (2012):Modal logics for reasoning about infinite unions and intersections of binary relations.J. Appl. Non Class. Logics22(4), p. 275–294, doi:10.1080/11663081.2012.705960. [3] K.R. Apt, E. Kopczynski & D. Wojtczak (2017):On the Computational Complexity of Gossip Protocols. In: Proceedings of the 26th IJCAI, p. 765–771, doi:10.24963/ijcai.2017/106. [4] C. Areces & B. ten Cate (2007):Hybrid Logics. In J. van Benthem, P. Blackburn & F. Wolter, editors:The Handbook of Modal Logic, Elsevier, Amsterdam, The Netherlands, doi:10.1016/S1570-2464(07)80017-6. [5] P. Balbiani & H. van Ditmarsch (2024):Towards Dynamic Distributed Knowledge. In A. Ciabattoni, D. Gabelaia & I. Sedlár, editors:Proceedings of Advances in Modal Logic, College Publications, p. 125– 146. [6] P. Balbiani & D. Vakarelov (2003):PDL with Intersection of Programs: A Complete Axiomatization.Journal of Applied Non-Classical Logics13(3-4), p. 231–276, doi:10.3166/jancl.13.231-276. 90Resolving Asynchronous Distributed Knowledge [7] A. Baltag, R. Boddy & S. Smets (2018):Group knowledge in interrogative epistemology. In H. van Dit- marsch & G. Sandu, editors:Jaakko Hintikka on Knowledge and Game-Theoretical Semantics, Outstanding contributions to logic 12, Springer, p. 131–164, doi:10.1007/978-3-319-62864-6_5. [8] A. Baltag, L.S. Moss & S. Solecki (1998):The Logic of Public Announcements, Common Knowledge, and Private Suspicions. In:Proceedings of 7th TARK, p. 43–56, doi:10.1007/978-3-319-20451-2_38. [9] A. Baltag & S. Smets (2013):Protocols for belief merge: Reaching agreement via communication.Log. J. IGPL21(3), p. 468–487, doi:10.1093/JIGPAL/JZS049. [10] A. Baltag & S. Smets (2020):Learning What Others Know. In:Proceedings of 23rd LPAR,EPiC Series in Computing73, p. 90–119, doi:10.29007/plm4. [11] A. Baltag & S. Smets (2024):Logics for Data Exchange and Communication. Proceedings of the 15th Advances in Modal Logic Prague. [12] J. van Benthem & S. Minica (2009):Toward a Dynamic Logic of Questions. In X. He, J.F. Horty & E. Pacuit, editors:Logic, Rationality, and Interaction. Proceedings of LORI 2009, LNCS 5834, Springer, p. 27–41, doi:10.1007/s10992-012-9233-7. [13] P. Blackburn & J. Seligman (1995):Hybrid languages.Journal of Logic, Language, and Information4, p. 251–272, doi:10.1007/BF01049415. [14] R. Boddy (2014):Epistemic Issues and Group Knowledge. Master’s thesis, ILLC, University of Amsterdam. Available athttps://eprints.illc.uva.nl/id/document/2156/. Master of Logic Series MoL-2014- 03. [15] R. Carrington (2013):Learning and Knowledge in Social Networks. Master’s thesis, ILLC, University of Amsterdam. Available athttps://eprints.illc.uva.nl/id/document/2124/. Master of Logic Series MoL-2013-18. [16] A. Castañeda, H. van Ditmarsch, D.A. Rosenblueth & D.A. Velázquez (2023):Communication Pattern Logic: Epistemic and Topological Views.Journal of Philosophical Logic, doi:10.1007/s10992-023-09713-8. [17] A. Castañeda, H. van Ditmarsch, D.A. Rosenblueth & D.A. Velázquez (2023):Comparing the update ex- pressivity of communication patterns and action models.Electronic Proceedings in Theoretical Computer Science379, p. 157–172, doi:10.4204/EPTCS.379.14. [18] Z. Christoff, N. Gratzl & O. Roy (2022):Priority Merge and Intersection Modalities.The Review of Sym- bolic Logic15(1), p. 165–196, doi:10.1017/S1755020321000058. [19] R. Danecki (1985):Nondeterministic propositional dynamic logic with intersection is decidable. In:Com- putation Theory, Springer, p. 34–53, doi:10.1007/3-540-16066-3_5. [20] C. Degremont, B. Löwe & A. Witzel (2011):The synchronicity of dynamic epistemic logic. In:Proceedings of 13th TARK, ACM, p. 145–152, doi:10.1145/2000378.2000395. [21] H. van Ditmarsch & M. Gattinger (2024):You can only be lucky once: optimal gossip for epistemic goals. Mathematical Structures in Computer Science, p. 1–28, doi:10.1017/S0960129524000082. [22] H. van Ditmarsch, W. van der Hoek & B. Kooi (2007):Dynamic Epistemic Logic.Synthese Library337, Springer, doi:10.1007/978-1-4020-5839-4. [23] H. van Ditmarsch, W. van der Hoek & L.B. Kuijer (2020):The logic of gossiping.Artificial Intelligence286, p. 103306, doi:10.1016/j.artint.2020.103306. [24] R. Fagin, J.Y. Halpern & M.Y. Vardi (1992):What Can Machines Know? On the Properties of Knowledge in Distributed Systems.J. ACM39(2), p. 328–376, doi:10.1145/128749.150945. [25] R. Galimullin & L.B. Kuijer (2024):Varieties of Distributed Knowledge. Proceedings of the 15th Advances in Modal Logic Prague. [26] G. Gargov & S. Passy (1990):A note on Boolean Modal Logic. In:Mathematical Logic, Plenum Press, p. 299–309, doi:10.1007/978-1-4613-0609-2_21. [27] G. Gargov, S. Passy & T. Tinchev (1987):Modal environment for Boolean speculations. In:Mathematical Logic and its Applications, Plenum Press, p. 253–263, doi:10.1007/978-1-4613-0897-3_17. Philippe Balbiani et al.91 [28] R. Goldbach (2015):Modelling Democratic Deliberation. Master’s thesis, ILLC, University of Amsterdam. Available athttps://eprints.illc.uva.nl/id/document/2216/. Master of Logic Series MoL-2015- 05. [29] V. Goranko (1996):Hierarchies of modal and temporal logics with reference pointers.Journal of Logic, Language, and Information5, p. 1–24, doi:10.1007/BF00215625. [30] V. Goranko & S. Passy (1992):Using the universal modality: gains and questions.Journal of Logic and Computation2, p. 5–30, doi:10.1093/logcom/2.1.5. [31] J.Y. Halpern & Y. Moses (1984):Knowledge and Common Knowledge in a Distributed Environment. In: Proceedings of the 3rd PODC, p. 50–61, doi:10.1145/800222.806735. [32] J.Y. Halpern & Y. Moses (1990):Knowledge and Common Knowledge in a Distributed Environment.Journal of the ACM37(3), p. 549–587, doi:10.1145/79147.79161. [33] D. Harel (1985):Recurring dominoes: making the highly undecidable highly understandable.North-Holland Mathematical Studies102, p. 51–71, doi:10.1016/S0304-0208(08)73075-5. [34] D. Harel, D. Kozen & J. Tiuryn (2000):Dynamic Logic.MIT Press, Cambridge MA, doi:10.7551/mitpress/2516.001.0001. Foundations of Computing Series. [35] F. Hayek (1945):The Use of Knowledge in Society.American Economic Review35, p. 519–530. Available athttps://w.jstor.org/stable/1809376. [36] R. Hilpinen (1977):Remarks on personal and impersonal knowledge.Canadian Journal of Philosophy7, p. 1–9, doi:10.1080/00455091.1977.10716173. [37] W. van der Hoek & J.-J.Ch. Meyer (1992):Making Some Issues of Implicit Knowledge Explicit.Int. J. Found. Comput. Sci.3(2), p. 193–223, doi:10.1142/S0129054192000139. [38] M. Lange (2005):A lower complexity bound for propositional dynamic logic with intersection. In:Advances in Modal Logic 5, College Publications, p. 133–147. [39] M. Lange & C. Lutz (2005):2-Exp Time lower bounds for propositional dynamic logics with intersection. Journal of Symbolic Logic70(4), p. 1072–1086, doi:10.2178/jsl/1129642115. [40] F. Massacci (2001):Decision procedures for expressive description logics with intersection, composition, converse of roles and role identity. In:Proceedings of the 17th IJCAI, Morgan Kaufmann, p. 193–198. [41] Y. Moses & M.R. Tuttle (1988):Programming Simultaneous Actions Using Common Knowledge.Algorith- mica3, p. 121–169, doi:10.1007/BF01762112. [42] L.S. Moss (2015):Dynamic Epistemic Logic. In H. van Ditmarsch, J.Y. Halpern, W. van der Hoek & B. Kooi, editors:Handbook of epistemic logic, College Publications, p. 261–312. [43] E. Orłowska (1990):Kripke semantics for knowledge representation logics.Studia Logica49, p. 255–272, doi:10.1007/BF00935602. [44] R. Parikh & R. Ramanujam (1985):Distributed Processes and the Logic of Knowledge. In:Proceedings of Logics of Programs,Lecture Notes in Computer Science193, p. 256–268, doi:10.1007/3-540-15648-8_21. [45] R. Parikh & R. Ramanujam (2003):A knowledge based semantics of messages.Journal of Logic, Language and Information12, p. 453–467, doi:10.1023/A:1025007018583. [46] S. Passy & T. Tinchev (1985):PDL with data constants.Information Processing Letters20, p. 35–41, doi:10.1016/0020-0190(85)90127-9. [47] S. Passy & T. Tinchev (1991):An essay in Combinatory Dynamic Logic.Information and Computation93, p. 263–332, doi:10.1016/0890-5401(91)90026-X. [48] J.A. Plaza (2007):Logics of Public Communications.Synthese158(2), p. 165–179, doi:10.1007/s11229- 007-9168-7. Reprint of Plaza’s 1989 workshop paper. [49] M. de Rijke (1992):The modal logic of inequality.Journal of Symbol Logic57, p. 566–584, doi:10.2307/2275293. 92Resolving Asynchronous Distributed Knowledge [50] D.R. Swanson (1986):Undiscovered Public Knowledge.The Library Quarterly: Information, Community, Policy56(2), p. 103–118, doi:10.1086/601720. [51] D. Vakarelov (1991):Modal logics for knowledge representation systems.Theoretical Computer Science90, p. 433–456. [52] D.A. Velázquez (2019):Una relación entre las lógicas modales y el enfoque topológico del cómputo dis- tribuido. Master’s thesis, Instituto de Investigaciones en Matemáticas Aplicadas y en Sistemas, UNAM, Mexico. [53] D.A. Velázquez (2024):Pattern Models: Dynamic Epistemic Logics for Distributed Systems. Ph.D. thesis, Instituto de investigaciones en matemáticas aplicadas y en sistemas, UNAM, Mexico. [54] D.A. Velázquez, A. Castañeda & D.A. Rosenblueth (2021):Communication Pattern Models: an Extension of Action Models for Dynamic-Network Distributed Systems. In:Proceedings of TARK XVIII,EPTCS335, p. 307–321, doi:10.4204/EPTCS.335.29.