1 Introduction↩︎

Information may come in both propositional form (Boolean variables) and non-propositional form (e.g. numbers, names, addresses, pictures, videos, etc). Such data can be encoded as values of local variables (e.g. a cryptographic key or a password), that are stored and processed in certain locations or ‘sites’(e.g., websites, folders, databases, etc), and can be retrieved when these sites are accessed as ‘sources’. Each such source can be thought of as an agent (either because it actually is the knowledge base of a natural or artificial agent, or because we think of it as an abstract ‘agent’ possessing exactly the information that is stored at it).¹ Such agents either ‘own’ their data, or else have gained access to them from other sources: we say that the agents ‘know’ the values of these variables, and some of them can also modify these values. More complex data may have an extended location, the information being distributed among a number of agents: one can recover the value of such complex variables only by accessing several sources.

To deal with non-propositional information, multi-agent epistemic logic has been extended in recent years with “knowing-what” operators \(K_a x\) or \(K_A x\) for (individual or distributed) knowledge of (the value of) some variable \(x\) (in addition to the traditional modalities \(K_a \varphi\) and \(K_A \varphi\) for individual or distributed knowledge of a proposition \(\varphi\)). This work traces back to Plaza [@Plaza] and subsequent investigations by [@vEGWang; @Yanjing; @WangFan1; @WangFan2; @GuWang; @Ding; @Hong; @Baltag2016; @BS25] on formalizing ‘knowledge de re’. While Plaza axiomatized the static logic of ‘knowing what’, the extension with dynamic operators \([!\varphi]\psi\) for (propositional) public announcements \(!\varphi\) was only later axiomatized by Wang and Fan [@WangFan2]. To ‘pre-encode’ this dynamics using DEL-style reduction axioms [@sep-dynamic-epistemic], these authors needed a conditional version of ‘knowing what’: \(K_a^\varphi x\) means that \(a\) knows the value of \(x\) given the information that proposition \(\varphi\) was the case.

In recent work [@BS25], we extended this setting with operators \(K_A^\varphi x\) for conditional distributed knowledge of the value of \(x\) by a group \(A\). This was motivated by the need to deal with a more complex dynamics, going beyond propositional announcements or other traditional DEL-events [@sep-dynamic-epistemic; @BM; @BMS; @DHK; @NEW-BMS; @BMD; @LDII]. In a data-exchange event, agents may gain access to ‘sources’ (i.e., to other agents’ knowledge bases), in which case they can be assumed to instantly ‘read’ (and copy in their own knowledge base) all the information stored at those sources. Such events were previously considered in our work [@BS20; @BS24], and in fact they subsume many other forms of non-propositional informational dynamics that were previously considered, e.g. “tell us all you know” in [@Baltag2010] (and with a different, interrogative interpretation in [@BenthemMinica1; @BenthemMinica2]), in-group sharing [@Baltag2010; @Boddy2014; @Goldbach2015; @BBS2016], and ‘resolution’ [@AgotnesWang2017]. Other examples of data-exchange events covered in [@BS25] include private changing of the value of a variable (e.g. one’s password), parallel data-sharing within different subgroups (e.g., in a poster session), suspected hacking of a private database, private detection of such hacking, etc. As noted in [@BS20], when an agent \(a\) gains access to another agent \(b\)’s knowledge base, her new state of knowledge matches the distributed knowledge of the group \(\{a, b\}\). So on the side of propositional knowledge, we needed operators \(K_A \varphi\) for distributed knowledge² within group \(A\). A similar move was also necessary on the side of “knowing what”: operators \(K_A x\), expressing that the group \(A\) has distributed knowledge of the value of \(x\); in fact, to pre-encode public-announcement dynamics we needed the conditional version \(K_A^\varphi x\) of these operators. Note that this type of conditional knowledge may not imply knowledge of the ‘real’ value of \(x\) (in the actual world), but only the fact that the agent or group can uniquely determine a hypothetical value of \(x\) (applicable only to worlds satisfying \(\varphi\)). To axiomatize these notions, in the presence of equality of values \(x=y\), we were lead to introduce definite description terms \(x_A^\varphi\) that can explicitly refer to such hypothetical values: \(x_a^\varphi\) denotes (in the actual world) the (unique) value that \(x\) would have according to agent \(a\) if \(\varphi\) were true. Using this, we were able to provide in [@BS25] a complete axiomatization for the corresponding dynamic-epistemic logic. But for this, we had to restrict the dynamics to ‘semi-public’ events (a class that does not include e.g. secret hacking). On the other hand, in [@BS24] we axiomatized a logic with unrestricted dynamics, covering ‘arbitrary’ data-exchange events (including complicated hacking scenarios). But this was based on a restricted static logic base, that did not include non-propositional knowledge operators, but only the traditional epistemic modalities \(K_a \varphi\) and \(K_A\varphi\), as well as (a major generalization of) common knowledge \(C_A \varphi\) (in the form of polyadic conditional-epistemic group modalities \(C_A^{\mathbf{e}}\varphi_1 \ldots \varphi_n\), indexed by data-exchange events \({\mathbf{e}}\)). There were no explicit variables \(x\) in the logic, so no assertions \(x=y\) or \(Px_1\ldots x_n\) talking about the properties of specific pieces of (non-propositional) data, as well as no “knowledge-what” operators \(K_a x\), \(K_A x\) or \(K_A^\varphi x\). And, because of these limitations, the class of data-exchange events was still inherently restricted: e.g., there was no event of privately changing the value (such as one’s password), and no events involving preconditions of the form \(K_a x\) (for instance, no “conditional hacking”, in which it is common knowledge that an agent \(a\) may be hacking another agent \(b\)’s database if and only if she came to know \(b\)’s password).

In this paper, we overcome the limitations present in the frameworks of both [@BS24] and [@BS25], by providing a common generalization, while also greatly increasing the expressivity of the logic. More specifically, we generalize the operators \(K_A ^\varphi x\) to expressions \(|x|_A^\varphi\leq N\) (for any natural number \(N\)), saying that: if given additional information \(\varphi\), the group \(A\) can narrow down the possible values of variable \(x\) to at most \(N\) possibilities (for any natural number \(N\)). In other words, the group has distributed knowledge that, if \(\varphi\) is the case then the value of \(x\) belongs to a given list of \(N\) possible values.³ This is a useful addition when dealing with cryptographic protocols. Indeed, if \(N\) is ‘small enough’ and \(x\) is say another agent \(b\)’s communication key or private password, then any intruder \(a\) having the capability \(|x|_a^\varphi \leq N\) will be able to hack \(b\)’s communication (by simply trying out all the \(N\) possible values), as soon as she may receive the information \(\varphi\). The same applies to a group \(A\) of hackers if they can collectively narrow down the possibilities, i.e., have the capability \(|x|_A^\varphi \leq N\). As done in [@BS25] for \(K_A^\varphi x\), whenever we have \(|x|_a \leq N\) we introduce definite descriptions denoting each of the \(N\) hypothetical values of \(x\). For this, we assume given a salient total order \(\leq\) on the set of values. This is useful in numerical applications, but it also allows us to convert cardinality statements \(|x|_a \leq N\) into ordinal descriptions \(1_N.x_A^\varphi\), \(2_N.x_A^\varphi\) etc, denoting “the first (or the second, etc) of the \(\leq N\) possible values of \(x\) according to \(A\) given \(\varphi\)”.⁴ To capture the properties of the total order, we include in our language order statements \(x\leq y\) (besides equality of values \(x=y\) and possibly other predicates \(P x_1\ldots x_n\)). We obtain a very expressive dynamic-epistemic logic, and we are able to completely axiomatize it and prove its decidability. Our proofs make an innovative use of known methods. For the static logic, we first use filtration to obtain a quasi-model: this is not a ‘real’ model, but just a syntactic construction, in which variables have no values (and the group relations are non-standard, as they are not intersections of the individual relations). We then follow the usual method for dealing with distributed knowledge, by unraveling the model into an infinite tree and redefining the relations to make them standard. However, new complications ensue due to the variables, and especially due to the combination of equality \(x=y\) and non-propositional knowledge \(K_A x\); the problems are in fact compounded by the presence of formulas for order \(x\leq y\) and narrowing down \(|x|_A^\varphi\leq N\). Here, we use our definite descriptions to ensure that the local properties of variables \(x\) are preserved and continuously transmitted at far-away nodes of the tree.⁵ Defining the total order on values over the tree requires a use of the Order Extension Principle, and hence of the Axiom of Choice. Finally, the completeness for the dynamic logic uses DEL-style reduction axioms; but again, the details are quite tantalizing. Even the soundness of some reduction laws (e.g., the ‘Cutoff-Min. Change’ axiom) is not at all obvious!

We should mention a self-imposed limitation: due to the page-limit, we chose not to include common knowledge operators \(C_A \varphi\), whose dynamics introduces another source of complexity, requiring additional technical developments and proofs. We leave this step for the journal-version of this paper.

2 Motivating Examples↩︎

Example 1 Alice and Bob are each given a number \(x(a), x(b)\in \mathbb{N}=\{0, 1, 2,\ldots\}\), while the value of the sum \(x(e):=x(a)+ x(b)\) is stored in a closed envelope \(e\). It is common knowledge that: (1) each of the two sees his/her own number, but neither of them can see the others’ number, nor the sum \(x(e)\); (2) one of the two numbers \(x^a, x^b\) is the immediate successor of the other (i.e. either \(x(a)= x(b) + 1\) or \(x(b) = x(a) + 1\)). We represent this situation using an infinite Kripke model, where states are triplets of numbers \((x(a), x(b), x(e))\), and the accessibility relations \(\sim_a\) and \(\sim_b\) encode the agents’ uncertainty. We also have an accessibility relation \(\sim_e\) for the ‘envelope’ (treated as an abstract ‘agent’), encoding the information contained in it. The formula \(K_a x(a) \wedge K_b x(b)\), saying that agents know their numbers, is valid on this model, while \(K_e x(e)\) says that the sum \(x(e)\) is stored in the envelope. On the other hand, agents \(a\) and \(b\) can together figure out the sum: we have \(K_{\{a,b\}} x(e)\), i.e. the group \(A=\{a,b\}\) has “distributed” knowledge of \(x(e)\). The formulas \(|x(a)|_b \leq 2\), \(|x(b)|_a\leq 2\), \(|x(e)|_a\leq 2\) and \(|x(e)|_b\leq 2\) say that the live agents can narrow down the possibilities (for the other’s number, as well as for the sum) to at most two. To name these values, we write e.g. \(1_2.x(e)_a\) for the first (i.e., the least) of the two possible values of the sum \(x(e)\) according to Alice, \(2_2.x(e)_a\) for the second least (=largest) of the two, etc. The picture is:

Example 1, continued Next, it is common knowledge that Alice ‘hacks’ Bob’s database. This is a ‘semi-public’ event \(!(a:b)\), which updates the model by replacing \(\sim_a\) with the intersection \(\sim_a\cap\sim_b\):

Example 2: an alternative scenario Start in the initial situation from Example 1. This time no hacking is allowed, but Alice and Bob are asked: “Do you know each other’s number”? They both answer (truthfully, publicly and simultaneously): “I don’t know”. This is a public announcement \(! (\neg K_a x(b) \wedge \neg K_b x(a))\). The updated model is obtained by deleting states \((0,1,1)\) and \((1,0,1)\) from the initial model:

If asked the same question again, they again answer “I don’t know”, which deletes \((2,1,3)\) and \((1,2,3)\):

If asked for the 3rd time, Alice says ” I know Bob’s number” and Bob says “I don’t know”. The announcement \(! (K_a x(b) \wedge \neg K_b x(a))\) deletes all states but \((2,3,5)\): so we have \(x(a)=2, x(b)=3, x(e)=5\).

Example 3 Starting again in the initial situation from Example 1, agents are publicly announced that \(x(a)<x(b)\). After that, Alice knows Bob’s number, i.e. \([!(x(a)<x(b))] K_a x(b)\). We can reason hypothetically about this scenario in the original model, without updating it, using conditional knowledge \(K_a^{x(a)< x(b)} x(b)\) of the (hypothetical) value of \(x(b)\) given the condition \(x_a<x_b\). We can also name this hypothetical value using a conditionalized version of the “least-of-\(N\)" description introduced above, e.g. writing \(1_1.x(b)_a^{x(a)<x(b)}\) for the unique (=least out of only one) value of \(x(b)\) that is considered possible by Alice conditional on \(x(a)<x(b)\). But note that, when considering a condition that is known to be false (e.g., \(x(a)=x(b)\)), there are no such hypothetical values: so the best we can do is to interpret the ‘least’ value as the ‘infimum’ \(1_1. x(b)_a^{x(a)=x(b)}= inf\,\emptyset= \infty\). This means that we are working in \(\mathbb{N}^\top:=\mathbb{N}\cup \{\infty\}\).

Example 4: Back in time Imagine now that our story starts earlier, at a time when each ‘agent’ (Alice \(a\), Bob \(b\), and the envelope \(e\)) only ‘knows’ their own number (but not yet the correlations between numbers). The model is just \(\mathbb{N}\times \mathbb{N}\times \mathbb{N}\), with \((x(a), x(b), x(c))\sim_a(x'(a), x'(b), x'(c))\) iff \(x(a) =x'(a)\), and similarly for \(b\) and \(e\). Next, the correlations are publicly announced \(!((x(a)=x(b)+1\vee x(b)=x(a)+1)\wedge x(e)=x(a)+x(b))\), and after that the semi-public hacking !(a:b) happens. Can we check that Alice will know \(x(e)\) after this scenario without updating the model \(\mathbb{N}\times \mathbb{N}\times \mathbb{N}\)? For this, we will need an operator \(K_{a,b}^{ (x(a)=x(b)+1\vee x(b)=x(a)+1) \wedge (x(e)=x(a)+x(b))} x(e)\) for conditional distributed knowledge of a value.

To formalize the examples, we need the following ingredients: equality \(x=y\); order \(x<y\); functions \(x=y+1\), \(z=x+y\); (conditional) (distributed) knowledge of a number \(K_A^\varphi x\); a way to express than an agent/group can (conditionally) narrow down to \(N\) possible values (\(|x|_A^\varphi \leq N\)), and to name these values in increasing order: \(1_N.x_A^\varphi\), \(2_N.x_A^\varphi\), etc; public announcements \(!\varphi\), semi-public hacking \(!(a:b)\), etc.

3 Syntax and Semantics of \(LDA\) and \(LDAE\)↩︎

Vocabularies: static and dynamic. A static vocabulary \(\mathcal{V}=(\mathcal{A}, V, Prop, Pred, Funct, ar, \epsilon)\) consists of the following:⁶ a finite set \(\mathcal{A}\) of agents \(a, b, c, \ldots\), also called ‘locations’ (e.g., websites, databases, processors, etc), where data are stored and processed; a set \(V\) of basic variables \(v\), \(v', v'', \ldots\); a set \(Prop\) of atomic propositions \(p, q, \ldots\); a set \(Pred\) of predicate symbols \(P, Q, \ldots\), including equality (\(=\)) and an order predicate \(\leq\); a set \(Funct\) of function symbols \(F, G, \ldots\), including two constants \(\bot, \top\); an arity map \(ar: Pred\cup Funct\to \mathbb{N}\), sending predicate symbols \(P\in Pred\) and function symbols \(F\in Funct\) to natural numbers \(ar(P), ar(F)\in \mathbb{N}\), with \(ar(\top)=ar(\bot)=0\) and \(ar(=)=ar(\leq)=2\); an auxiliary symbol \(\epsilon\not\in \mathcal{A}\cup V\cup Prop\cup Pred\cup Funct\), denoting “the environment” (e.g., the ‘envelope’ in our example).

A dynamic vocabulary \((\mathcal{V}, \mathcal{E})\) is a pair consisting of a static vocabulary \(\mathcal{V}\) and a countable set \(\mathcal{E}\) of ‘event names’ (denoted by \(e, e', f, \ldots\)), that includes some special symbols \(!, ?, \tau\).

Groups Given the static vocabulary \(\mathcal{V}\), a group \(A\subseteq\mathcal{A}\) is any non-empty set of agents in \(\mathcal{A}\). We use capital letters \(A, B, \ldots\) to denote groups.

Ordered Value Domains A value domain (for a given vocabulary \(\mathcal{V}\)) is a first-order model \(\mathbf{D}=(D, I)\) for \(\mathcal{V}\), consisting of: a domain of ‘values’ \(D\), of cardinality \(|D|>1\); and an interpretation function \(I\), mapping each functional symbol \(F\) of arity \(n\) into a function \(I(F)=F_\mathbf{D}: D^n\to D\) (so that the constants \(\bot\) and \(\top\) are interpreted as values \(\bot_\mathbf{D}, \top_\mathbf{D}\in D\)), and each relational symbol \(P\) of arity \(n\) into a set \(I(P)=P_\mathbf{D}\subseteq D^n\) of \(n\)-tuples of values in \(D\), subject to the following conditions: the equality symbol \(=\) is interpreted as the identity relation \(=_\mathbf{D}\) on \(D\); and the order symbol \(\leq\) is interpreted as some total order \(\leq_\mathbf{D}\subseteq D\times D\) on the set \(D\) having \(\bot_\mathbf{D}\) as its bottom element and \(\top_\mathbf{D}\) as its top element (i.e., \(\bot_\mathbf{D}\leq_\mathbf{D}\, d \leq_\mathbf{D}\top_\mathbf{D}\) for all \(d\in D\)).

Minimization Given an ordered value domain \(\mathbf{D}=(D, I)\), it is easy to see that every finite non-empty subset \(D'\subseteq D\) has a unique minimum \(min\, D'\in D'\), s.t. \(min\, D'\leq_\mathbf{D}d'\) for all \(d'\in D'\).

Notation: ‘Cutoff Minimization’ We can also consider, for any natural number \(N\geq 1\), an “\(N\)-cutoff” version of minimization \(min_N\), defined on all sets \(D'\subseteq D\) (including the infinite ones), by putting: \[\begin{array}{lllll} min_N \, D' \; \;& := \;& \top_\mathbf{D}\, (`trivial'), &when D'=\emptyset, \;\\ min_N \, D' \; \;& := \;\;& min\, D', &when 1\leq |D'|\leq N, \,\,and \;\\ min_N \, D' \; \;& := \;\;& \bot_\mathbf{D}\, (`undefined'), &otherwise (for |D'|> N).\end{array}\]

Notation: ‘Cutoff’ \(n^{th}\) element For all sets \(D'\subseteq D\) and all \(1\leq n\leq N\), we can now introduce a notation \(n_N (D')\) for “the \(n^{th}\) element of the \(\leq N\) elements” of \(D\), by putting: \[1_N (D')\, \, := \, \, min_N\, D', \,\,\,\,\,\,\,\,\,\,\,\,\, (n+1)_N (D') \,\, :=\,\, min_{N-1}\, (D'- \{n_N (D')\}) \, \,\,\,for 1\leq n < N.\]

Epistemic State Models An epistemic state model over a value domain \(\mathbf{D}=(D, I)\) is a tuple \({\mathbf{M}}= (S, \sim, \underline{\bullet}(\bullet))\), where: (i) \(S\) is a set of states (or ‘possible worlds’), typically denoted by \(s, w, \ldots\); (ii) \(\sim: \mathcal{A}\to \mathcal{P}(S\times S)\) maps agents \(a\in\mathcal{A}\) to equivalence relations \(\sim_a\subseteq S\times S\), called ‘indistinguishability’ relations; (iii) \(\underline{\bullet}(\bullet):S\times (V\cup Prop) \to D\) is an assignment map (‘valuation’), mapping pairs \((s,v)\in S\times V\) into arbitrary values \(\underline{s}(v)\in D\), and mapping pairs \((s,p)\in S\times Prop\) into values \(\underline{{s}}(p)\in\{\bot_\mathbf{D}, \top_\mathbf{D}\}\).

Group indistinguishability Given a state model \({\mathbf{M}}= (S, \sim, \underline{\bullet}(\bullet))\), we define group indistinguishability relations \(\sim_A:=\bigcap_{a\in A} \sim_a\) on \(S\) (for all groups \(A\subseteq \mathcal{A}\)) by taking intersections.

Syntax of \(LDAE\) For a fixed dynamic vocabulary \((\mathcal{V}, \mathcal{E})\), the (dynamic) Logic of (group) Data Access & Exchange (\(LDAE\)) has a syntax consisting of: (1) a set \(Var:=Var (\mathcal{V})\) of compound variables (or ‘terms’) \(x\); (2) a set \(Fml:=Fml(\mathcal{V})\) of formulas \(\varphi\); (3) a set of ‘syntactic’ event models; (4) a set \(Events\) of data-exchange events. These components are simultaneously defined by mutual recursion, as follows:

(1) & (2) Variables and Formulas The sets \(Var\) and \(Fml\) are given by the clauses: \[\begin{array}{ccc ccc cc cc cc} x & ::= & v &|& F(\overline{x}) &|&\varphi\!\!\to\!\! x|x &|& \mu_N\, x_A^\varphi &|& {\mathbf{e}}(x) \\ \varphi & :: = & p &|& P\overline{x} &|& \varphi \to \varphi &|& K_A \varphi &|& [{\mathbf{e}}] \varphi \end{array}\] where: \(v\in V\) are basic variables; \(p\in Prop\) are atoms; \(\overline{x}=(x_1, \ldots, x_n)\) are tuples of terms; \(P\in Pred\) are \(n\)-ary predicate symbols; \(F\) are \(n\)-ary function symbols; \(a\in \mathcal{A}\) are agents; \(A\subseteq \mathcal{A}\) are groups; \(N\geq 1\) are integers; and the events \({\mathbf{e}}\) are technically “pointed event models” \(({\mathbf{E}},e)\), as defined below.

(3) & (4) Event Models and Events An event model \({\mathbf{E}}=(E, \sim, \underline{\bullet}(\bullet))\) consists of: (i) a finite set \(E\subseteq \mathcal{E}\) of event names; (ii) an equivalence relation \(\sim_a\subseteq E\times E\) (agent \(a\)’s indistinguishability over events) for each \(a\in\mathcal{A}\); (iii) a change map \(\underline{e}(\bullet): Prop\cup V\cup \mathcal{A}\cup\{\epsilon\}\to Fml\cup Var\cup \mathcal{P}(\mathcal{A})\) for each event \(e\in E\), mapping \(\epsilon\) to a formula \(\underline{{e}}(\epsilon)\in Fml\), atoms \(p\in Prop\) to formulas \(\underline{{e}}(p)\in Fml\), basic variables \(v\in V\) to terms \(\underline{e}(v)\in Var\), and agents \(a\in \mathcal{A}\) to groups \(\underline{e}(a)\subseteq \mathcal{A}\). We require these items to satisfy two conditions:

1. Self-Access (agents access their own database): \(a\in \underline{e}(a)\);

2. Known Access (agents know their sources): \(e \sim_af\)  implies  \(\underline{e}(a)=\underline{f}(a)\);

As mentioned, a data-exchange event is just a ‘pointed’ event model \({\mathbf{e}}=({\mathbf{E}}, e)\), i.e. a pair of an event model \({\mathbf{E}}=(E, \sim, \underline{\bullet}(\bullet))\) and an event name \(e\in E\). We denote by \(Events\) the set of data-exchange events.

The Static Logic \(LDA\) The ‘static’ fragment of our logic, called the (static) Logic of (group) Data Access (\(LDA\)), consists of all formulas of \(LDAE\) that are built without the use of dynamic operators \([{\mathbf{e}}]\varphi\) or \({\mathbf{e}}(x)\).

Precondition and Postconditions The precondition of any event \({\mathbf{e}}=({\mathbf{E}},e)\) is the formula \(pre_{\mathbf{e}}:=\underline{e}(\epsilon)\), which intuitively gives the event’s condition of possibility: \({\mathbf{e}}\) can only happen in states satisfying its precondition \(pre_{\mathbf{e}}\). The event \({\mathbf{e}}\)’s postcondition for \(p\in Prop\) is the formula \(post_{\mathbf{e}}(p):=\underline{{e}}(p)\); similarly, the event’s postcondition for \(v\in V\) is the term \(post_{\mathbf{e}}(v):= \underline{{e}}(v)\). Intuitively, the postconditions determine the way an event changes the values of atoms and variables: the new value of variable \(v\) (or atom \(p\)) after event \({\mathbf{e}}\) coincides with the ‘old’ value of the formula \(post_{\mathbf{e}}(p)\) (or the term \(post_{\mathbf{e}}(v)\)) before the event.

(Extended) Access Map Event \({\mathbf{e}}\)’s access map is the restriction of \(\underline{{e}}\) to \(\mathcal{A}\), specifying for each agent \(a\in\mathcal{A}\) the group \(\underline{{e}}(a)\subseteq \mathcal{A}\) of all sources/agents (whose locations/databases are) accessed by agent \(a\) during the event. We can also extend the access map to groups \(A\subseteq \mathcal{A}\), by putting \(\underline{e}(A):=\bigcup \{\underline{e}(a): a\in A\}\), for the set of sources that are distributedly accessible to the group \(A\) during event \(e\).

Subexpression-complexity An expression \(\alpha\) is any formula \(\varphi\), term \(x\) or event \({\mathbf{e}}\) of \(LDAE\). The sub-expression complexity order \(<\) is the least transitive relation s.t.: (1) every formula is \(>\) its subformulas, and also \(>\) all terms and events occurring in it; (2) every term is \(>\) its subterms, and also \(>\) all formulas and events in it; (3) every event \({\mathbf{e}}=({\mathbf{E}},e)\) is \(>\) all preconditions and postconditions of the form \(pre_f\), \(\underline{f}(p)\) and \(\underline{f}(v)\) with \(f\in E\), \(p\in Prop\) and \(v\in V\). It is easy to see that \(<\) is a well-founded partial order.

Semantics We simultaneously define three semantic notions on state models \({\mathbf{M}}= (S, \sim, \underline{\bullet}(\bullet))\):

1. a satisfaction relation \(s\models_{{\mathbf{M}}} \varphi\) between states \(s\in S\) (in any state model \({\mathbf{M}}\)) and formulas \(\varphi\in Fml\);

2. an extended assignment/valuation function from \(S\times (Var\cup Fml)\) to \(D\), mapping \((state, variable)\)-pairs \((s,x)\in S\times Var\) into arbitrary values \(s(x)_{\mathbf{M}}\in D\), and mapping \((state, formula)\)-pairs \((s,\varphi)\in S\times Fml\) into extreme values \(s(\varphi)_{\mathbf{M}}\in \{\bot_\mathbf{D}, \top_\mathbf{D}\}\).

3. a product update operation, mapping state models \({\mathbf{M}}=(S,\sim,\underline{\bullet}(\bullet))\) and event models \({\mathbf{E}}=(E,\sim,\underline{\bullet}(\bullet))\) into updated state models \({\mathbf{M}}\bigotimes {\mathbf{E}}=(S\otimes E,\sim, \underline{\bullet}(\bullet))\) (over the same value domain \(\mathbf{D}\)).

For this definition, we need an auxiliary notation: for variables \(x\in Var\), groups \(A\), formulas \(\varphi\) and states \(s\in S\), the set of possible values of \(x\) at state \(s\) according to group \(A\) conditional on \(\varphi\) is \[(x_A^\varphi)_{s,{\mathbf{M}}} \, :=\, \{w(x)_{\mathbf{M}}: w\sim_As, w\models_{\mathbf{M}}\varphi\}.\] With this notation, we define our three semantic notions by mutual recursion: \[\begin{array}{lllll} s\models_{\mathbf{M}}p \; \;& iff \;\;&& \underline{s}(p)=\top_\mathbf{D}\\ s\models_{\mathbf{M}}P x_1\ldots x_n \; \;& iff \;\;&& (s(x_1)_{\mathbf{M}}, \ldots, s(x_n)_{\mathbf{M}})\in I(P)\\ s\models_{\mathbf{M}}\varphi\to\psi \; \;& iff \;\;&& s\models_{\mathbf{M}}\varphiimpliess\models_{\mathbf{M}}\psi \\ s\models_{\mathbf{M}}K_A \varphi \;\;& iff \;\;&& w\models_{\mathbf{M}}\varphifor all w\sim_As \\ s\models_{\mathbf{M}}[{\mathbf{e}}] \varphi \;\;& iff \;\;&& (s,e)\in S\otimes E \,implies(s,e)\models_{{\mathbf{M}}\bigotimes {\mathbf{E}}} \varphi, \,\,\,\,\,where{\mathbf{e}}=({\mathbf{E}},e).\\ s(v)_{\mathbf{M}}\;\;& = \;\;&& \underline{s}(v) \,\,\,\,\,\,\,\,\,\, \,\,\,\,\, \,\,\,\,\,as given in the model {\mathbf{M}} \\ s(\varphi\!\!\to\!\! x|y)_{\mathbf{M}}\;\;& = \;\;&& s(x)_{\mathbf{M}}\,\,\,\,\, \,\,\,\,\, \,\,\,\,\,if s\models_{\mathbf{M}}\varphi, and \\ s(\varphi\!\!\to\!\! x|y)_{\mathbf{M}}\;\;& = \;\;&& s(y)_{\mathbf{M}}\,\,\,\,\, \,\,\,\,\, \,\,\,\,\,if s\not\models_{\mathbf{M}}\varphi \\ s(F(x_1,\ldots, x_n))_{\mathbf{M}}\;\;& = \;\;&& (I(F)) (s(x_1)_{\mathbf{M}}, \ldots, s(x_n)_{\mathbf{M}}) \\ s(\mu_N x_A^\varphi)_{\mathbf{M}}\;\;& = \;\;&& min_N \, Val(x_A^\varphi)_{s,{\mathbf{M}}} \\ s({\mathbf{e}}(x))_{\mathbf{M}}\;\;& = \;\;&& (s,e)(x)_{{\mathbf{M}}\bigotimes {\mathbf{E}}} \,\,\,\,\, \,\,\,\,\,if {\mathbf{e}}=({\mathbf{E}},e) is s.t. (s,e)\in S\otimes E, and\\ s({\mathbf{e}}(x))_{\mathbf{M}}\;\;& = \;\;&& \top_\mathbf{D}\,\,\,\,\, \,\,\,\,\, \,\,\,\,\,\,\,\,\,\,\,\,\,\,\, \,\,\,\,\,\,\,\,\,\, \,\,\,\,\,\,\,\,\,\, { otherwise.} \\ s(\varphi)_{\mathbf{M}}\;\;& = \;\;&& \top_\mathbf{D}\,\,\,\,\, \,\,\,\,\, \,\,\,\,\,if s\models_{\mathbf{M}}\varphi, and \\ s(\varphi)_{\mathbf{M}}\;\;& = \;\;&& \bot_\mathbf{D}\,\,\,\,\, \,\,\,\,\, \,\,\,\,\,if s\not\models_{\mathbf{M}}\varphi. \\ {\mathbf{M}}=(S, \sim, \underline{\bullet}(\bullet)), \,\, {\mathbf{E}}=(E, \sim, \underline{\bullet}(\bullet)) \;\;& \mapsto \;\;&& {\mathbf{M}}\bigotimes{\mathbf{E}}=(S\otimes E, \sim, \underline{\bullet}(\bullet)), \,\,\, \,\,\,\,\,\,\,where:\\\ S\otimes E \;\;& = \;\;&& \{(s,e)\in S\times E \mid s\models_{\mathbf{M}}pre_{\mathbf{e}}\} \\\ (s,e)\sim_a (s', e') \;\;& iff \;\;&& s\sim_{\underline{e}(a)} s'ande\sim_a e' \\\ \underline{(s,e)} (p) \;\;& = \;\;&& s (post_{\mathbf{e}}(p))_{\mathbf{M}} \\\ \underline{(s,e)}(v) \;\;& = \;\;&& s(post_{\mathbf{e}}(v))_{\mathbf{M}} \end{array}\]

Extended assignment on sets of expressions We can ‘lift’ the assignment map to the level of sets of variables \(X\subseteq Var\) and sets of formulas \(\Phi\subseteq Fml\)), by putting: \(s(X)_{\mathbf{M}}\, :=\, \{s(x)_{\mathbf{M}}: x\in X\}\); \(s(\Phi)_{\mathbf{M}}\, :=\, \{s(\varphi)_{\mathbf{M}}: \varphi\in \Phi\}\). Whenever the model is understood, we skip the subscript \({\mathbf{M}}\), writing simply \(s\models \varphi\), \(s(x)\), \(s(X)\) and \(s(\Phi)\). For sets of formulas \(\Phi\), we also write \(s\models \Phi\) whenever \(s\models\varphi\) for all \(\varphi\in \Phi\).

Abbreviations. We define the usual Boolean connectives \(true := (\top=\top)\), \(false:= (\top=\bot)\), \(\neg\varphi := (\varphi\to false)\), \(\varphi\wedge \psi\), \(\varphi\vee\psi\), \(\varphi\leftrightarrow \psi\), as well as the dual existential (Diamond) modalities \(\langle K_A\rangle \varphi :=\neg K_A\neg \varphi\), \(\langle K_A^\theta\rangle \varphi := \neg K_A^\theta\neg \varphi\), \(\langle {\mathbf{e}}\rangle \varphi := \neg [{\mathbf{e}}] \neg \varphi\). We also use the following abbreviations, for variables \(x,y\in Var\), finite sets of variables \(X,Y\subseteq Var\) and natural numbers \(n,N\) with \(1\leq n\leq N\):

\(x\in Y \, :=\, \bigvee\{ x=y: y\in Y\}, \,\,\, \,\,\,\,\,\, ?_\varphi \, :=\, \varphi\!\!\to\!\! \top|\bot, \,\,\, \,\,\,\,\,\, \varphi\!\!\to\!\! x \, :=\, \varphi\!\!\to\!\! x|\top,\)

\(K_A^\theta \varphi \, :=\, K_A (\theta\to \varphi), \,\,\, K_A^\theta x \, :=\, K_A^\theta (x= \mu_1 x_A^\theta), \,\,\,\,\, K_A x \,\, :=\,\, K_A^{true} x,\)

\(1_N.x_A^\theta \,\, :=\,\, \mu_N x_A^\theta, \,\, \,\,\, (n+1)_N.x_A^\theta \,\, :=\,\, \mu_{N-1} x_A^{\theta \wedge x> n_N.x_A^\theta},\)

\(|x|_A^\theta\leq 0 \,\, :=\,\, K_A \neg\theta, \,\,\,\,\, \,\,\,\,\, |x|_A^\theta \leq n \,\, :=\,\, K_A^\theta (x\in Var^n (x_A^\theta)), \,\,\,\, { where } Var^n(x_A^\theta):= \{i_n.x_A^\theta : 1\leq i\leq n\},\)

\(|x|_A^\theta= 0 \,\, :=\,\, |x|_A^\theta\leq 0, \,\,\,\,\, |x|_A^\theta > n \,\, :=\,\, |x|_A^\theta\not\leq n,\)

\(|x|_A^\theta = (n+1) \,\, :=\,\, |x|_A^\theta> n \wedge |x|_A^\theta \leq (n+1)\, for n\geq 0,\)

\(min \, \{x\} \, :=\, x, \,\,\, min \, (X\cup \{y\}) \, :=\, (min \, X\leq y)\!\!\to\!\! (min\, X)|y.\)

Intuitively, \(x\in Y\) says that \(x\) currently takes the same value as some term in \(Y\). The term \(?_\varphi\) is a Boolean variable, taking value \(\top_\mathbf{D}\) if \(\varphi\) is true, and value \(\bot_\mathbf{D}\) otherwise. The operator \(\varphi\!\!\to\!\! x\) is the term analogue of material implication: it takes the value of \(x\) if \(\varphi\) is true, and value \(\top_\mathbf{D}\) otherwise. Next, ‘knowledge of value’ is definable in our logic, in both conditional and unconditional forms, for groups and individuals, via the abbreviations \(K_A^\theta x\), \(K_A x\), \(K_A^\theta\overline{{x}}\), \(K_A\overline{{x}}\). Note that, for the empty tuple \(\lambda=()\), we have \(K_A^\theta \lambda = \bigwedge \emptyset =\top\). The term \(n.x_A^\theta\) denotes the \(n^{th}\) value of \(x\) (in \(\leq_\mathbf{D}\)-order) considered possible by \(A\), conditional on \(\theta\). The expressions \(|x|_A^\theta =n\), \(|x|_A^\theta \leq n\) and \(|x|_A^\theta >n\) refer to the cardinality of the set of possible values of \(x\), according to group \(A\), given \(\theta\). Finally, \(min\, X\) denotes the minimum value of all terms in \(X\).

Distributed Location For any expression, i.e., any term, formula or event \(\alpha\in Var\cup Fml\cup Events\), its (distributed) location \(\mathcal{L}(\alpha)\subseteq\mathcal{A}\cup \{\epsilon\}\) is given by the following recursive clauses:

\(\mathcal{L}(p)= \mathcal{L} (v) \, \, =\,\, \{\epsilon\}, \,\,\, \,\,\,\, \, \,\,\,\,\, \, \,\,\,\,\,\, \,\,\,\,\, \,\,\, \,\,\,\, \mathcal{L}(K_A \varphi)= \mathcal{L}(\mu_N x_A^\varphi)\,\, =\,\, A,\)

\(\,\,\,\,\, \mathcal{L}(Px_1\ldots x_n)=\mathcal{L}(F(x_1, \ldots, x_n)) \,\, =\,\, \bigcup \{\mathcal{L}(x_i):1\leq i\leq n\},\)

\(\mathcal{L}(\varphi\to \psi) \,\, =\,\, \mathcal{L}(\varphi)\cup \mathcal{L}(\psi), \,\,\, \,\,\,\, \, \,\,\,\,\, \,\,\,\, \, \,\,\,\,\, \, \,\,\,\,\,\mathcal{L}(\varphi\!\!\to\!\! x|y)\,\, =\,\, \mathcal{L}(x)\cup \mathcal{L}(\varphi)\cup \mathcal{L}(y),\)

\(\mathcal{L}({\mathbf{e}})\,\, = \,\, \mathcal{L}(pre_{\mathbf{e}}), \,\,\, \,\,\,\, \, \,\,\,\,\, \, \,\,\,\,\, \mathcal{L}([{\mathbf{e}}] \varphi) \,\, = \,\, \mathcal{L}({\mathbf{e}})\cup \underline{e}(\mathcal{L}(\varphi)), \,\,\,\, \, \,\,\,\,\, \, \,\,\,\,\, \mathcal{L}({\mathbf{e}}(x)) \,\, = \,\, \mathcal{L}({\mathbf{e}})\cup \underline{e}(\mathcal{L}(x)),\)

where we used the extended access map \(\underline{e}(A)\). In particular, this gives us that \(\mathcal{L}(\bot)=\mathcal{L}(\top)=\mathcal{L}(true)=\mathcal{L}(false)=\emptyset\), \(\mathcal{L}(\neg\varphi)=\mathcal{L}(\varphi)\), \(\mathcal{L}(\varphi\wedge \psi)= \mathcal{L}(\varphi)\cup \mathcal{L}(\psi)\) and \(\mathcal{L}(K_A^\theta x)=A\).

We can also extend the location map to finite sets of terms \(X\subseteq Var\), by putting: \[\mathcal{L}(X) \,\, :=\,\, \bigcup_{x\in X} \mathcal{L}(x).\]

Locality The values of terms or propositions having a distributed location within a group \(A\subseteq \mathcal{A}\) are distributed knowledge among group \(A\)’s members, as shown by the results below.

3.1 Examples of Data-Exchange Events and Event Models↩︎

In ‘semi-public’ event models (with only one event), it is common knowledge who can read whose data.

Public Announcements For every formula \(\varphi\), the event \(!\varphi= ({\mathbf{E}}_{!\varphi}, !)\) of publicly announcing \(\varphi\) has an event model \({\mathbf{E}}_{!\varphi}= (\{!\}, \sim, \underline{\bullet}(\bullet))\) whose only event name is the special symbol \(!\), with identity \(\sim_a =\{(!,!)\}\) as accessibility relation for every agent, and where we put \(\underline{!}(p)=p\), \(\underline{!}(v)=v\), \(\underline{!}(a)=\{a\}\) and \(\underline{!} (\epsilon)=\varphi\), hence \(pre_{!\varphi}=\varphi\). This event encodes the dynamics of truthful public announcements [@Plaza]: the updated model \({\mathbf{M}}\otimes {\mathbf{E}}_{!\varphi}\) is (isomorphic to the one) obtained by deleting all the \(\varphi\)-worlds from the original model \({\mathbf{M}}\) (and keeping everything else the same).

Public and Semi-Public Sharing (“Tell Us All You Know”) For groups \(A,B\subseteq\mathcal{A}\), \(!(A:B)= ({\mathbf{E}}_{!(A:B)}, !)\) is a semi-public event whose model \({\mathbf{E}}_{!(A:B)}= (\{!\}, \sim, \underline{\bullet}(\bullet))\) has the same structure as \({\mathbf{E}}_{!\varphi}\), except for the access map and the precondition, which are given by putting: \(\underline{!}(a)=B\cup\{a\}\) for all \(a\in A\): \(\underline{!}(a)=\{a\}\) for \(a\not\in A\); and \(\underline{!} (\epsilon)=true\) (so the precondition \(pre_{!(A:B)}=true\) is tautological). In this action, it is common knowledge that all agents in \(A\) gain access to the databases of all agents in \(B\). Its effect is to replace all the relations \(\sim_a\) (with \(a\in A\)) from the original model \({\mathbf{M}}\) by the new relations \(\sim_a^{!(A:B)} := \sim_a\cap \sim_B\) in the updated model \({\mathbf{M}}\otimes {\mathbf{E}}_{!(A:B)}\), while keeping everything else unchanged (including the relations \(\sim_a\) with \(a\not\in A\)). A special case is semi-public sharing \(!(a: b)\) from \(b\) to \(a\), obtained by taking \(A=\{a\}\) and \(B=\{b\}\): it is common that \(b\) shares all his knowledge with \(a\). Another special case is \(A\)-public sharing \(!B:= !(\mathcal{A}: B)\), which is obtained by taking \(A=\mathcal{A}\): all agents in \(B\) publicly share all their information. An even more special case is \(b\)-public sharing \(!b=!\{b\}= !(\mathcal{A}:\{b\})\), obtained by taking \(A=\{a\}\) for some designated agent \(a\) (and \(B=\mathcal{A}\)): agent \(a\) publicly “tells all she knows”.⁷

Sharing between Multiple Groups For groups \(A_1, B_1, \ldots, A_n, B_n\), the event \(!(A_1:B_1, \ldots, A_n: B_n)\) is a semi-public event, whose model \({\mathbf{E}}_{!(A_1:B_1, \ldots, A_n: B_n)}= (\{!\}, \sim, \underline{\bullet}(\bullet))\) has the same structure as \({\mathbf{E}}_{!(A:B)}\), except that the access map is given by \(\underline{!}(a)=\{a\}\cup \bigcup \{B_i: i\leq n, a\in A_i\}\) for all \(a\): it is common knowledge that all agents in each group \(A_i\) gain access to the databases of all agents in the corresponding group \(B_i\).

Sharing within Groups For groups \(A_1, \ldots, A_n\subseteq \mathcal{A}\), the event of parallel sharing within different groups
\(!(A_1, \ldots, A_n)=!(A_1:A_1, \ldots, A_n: A_n)\) is the special case of \(!(A_1:B_1, \ldots, A_n: B_n)\) where \(B_i=A_i\). In this action, it is common knowledge that all agents in each group \(A_i\) simultaneously share all their knowledge with all other agents in the same group \(A_i\). A very special case is \(n=1\), which represents the resolution action \(!(A)\): it is common knowledge that all the agents in \(A\) share their information with each other.⁸

Public Hacking \(!H_{a:b}\) (as in the WikiLeaks case). It is common knowledge that agent \(a\) ‘hacks’ agent \(b\)’s database, using her knowledge of \(b\)’s password (represented by some variable \(v_b\)), and makes all \(b\)’s data public. Everybody gets to see all \(b\)’s data (including the value of his password \(v_b\)), but only \(a\) and \(b\) knew the password beforehand. The model is the same as for public sharing \(!b\), except for the precondition, which is \(\it{pre}_{!}:=K_a v_b\wedge K_b v_b\): this event happens only if \(a\) knew \(b\)’s password \(v_b\) before the event.

Semi-public Hacking This time, it is common knowledge that agent \(a\) hacks agent \(b\)’s database (using her prior knowledge of his password \(v_b\)) and can read all his data; but the others cannot read these data. The event model is similar to the one for semi-public sharing \(!(a:b)\) (and in particular, the access map is the same), except that the precondition is \(K_a v_b\wedge K_b v_b\) (as in the case of public hacking \(!H_{a:b}\)).

Semi-public Change of Password \(!(v_a:= F(v_a, v'_a))\). It is common knowledge that \(a\) changes her password \(v_a\) to a value \(F(v_a, v'_a)\), that is a function of her current password \(v_a\) and of another (secret) local variable \(v'_a\). The encryption function \(F\) is common knowledge, but the values of the former password \(v_a\) and of the other secret number \(v'_a\) are known (hopefully) only by \(a\). The event model is similar for \(!\varphi\), except that the precondition is \(\it{pre}_{!}= K_a v_a\wedge K_a v'_a\), and the postcondition for \(v_a\) is \(\underline{!}(v_a)= F(v_a, v'_a)\).

Using larger event models, we can represent various forms of private and semi-private data-exchanges.

Secret Hacking Agent \(a\) may be hacking \(b\)’s database iff she got hold of \(b\)’s password \(v_b\). Only the hacker (\(a\)) knows whether or not she succeeded to get \(v_b\). We represent this event \(SH_{a:b}= ({\mathbf{E}}, !)\) using a model \({\mathbf{E}}= (\{!, \tau\}, \sim, \underline{\bullet}(\bullet))\) with two events \(!\) (for successful hacking) and \(\tau\) (unsuccessful hacking). The preconditions are \(\it{pre}_{!}:= K_a v_b \wedge K_b v_b\) and \(\it{pre}_{\tau}:= \neg K_a v_b \wedge K_b v_b\). The access maps are \(\underline{!}(a):=\{a,b\}\), \(\underline{\tau}(a)=\{a\}\), and \(\underline{!}(c)=\underline{\tau}(c)=\{c\}\) for all \(c\not=a\); all postconditions are given by identity; \(a\)’s accessibility is the identity relation, and the others’ relations are the universal relation.

Conditional Change of Password \(!(K_a |v_a|_b^{true} \leq N /v_a:= F(v_a, v'_a))\). It is common knowledge that \(a\) changes her password \(v_a\) (as in the semi-public change) only iff she knows that \(b\) has succeeded to narrow down her possible passwords to \(N\) possibilities. This is an event \(({\mathbf{E}}, !)\), whose event model \({\mathbf{E}}= (\{!, ?\}, \sim, \underline{\bullet}(\bullet))\) has two event names \(!\) (for changing \(a\)’s password) and \(?\) (for no change). The preconditions are \(\it{pre}_{!}:= K_a |v_a|_b^{true} \leq N\) and \(\it{pre}_{?}:= \neg K_a |v_a|_b^{true} \leq N\). The postconditions for \(v_a\) are \(\underline{!} (v_a):= F(v_a, v'_a)\) and \(\underline{?} (v_a):= v_a\), while all other postconditions and access map are given by identity: nobody gains access to others’ databases (since the hacking is prevented by password-change). Finally, agent \(a\)’s accessibility is the identity relation, while all others’ accessibility is the universal relation.

Secret Detection of Hacking We can modify the secret hacking example \(SH_{a:b}\) to allow the possibility that \(b\) might detect \(a\)’s hacking attack (so that he might come to know that he is being hacked). Only \(b\) knows whether he actually detects an attack. This event \(({\mathbf{E}}, !)\) has a model \(E=\{!,?,\tau\}\) with three event names \(!\) (detected hacking), \(?\) (successful, undetected hacking) and \(\tau\) (unsuccessful hacking). The access maps for \(!\) and \(\tau\) are as in the model for \(SH_{a:b}\), while the access map for \(?\) is the same as for \(!\); and the same goes for \(pre_!\), \(pre_\tau\) and \(pre_?\). Besides loops for all agents, we also have \(!\sim_a?\) (i.e. \(a\) doesn’t know whether his hacking is detected or not) and \(? \sim_b\tau\) (\(b\) can’t distinguish between undetected hacking and unsuccessful hacking), while \(\sim_c\) is the universal relation for all outsiders \(c\neq a,b\).

4 Axiomatization and Decidability↩︎

We first look at the static fragment \(LDA\): its proof system \(\mathbf{LDA}\) is in Table ¿tbl:tb0?.

As for the full dynamic logic \(LDAE\), we need a few more notations and results to state our axioms.

Possible Values after an Event Recall that \(Val(x_A^\varphi)_{s, {\mathbf{M}}} =\{w(x)_{\mathbf{M}}: w\sim_As, w\models_{\mathbf{M}}\varphi\}\) is the set of possible values at state \(s\) according to \(A\) given \(\varphi\). The following (easily checked) result gives us a characterization of the corresponding set of possible values of \(x\) (according to \(A\) given \(\varphi\)) after an event \({\mathbf{e}}\):

Counting the Possible Values after an Event We want a formula expressing the fact that there will be at most \(N\) possible values of \(x\) (according to \(A\) given \(\varphi\)) after the event \({\mathbf{e}}\). Moreover, we want to express this at the current state (before the event). Put now \(Var_e^N (x_A^\varphi) := \{n_N \mathbf{f}(x)_{\underline{f}(A)}^{\langle \mathbf{f}\rangle \varphi} : f\sim_Ae, n\leq N\}\). Semantically, given Lemma 1, it should be clear that, if \(|Val(\mathbf{f}(x)_{\underline{f}(A)}^{\langle f\rangle \varphi})_{s,{\mathbf{M}}}|\leq N\) holds for all events \(f\sim_Ae\), then \(Val(x_A^\varphi)_{(s,{\mathbf{e}}), {\mathbf{M}}\otimes {\mathbf{E}}}\subseteq s(Var_e^N (x_A^\varphi))_{\mathbf{M}}\). However, this inclusion might be strict: it can happen that not all of the values in \(s(Var_e^N (x_A^\varphi))_{\mathbf{M}}\) are possible values of \(x\) according to \(A\) (given \(\varphi\), after the event \(e\)). The problem is that whenever \(|Val(\mathbf{f}(x)_{\underline{f}(A)}^{\langle f\rangle \varphi})_{s,{\mathbf{M}}}| < N\) for some \(f\sim_Ae\), we get a possibly ‘fake’ \(x\)-value \(N_N. \mathbf{f}(x)_{\underline{f}(A)}^{\langle \mathbf{f}\rangle \varphi}=\top_\mathbf{D}\). So, for any \(z\in Var_e^N (x_A^\varphi)\), its condition of possibility is given by the formula: \[\Diamond z \,\, :=\,\, \left(z=\top \, \to\, \bigvee_{f\sim_Ae} \langle K_{f(A)}^{\langle f\rangle\varphi} \rangle \mathbf{f}(x)=\top \right).\] Thus, for any subset \(Z\subseteq Var_e^N (x_A^\varphi)\), the formula \[|Z|^\Diamond \leq N \,\, :=\,\, \bigvee_{Y\subseteq Z, |Y|\leq N} \, \bigwedge_{z\in Z} \left( \Diamond z \to \bigvee_{y\in Y} z=y\right)\] says that the number of possible values of \(x\) in \(Z\) (according to \(A\) given \(\varphi\)) is at most \(N\). Finally, by applying this to the whole set \(Z= Var_e^N (x_A^\varphi)\) above, we obtain the desired formula:

Using these notations, the proof system \(\mathbf{LDAE}\) for our full dynamic logic is given in Table ¿tbl:tb1?.

5 Completeness and Decidability Proofs for \(LDA\)↩︎

Throughout this section, we fix a formula \(\varphi_0\in Fml\). We prove Theorem 1 by the method of quasi-models. But, to obtain an appropriate analogue of Fischer-Ladner closure, we need two auxiliary notions:

Restricted Vocabulary For any finite set \(\Sigma\subseteq Fml\), the \(\Sigma\)-restricted vocabulary \({\mathcal{V}_\Sigma := (\mathcal{A}_\Sigma, V_\Sigma, Prop_\Sigma,}\) \({Pred_\Sigma, Funct_\Sigma, ar_\Sigma, \epsilon)}\) is formed as follows: \(\mathcal{A}_\Sigma\) is the set of agents occurring (inside terms or modalities in formulas) in \(\Sigma\); \(V_\Sigma\) is the set of basic variables occurring (as subterms of any term) in formulas of \(\Sigma\); \(Prop_\Sigma: = Prop\cap \Sigma\) is the set of atomic propositions in \(\Sigma\); \(Pred_\Sigma\) is the set of predicates occurring in (formulas of) \(\Sigma\); \(Funct_\Sigma\) is the set of function symbols occurring in (formulas of) \(\Sigma\); \(ar_\Sigma\) is the restriction of \(ar\) to \(Pred_\Sigma\cup Funct_\Sigma\). Clearly, if \(\Sigma\) is finite, then all the sets in \(\mathcal{V}_\Sigma\) are finite.

The \(\Sigma\)-Restricted Set of Terms For any finite set of formulas \(\Sigma\subseteq Fml\), the \(\Sigma\)-restricted set of terms \(Var_\Sigma\) is the smallest set of terms satisfying the following closure conditions: \(Var_\Sigma\) contains \(\bot\) and \(\top\), as well as all terms occurring in any formula of \(\Sigma\) (hence \(V_\Sigma\subseteq Var_\Sigma\)); \(Var_\Sigma\) is closed under subterms; if \(i_N.x_A^\varphi\in Var_\Sigma\) for some \(i\leq N\), then \(j_N.x_A^\varphi\in Var_\Sigma\) for all \(j\leq N\). Note that \(Var_\Sigma\) is only a finite subset of the (typically infinite) set \(Var(\mathcal{V}_\Sigma)\) of terms of the language \(LDA(\mathcal{V}_\Sigma)\).

We now proceed to introduce the appropriate notions of Fisher-Ladner Closure, syntactic types, and special sets of types called quasi-models.

Fisher-Ladner Closure Given now our fixed formula \(\varphi_0\), the closure of \(\varphi_0\) is the smallest set of formulas \(\Sigma=\Sigma(\varphi_0)\) satisfying the following closure conditions: \(\varphi_0\in \Sigma\); \(true, false\in \Sigma\); \(\Sigma\) is closed under subformulas and single negations \(\sim\varphi\); if \(P\in Pred_\Sigma\) has arity \(ar(P)=n\) and \(\overline{{x}}=(x_1, \ldots, x_n)\) is an \(n\)-tuple with all \(x_1, \ldots, x_n\in Var_\Sigma\), then \(P\overline{{x}}\in \Sigma\); if \((K_A\varphi)\in \Sigma\), \(\theta\) is a subformula of \(\sim\varphi\) and \(B\subseteq\mathcal{A}_\Sigma\), then \((K_B\theta)\in \Sigma\) (hence also \(\langle K_A \rangle \theta\in \Sigma\)); if \((\varphi\!\!\to\!\!x|y)\in Var_\Sigma\), then \(\varphi\in \Sigma\); if \(x,y\in Var_\Sigma\), then \((x=y), (x\leq y)\in \Sigma\); if \((\mu_N x_A^\varphi), z\in Var_\Sigma\) and \(Y\subseteq Var_\Sigma\), then \(K_A^\varphi(z\in Y), \langle K_A^\varphi\rangle (z\in Y) \in\Sigma\).

Types Let \(\Sigma\) be the closure of \(\varphi_0\). A \(\Sigma\)-type is a subset of \(\Sigma\) with the following properties:

1. for every \(\varphi\in\Sigma\): \((\sim\varphi)\in \Delta\) iff \(\varphi\not\in\Delta\);

2. for every \((\varphi\wedge \psi)\in \Sigma\): \((\varphi\wedge \psi)\in \Delta\) iff \(\varphi\in\Delta\) and \(\psi\in \Delta\);

3. for every \(P\overline{{x}}\overline{{z}}\in \Sigma\): if \((\overline{{x}}=\overline{{y}}), P\overline{{x}}\overline{{z}}\in \Delta\) then \(P\overline{{y}}\overline{{z}}\in \Delta\);

4. for \(F(\overline{{x}}), F(\overline{{y}})\in Var_\Sigma\): if \((\overline{{x}}=\overline{{y}})\in \Delta\), then \((F(\overline{{x}})=F(\overline{{y}}))\in \Delta\);

5. if \((x\leq y), (y\leq z)\in \Delta\), then \((x\leq z)\in \Delta\);

6. if \((x\leq y), (y\leq x)\in \Delta\), then \((x=y)\in \Delta\);

7. either for all \(x, y\in Var_\Sigma\), we have either \((x\leq y)\in \Delta\) or \((y\leq x)\in \Delta\);

8. for all \(x\in Var_\Sigma\), we have \((\bot\leq x), (x\leq \top)\in \Delta\);

9. \((\top\neq\bot)\in \Delta\);

10. for every \((\varphi\!\!\to\!\! x|y)\in\Sigma\): \(\varphi\in \Delta\) implies \((x=(\varphi\!\!\to\!\! x|y))\in\Delta\); and \(\varphi\not\in\Delta\) implies \((y=(\varphi\!\!\to\!\! x|y))\in \Delta\);

11. if \((K_A\varphi)\in\Delta\) then \(\varphi\in\Delta\);

12. for all \(\mu_N x_A^\varphi\in Var_\Sigma\): \((\mu_N x_A^\varphi\leq x)\in \Delta\);

13. if \(\varphi, K_A^\varphi (\mu_N x_A^\varphi \neq x)\in \Delta\) and \(Y\subseteq Var_\Sigma\) is s.t. \(\mathcal{L}(Y)\subseteq A\) and \(|Y|\leq N\), then \(\langle K_A^\varphi\rangle (x\not\in Y)\in \Delta\);

14. for all \(\mu_N x_A^\varphi\in Var_\Sigma\): if \((K_A\neg\varphi)\in \Delta\), then \((\mu_N x_A^\varphi=\top)\in \Delta\);

15. for all \(\mu_N x_A^\varphi\in Var_\Sigma\): if \((|x|_A^\varphi>N)\in \Delta\), then \((\mu_N x_A^\varphi=\bot)\in \Delta\).

Observation Types are closed under modus ponens: if \(\Delta\) is a type and \((\varphi\to\psi), \varphi\in \Delta\), then \(\psi\in \Delta\).

Accessibility relations on types For types \(\Delta, \Delta'\) and group \(A\subseteq \mathcal{A}_\Sigma\), we put: \[\Delta \sim_A\Delta' \,\,iff\,\, \varphi\in \Delta \Leftrightarrow \varphi\in\Delta' \,for all\varphi\in\Sigmas.t.\mathcal{L}(\varphi)\subseteq A.\]

Hat notation. For every type \(\Delta\), we put \(\widehat{\Delta} \, \,\,\, :=\,\, \, \, \bigwedge\Delta\) for the conjunction of all formulas in \(\Delta\).

Quasi-Models A quasi-model for \(\varphi_0\) is a set \(S\) of types over \(\Sigma\), with the following two properties: (*) \(\varphi_0\in \Delta_0\) for some type \(\Delta_0\in S\); (**) if \(\langle K_A \rangle \varphi\in \Delta\in S\), then there is some \(\Delta'\in S\) with \(\Delta\sim_A\Delta'\) and \(\varphi\in \Delta'\).

The \(\Sigma\)-canonical quasi-model A \(\Sigma\)-theory is any maximally consistent subset of \(\Sigma\). We denote by \(S_\Sigma\) the set of all \(\Sigma\)-theories. We will show that \(S_\Sigma\) is a (finite) “canonical” quasi-model for \(\Sigma\).

The hard part is to prove the converse of this:

The rest of this section is dedicated to the proof of Proposition [Satisfiability].

Unravelling: the tree of histories Let us fix a quasi-model \(S\), a formula \(\varphi_0\) and a type \(\Delta_0\in S\) with \(\varphi_0\in \Delta_0\). We will construct a model for \(\varphi_0\), based on an unravelling of \(S\) around \(\Delta_0\). A history is a finite sequence \(h=(\Delta_0, A^1, \Delta_1, \ldots, A^n, \Delta_n)\) of any length \(n\geq 0\), where \(\Delta_1, \ldots,\Delta_n\in S\) are types and \(A^1, \ldots, A^n\subseteq\mathcal{A}_\Sigma\) are groups, such that we have \(\Delta_{i-1}\sim_{A^i} \Delta_i\) for all \(i=1,n\). Let \(H\) be the set of all histories. We denote by \(last(h):=\Delta_n\) the last state in history \(h\), and by \(\to_{sec:A}\) the natural forward one-step relation on histories in \(H\), given by putting: \(h\to_A h'\) iff \(h'=(h, A, \Delta')\) (with \(last(h) \sim_A\Delta'=last(h')\)). We denote by \(\leftarrow_{sec:A}\) the backward one-step relation, defined as the converse of the forward relation: \(h \leftarrow_A h'\) iff \(h'\to_A h\). The one-step relations structure \(H\) into a tree rooted at \(\Delta_0\) (with the immediate successor relation given by \(h\to h'\) iff \(h\to_A h'\) for some group \(A\)). In particular, we have the tree property : every two nodes \(h, h'\) of the tree are connected by a unique non-redundant path \(h=h_0 \leftarrow_{A^1} h_1 \leftarrow_{A^2} \ldots \leftarrow_{A^i} h_{i}\to_{A^{i+1}} \ldots \to_{A^n} h_n=h'\) (-in which neighboring nodes are immediate successors, in one order or another, and no nodes are repeated).

Epistemic relations on histories To make this tree into a model for our restricted vocabulary \(\mathcal{V}_\Sigma\), we define our single-agent indistinguishability relations \(\sim_a\subseteq H\times H\) on histories, by putting \[\sim_a\,\, :=\,\, \left( \bigcup_{A\ni a} \to_A \cup \bigcup_{A\ni a} \leftarrow_A \right)^*,\] where \(\leftarrow_A\) is the converse of \(\to_A\), the unions range over groups \(A\subseteq \mathcal{A}_\Sigma\) s.t. \(a\in A\), and \(R^*\) is the reflexive-transitive closure of \(R\). Since our goal is to build a standard model, the group indistinguishability relations \(\sim_A\subseteq H\times H\) are taken to be simply the intersections \(\sim_A\,\, :=\,\, \bigcap_{a\in A} \sim_a\) of all the individual relations.

It is useful to give more concrete characterizations of the relations \(\sim_A\) (and \(\sim_a\)) on histories:

The Value Domain: a Quotient Construction The set of values \(D\) of our model will be a quotient of the Cartesian product \(H\times Var_\Sigma\). We define an equivalence relation \(\approx\) on pairs \((history, variable)\) in \(H\times Var_\Sigma\) (telling us when two such pairs represent the same value), as well as a total preorder \(\lessapprox\) on these pairs in \(H\times Var_\Sigma\) (telling us when the value of a pair is at most equal to another pair’s value). Then we take our canonical set of objects \(D\) to be the quotient of \(H\times Var_\Sigma\) with respect to \(\approx\), while the preorder \(\lessapprox\) induces our desired total order \(\leq\) on the quotient \(D\).

For this, we first introduce another equivalence relation \(\sim\) on \(H\times Var_\Sigma\) (representing identity of objects at a given node), and another partial preorder \(\lesssim\) on \(\sim\) on \(H\times Var_\Sigma\) (representing the order relation on values at a given node). This is given by putting: \[(h,x) \sim (h', x') \,\,iff\,\, h=h'and(x= x')\in last(h),\] \[(h,x) \lesssim (h', x') \,\,iff\,\, h=h'and(x\leq x')\in last(h).\]

Second, we define (forward and backward) one-step relations \(\to_=\) and \(\to_\leq\) on pairs in \(H\times Var_\Sigma\): \[(h,x) \to_= (h', x') \,\,iff\,\, \exists y\in Var_\Sigma\, \exists A\supseteq \mathcal{L}(y)s.t.h\to_A h', (x=y)\in last(h)\&(y=x')\in last(h');\] \[(h,x) \leftarrow_= (h', x') \,\,iff\,\, \exists y\in Var_\Sigma\, \exists A\supseteq \mathcal{L}(y)s.t.h\leftarrow_A h', (x=y)\in last(h)\&(y=x')\in last(h');\] \[(h,x) \to_\leq (h', x') \,\,iff\,\, \exists y\in Var_\Sigma\, \exists A\supseteq \mathcal{L}(y)s.t.h\to_A h', (x\leq y)\in last(h)\&(y\leq x')\in last(h');\] \[(h,x) \leftarrow_\leq (h', x') \,\,iff\,\, \exists y\in Var_\Sigma\, \exists A\supseteq \mathcal{L}(y)s.t.h\leftarrow_A h', (x\leq y)\in last(h)\&(y\leq x')\in last(h').\] Note that \(\leftarrow_=\) is just the converse of \(\to_=\), but \(\leftarrow_\leq\) is not the converse of \(\to_\leq\).

Value Identity and Order Finally, we define our main equivalence relation \(\approx\) and our total preorder \(\lessapprox\) on pairs \((history, variable)\) in \(H\times Var_\Sigma\), by putting: \(\approx \, \,\, :=\, \,\, (\sim\cup\to_=\cup \leftarrow_=)^*\); and \(\lessapprox \, \,\, :=\, \,\, (\lesssim\cup \to_\leq \cup \leftarrow_\leq)^*\), where \(R^*\) is the reflexive-transitive closure of a relation \(R\). It is useful to have a more concrete characterization of \(\approx\) and \(\lessapprox\), in terms of the non-redundant path from \(h\) to \(h'\):

From Quasi-Model to Model We are first defining our first-order data model \(\mathbf{D}=(D, I)\) for the restricted vocabulary \(\mathcal{V}_\Sigma\): as announced, the set of ‘values’ \(D\) is the quotient \[D\,\, :=\,\, (H\times Var_\Sigma)/\approx \, =\, \{[h,x]: (h,x)\in H\times Var_\Sigma\},\] where \([h,x]\) denotes the equivalence class of \((h,x)\) modulo \(\approx\), defined by \[[h,x]:=\{(h', x')\in H\times Var_\Sigma: (h,x) \approx (h', x')\} \, \,(for any given pair (h,x)\in H\times Var_\Sigma).\] The partial preorder \(\lessapprox\) on pairs \((h,x)\in H\times Var_\Sigma\) induces a partial order on the equivalence classes \([h,x]\in D\), which in its turn can be extended to some total order on \(D\), that we will denote by \(\leq_\mathbf{D}\).¹⁰

The interpretation function \(I\) will map \(n\)-ary functional symbols \(F\in Funct_\Sigma\) into \(n\)-ary functions \(I(F): D^n\to D\) given by: \(I(F) ([h,x_1], \ldots, [h,x_n]) \, :=\, [h, F(x_1, \ldots, x_n)]\) if \(F(x_1, \ldots, x_n)\in Var_\Sigma\); and
\(I(f) ([h,x_1], \ldots, [h,x_n]) :=\, \bot_\mathbf{D}\), otherwise; it will also map \(n\)-ary predicate symbols \(P\in Pred_\Sigma\setminus \{\leq\}\) into \(n\)-ary relations \(I(P)\subseteq D^n\) given by: \(I(P) \, := \, \{([h,x_1], \ldots, [h,x_n])\in D^n: h\in H, \overline{{x}}=(x_1, \ldots, x_n)\in Var_\Sigma^n s.t. P \overline{{x}}\in last(h)\}\); while the interpretation \(I(\leq)\) will be just the total order \(\leq_\mathbf{D}\) constructed above.

The Model Finally, our epistemic state model \({\mathbf{M}}= (H, \sim, \underline{\bullet}, \underline{\bullet}(\bullet))\) is given by taking: as set of states, the set \(H\) of all histories; the indistinguishability relations \(\sim_a\subseteq H\times H\) are as defined above on histories¹¹; the valuation/assignment map \(\underline{\bullet}(\bullet): H\times (V_\Sigma\cup Prop_\Sigma) \to D\) is given by putting: \(\underline{h}(v) := [h,v]\) for \(v\in V_\Sigma\); and \(\underline{h}(p):=\top_\mathbf{D}\) iff \(p\in last (h)\) (-else, \(\underline{h}(p):=\bot_\mathbf{D}\)) for \(p\in Prop_\Sigma\).

The next results use the following notation, for \(h\in H\), \(x\in Var_\Sigma\), \(\varphi\in\Sigma\) and \(A\subseteq \mathcal{A}\): \[Val_h (x_A^\varphi)\,\, :=\,\, \{[h', x]\in D \mid h'\sim_Ah, \varphi \in last (h')\}\]

Proof of Proposition [Satisfiability]: If \(S\) is a quasi-model for \(\varphi_0\), then by applying claim 1 of the Truth Lemma 16 to \(\varphi_0\) and to the history \(h_0:=(\Delta_0)\), we conclude that \(h_0\models \varphi_0\) in our history-based model \({\mathbf{M}}\) above.

6 Completeness and Decidability Proofs for \(LDAE\)↩︎

In this section we prove Theorem 2. We first establish our co-expressivity result: \(LDAE\) and \(LDA\) are provably co-expressive. For this, we need a few preliminary notions and results.

Reducible expressions A formula \(\theta\) in \(LDAE\) is said to be reducible if it is provably equivalent to a ‘static’ formula; i.e., if there exists some formula \(\theta'\) in the static fragment \(LDA\) s.t. \(\vdash \, \theta \leftrightarrow \theta'\) is provable in \(\mathbf{LDAE}\). A term \(x\in Var_{LDAE}\) is reducible if it is provably equal to a static term; i.e., if there exists some \(x'\in Var_{LDA}\) s.t. \(\vdash \, x=x'\) is provable in \(\mathbf{LDAE}\). Finally, an event \({\mathbf{e}}=({\mathbf{E}},e)\) is reducible if all preconditions \(pre_f\) and all post-conditions of the form \(\underline{e}(p)\) or \(\underline{e}(v)\) are reducible (for all \(f\in E\), \(p\in Prop\) and \(v\in V\)).

We first prove a preliminary “one-step reduction” result:

Using this, we can establish our full reduction result:

Proof of Theorem 2: Completeness follows immediately from Lemma 19, the soundness of \(\mathbf{LDAE}\), and the completeness of the system \(\mathbf{LDA}\) (Theorem 1); decidability follows from the decidability of the static logic \(LDA\) (Theorem 1) and the co-expressivity of \(LDA\) and \(LDAE\) (Lemma 19).

7 Conclusions and Future Work↩︎

In this paper we axiomatize a decidable but richly expressive logic, that deals with a large class of data-exchange events, while capturing group knowledge of both propositional and non-propositional data, as well as a group’s ability to narrow down the values of a variable to finitely many possibilities.

There are a number of things still left to do. As already mentioned, one can add common knowledge operators \(C_A\varphi\), but pre-encoding their dynamics requires a generalization to polyadic conditionals \(C_A^e \varphi\) as in [@BS24]. We leave this for a journal version, where we also plan to explore the relationships of our formalism with the Logic of Functional Dependence [@BvB2020a] and Graded (Multi)Modal Logic.

Our axioms are somewhat complicated due to the fact that we did not succeed to prove FMP (Finite Model Property) for our logics. This would have allowed us to replace cutoff-minimization \(\mu_N x_A^\varphi\) by plain minimization \(min\, x_A^\varphi\) (over all \(A\)-possible \(x\)-values given \(\varphi\)), which would greatly simplify our axioms. On the other hand, we don’t have a counterexample to FMP, so this issue is still an open question.

---

1. The same piece of data can be stored/copied at multiple locations, and each location can store multiple pieces of data.↩︎

2. The notation \(D_A\varphi\) is typically used for distributed knowledge, but we prefer here \(K_A\varphi\) because we think of this as capturing a natural notion of (virtual) group knowledge.↩︎

3. Conditional knowledge \(K_A^\varphi x\) of the value can now be recovered as a special case (for \(N=1\)).↩︎

4. We can define all these using a cutoff-minimization construct \(\mu_N x_A^\varphi\), which is the same as \(1_N.x_A^\varphi\): it denotes the least of the \(\leq N\) possible values of \(x\) (according to \(A\) given \(\varphi\)).↩︎

5. In effect, the ‘values’ of variables \(x\) “hitch a ride” on the back of various group epistemic transitions \(\to_A\) in the tree, and their properties are transmitted by passing them to other (\(A\)-preserved) terms.↩︎

6. All the sets (\(\mathcal{A}, V, Prop, Pred, Funct,\mathcal{E})\) in a vocabulary are assumed to be mutually disjoint.↩︎

7. This corresponds to a dynamics introduced and axiomatized in this form in [@Baltag2010], though technically isomorphic to the action of public resolution of an issue/question [@BenthemMinica1].↩︎

8. The special case \(\mathbf{!({\cal A})}\) was introduced in [@Baltag2010], and axiomatized in different contexts in [@Boddy2014; @Goldbach2015; @BBS2016]. The general case \(\mathbf{!(G)}\) was studied (as “group resolution”) in [@AgotnesWang2017].↩︎

9. Note that this would immediately give us the completeness and decidability of \(\mathbf{LDA}\) (by Proposition [Satisfiability], Proposition [QuasiModel] and the soundness of the system \(\mathbf{LDA}\), as well as the finiteness of the closure \(\Sigma=\Sigma(\varphi_0)\), and the decidability of checking that a subset of \(\Sigma\) is a quasi-model).↩︎

10. Though not unique, such a total order \(\leq_\mathbf{D}\) exists by the Order-Extension Principle, a well-known consequence of the Axiom of Choice.↩︎

11. Note that this is meant to be a (standard) model, so the group indistinguishability relations \(\sim_A\) are just the intersections \(\bigcap_{a\in A}\sim_a\), thus coinciding with the general relations \(\sim_A\) introduced above.↩︎