1 Introduction↩︎

If Anne (\(a\)) knows \(p\) and Bill (\(b\)) knows \(p \rightarrow q\) then neither knows \(q\) but they still have distributed knowledge of \(q\). If they were to share their information, they would both know \(q\). Distributed knowledge modalities are intersection modalities: \(p\) is distributed knowledge for \(a\) and \(b\) in a world \(w\), iff \(p\) is true in all worlds \(v\) which are indistinguishable for \(a\) and for \(b\) from the actual world \(w\). In this case, distributed knowledge of \(p\) becomes common knowledge of \(p\) by sharing. However, as is well known, propositions may be distributed knowledge even when the agents cannot share this information. For another scenario, if \(p\) is true but \(a\) does not know this, and \(b\) knows that, then \(a\) and \(b\) have distributed knowledge of the former, as it is true in all worlds which are indistinguishable for \(a\) and for \(b\). But when \(b\) informs \(a\) of \(p\), or even of \(p\) and that she does not know \(p\), agent \(a\) learns that \(p\) which makes her ignorance false. Modalities for sharing information are intersection updates (intersection update modalities): in a world \(w\) proposition \(q\) is true after \(a\) and \(b\) share their knowledge iff \(q\) is true in the model wherein we have replaced the indistinguishability relations for \(a\) and \(b\) by 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 agents \(a,b,c\) are initially aware that \(a\) knows \(p\) and \(b\) knows \(p \rightarrow 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 know \(q\). 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 does not know \(q\). 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 knows \(p\). 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 \(\Box_a\) and \(\Box_b\), interpreted on Kripke models with binary relations \(R_a\) and \(R_b\), resp., the problem of intersection modalities boils down to the observation that adding a novel modality (suggestively named) \(\Box_{a\cup b}p\) is true in a world \(w\) iff \(p\) is true in all worlds \(v\) which are \(R_{a}\)-accessible or \(R_{b}\)-accessible does not create problems. This is so because in such a case, \(R_{a\cup b}=R_{a}\cup R_{b}\) and one simply has that \(\Box_{a\cup b}p\) is equivalent to \(\Box_{a}p\wedge\Box_{b}p\). Whereas adding a modality \(\Box_{a\cap b}\) such that \(\Box_{a\cap b}p\) is true in a world \(w\) iff \(p\) is true in all worlds \(v\) which are \(R_{a}\)-accessible and \(R_{b}\)-accessible creates problems. One now has that \(R_{a\cap b}=R_{a}\cap R_{b}\) and we can no longer define \(\Box_{a\cap b}p\) with the other modalities, the canonical model is not of the right kind. One way to address this is to expand the logical language with nominals [@Passy:Tinchev:1985; @Passy:Tinchev:1991] which led to the development of hybrid logics [@Blackburn:Seligman:1995; @Areces:tenCate:2007] and related logics [@Goranko:1996; @Goranko:Passy:1992; @derijke:1992]. Another way to address this led to the development of modal logics with intersection modalities, where we highlight Propositional Dynamic Logic (\(\mathbf{PDL}\)) with intersection [@Danecki:1985; @Harel:1985], and epistemic logics with distributed knowledge [@FaginHV92; @halpernmoses:1990; @AlechinaBS12], although there are many further approaches such as Boolean Modal Logic [@Gargov:Passy:1990; @Gargov:et:al:1986], and knowledge representation logics [@Orlowska:1990; @Vakarelov:1991].

Propositional dynamic logic. In \(\mathbf{PDL}\) we generalize from modalities \(\Box_a\) to modalities \(\Box_\alpha\) where \(\alpha\) is a program and that are interpreted in models with recursively defined relations \(R_\alpha\), with the same basic programs \(a,b,\dots\) as above but apart from \(\cup\) operations of sequential execution and arbitrary iteration, as well as another basic program called test [@hareletal:2000]. By also adding intersection \(\alpha\cap\beta\) of programs to \(\mathbf{PDL}\), we obtain \(\mathbf{IPDL}\) [@Danecki:1985; @Harel:1985]. Here, \(\alpha\cap\beta\) represents parallel execution of programs \(\alpha\) and \(\beta\) as \(R_{\alpha\cap\beta}=R_\alpha\cap R_\beta\), so again, similar to \(R_a \cap R_b\) above. Various works involving the complexity [@Lange:2005; @Lange:Lutz:2005; @Massacci:2001] and axiomatization [@balbianietal:2003] of \(\mathbf{IPDL}\) have appeared.

Distributed knowledge. The notion of distributed knowledge is rooted in sociology, economics, and philosophy [@HayekAER45; @hilpinen:1977; @swanson:1986] under different terms; [@HayekAER45] is an admirable pamphlet against centralized planning and in favour of distributed planning (and authority), [@hilpinen:1977] calls it ‘impersonal knowledge’, and [@swanson:1986] ‘undiscovered public knowledge’. The earliest epistemic logical source is [@halpernmoses:85b] (the later journal version [@halpernmoses:1990] also gives a logical semantics), wherein the notion was called ‘implicit knowledge’, followed on the heals by [@ParikhR85] 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 [@FaginHV92; @HoekM92], where these publications achieved completeness by different methods. All such works interpret modalies \(\Box_a\) not on models with arbitrary relations \(R_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 [@FaginHV92; @HoekM92] and continue to be investigated in more recent times [@rusbouke.aiml:2024].

Intersection updates. After the history of intersection modalities we now proceed with the history of intersection updates, the history of sharing information. Given a Kripke model with two (typically) equivalence relations \(R_a\) and \(R_b\), the intersection update modality \(\Box_{a \cap b}^{\mathsf{update}}\) is such that \(\Box_{a \cap b}^{\mathsf{update}} p\) is true in a world \(w\) of a model \(M\) iff \(p\) is true in the same world \(w\) but in the updated model \(M^{a \cap b}\) wherein the relations \(R_a\) and \(R_b\) are replaced by the relation \(R_a \cap R_b\). That is all. Note that when we interpret the intersection modality we (may) change the point of evaluation in a given model but we do not change the model wherein we evaluate the formula bound by the modality, whereas if we interpret the intersection update modality we do not change the point of evaluation but we (may) change the model wherein 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 in dynamic epistemic logics, such as public announcement logic [@plaza:2007] and action model logic [@baltagetal:1998] (for references see [@hvdetal.del:2007; @moss.handbook:2015]), although these are updates with very different properties.

The first paper involving the intersection update to our knowledge was [@stefanjohan:2009], in a mixed setting of epistemic and inquisitive logic. The intersection update here is the resolve action, encoding the answer to a question thus resolving an issue (intersecting an epistemic relation with an issue relation). On the heals of [@stefanjohan:2009] were a number of related publications [@BaltagS13; @carrington:2013; @boddy:2014; @goldbach:2015; @baltagetal.hintikka:2018]. Here, [@BaltagS13] introduces intersection updates on plausibility structures whereas [@baltagetal.hintikka:2018] further generalizes the inquisitive and epistemic setting of [@stefanjohan:2009]. Independently, slightly later again, [@AgotnesW17] focuses on intersection updates (called resolution) and distributed knowledge for arbitrary sets of agents and their interaction. Further developments introduce uncertainty even among agents who have shared information [@Baltag20; @baltagsmets.aiml:2024], which also relates to a different strand of research coming out of distributed computing, and intersection updates incarnate the execution of communication graphs or communication patterns [@diego:2021; @cdrv:2023; @armandoetal.tark:2023; @diego:2019; @diego:2024]. The operation of pooling or basic intersection in [@ChristoffGratzlRoy2022] corresponds to a intersection (update) modality similar to what we call resolution here; this updates models with plausibility relations. An attempt to combine distributed knowledge and intersection updates into a single modality for sharing knowledge is [@BalbianiD24].

Asynchrony. Intersection modalities like distributed knowledge and intersection updates such as resolution and communication patterns assume synchrony (and even so in distributed computing, were a round of 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 [@halpernmoses:1990], and ‘full information protocols’ in distributed computing [@MosesT88] correspond to intersection updates. In dynamic epistemic logics such asynchrony requires a history-based semantics [@parikhetal:2003; @degremontetal:2011]. Even with more restricted information exchange such as in gossip protocols this leads to far more challenging axiomatizations (and higher complexities) [@logicofgossiping:2020; @hvdetal.lucky:2024; @AptKW17].

Overview of content. In Section 2 we review the logic of resolving (synchronous) distributed knowledge. 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 [@AgotnesW17]. Let \(A\) be a finite non-empty set of agents, and \(P\) a countable set of propositional variables (atoms). The language \(\mathcal{L}_{DR}\) is defined by \(\varphi::= p \mid \top \mid (\varphi\wedge\varphi) \mid \neg \varphi\mid D_B \varphi\mid R_B \varphi\), where \(p \in P\) and \(B \subseteq A\). The sublanguage \(\mathcal{L}_{D}\) with only modalities \(D_B\varphi\) is the language of distributed knowledge. For \(\Box_a\) we now write \(K_a\), and it is defined by abbreviation as \(D_{\lbrace a \rbrace}\). Formula \(R_B \varphi\) is read as ‘after resolution for group of agents \(B\), \(\varphi\) (is true)’.

The structures are multi-agent epistemic models \((W,\sim,V)\) for the set \(A\) of agents (where \((W,\sim)\) is a multi-agent frame). We can see \(\sim\) as a set \(\{\sim_a\}_{a \in A}\) of binary indistinguishability relations (or as a function mapping each agent to such a relation \(\sim_a\)). Valuation \(V\) is a function from the set of atoms to the powerset of \(W\) mapping each atom to the subset of worlds where it is true. We write \({\sim_B} := {\bigcap_{a \in B} \sim_a}\) for the epistemic relation of a group \(B\) (so that \(\sim_\emptyset \;= W \times W\)).

If \(M = (W,\sim,V)\) and \(B\subseteq A\) then updated model \(M^B := (W,\sim^B,V)\) is the result of resolution for group \(B\), where \({\sim^B_a} := {\bigcap_{b \in B} \sim_b}\) if \(a \in B\) and \({\sim^B_a} := {\sim_a}\) otherwise. In updated model \(M^B\) the relations for the agents \(a \in B\) have been updated from \(\sim_a\) to \(\sim_B\). Hence, in \(M^B\) we have that \({\sim^B_B} = {\sim^B_a}\) for all \(a \in B\), unlike in \(M\). Given these notations, we have that \({\sim^B_C} = {\sim_C}\) if \(B \cap C = \emptyset\) and that \({\sim^B_C} = {\sim_{B\cup C}}\) if \(B\cap C \neq \emptyset\). Note that \(M^a = M\) and that \(M^\emptyset = M\). For \(M^{\{a_1,\dots,a_n\}}\) we write \(M^{a_1\dots a_n}\), and for \((M^B)^C\) we write \(M^{B.C}\).

Let a vector \(\vec{G}\) represent a sequence \(B_1\dots B_n\), where \(B_i \subseteq A\) for \(1 \leq i \leq n\)—the empty sequence is \(\epsilon\). By \(|\vec{G}|\) we denote the length of \(\vec{G}\), and \(a \notin \vec{G}\) means that \(a\notin B\) for any \(B \subseteq A\) such that \(B\) occurs in \(\vec{G}\). We write \(\sim^{\vec{G}}_a\) for the accessibility relation of an agent \(a\) in \(M^{\vec{G}}\).

We now present the semantics. The satisfaction relation \(\models\) is defined by induction on \(\varphi\in \mathcal{L}_{DR}\), where \(p\in P\) and \(G \subseteq A\). \[\begin{array}{lcccl} M,w \models p & &\text{iff} & &w \in V(p) \\ M,w \models \top & &\text{iff} & &\text{true} \\ M,w \models \neg \varphi& &\text{iff} & &M,w \not\models\varphi\\ M,w \models \varphi\wedge\psi & &\text{iff} & &M,w \models\varphi\text{ and } M,w \models \psi \\ M,w \models D_B \varphi& &\text{iff} & &M,v \models \varphi\text{ for all } v \in W \text{ such that } w \sim_B v \\ M,w \models R_B \varphi& &\text{iff} & &M^B,w \models \varphi \end{array}\] A formula \(\varphi\in\mathcal{L}_{DR}\) is valid iff for all models \(M = (W,\sim,V)\) and for all \(w \in W\), \(M,w \models\varphi\).

The axiomatization RD for 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 reducing \(\mathcal{L}_{DR}\)-formulas to \(\mathcal{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 that Replacement of Equivalents (RE: from \(\varphi\leftrightarrow\psi\) derive \(\chi[p/\varphi] \leftrightarrow\chi[p/\psi]\), where \(\chi[p/\varphi]\) is uniform substitution of \(p\) in \(\chi\) by \(\varphi\)) is derivable in RD. This is needed to reduce formulas of form \(R_G R_H \varphi\) where \(G \neq H\), as there is no axiom of shape \(R_G R_H \varphi\leftrightarrow\dots\)

3 Resolving asynchronous distributed knowledge↩︎

We now propose a logical framework for resolving asynchronous distributed knowledge. The logical language \(\mathcal{L}_{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 \(\varphi\) in pointed models \((M,w)\), where such an \(M\) could be an updated \(M^{\vec{G}}\), we now wish to interpret formulas in pointed models \((M,w,\vec{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 \(\vec{G}\) than from when she was not. In order to compare pairs \((w,\vec{G})\) and \((v,\vec{H})\) we not only need the indistinguishability relation \(\sim_a\) between worlds \(w\) and \(v\) but also a novel resolution relation \(\approx_a\) between resolution sequences \(\vec{G}\) and \(\vec{H}\). Connecting both relations is the view by agent \(a\) of sequence \(\vec{G}\), denoted \(\mathsf{see}_a(\vec{G})\), that is the set of agents \(B\) with whom \(a\) has shared the equivalence relations (e.g., recalling the introduction, after resolution \(ab\), she has shared it with \(b\) as the new \(\sim_a\) is now \(\sim_{a \cap b}\)). The set \(\mathsf{see}_a(\vec{G})\) determines the knowledge gained by agent \(a\) after history \(\vec{G}\)—or after any other history \(\vec{H}\) that she cannot distinguish from \(\vec{G}\). Let us begin by defining the resolution relation and the view, and show some relevant results relating them.

Resolution relation. Let \(a \in A\), and \(\vec{G},\vec{H} \in \mathcal{P}(A)^\ast\) be given. The resolution relation \(\approx_a\) between resolution sequences is the equivalence closure of: \[\begin{array}{lcll} \epsilon \approx_a \epsilon & \text{iff} & \text{true} \\ \vec{G}.B \approx_a \vec{H} & \text{iff} & \vec{G} \approx_a \vec{H} &\text{when } a \notin B \\ \vec{G}.B \approx_a \vec{H}.B & \text{iff} & \vec{G} \approx_b \vec{H} \text{ for all } b \in B \hfill \qquad\qquad\qquad &\text{when } a \in B \end{array}\] We further define \({\approx_B} := {\bigcap_{a\in B} \approx_a}\). Note that \(\approx_\emptyset\) is the universal relation.

View. The view \(\mathsf{see}_a(\vec{G})\) of agent \(a\) of a resolution sequence \(\vec{G}\) is the set \(B \subseteq A\) of agents such that given any model \(M = (W,\sim,V)\), agent \(a\)’s current relation \(\sim_a^{\vec{G}}\) is \(\cap_{b \in B} \sim_b\). Let \(B \subseteq A\), then:

• \(\mathsf{see}_B(\epsilon) := B\);

• \(\mathsf{see}_B(\vec{G}.C) := \mathsf{see}_{B \cup C}(\vec{G})\) when \(B \cap C \neq \emptyset\);

• \(\mathsf{see}_B(\vec{G}.C) := \mathsf{see}_B(\vec{G})\) when \(B \cap C = \emptyset\).

For \(\mathsf{see}_{\{a\}}(\vec{G})\) we write \(\mathsf{see}_a(\vec{G})\). Note that \(\mathsf{see}_B(\vec{G}) = C\) does not mean that the view of all agents in \(B\) is \(C\), but only that the union of the views of all agents in \(B\) is \(C\). It is easy to see that \(\mathsf{see}_B(\vec{G}) = \bigcup_{b \in B} \mathsf{see}_b(\vec{G})\) (induction on the length of \(\vec{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.

Similarly, if \(\vec{I}\in \mathcal{P}(A\setminus B)^\ast\), then \(\vec{G}\approx_B \vec{H}.\vec{I}\) if, and only if, \(\vec{G} \approx_B \vec{H}\).

Consequently, we also have as a corollary that whenever \(B\cap C = \emptyset\), then \(C \approx_B \vec{G}\) iff \(\vec{G}\in \mathcal{P}(A\setminus B)^\ast\).

Consequently, we also have that \(\vec{G} \approx_B \vec{H}\) implies \(\mathsf{see}_B(\vec{G}) = \mathsf{see}_B(\vec{H})\). From [@BalbianiD24] we further recall that for all models \(M=(S,\sim,V)\), \({\sim^{\vec{G}}_B} = {\sim_{\mathsf{see}_B(\vec{G})}}\). In other words, we might as well have stated that \(\vec{G} \approx_B \vec{H}\) implies \({\sim^{\vec{G}}_B} = {\sim^{\vec{H}}_B}\), or that \(\vec{G} \approx_B \vec{H}\) implies \(\sim_{\mathsf{see}_B(\vec{G})} = \sim_{\mathsf{see}_B(\vec{H})}\), and will quote Lemma 6 in such cases.

However, \(\mathsf{see}_a(\vec{G}) = \mathsf{see}_a(\vec{H})\) does not imply \(\vec{G} \approx_a \vec{H}\). Typical counterexamples are that \(\mathsf{see}_a(\vec{G}.a)=\mathsf{see}_a(\vec{G})\) whereas \(\vec{G}.a \not\approx_a \vec{G}\) and \(\mathsf{see}_a(ab.ab) = \mathsf{see}_a(ab)\) whereas \(ab.ab \not\approx_a ab\).

We proceed to define the semantics.

As not uncommon in history-based semantics, two notions of validity emerge. A formula \(\varphi\in\mathcal{L}_{DR}\) is \(\epsilon\)-valid if \(M,w,\epsilon \models\varphi\) for all models \(M = (W,\sim,V)\) and for all \(w \in W\). A formula \(\varphi\in\mathcal{L}_{DR}\) is \(\ast\)-valid (or always valid) if \(M,w,\vec{G} \models\varphi\) for all \(M = (W,\sim,V)\), \(w \in W\), and all \(\vec{G} \in \mathcal{P}(A)^*\). We should acknowledge that we are uncertain if \(\epsilon\)-validity and \(\ast\)-validity correspond. This is a question left for future research.

This asynchronous semantics looks very much like the synchronous semantics of the previous section, except for the clause for distributed knowledge. Let us be explicit about some differences and correspondences. First, Example 1 shows that \(M,w,\vec{G} \models \varphi\) is not equivalent to (in the synchronous semantics) \(M^{\vec{G}},w \models \varphi\). So there is a real difference.

But we can also look at this in another way, rather illustrating a correspondence. Let us for a vanishing moment consider a synchronous distributed knowledge modality \(\boldsymbol{D}_B \varphi\), interpreted as follows on our history-based models, wherein we only have replaced \(\vec{G} \approx_B \vec{H}\) by \(\vec{G} = \vec{H}\). \[\begin{array}{lll} M,w,\vec{G} \models \boldsymbol{D}_B \varphi& \text{iff} & M,v,\vec{H} \models \varphi\text{ for all } v \in W, \;\vec{H} \in \mathcal{P}(A)^\ast \text{ such that } w \sim^{\vec{G}}_B v \text{ and } \vec{G} = \vec{H} \end{array}\] Now write \(M,w,\vec{G}\models \varphi\) anywhere for the synchronous \(M^{\vec{G}},w\models\varphi\) (while replacing all \(D_B\) by \(\boldsymbol{D}_B\)). This embeds the synchronous semantics into the asynchronous semantics. So, with respect to the above example, indeed, \(M,pq,ab \not\models K_cK_a p\), but on the other hand we now have \(M,pq,ab \models \boldsymbol{K}_c\boldsymbol{K}_a p\), which after all corresponds to \(M^{ab}, pq \models K_cK_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 resolution \(R_B\) has the same semantics either way, only the interpretation of distributed knowledge \(D_B\) is different synchronously and asynchronously. Despite the identical semantics, with asynchrony, resolution \(R_B\) encodes partial synchronization for group of agents \(B\) without any agents not in \(B\) being aware of that, whereas, with synchrony, resolution \(R_B\) encodes full synchronization for all agents however with aspects of partial observation: group of agents \(B\) jointly learn (all) each other’s knowledge whereas all agents not in \(B\) learn that, but not what the agents in \(B\) learn. The agents not in \(B\) only 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. All axioms and rules of RD remain valid (or validity preserving), except (RD1) and (RD2); and maybe (NecR). If \(\epsilon\)-valid and \(*\)-valid were the same (the open question), then we would have necessitation of resolution. (It is easy to see why: assume \(\models\varphi\) and (NecR). Given arbitrary \((M,w)\), from the first we get that \(M,w,\epsilon \models \varphi\), and from that and the second \(M,w,\epsilon \models R_B \varphi\), so that \(M,w,B \models \varphi\). We therefore easily show that \(\varphi\) is \(*\)-valid by induction on the length of resolution sequences.)

On the other hand, there are now novel validities involving distributed knowledge and resolution.

We recall once more, comparing to the first and second items jointly, (RD1) \(\models R_B D_C \varphi\leftrightarrow D_{B \cup C} R_B \varphi\) when \(B \cap C \neq \emptyset\), and, comparing to the third item (RD2) \(\models R_B D_C \varphi\leftrightarrow D_C R_B \varphi\) when \(B \cap C = \emptyset\). The proofs of the above are fairly straightforward but are omitted, as we will present a complete axiomatization RAD in the next section. Then, the third item is (in one direction) an instantiation of the later axiom (RD) for the case that \(\vec{G}=B\) and \(\vec{H}=\epsilon\), whereas for the first item we have \(\vec{G} = B\) as well as \(\vec{H}= B.\vec{I}\). The second item instantiates derivation rule (RDI) of RAD.

Even for fairly simple (‘small’) models given a set of agents \(A\), and even when everyone’s view is \(A\) (for all \(a\), \(\mathsf{see}_a(\vec{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 is \(A\), 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 is \(A\), namely after resolution with \(A\) (full synchronization).

4 Axiomatization↩︎

In this section we show soundness and completeness of the axiomatization RAD, that is composed of the axioms and rules given in Table 2. That \(\varphi\in \mathcal{L}_{DR}\) is derivable in RAD is denoted \(\vdash \varphi\). Axiomatization RAD contains 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 involves ‘unravelling’ a canonical model, in order to get it into the right shape. Before we proceed, let us comment on the differences between axiomatizations RD and RAD. First, as \(R_\epsilon\varphi\) is \(\varphi\) by definition, the RD axioms (K\(_D\)) …(DG) involving distributed knowledge are derivable from (in fact, instantiations of) the RAD axioms (RK\(_D\)) …(RDG). Second, as resolutions \(R_{\vec{G}}\) for a singleton sequence \(\vec{G}\) are simply \(R_B\) for some \(B \subseteq A\), we can also equate the RD axioms (RA), (RN) and (RC) with the similarly named RAD axioms (where the RAD axiom R\(\top\) is derivable in RD using (NecR)). So the only difference is that the RD axioms (RD1) and (RD2) are missing (and they are not theorems, because we have shown through 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 7). Finally, RD has (NecR) but not RAD, where an open question is whether (NecR) is derivable in RAD. Let us now proceed.

An admissible form \(\alpha\) is defined by \(\alpha ::= \sharp \;|\;(\varphi\rightarrow\alpha) \;|\;D_B \alpha\) where \(\varphi\in \mathcal{L}_{DR}\) and \(B \subseteq A\). The set of admissible forms is denoted \(AForm\). An admissible form contains a unique occurrence of \(\sharp\). For \(\alpha \in AForm\) and \(\varphi\in \mathcal{L}_{DR}\), \(\alpha(\varphi)\) is the formula obtained by replacing \(\sharp\) in \(\alpha\) by \(\varphi\).

Standard frames and semi-standard frames. Instead of models wherein \(\sim_B\) is equal to \(\cap_{b \in B} \sim_b\) (and even by definition) we need models wherein \(\sim_B\) may be a proper subset of \(\cap_{b \in B} \sim_b\). The first we name standard models, based on standard frames, whereas the second are semi-standard models based semi-standard frames. More precisely, a semi-standard frame is a structure \((W,\sim)\) where \(W\) is a non-empty set and, for all \(B\subseteq A\), \(\sim_B\) is an equivalence relation on \(W\) such that for all \(B,C\subseteq A\), if \(B\subseteq C\) then \(\sim_C \subseteq \sim_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 [@FaginHV92; @AgotnesW17]. In our completeness proof we employ the results relating standard and semi-standard frames obtained in [@BalbianiD24] and in particular [@BalbianiD24] 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 model \(M = (W,\sim,V)\) based on a semi-standard frame we can construct a model \(M' = (W',\sim',V')\) based on a standard frame; in \(M'\) the worlds consist of pairs \((w,f)\) where \(w \in W\) and \(f\) is a function of the set \(\mathcal{F}\) of such functions of type \(\mathcal{P}(A) \times A \rightarrow\mathcal{P}(W)\). One can then show that (i) if \((w,f)\sim'^{\vec{G}}_B (v,g)\), then \(w\sim^{\vec{G}}_B v\), and that (ii) if \(w\sim^{\vec{G}}_B v\), then there is \(g\in \mathcal{F}\) such that \((w,f)\sim'^{\vec{G}}_B (v,g)\), for all \(\vec{G}\in \mathcal{P}(A)^\ast\).

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 all \(B \subseteq A\) and for all \(w \in W\), \(\lbrack w\rbrack_{B}\) is the equivalence class of \(w\) modulo \(\sim_{B}\). For all \(X,Y \in \mathcal{P}(W)\), let \(X+Y=(X\setminus Y)\cup(Y\setminus X)\)¹. We recall that \({\mathcal{F}}\) is the set of all functions of type \(f:\mathcal{P}(A)\times A\longrightarrow\mathcal{P}(W)\).

Let now \(M=(W,\sim,V)\) be a model based on a semi-standard frame. We define the model \(M'=(W',\sim',V')\) by \(W':=W\times{\mathcal{F}}\), \((w,f) \in V'(p)\) iff \(w\in V(p)\) and for all \(B \subseteq A\), \(\sim'_{B}\) is the binary relation on \(W'\) such that for all \((w,f),(v,g) \in W'\), \((w,f){\sim'_{B}}(v,g)\) iff, for all \(C \subseteq A\), the two following conditions hold:

\(- \quad \lbrack w\rbrack_{C}+\Sigma_{a \in C}f(C,a)=\lbrack v\rbrack_{C}+\Sigma_{a \in C}g(C,a)\)

\(- \quad \text{if } a\in B \cap C, \text{ then } f(C,a)=g(C,a) \text{ for all } a \in A\).
Obviously, all \(\sim'_B\) are equivalence relations, so \((W',\sim')\) is a frame. We now show that it is a standard frame.

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.

We now move to the proof of the completeness of RAD. This requires further terminology.

A theory \(T\) is a set of formulas \(\varphi\in \mathcal{L}_{DR}\) such that \(T\) contains all formulas derivable in RAD; \(T\) is closed under (MP) and \(T\) is closed under (RDI). A theory \(T\) is consistent if it does not contain \(\bot\). Furthermore, \(T\) is maximal consistent if \(T\) is consistent and, for all theories \(T'\), if \(T \subsetneq T'\), then \(T'\) is not consistent. Note that the only inconsistent theory is the theory containing all formulas. For \(T\) a theory, \(\chi \in \mathcal{L}_{DR}\) and \(B\subseteq A\) we define \(T + \chi:= \lbrace \varphi\;|\;\chi \rightarrow\varphi\in T \rbrace\) and \(D_BT := \lbrace \varphi\;| \;D_B \varphi\in T \rbrace\).

We now (re)introduce the relation \(\sim_B\). Let \(\Sigma,\Delta\) be two maximal consistent theories, \(B\subseteq A\). Then \(\Sigma \sim_B \Delta\) iff \(D_B \Sigma \subseteq \Delta\). Note that by definition \(\sim_{B \cup C} \;\subseteq \;\sim_B \cap \sim_C\), but equality is not guaranteed.

Notice the canonical model is defined on a semi-standard frame.

5 Conclusion and further research↩︎

We presented a logic of resolving asynchronous distributed knowledge, compared it to the logic of resolving (synchronous) distributed knowledge known from the literature, and provided an infinitary axiomatization 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 validities. (ii) We gave an infinitary axiomatization, but we have no proof that a finitary axiomatization does not exist. (iii) 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 synchronous into the asynchronous semantics, what is the expressivity hierarchy comparing the language fragments with synchronous and with asynchronous distributed knowledge, and with or without resolution? 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 resolutions \(ab.bc\) does not correspond to a single resolution \(B\) for some \(B \subseteq A\), wherein all agents in \(B\) 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 [@Baltag20; @baltagsmets.aiml:2024; @cdrv:2023]. For example, a sequence of resolutions \(ab.bc\) corresponds to a single communication graph (as in [@cdrv:2023]) namely were \(b\) and \(c\) receive information from \(a,b,c\) whereas \(a\) only receives information from \(a,b\), and, for a more involved example, the uncertainty of an agent \(d\) between resolutions \(ab\) and \(ab.bc\) can be simulated as non-public information exchange as in [@baltagsmets.aiml:2024]. 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 essential for improving the readability of a preliminary version of this paper.

---

1. Note that \((\mathcal{P}(W),\emptyset,W,+,\cap)\) is a Boolean ring.↩︎