Paper deep dive
The Logic of Data Access and Data Exchanges
Alexandru Baltag, Sonja Smets
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 96%
Last extracted: 7/5/2026, 1:36:48 AM
Summary
The paper introduces the Logic of Data Access and Data Exchanges (LDAE), an extension of Dynamic Epistemic Logic (DEL). It combines standard propositional knowledge with non-propositional (numerical) knowledge and operators for narrowing down possible values (cutoff minimization). The logic handles 'data-exchange events' where agents gain access to entire 'chunks' of information from sources (databases, websites, etc.). The authors provide complete axiomatizations, prove decidability, and demonstrate the logic's ability to model complex scenarios like hacking and public data sharing.
Entities (6)
Relation Signals (3)
LDAE → extends → Dynamic Epistemic Logic
confidence 100% · investigate a new logic that extends Dynamic Epistemic Logic (DEL)
LDA → isstaticfragmentof → LDAE
confidence 100% · The 'static' fragment of our logic, called the (static) Logic of (group) Data Access (LDA)
Agent → accesses → Data-exchange event
confidence 90% · In a data-exchange event, agents may gain access to 'sources'
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:We investigate a new logic that extends Dynamic Epistemic Logic (DEL), by combining standard epistemic modalities for (individual and distributed) propositional knowledge with operators for (conditional) non-propositional knowledge of a number (in which an agent or a group have knowledge of the value of some variable x, conditional on some additional information). We also generalize these operators, by considering formulas that express the fact that an agent or group can (conditionally) narrow down the possible values of the variable x to at most N possibilities (for some natural number N). In order to name and compare such hypothetical values, we extend the logic further with definite descriptions based on minimization operators, denoting the least of the N possible values of x (according to some fixed order) that are considered possible by the agent or group. On this static base, we consider DEL-style extensions with dynamic modalities for general 'data-exchange events' (covering private and public propositional announcements, but also secret hacking of a private database, or public sharing of one's data via open-source repositories, etc.). In such scenarios, whole 'chunks' of information may be exchanged or modified: once access to a given source is gained, all the 'data' stored at that specific location becomes available. We give complete axiomatizations for the resulting logics, and prove their decidability and co-expressivity.
Tags
Links
- Source: https://arxiv.org/abs/2606.31858v1
- Canonical: https://arxiv.org/abs/2606.31858v1
Trouble viewing inline? Open PDF directly →
Full Text
81,087 characters extracted from source content.
Expand or collapse full text
M. Bílková, M. Gattinger, I. van der Giessen, M. Girlando, Y. Wang (Eds.): Advances in Modal Logic 2026 (AiML 2026) EPTCS 447, 2026, p. 93–116, doi:10.4204/EPTCS.447.6 © A. Baltag, S. Smets This work is licensed under the Creative Commons Attribution License. The Logic of Data Access and Data Exchanges Alexandru Baltag University of Amsterdam, ILLC Amsterdam, Netherlands thealexandrubaltag@gmail.com Sonja Smets University of Amsterdam, ILLC Amsterdam, Netherlands s.j.l.smets@uva.nl We investigate a new logic that extends Dynamic Epistemic Logic (DEL), by combining standard epistemic modalitiesK a φandK A φfor (individual and distributed)propositional knowledgewith operatorsK φ a x,K φ A xdenoting(conditional) non-propositional knowledge of a number(in which an agentaor a groupAhave knowledge of the value of some variablex, if given additional information φ). We also generalize these operators, by considering formulas|x| φ A ≤N(for any natural number N), saying that:conditional onφ, A can narrow down the possible values of variable x to at most N possibilities. In order to name and compare such hypothetical values, we extend the logic further withdefinite descriptions based on minimization operators:μ N x φ A denotes theleast of the N possible values of x(according to some fixed order≤) that are considered possible by groupA(given condition φ). On this static base, we consider DEL-style extensions withdynamic modalities for general ‘data- exchange events’(covering private and public propositional announcements, but also secret hacking of a private database, or public sharing of one’s data via open-source repositories, etc). In such scenarios, whole ‘chunks’ of information may be exchanged or modified: once access to a given source is gained, all the ‘data’ stored at that specific location becomes available. We give complete axiomatizations for the resulting logics, and prove their decidability and co-expressivity. 1 Introduction Information may come in both propositional form (Boolean variables) and non-propositional form (e.g. numbers, names, addresses, pictures, videos, etc). Suchdatacan be encoded asvalues of local variables (e.g. a cryptographic key or a password), that are stored and processed in certainlocationsor ‘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 anagent(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). 1 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 anextended location, the information beingdistributedamong 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” operatorsK a xorK A xfor (individual or distributed)knowledge of (the value of) some variable x(in addition to the traditional modalitiesK a φandK A φfor individual or distributed knowledge of a propositionφ). This work traces back to Plaza [22] and subsequent investigations by [18, 25, 26, 27, 20, 16, 21, 3, 12] on formalizing ‘knowledge de re’. While Plaza axiomatized the static logic of ‘knowing what’, the extension with dynamic operators[!φ]ψfor (propositional) public announcements !φwas only later axiomatized by Wang and Fan [27]. To ‘pre-encode’ this dynamics using DEL-style reduction axioms [9], these authors needed aconditional version of ‘knowing what’: K φ a xmeans thataknows the value ofxgiven the information that propositionφwas the case. 1 The same piece of data can be stored/copied at multiple locations, and each location can store multiple pieces of data. 94The Logic of Data Access and Data Exchanges In recent work [12], we extended this setting with operatorsK φ A xforconditional distributed knowl- edge of the value of x by a group A. This was motivated by the need to deal with a more complex dynam- ics, going beyond propositional announcements or other traditional DEL-events [9, 7, 5, 17, 6, 8, 23]. In adata-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)allthe information stored at those sources. Such events were previously considered in our work [10, 11], and in fact they subsume many other forms of non-propositional informational dynamics that were previ- ously considered, e.g. “tell us all you know” in [2] (and with a different, interrogative interpretation in [24, 14]), in-group sharing [2, 15, 19, 4], and ‘resolution’ [1]. Other examples of data-exchange events covered in [12] 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 [10], when an agentagains access to another agent b’s knowledge base, her new state of knowledge matches thedistributed knowledgeof the groupa,b. So on the side of propositional knowledge, we needed operatorsK A φfordistributed knowledge 2 within group A. A similar move was also necessary on the side of “knowing what”: operatorsK A x, expressing thatthe group A has distributed knowledge of the value of x; in fact, to pre-encode public-announcement dynamics we needed theconditional version K φ A xof these operators. Note that this type of conditional knowledge maynotimply knowledge of the ‘real’ value ofx(in the actual world), but only the fact that the agent or groupcan uniquely determine a hypothetical valueofx(applicable only to worlds satisfying φ). To axiomatize these notions, in the presence of equality of valuesx=y, we were lead to introduce definite description terms x φ A that canexplicitly refer to such hypothetical values:x φ a denotes (in the actual world) the(unique) value that x would have according to agent a ifφwere true. Using this, we were able to provide in [12] a complete axiomatization for the corresponding dynamic-epistemic logic. But for this, we had torestrictthe dynamics to ‘semi-public’ events (a class that doesnotinclude e.g. secret hack- ing). On the other hand, in [11] we axiomatized a logic withunrestricted dynamics, covering ‘arbitrary’ data-exchange events (including complicated hacking scenarios). But this was based on arestricted static logic base, that didnotinclude non-propositional knowledge operators, but only the traditional epistemic modalitiesK a φandK A φ, as well as (a major generalization of) common knowledgeC A φ(in the form of polyadic conditional-epistemic group modalitiesC e A φ 1 ...φ n , indexed by data-exchange eventse). There wereno explicit variables xin the logic, so no assertionsx=yorPx 1 ...x n talking about the properties of specific pieces of (non-propositional) data, as well asno“knowledge-what” operatorsK a x,K A xorK φ A 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 formK a x(for instance, no “conditional hacking”, in which it is common knowledge that an agentamay be hacking another agentb’s database if and only if she came to knowb’s password). In this paper, we overcome the limitations present in the frameworks of both [11] and [12], by providing a common generalization, while also greatly increasing the expressivity of the logic. More specifically, we generalize the operatorsK φ A xto expressions|x| φ A ≤N(for any natural numberN), saying that:if given additional informationφ, the group A can narrow down the possible values of variable x to at most N possibilities(for any natural numberN). In other words, the group has distributed knowledge that, ifφis the case then the value ofxbelongs to a given list ofNpossible values. 3 This is a useful addition when dealing with cryptographic protocols. Indeed, ifNis ‘small enough’ andxis say another 2 The notationD A φis typically used for distributed knowledge, but we prefer hereK A φbecause we think of this as capturing a natural notion of (virtual) group knowledge. 3 Conditional knowledgeK φ A xof the value can now be recovered as a special case (forN=1). A. Baltag, S. Smets95 agentb’s communication key or private password, then any intruderahaving the capability|x| φ a ≤Nwill be able to hackb’s communication (by simply trying out all theNpossible values), as soon as she may receive the informationφ. The same applies to a groupAof hackers if they can collectively narrow down the possibilities, i.e., have the capability|x| φ A ≤N. As done in [12] forK φ A x, whenever we have|x| a ≤N we introducedefinite descriptions denoting each of the N hypothetical values of x. For this, we assume given a salienttotal order≤on the set of values. This is useful in numerical applications, but it also allows us to convert cardinality statements|x| a ≤Ninto ordinal descriptions 1 N .x φ A , 2 N .x φ A etc, denoting “the first (or the second, etc) of the≤Npossible values ofxaccording toAgivenφ”. 4 To capture the properties of the total order, we include in our languageorder statements x≤y(besides equality of values x=yand possibly other predicatesPx 1 ...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 whichvariables have no values(and the group relations are non-standard, as they arenot intersectionsof 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 equalityx=yand non-propositional knowledgeK A x; the problems are in fact compounded by the presence of formulas for orderx≤yand narrowing down|x| φ A ≤N. Here, we use our definite descriptions to ensure that the local properties of variablesxare preserved and continuously transmitted at far-away nodes of the tree. 5 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 chosenotto include common knowledge operatorsC A φ, 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 1Alice and Bob are each given a numberx(a),x(b)∈N=0,1,2,..., while the value of the sumx(e):=x(a) +x(b)is stored in a closed envelopee. 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. eitherx(a) =x(b) +1 orx(b) =x(a)+1). We represent this situation using aninfinite Kripke model, where states are triplets of numbers(x(a),x(b),x(e)), and the accessibility relations∼ a and∼ b encode the agents’ uncertainty. We also have an accessibility relation∼ e for the ‘envelope’ (treated as an abstract ‘agent’), encoding the information contained in it. The formulaK a x(a)∧K b x(b), saying thatagents know their numbers, is valid on this model, whileK e x(e)says that the sumx(e)is stored in the envelope. On the other hand, agents aandbcantogetherfigure out the sum: we haveK a,b x(e), i.e. thegroup A=a,bhas“distributed” knowledgeofx(e). The formulas|x(a)| b ≤2,|x(b)| a ≤2,|x(e)| a ≤2 and|x(e)| b ≤2 say that the live agents cannarrow down the possibilities(for the other’s number, as well as for the sum)to at most two. Tonamethese values, we write e.g. 1 2 .x(e) a for thefirst(i.e., theleast) of thetwopossible values of the sumx(e)according to Alice, 2 2 .x(e) a for thesecondleast (=largest) of thetwo, etc. The picture is: 4 We can define all these using acutoff-minimization constructμ N x φ A , which is the same as 1 N .x φ A : it denotesthe least of the ≤N possible values of x (according to A givenφ). 5 In effect, the ‘values’ of variablesx“hitch a ride” on the back of various group epistemic transitions→ A in the tree, and their properties are transmitted by passing them toother (A-preserved) terms. 96The Logic of Data Access and Data Exchanges 0, 1, 1 1, 0, 1 2, 1, 32, 3, 54, 3, 7 1, 2, 3 3, 2, 5 3, 4, 7 a b a b a b b e e e e ... ... Example 1, continuedNext, it is common knowledge thatAlice ’hacks’ Bob’s database. This is a ‘semi-public’ event !(a:b), whichupdates the modelby replacing∼ a with the intersection∼ a ∩∼ b : 0, 1, 1 1, 0, 1 2, 1, 32, 3, 54, 3, 7 1, 2, 3 3, 2, 5 3, 4, 7 b b b b e e e e ... Example 2: an alternative scenarioStart 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 apublic announcement!(¬K a x(b)∧ ¬K b x(a)). Theupdated modelis obtained by deleting states(0,1,1)and(1,0,1)from the initial model: 2, 1, 32, 3, 54, 3, 7 1, 2, 3 3, 2, 5 3, 4, 7 b a b a b e e e ... ... Ifasked the same question again, they again answer “I don’t know”, which deletes(2,1,3)and(1,2,3): 2, 3, 54, 3, 7 3, 2, 5 3, 4, 7 a b a b e e ... ... Ifasked for the 3rd time, Alice says “I know Bob’s number” and Bob says “I don’t know”. The an- nouncement !(K a x(b)∧¬K b x(a))deletes all states but(2,3,5): so we havex(a) =2,x(b) =3,x(e) =5. Example 3Starting 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). Wecanreason hy- pothetically about this scenarioin the original model, without updating it, usingconditional knowledge K x(a)<x(b) a 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) x(a)<x(b) a for the unique (=least out of only one) value ofx(b)that is considered possible by A. Baltag, S. Smets97 Alice conditional onx(a)<x(b). But note that, when considering a condition that isknown to be false (e.g.,x(a) =x(b)), there areno such hypothetical values: so the best we can do is to interpret the ‘least’ value as the ‘infimum’ 1 1 .x(b) x(a)=x(b) a =in f/0=∞. This means that we are working inN ⊤ :=N∪∞. Example 4: Back in timeImagine now that our story startsearlier, at a time when each ‘agent’ (Alice a, Bobb, and the envelopee) only ‘knows’ their own number (but not yet the correlations between numbers). The model is justN×N×N, with(x(a),x(b),x(c))∼ a (x ′ (a),x ′ (b),x ′ (c))iffx(a) =x ′ (a), and similarly forbande. Next, the correlations are publicly announced !((x(a) =x(b) +1∨x(b) = x(a)+1)∧x(e) =x(a)+x(b)), and after that the semi-public hacking !(a:b) happens. Can we check that Alice will knowx(e)after this scenariowithout updating the modelN×N×N? For this, we will need an operatorK (x(a)=x(b)+1∨x(b)=x(a)+1)∧(x(e)=x(a)+x(b)) a,b x(e)forconditional 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 x; a way to express than an agent/group can(conditionally) narrow down to N possible values(|x| φ A ≤N), and toname these values in increasing order: 1 N .x φ A , 2 N .x φ A , etc;public announcements!φ,semi-public hacking!(a:b), etc. 3 Syntax and Semantics ofLDAandLDAE Vocabularies: static and dynamic.Astatic vocabularyV= (A,V,Pro p,Pred,F unct,ar,ε)consists of the following: 6 a finite setAofagents a,b,c,..., also called ‘locations’ (e.g., websites, databases, processors, etc), where data are stored and processed; a setVofbasic variables v,v ′ ,v ′ ,...; a setPro p ofatomic propositions p,q,...; a setPredofpredicate symbols P,Q,..., includingequality(=) and an order predicate≤; a setF unctoffunction symbols F,G,..., including twoconstants⊥,⊤; anarity mapar:Pred∪F unct→N, sending predicate symbolsP∈Predand function symbolsF∈F unctto natural numbersar(P),ar(F)∈N, withar(⊤) =ar(⊥) =0 andar(=) =ar(≤) =2; an auxiliary symbol ε̸∈A∪V∪Pro p∪Pred∪F unct, denoting “theenvironment” (e.g., the ‘envelope’ in our example). Adynamic vocabulary(V,E)is a pair consisting of a static vocabularyVand acountablesetEof ‘event names’(denoted bye,e ′ ,f,...), that includes some special symbols !,?,τ. GroupsGiven the static vocabularyV, agroup A⊆Ais any non-empty set of agents inA. We use capital lettersA,B,...to denote groups. Ordered Value DomainsAvalue domain(for a given vocabularyV) is a first-order modelD= (D,I)for V, consisting of: adomain of ‘values’ D, of cardinality|D|>1; and aninterpretation function I, mapping each functional symbolFof arityninto a functionI(F) =F D :D n →D(so that the constants⊥and⊤ are interpreted as values⊥ D ,⊤ D ∈D), and each relational symbolPof arityninto a setI(P) =P D ⊆D n ofn-tuples of values inD, subject to the following conditions: the equality symbol=is interpreted as the identity relation= D onD; and the order symbol≤is interpreted assome total order≤ D ⊆D×Don the setDhaving⊥ D as its bottom element and⊤ D as its top element(i.e.,⊥ D ≤ D d≤ D ⊤ D for alld∈D). MinimizationGiven an ordered value domainD= (D,I), it is easy to see thatevery finite non-empty subset D ′ ⊆D has a unique minimum min D ′ ∈D ′ , s.t.min D ′ ≤ D d ′ for alld ′ ∈D ′ . Notation: ‘Cutoff Minimization’We can also consider, for any natural numberN≥1, an “N-cutoff” version of minimizationmin N , defined onallsetsD ′ ⊆D(including the infinite ones), by putting: min N D ′ :=⊤ D (‘trivial’),whenD ′ =/0, min N D ′ :=min D ′ ,when 1≤|D ′ |≤N, and min N D ′ :=⊥ D (‘undefined’),otherwise (for|D ′ |>N). 6 All the sets (A,V,Pro p,Pred,F unct,E)in a vocabulary are assumed to be mutually disjoint. 98The Logic of Data Access and Data Exchanges Notation: ‘Cutoff’n th elementFor all setsD ′ ⊆Dand all 1≤n≤N, we can now introduce a notation n N (D ′ )for“the n th element of the≤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≤n<N. Epistemic State ModelsAnepistemic state model over a value domainD= (D,I)is a tupleM= (S,∼ ,•(•)), where: (i)Sis a set ofstates(or ‘possible worlds’), typically denoted bys,w,...; (i)∼:A→ P(S×S)maps agentsa∈Atoequivalence relations∼ a ⊆S×S, called‘indistinguishability’ relations; (i)• (•):S×(V∪Pro p)→Dis anassignment map(‘valuation’), mapping pairs(s,v)∈S×Vinto arbitrary valuess(v)∈D, and mapping pairs(s,p)∈S×Pro pinto valuess(p)∈⊥ D ,⊤ D . Group indistinguishabilityGiven a state modelM= (S,∼,•(•)), we definegroup indistinguishability relations∼ A := T a∈A ∼ a onS(for all groupsA⊆A) bytaking intersections. Syntax ofLDAEFor a fixed dynamic vocabulary(V,E), the(dynamic) Logic of (group) Data Access & Exchange(LDAE) has a syntax consisting of: (1) a setVar:=Var(V)of compoundvariables(or ‘terms’)x; (2) a setF ml:=F ml(V)offormulasφ; (3) a set of‘syntactic’ event models; (4) a setEvents ofdata-exchange events. These components are simultaneously defined by mutual recursion, as follows: (1) & (2)Variables and FormulasThe setsVarandF mlare given by the clauses: x::=v|F( x)|φ→x|x|μ N x φ A |e(x) φ::=p|P x|φ→φ|K A φ|[e]φ where:v∈Vare basic variables;p∈Pro pare atoms;x= (x 1 ,...,x n )are tuples of terms;P∈Predare n-ary predicate symbols;Faren-ary function symbols;a∈Aare agents;A⊆Aare groups;N≥1 are integers; and theeventseare technically “pointed event models”(E,e), as defined below. (3) & (4)Event Models and EventsAnevent modelE= (E,∼,• (•))consists of: (i) a finite set E⊆Eof event names; (i) an equivalence relation∼ a ⊆E×E(agent a’s indistinguishabilityover events) for eacha∈A; (i) achange map e (•):Pro p∪V∪A∪ε→F ml∪Var∪P(A)for each evente∈E, mappingεto a formulae (ε)∈F ml, atomsp∈Pro pto formulase(p)∈F ml, basic variablesv∈Vto termse (v)∈Var, and agentsa∈Ato groupse(a)⊆A. We require these items to satisfytwo conditions: 1.Self-Access(agents access their own database):a∈e(a); 2.Known Access(agents know their sources):e∼ a fimpliese(a) =f(a); As mentioned, adata-exchange eventis just a‘pointed’ event modele= (E,e), i.e. apairof an event modelE= (E,∼,• (•))and an event namee∈E. We denote byEventsthe set of data-exchange events. The Static LogicLDAThe ‘static’ fragment of our logic, called the(static) Logic of (group) Data Access (LDA), consists of all formulas ofLDAEthat are built without the use of dynamic operators[e]φore(x). Precondition and PostconditionsThepreconditionof any evente= (E,e)is the formulapre e :=e (ε), which intuitively givesthe event’s condition of possibility:ecan only happen in states satisfying its preconditionpre e . Theevente’s postcondition for p∈Pro pis the formulapost e (p):=e(p); similarly, theevent’s postcondition for v∈Vis the termpost e (v):=e(v). Intuitively, the postconditions determine the way an event changes the values of atoms and variables: the new value of variablev(or atomp) after eventecoincides with the ‘old’ value of the formulapost e (p)(or the termpost e (v)) before the event. (Extended) Access MapEvente’s access mapis the restriction ofetoA, specifying for each agenta∈ Athe groupe (a)⊆Aofall sources/agents (whose locations/databases are) accessed by agent a during the event. We can alsoextendthe access map togroups A⊆A, by puttinge(A):= S e(a):a∈A, for the set ofsources that are distributedly accessible to the group A during event e. A. Baltag, S. Smets99 Subexpression-complexityAnexpressionαis any formulaφ, termxor eventeofLDAE. Thesub- 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 evente= (E,e)is>all preconditions and postconditions of the formpre f , f (p)andf(v)withf∈E,p∈Pro pandv∈V. It is easy to see that<is a well-founded partial order. SemanticsWe simultaneously define three semantic notions on state modelsM= (S,∼,• (•)): 1. asatisfaction relation s|= M φbetween statess∈S(in any state modelM) and formulasφ∈F ml; 2. anextended assignment/valuation functionfromS×(Var∪F ml)toD, mapping(state,variable)- pairs(s,x)∈S×Varinto arbitrary valuess(x) M ∈D, and mapping(state,f ormula)-pairs(s,φ)∈ S×F mlinto extreme valuess(φ) M ∈⊥ D ,⊤ D . 3. aproduct update operation, mapping state modelsM= (S,∼,•(•))and event modelsE= (E,∼ ,•(•))intoupdated state modelsM N E= (S⊗E,∼,•(•))(over the same value domainD). For this definition, we need an auxiliary notation: for variablesx∈Var, groupsA, formulasφand states s∈S, theset of possible values of x at state s according to group A conditional onφis (x φ A ) s,M :=w(x) M :w∼ A s,w|= M φ. With this notation, we define our three semantic notions by mutual recursion: s|= M piffs (p) =⊤ D s|= M Px 1 ...x n iff(s(x 1 ) M ,...,s(x n ) M )∈I(P) s|= M φ→ψiffs|= M φimpliess|= M ψ s|= M K A φiffw|= M φfor allw∼ A s s|= M [e]φiff(s,e)∈S⊗Eimplies(s,e)|= M N E φ,wheree= (E,e). s(v) M =s(v)as given in the modelM s(φ→x|y) M =s(x) M ifs|= M φ, and s(φ→x|y) M =s(y) M ifs̸|= M φ s(F(x 1 ,...,x n )) M =(I(F))(s(x 1 ) M ,...,s(x n ) M ) s(μ N x φ A ) M =min N Val(x φ A ) s,M s(e(x)) M =(s,e)(x) M N E ife= (E,e)is s.t.(s,e)∈S⊗E, and s(e(x)) M =⊤ D otherwise. s(φ) M =⊤ D ifs|= M φ, and s(φ) M =⊥ D ifs̸|= M φ. M= (S,∼,• (•)),E= (E,∼,•(•))7→M N E= (S⊗E,∼,•(•)),where: S⊗E=(s,e)∈S×E|s|= M pre e (s,e)∼ a (s ′ ,e ′ )iffs∼ e(a) s ′ ande∼ a e ′ (s,e)(p)=s(post e (p)) M (s,e)(v)=s(post e (v)) M Extended assignment on sets of expressionsWe can ‘lift’ the assignment map to the level ofsetsof variablesX⊆Varandsetsof formulasΦ⊆F ml), by putting:s(X) M :=s(x) M :x∈X;s(Φ) M := s(φ) M :φ∈Φ. Whenever the model is understood, we skip the subscriptM, writing simplys|=φ, s(x),s(X)ands(Φ). For sets of formulasΦ, we also writes|=Φwhenevers|=φfor allφ∈Φ. Abbreviations. We define the usual Boolean connectivestrue:= (⊤=⊤),f alse:= (⊤=⊥),¬φ:= (φ→f alse),φ∧ψ,φ∨ψ,φ↔ψ, as well as the dual existential (Diamond) modalities⟨K A ⟩φ:= 100The Logic of Data Access and Data Exchanges ¬K A ¬φ,⟨K θ A ⟩φ:=¬K θ A ¬φ,⟨e⟩φ:=¬[e]¬φ. We also use the following abbreviations, for variables x,y∈Var, finite sets of variablesX,Y⊆Varand natural numbersn,Nwith 1≤n≤N: x∈Y:= W x=y:y∈Y,? φ :=φ→⊤|⊥,φ→x:=φ→x|⊤, K θ A φ:=K A (θ→φ),K θ A x:=K θ A (x=μ 1 x θ A ),K A x:=K true A x, 1 N .x θ A :=μ N x θ A ,(n+1) N .x θ A :=μ N−1 x θ∧x>n N .x θ A A , |x| θ A ≤0 :=K A ¬θ,|x| θ A ≤n:=K θ A (x∈Var n (x θ A )),whereVar n (x θ A ):=i n .x θ A : 1≤i≤n, |x| θ A =0 :=|x| θ A ≤0,|x| θ A >n:=|x| θ A ̸≤n, |x| θ A = (n+1):=|x| θ A >n∧|x| θ A ≤(n+1)forn≥0, minx:=x,min(X∪y):= (min X≤y)→(min X)|y. Intuitively,x∈Ysays thatxcurrently takes the same value as some term inY. The term ? φ is a Boolean variable, taking value⊤ D ifφis true, and value⊥ D otherwise. The operatorφ→xis the term analogue of material implication: it takes the value ofxifφis true, and value⊤ D otherwise. Next,‘knowledge of value’ is definable in our logic, in both conditional and unconditional forms, for groups and individuals, via the abbreviationsK θ A x,K A x,K θ A x,K A x. Note that, for the empty tupleλ= (), we haveK θ A λ= V /0=⊤. The termn.x θ A denotes then th value ofx(in≤ D -order) considered possible byA, conditional onθ. The expressions|x| θ A =n,|x| θ A ≤nand|x| θ A >nrefer to the cardinality of the set of possible values ofx, according to groupA, givenθ. Finally,min Xdenotes the minimum value of all terms inX. Distributed LocationFor anyexpression, i.e., any term, formula or eventα∈Var∪F ml∪Events, its (distributed) locationL(α)⊆A∪εis given by the following recursive clauses: L(p) =L(v) =ε,L(K A φ) =L(μ N x φ A ) =A, L(Px 1 ...x n ) =L(F(x 1 ,...,x n )) = S L(x i ): 1≤i≤n, L(φ→ψ) =L(φ)∪L(ψ),L(φ→x|y) =L(x)∪L(φ)∪L(y), L(e) =L(pre e ),L([e]φ) =L(e)∪e (L(φ)),L(e(x)) =L(e)∪e(L(x)), where we used the extended access mape(A). In particular, this gives us thatL(⊥) =L(⊤) = L(true) =L(f alse) =/0,L(¬φ) =L(φ),L(φ∧ψ) =L(φ)∪L(ψ)andL(K θ A x) =A. We can also extend the location map tofinite sets of terms X⊆Var, by putting: L(X):= [ x∈X L(x). LocalityThe values of terms or propositions having a distributed location within a groupA⊆Aare distributed knowledge among group A’s members, as shown by the results below. Proposition 3.1.(Preservation) Let s,w be states in a modelMs.t. s∼ A w for some group A⊆A, letφ be a static formula s.t.L(φ)⊆A, and let x∈Var be a static term s.t.L(x)⊆A. Then we have: 1. s|= M φiff w|= M φ; 2. s(x) M =w(x) M . Corollary 3.2.(Local Knowledge) For formulasφand terms x, we have the following validities: |=φ→K A φ,wheneverL(φ)⊆A;|=K A x,wheneverL(x)⊆A. A. Baltag, S. Smets101 3.1 Examples of Data-Exchange Events and Event Models In‘semi-public’ event models(withonly one event), it is common knowledge who can read whose data. Public AnnouncementsFor every formulaφ, the event !φ= (E !φ ,!)of publicly announcingφhas an event modelE !φ = (!,∼,•(•))whose only event name is the special symbol !, with identity∼ a = (!,!)as accessibility relation for every agent, and where we put !(p) =p, !(v) =v, !(a) =aand !(ε) =φ, hencepre !φ =φ. This event encodes the dynamics of truthful public announcements [22]: the updated modelM⊗E !φ is (isomorphic to the one) obtained by deleting all theφ-worlds from the original modelM(and keeping everything else the same). Public and Semi-Public Sharing(“Tell Us All You Know”) For groupsA,B⊆A, !(A:B) = (E !(A:B) ,!) is a semi-public event whose modelE !(A:B) = (!,∼,• (•))has the same structure asE !φ , except for the access map and the precondition, which are given by putting: !(a) =B∪afor alla∈A: !(a) =afor a̸∈A; and ! (ε) =true(so the preconditionpre !(A:B) =trueis tautological). In this action, it is common knowledge thatall agents in A gain access to the databases of all agents in B. Its effect is to replace all the relations∼ a (witha∈A) from the original modelMby the new relations∼ !(A:B) a :=∼ a ∩∼ B in the updated modelM⊗E !(A:B) , while keeping everything else unchanged (including the relations∼ a witha̸∈A). A special case is semi-public sharing !(a:b)frombtoa, obtained by takingA=aand B=b: it is common thatbshares all his knowledge witha. Another special case isA-public sharing !B:=!(A:B), which is obtained by takingA=A: all agents inBpublicly share all their information. An even more special case isb-public sharing!b=!b=!(A:b), obtained by takingA=afor some designated agenta(andB=A): agentapublicly “tells all she knows”. 7 SharingbetweenMultiple GroupsFor groupsA 1 ,B 1 ,...,A n ,B n , the event !(A 1 :B 1 ,...,A n :B n )is a semi-public event, whose modelE !(A 1 :B 1 ,...,A n :B n ) = (!,∼,• (•))has the same structure asE !(A:B) , except that the access map is given by ! (a) =a∪ S B i :i≤n,a∈A i for alla: 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 . SharingwithinGroupsFor groupsA 1 ,...,A n ⊆A, the event ofparallel sharing within different groups !(A 1 ,...,A n ) =!(A 1 :A 1 ,...,A n :A n )is the special case of !(A 1 :B 1 ,...,A n :B n )whereB i =A i . In this action, it is common knowledge thatall 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 isn=1, which represents theresolution action !(A): it is common knowledge that all the agents inAshare their information with each other. 8 Public Hacking!H a:b (as in theWikiLeakscase). It is common knowledge thatagent a ‘hacks’ agent b’s database, using her knowledge of b’s password(represented by some variablev b ),and makes all b’s data public. Everybody gets to see allb’s data (including the value of his passwordv b ), but onlyaandbknew the password beforehand. The model is the same as for public sharing !b, except for the precondition, which ispre ! :=K a v b ∧K b v b : this event happens only ifaknewb’s passwordv b before the event. Semi-public HackingThis time, it is common knowledge thatagent 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 isK a v b ∧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 thata changes her pass- word 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 7 This corresponds to a dynamics introduced and axiomatized in this form in [2], though technically isomorphic to the action of public resolution of an issue/question [24]. 8 The special case !(A)was introduced in [2], and axiomatized in different contexts in [15, 19, 4]. The general case !(G) was studied (as “group resolution”) in [1]. 102The Logic of Data Access and Data Exchanges variable v ′ a . The encryption functionFis common knowledge, but the values of the former passwordv a and of the other secret numberv ′ a are known (hopefully) only bya. The event model is similar for !φ, except that the precondition ispre ! =K a v a ∧K a v ′ a , and the postcondition forv a is ! (v a ) =F(v a ,v ′ a ). Using larger event models, we can represent various forms ofprivate and semi-private data-exchanges. Secret HackingAgentamay be hackingb’s database iff she got hold ofb’spassword v b . Only the hacker (a) knows whether or not she succeeded to getv b . We represent this eventSH a:b = (E,!)using a modelE= (!,τ,∼,• (•))with two events ! (forsuccessful hacking) andτ(unsuccessful hacking). The preconditions arepre ! :=K a v b ∧K b v b andpre τ :=¬K a v b ∧K b v b . The access maps are !(a):=a,b, τ (a) =a, and !(c) =τ(c) =cfor allc̸=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 | true b ≤N/v a :=F(v a ,v ′ a )). It is common knowledge thata 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(E,!), whose event model E= (!,?,∼,• (•))has two event names ! (forchanging a’s password) and ? (forno change). The preconditions arepre ! :=K a |v a | true b ≤Nandpre ? :=¬K a |v a | true b ≤N. The postconditions forv a are ! (v a ):=F(v a ,v ′ a )and ?(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, agenta’s accessibility is the identity relation, while all others’ accessibility is the universal relation. Secret Detection of HackingWe can modify the secret hacking exampleSH a:b to allow the possibility thatbmightdetect a’s hacking attack (so that he might come to know that he is being hacked). Onlyb knows whether he actually detects an attack. This event(E,!)has a modelE=!,?,τwiththreeevent names ! (detected hacking), ? (successful, undetected hacking) andτ(unsuccessful hacking). The access maps for ! andτare as in the model forSH a:b , while the access map for ? is the same as for !; and the same goes forpre ! ,pre τ andpre ? . Besides loops for all agents, we also have !∼ a ? (i.e.adoesn’t know whether his hacking is detected or not) and ?∼ b τ(bcan’t distinguish between undetected hacking and unsuccessful hacking), while∼ c is the universal relation for all outsidersc̸=a,b. 4 Axiomatization and Decidability We first look at thestatic fragment LDA: its proof systemLDAis in Table 1. Proposition 4.1.The following theorems are provable in the systemLDA: 1. (Propositional Introspection)K A φ→K A K A φ;¬K A φ→K A ¬K A φ; 2. (Term Introspection) K A x,forL(x)⊆A; 3. (Group Monotonicity) K A φ→K B φ,for A⊆B. Theorem 4.2.(Soundness, Completeness and Decidability ofLDA) The proof systemLDAis complete for the static fragment LDA. Moreover, the static logic LDA is decidable. Proof. Completenessis shown in Section 5, using Prop 4.1.Soundnessis trivial, except for the ’Reaching the Minimum’ axiom, whose soundness we sketch here. Suppose thats|=φ∧K φ A (x∈Y)for some Y⊆Vars.t.|Y|≤NandL(Y)⊆A. To show thats|=⟨K φ A ⟩ μ N x φ A =x , we first prove the following: Claim: Val(x φ A ) s,M ⊆s(Y) M . To show this, letd∈Val(x φ A ) s,M , i.e. there is somew∼ A s.t.w|=φandw(x) =d. Sinces|= K φ A (x∈Y), we infer thatw|= (x∈Y), hencew(x)∈w(Y). But, given thatw∼ A sandL(Y)⊆A, we have thatw(Y) =s(Y)(by Proposition 3.1). So we obtaind=w(x)∈w(Y) =s(Y). Since this holds for anyd∈Val(x φ A ) s,M , we conclude thatVal(x φ A ) s,M ⊆s(Y), thus establishing our Claim. A. Baltag, S. Smets103 (I)Axioms and rules of classical propositional logic (CPL): Modus Ponens rule&all instances of CPL axioms in the language ofLDAE (I)Axioms for equality and order: (Indiscernability) x=y→(Pxz↔Pyz) (Functionality)x=y→F(x) =F(y) (Definition by Cases)φ→(x= (φ→x|y)),¬φ→(y= (φ→x|y)) (Transitivity)(x≤y∧y≤z)→x≤z (Anti-symmetry)(x≤y∧y≤x)→x=y (Totality)x≤y∨y≤x (Top and Bottom)⊥≤x≤⊤ (Non-trivial Constants)⊤̸=⊥ (I)Axioms and rules for (distributed) knowledge: (Necessitation)Fromφ, inferK A φ (Distribution)K A (φ→ψ)→(K A φ→K A ψ) (Veracity)K A φ→φ (Local Knowledge)φ→K A φ,forL(φ)⊆A (IV)Axioms for (cutoff) minimum value: (Lower Bound)φ→μ N x φ A ≤x (Trivial Minimum)K A ¬φ→μ N x φ A =⊤ (Undefined Minimum)|x| φ A >N→μ N x φ A =⊥ (Reaching the Minimum) φ∧K φ A (x∈Y) → ⟨K φ A ⟩ μ N x φ A =x , for|Y|≤Ns.t.L(Y)⊆A Table 1: The proof systemLDAfor the static fragment, using abbreviationsK θ A φ,⟨K θ A ⟩φ,x∈Y,|x| φ A >N. Using the above Claim and the fact that|Y|≤N, we have that|Val(x φ A ) s,M |≤N. Since we also have thats(x)∈Val(x φ A ) s,M ̸=/0 (sinces|=φ), we obtain thats(μ N x φ A ) =min N Val(x φ A ) s,M =minVal(x φ A ) s,M ∈ Val(x φ A ) s,M (by the semantic clause forμ N and the definition ofmin N ), and hences(μ N x φ A ) =w(x)for some w∼ A swithw|=φ. Applying again Proposition 3.1, we havew(μ N x φ A ) =s(μ N x φ A ) =w(x)(since L(μ N x φ A ) =A). This, together withw∼ A sandw|=φ, yieldss|=⟨K φ A ⟩ μ N x φ A =x , as desired. As for the fulldynamic logic LDAE, we need a few more notations and results to state our axioms. Possible Values after an EventRecall thatVal(x φ A ) s,M =w(x) M :w∼ A s,w|= M φis the set of possible values at statesaccording toAgivenφ. The following (easily checked) result gives us a characterization of the corresponding set of possible values ofx(according toAgivenφ)after an evente: Lemma 4.3.Val(x φ A ) (s,e),M⊗E = S f∼ A e Val f(x) ⟨f⟩φ f (x) s,M Counting the Possible Values after an EventWe want a formula expressing the fact thatthere will be at most N possible values of x(according toAgivenφ)after the evente. Moreover, we want to express thisat the current state(before the event). Put nowVar N e (x φ A ):=n N f(x) ⟨f⟩φ f (A) :f∼ A e,n≤N. Semantically, given Lemma 4.3, it should be clear that,if|Val(f(x) ⟨f⟩φ f(A) ) s,M |≤N holds for all events f∼ A e, then Val(x φ A ) (s,e),M⊗E ⊆s(Var N e (x φ A )) M . However,this inclusion might be strict: it can happen thatnot all of the values in s(Var N e (x φ A )) M are possible valuesofxaccording toA(givenφ, after the evente). The problem is that whenever|Val(f(x) ⟨f⟩φ f (A) ) s,M |<Nforsome f∼ A e, we get a possibly ’fake’ x-valueN N .f(x) ⟨f⟩φ f(A) =⊤ D . So, for anyz∈Var N e (x φ A ), its condition of possibility is given by the formula: 104The Logic of Data Access and Data Exchanges ♢z:= z=⊤ → _ f∼ A e ⟨K ⟨f⟩φ f(A) ⟩f(x) =⊤ ! . Thus, for anysubset Z⊆Var N e (x φ A ), the formula |Z| ♢ ≤N:= _ Y⊆Z,|Y|≤N z∈Z ♢z→ _ y∈Y z=y ! says thatthe number of possible values of x in Z (according to A givenφ) is at most N. Finally, by applying this to the whole setZ=Var N e (x φ A )above, we obtain the desired formula: Lemma 4.4.Let s be a state in a state modelM, letebe an event in an event modelEwith s|= M pre e , and let x,A,φbe s.t.|Val(f(x) ⟨f⟩φ f(A) ) s,M |≤N holds foreveryf∼ A e. Then we have the equivalences: s|= M |Var N e (x φ A )| ♢ ≤N iff|Val(x φ A ) (s,e),M⊗E |≤N iff(s,e)|= M⊗E |x φ A |≤N. Using these notations, the proof systemLDAEfor our full dynamic logic is given in Table 2. (I)Static Axioms and rules of LDA AllLDArules & allLDAaxiom schemas extended to formulas of the full languageLDAE (I)Reduction axioms and rules for prop. formulas: ([e]-Necessitation)Fromφ, infer[e]φ (Change of Facts)[e]p↔(pre e →post e (p)) (Change of Properties)[e]Px↔(pre e →Pe(x)) (Distributivity)[e](φ→ψ)↔([e]φ→[e]ψ) (Knowledge Update)[e]K A φ↔ pre e → V K e(A) [f]φ:f∼ A e (I)Reduction axioms for data terms: (Basic Value Change)e(v) = (pre e →post e (v)) (Functional Change)e(F( x)) = (pre e →F(e(x))) (Change of Cases)e(φ→x|y) = ([e]φ→e(x)|e(y)) (Cutoff-Min. Change)e(μ N x φ A ) = pre e → |Var N e (x φ A )| ♢ ≤N→minμ N f(x) ⟨f⟩φ e (A) :f∼ A e|⊥ Table 2: The proof systemLDAE, wheree= (E,e),f= (E,f)∈Events. Proposition 4.5.The following derived reduction laws are provable in the systemLDAE: •(Impossible Change)[e]f alse↔ ¬pre e ; and[e]true↔true; •(Negation & Conjunction Reduction)[e]¬φ↔(pre e →¬[e]φ); and[e](φ∧ψ)↔([e]φ∧[e]ψ); •(Preservation of Constants)e(⊤) =⊤; ande(⊥) = (pre e →⊥); •(Minimum Reduction)e(min X) =mine(x):x∈X. Theorem 4.6.(Soundness, Completeness, Expressivity and Decidability ofLDAE) The proof system LDAEin Table 2 is sound and complete for the dynamic logic LDAE. Moreover, LDAE is provably co-expressive with its static fragment LDA, and thus it is decidable. Proof. Completenessis shown in Section 6.Soundnessis trivial, except for the ‘Cutoff-Min’ reduction axiom, which we sketch here. LetMbe any state model, andsbe any state. We considertwo cases: Case 1: s̸|=pre e . In this case, both terms of the equality claimed in the axiom take value⊤ S atsinM. Case 2: s|=pre e . In this case,s(e(μ N x φ A )) M = (s,e)(μ N x φ A )) M⊗E =min N Val(x φ A ) (s,e),M⊗E , and there aretwo subcasesto consider: A. Baltag, S. Smets105 Subcase (2A): there exists somef 0 ∈Es.t.f 0 ∼ A eand|Val(f 0 (x) ⟨f 0 ⟩φ f 0 (A) ) s,M |>N. Then we have by definition thats(μ N f 0 (x) ⟨f 0 ⟩φ e (A) ) =⊥ D (given thatf 0 ∼ A eimpliesf 0 (A) =e(A)), and thusminμ N f(x) ⟨f⟩φ e(A) : f∼ A etakes value⊥ D ats. So the right-hand side term of the equality in the ’Cutoff-Min’ reduction axiom takes value⊥ D ats(regardless of whether we haves|= M |Var N e (x φ A )| ♢ ≤Nor not). On the other hand, the left-hand side also evaluates to⊥ D ats(since by Lemma 4.3,|Val(f 0 (x) ⟨f 0 ⟩φ f 0 (A) ) s,M |>Nimplies that|Val(x φ A ) (s,e),M⊗E |>N, hence(s,e)(μ N x φ A )) M⊗E =min N Val(x φ A ) (s,e),M⊗E =⊥ D ), as desired. Subcase (2B): we have|Val(f(x) ⟨f⟩φ f (A) ) s,M |≤Nfor allf∈Es.t.f∼ A e. We are in the conditions of Lemma 4.4, and there are againtwo subcasesto consider: Subcase (2B1):s̸|= M |Var N e (x φ A )| ♢ ≤N. In this case, we can use Lemma 4.4 to check that both sides of the equality in the ’Cutoff-Min’ reduction axiom evaluate to⊥ D ats. Subcase (2B2):s|= M |Var N e (x φ A )| ♢ ≤N. In this case, we can use Lemma 4.3 to show thats(e(μ N x φ A )) M = (s,e)(μ N x φ A )) M⊗E =min N Val(x φ A ) (s,e),M⊗E =min N S f∼ A e Val f(x) ⟨f⟩φ f (x) s,M . So the left-hand side of the equality in the ’Cutoff-Min’ axiom evaluates at states(inM) tomin f∼ A e min N Val f(x) ⟨f⟩φ f (x) s,M . On the other hand, we can use Lemma 4.4 to check that the right-hand side of the equality in the ’Cutoff- Min’ reduction axiom evaluates to the same expression ats. 5 Completeness and Decidability Proofs forLDA Throughout this section,we fix a formulaφ 0 ∈F ml. We prove Theorem 4.2 by the method ofquasi- models. But, to obtain an appropriate analogue of Fischer-Ladner closure, we need two auxiliary notions: Restricted VocabularyFor any finite setΣ⊆F ml, theΣ-restricted vocabularyV Σ := (A Σ ,V Σ ,Pro p Σ , Pred Σ ,F unct Σ ,ar Σ ,ε)is formed as follows:A Σ is the set of agents occurring (inside terms or modalities in formulas) inΣ;V Σ isthe set of basic variables occurring (as subterms of any term) in formulas of Σ;Pro p Σ :=Pro p∩Σis the set of atomic propositions inΣ;Pred Σ is the set of predicates occurring in (formulas of)Σ;F unct Σ is the set of function symbols occurring in (formulas of)Σ;ar Σ is the restriction ofartoPred Σ ∪F unct Σ . Clearly, ifΣis finite, then all the sets inV Σ are finite. TheΣ-Restricted Set of TermsFor any finite set of formulasΣ⊆F ml, theΣ-restricted set of terms Var Σ is the smallest set of terms satisfying the following closure conditions:Var Σ contains⊥and⊤, as well as all terms occurring in any formula ofΣ(henceV Σ ⊆Var Σ );Var Σ is closed under subterms; if i N .x φ A ∈Var Σ for somei≤N, thenj N .x φ A ∈Var Σ for allj≤N. Note thatVar Σ is onlya finite subsetof the (typically infinite) setVar(V Σ )of terms of the languageLDA(V Σ ). We now proceed to introduce the appropriate notions of Fisher-Ladner Closure, syntactic types, and special sets of types called quasi-models. Fisher-Ladner ClosureGiven now our fixed formulaφ 0 , theclosure ofφ 0 is the smallest set of formulas Σ=Σ(φ 0 )satisfying the following closure conditions:φ 0 ∈Σ;true,f alse∈Σ;Σis closed under subfor- mulas and single negations∼φ; ifP∈Pred Σ has arityar(P) =nand x= (x 1 ,...,x n )is ann-tuple with allx 1 ,...,x n ∈Var Σ , thenPx∈Σ; if(K A φ)∈Σ,θis a subformula of∼φandB⊆A Σ , then(K B θ)∈Σ (hence also⟨K A ⟩θ∈Σ); if(φ→x|y)∈Var Σ , thenφ∈Σ; ifx,y∈Var Σ , then(x=y),(x≤y)∈Σ; if (μ N x φ A ),z∈Var Σ andY⊆Var Σ , thenK φ A (z∈Y),⟨K φ A ⟩(z∈Y)∈Σ. TypesLetΣbe the closure ofφ 0 . AΣ-typeis a subset ofΣwith the following properties: 1. for everyφ∈Σ:(∼φ)∈∆iffφ̸∈∆; 106The Logic of Data Access and Data Exchanges 2. for every(φ∧ψ)∈Σ:(φ∧ψ)∈∆iffφ∈∆andψ∈∆; 3. for everyPxz∈Σ: if(x=y),Pxz∈∆thenPyz∈∆; 4. forF(x),F(y)∈Var Σ : if(x=y)∈∆, then(F(x) =F(y))∈∆; 5. if(x≤y),(y≤z)∈∆, then(x≤z)∈∆; 6. if(x≤y),(y≤x)∈∆, then(x=y)∈∆; 7. either for allx,y∈Var Σ , we have either(x≤y)∈∆or(y≤x)∈∆; 8. for allx∈Var Σ , we have(⊥≤x),(x≤⊤)∈∆; 9.(⊤̸=⊥)∈∆; 10. for every(φ→x|y)∈Σ:φ∈∆implies(x= (φ→x|y))∈∆; andφ̸∈∆implies(y= (φ→x|y))∈∆; 11. if(K A φ)∈∆thenφ∈∆; 12. for allμ N x φ A ∈Var Σ :(μ N x φ A ≤x)∈∆; 13. ifφ,K φ A (μ N x φ A ̸=x)∈∆andY⊆Var Σ is s.t.L(Y)⊆Aand|Y|≤N, then⟨K φ A ⟩(x̸∈Y)∈∆; 14. for allμ N x φ A ∈Var Σ : if(K A ¬φ)∈∆, then(μ N x φ A =⊤)∈∆; 15. for allμ N x φ A ∈Var Σ : if(|x| φ A >N)∈∆, then(μ N x φ A =⊥)∈∆. ObservationTypes are closed under modus ponens: if∆is a type and(φ→ψ),φ∈∆, thenψ∈∆. Accessibility relations on typesFor types∆,∆ ′ and groupA⊆A Σ , we put: ∆∼ A ∆ ′ iffφ∈∆⇔φ∈∆ ′ for allφ∈Σs.t.L(φ)⊆A. Proposition 5.1.The relations∼ A are equivalence relations on types, satisfying Group Monotonicity: ∆∼ A ∆ ′ and B⊆A imply∆∼ B ∆ ′ . Proof.This follows directly from the definition of relations∼ A on types. Proposition 5.2.If∆∼ A ∆ ′ and(K A φ)∈∆, thenφ∈∆ ′ . Proof.SinceL(K A φ) =Aand∆∼ A ∆ ′ , we use the definition of∼ A on types and the fact that(K A φ)∈∆ to infer that(K A φ)∈∆ ′ . This together with condition 11 on types, gives us the desired conclusion. Hat notation. For every type∆, we put b ∆:= V ∆for theconjunction of all formulas in∆. Proposition 5.3.Given types∆andΛ, if b ∆∧⟨K A ⟩ b Λis consistent, then∆∼ A Λ. Proof.Let∆andΛbe types as above, and suppose towards a contradiction that we have∆̸∼ A Λ. Then there must existφ∈Σs.t.L(φ)⊆Aandφ∈∆, but(∼φ)∈Λ. From this together with the assumption that b ∆∧⟨K A ⟩ b Λis consistent, we infer thatφ∧⟨K A ⟩¬φis consistent, and thusφ∧¬K A φis consistent. But this contradicts the fact that⊢φ→K A φis anLDA-theorem for formulasφwithL(φ)⊆A. Quasi-ModelsAquasi-model forφ 0 is a setSof types overΣ, with the following two properties: (*) φ 0 ∈∆ 0 for some type∆ 0 ∈S; (**) if⟨K A ⟩φ∈∆∈S, then there is some∆ ′ ∈Swith∆∼ A ∆ ′ andφ∈∆ ′ . Proposition 5.4.If∆∈S is a type in a quasi-model S, then we have the following: (1)if K A (φ→ψ)∈∆and(K A φ)∈∆, then K A ψ∈∆; (2)for every(K A φ)∈Σs.t.L(φ)∈A, ifφ∈∆then(K A φ)∈∆; (3)if(K A φ)∈∆and B⊆A, then(K B φ)∈∆. A. Baltag, S. Smets107 TheΣ-canonical quasi-modelAΣ-theoryis any maximally consistent subset ofΣ. We denote byS Σ the set of allΣ-theories. We willshow that S Σ is a (finite) “canonical” quasi-modelforΣ. Lemma 5.5.EveryΣ-theory is aΣ-type. Proof.This is easy to check, using the axioms ofLDAand Proposition 4.1. Lemma 5.6.For every∆∈S Σ , if⟨K A ⟩φ∈∆then there is some∆ ′ ∈S Σ with∆∼ A ∆ ′ andφ∈∆ ′ . Proof.Put∆ A :=θ:θ∈∆s.t.L(θ)⊆A∪∼θ:θ∈(Σ−∆)s.t.L(θ)⊆A. Claim:∆ A ∪φis consistent wrt the systemLDA. Proof of Claim: Suppose not. Then we have⊢ c ∆ A →∼φ. Applying Necessitation and Distribution, we obtain⊢K A c D A →K A ∼φ. On the other hand, by inspecting the structure of∆ A , it is easy to see that L(∆ A )⊆A, so by Strong Introspection (Proposition 4.1) we have⊢ c ∆ A →K A c ∆ A . Putting these together, we get⊢ c ∆ A →K A ∼φ. Since∆ A ⊆∆and∆is closed underΣ-consequences, we have(K A ∼φ)∈∆. But this contradicts the assumption that⟨K A ⟩φ∈∆(given the consistency of∆). Using our Claim and the standard Lindenbaum Lemma, we get that∆ A ∪φhas aΣ-maximally consis- tent extension∆ ′ ∈S ′ Σ . So we haveφ∈∆ ′ and∆ A ⊆∆ ′ , which implies that∆∼ A ∆ ′ . Proposition 5.7.Ifφ 0 ∈Σis consistent, then there exists a quasi-model forφ 0 . Proof.Take the setS Σ of allΣ-theories. By the Lindenbaum Lemma, there exists a maximally consistent subset∆ 0 ∈S Σ , such thatφ 0 ∈∆ 0 . By Lemmas 5.5 and 5.6,S Σ is a quasi-model forφ 0 . Corollary 5.8.Ifφ 0 is satisfiable then there exists a quasi-model forφ 0 . The hard part is to prove theconverseof this: Proposition 5.9.If S is a quasi-model forφ 0 , thenφ 0 is satisfiable. 9 The rest of this section is dedicated to the proof of Proposition 5.9. Unravelling: the tree of historiesLet us fix a quasi-modelS, a formulaφ 0 and a type∆ 0 ∈Swith φ 0 ∈∆ 0 . We will construct a model forφ 0 , based on an unravelling ofSaround∆ 0 . Ahistoryis a finite sequenceh= (∆ 0 ,A 1 ,∆ 1 ,...,A n ,∆ n )of any lengthn≥0, where∆ 1 ,...,∆ n ∈Sare types andA 1 ,...,A n ⊆ A Σ are groups, such that we have∆ i−1 ∼ A i ∆ i for alli=1,n. LetHbe the set of all histories. We denote bylast(h):=∆ n the last state in historyh, and by→ A the naturalforward one-step relationon histories inH, given by putting:h→ A h ′ iffh ′ = (h,A,∆ ′ )(withlast(h)∼ A ∆ ′ =last(h ′ )). We denote by← A the backward one-step relation, defined as the converse of the forward relation:h← A h ′ iffh ′ → A h. The one- step relations structureHinto atree rooted at∆ 0 (with the immediate successor relation given byh→h ′ iffh→ A h ′ for some groupA). In particular, we havethe tree property:every two nodes h,h ′ of the tree are connected by a unique non-redundant path h=h 0 ← A 1 h 1 ← A 2 ...← A i h i → A i+1 ...→ 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 historiesTo make this tree into a model for our restricted vocabularyV Σ , we define oursingle-agent indistinguishability relations∼ a ⊆H×Hon histories, by putting ∼ a := [ A∋a → A ∪ [ A∋a ← A ! ∗ , 9 Note thatthis would immediately give us the completeness and decidability ofLDA(by Proposition 5.9, Proposition 5.7 and the soundness of the systemLDA, as well as the finiteness of the closureΣ=Σ(φ 0 ), and the decidability of checking that a subset ofΣis a quasi-model). 108The Logic of Data Access and Data Exchanges where← A is the converse of→ A , the unions range over groupsA⊆A Σ s.t.a∈A, andR ∗ is the reflexive- transitive closure ofR. Since our goal is to build a standard model, thegroup indistinguishability relations ∼ A ⊆H×Hare taken to be simply theintersections∼ A := T a∈A ∼ a of all the individual relations. It is useful to give more concrete characterizations of the relations∼ A (and∼ a ) on histories: Lemma 5.10.The following areequivalent, for A⊆A Σ and histories h,h ′ ∈H: 1. h∼ A h ′ ; 2. A⊆A i , for all groups A i that appear as transition labels on the non-redundant path from h to h ′ . Proof.Use the definitions of∼ a and∼ A = T a∈A ∼ a onH, and the uniqueness of non-redundant path. Lemma 5.11.If h∼ A h ′ , then last(h)∼ A last(h ′ ). Proof.The proof is byinduction on the length N of the non-redundant pathfromhtoh ′ . For thebase case h=h ′ , the conclusion follows trivially (given that∼ A are equivalence relations). Inductive case: Suppose the non-redundant path fromhandh ′ has lengthN+1, and let us look at the last transition on this path. Given Lemma 5.10, this transition can be either of the formh N → A N h N+1 =h ′ , or of the formh N ← A N h N+1 =h ′ , withA N ⊇A. By definition of→ A on histories, we have eitherh ′ = (h N ,A N ,last(h ′ ))orh N = (h ′ ,A N ,last(h N )), withlast(h N )∼ A N last(h ′ )in both cases. By Monotonicity (Proposition 5.1) and the fact thatA⊆A N , we obtainlast(h N )∼ A last(h ′ ). On the other hand, we also havelast(h)∼ A last(h N )(-since the non-redundant path fromhtoh N has lengthN, so by the induction hypothesis the pair(h,h N )satisfies the conclusion of our Lemma, withh ′ replaced byh N ). Putting these two together (and using the transitivity of∼ A ), we conclude thatlast(h)∼ A last(h ′ ), as desired. Lemma 5.12.If(K A φ)∈last(h)and h∼ A h ′ , thenφ∈last(h ′ ). Proof.By Lemma 5.11,h∼ A h ′ implieslast(h)∼ A last(h ′ ). This, together withK A φ∈last(h), implies by Proposition 5.2 thatφ∈last(h ′ ), as desired. Lemma 5.13.(Diamond Lemma) If⟨K A ⟩φ∈last(h), then there exists some h ′ ∼ A h s.t.φ∈last(h ′ ). Proof.By Lemma 5.6, there exists some type∆ ′ ∼ A last(h)s.t.φ∈∆ ′ . Takeh ′ = (h,A,∆ ′ ). By Lemma 5.10 we haveh ′ ∼ A h, and obviouslyφ∈∆ ′ =last(h ′ ), as desired. Corollary 5.14.If(K A φ)∈Σand h∈H, then:(K A φ)∈last(h)iff we haveφ∈last(h ′ )for all h ′ ∼ A h. The Value Domain: a Quotient ConstructionTheset of values Dof our model will be a quotient of the Cartesian productH×Var Σ . Wedefine an equivalence relation≈on pairs(history,variable)in H×Var Σ (telling uswhen two such pairs represent the same value), as well asa total preorder⪅on these pairs inH×Var Σ (telling uswhen the value of a pair is at most equal to another pair’s value). Then we take our canonical set of objectsDto bethe quotient of H×Var Σ with respect to≈, while the preorder⪅induces our desiredtotal order≤on the quotientD. For this, we first introduce anotherequivalence relation∼onH×Var Σ (representingidentity of objects at a given node), and another partial preorder≲on∼onH×Var Σ (representing theorder relation on values at a given node). This is given by putting: (h,x)∼(h ′ ,x ′ )iffh=h ′ and(x=x ′ )∈last(h), (h,x)≲(h ′ ,x ′ )iffh=h ′ and(x≤x ′ )∈last(h). Second, we define(forward and backward) one-step relations→ = and→ ≤ on pairsinH×Var Σ : (h,x)→ = (h ′ ,x ′ )iff∃y∈Var Σ ∃A⊇L(y)s.t.h→ A h ′ ,(x=y)∈last(h)&(y=x ′ )∈last(h ′ ); A. Baltag, S. Smets109 (h,x)← = (h ′ ,x ′ )iff∃y∈Var Σ ∃A⊇L(y)s.t.h← A h ′ ,(x=y)∈last(h)&(y=x ′ )∈last(h ′ ); (h,x)→ ≤ (h ′ ,x ′ )iff∃y∈Var Σ ∃A⊇L(y)s.t.h→ A h ′ ,(x≤y)∈last(h)&(y≤x ′ )∈last(h ′ ); (h,x)← ≤ (h ′ ,x ′ )iff∃y∈Var Σ ∃A⊇L(y)s.t.h← A h ′ ,(x≤y)∈last(h)&(y≤x ′ )∈last(h ′ ). Note that← = is just the converse of→ = , but← ≤ isnotthe converse of→ ≤ . Value Identity and OrderFinally, we define our main equivalence relation≈and our total preorder ⪅on pairs(history,variable)inH×Var Σ , by putting:≈:= (∼∪→ = ∪← = ) ∗ ; and⪅:= (≲∪→ ≤ ∪← ≤ ) ∗ , whereR ∗ is the reflexive-transitive closure of a relationR. It is useful to have a more concrete characterization of≈and⪅, in terms of the non-redundant path fromhtoh ′ : Lemma 5.15.(“Path Lemma”) Let(h,x),(h ′ ,x ′ )∈H×Var Σ , and let h=h 0 ←h 1 ←...←h i →...→ h n =h ′ be the non-redundant path from h to h ′ . Then the following are equivalent: •(h,x)≈(h ′ ,x ′ ); •either(h,x)∼(h ′ ,x ′ )(if n=0), or else there exist x 0 ,x 1 ,...,x i ,...,x n ∈Var Σ s.t. we have:(h,x) = (h 0 ,x 0 )← = (h 1 ,x 1 )← = (h 2 ,x 2 )← = ·← = (h i ,x i )→ = ·→ = (h n−1 ,x n−1 )→ = (h n ,x n ) = (h ′ ,x ′ ). Similarly, the following are equivalent: •(h,x)⪅(h ′ ,x ′ ); •either(h,x)≲(h ′ ,x ′ )(if n=0), or else there exist x 0 ,x 1 ,...,x i ,...,x n ∈Var Σ s.t. we have:(h,x) = (h 0 ,x 0 )← ≤ (h 1 ,x 1 )← ≤ (h 2 ,x 2 )← ≤ ·← ≤ (h i ,x i )→ ≤ ·→ ≤ (h n−1 ,x n−1 )→ ≤ (h n ,x n ) = (h ′ ,x ′ ). Corollary 5.16.If h,h ′ ∈H and x∈Var Σ are s.t. h∼ A h ′ andL(x)⊆A, then(h,x)≈(h ′ ,x). Proof.Leth=h 0 ← A 1 h 1 ← A 2 ...← A i h i → A i+1 ...→ A n h n =h ′ be the non-redundant path fromhtoh ′ . Sinceh∼ A h ′ , we know thatA⊆A k for allk(by Lemma 5.10). Using this together withL(x)⊆A(and the definition of the relation(h,x)→ = (h ′ ,x ′ )on history-variable pairs), we obtain(h,x)← = (h 1 ,x)← = ·(h i ,x)→ = ·→ = (h n ,x) = (h ′ ,x). By the Path Lemma, we have(h,x)≈(h ′ ,x). Corollary 5.17.Let x,x ′ ∈Var Σ and h,h ′ ∈H, and suppose that the non-redundant path from h to h ′ is of the form h=h 0 → A h 1 → A ...→ A h i → A ...→ A h n =h ′ . Then we have(h,x)≈(h ′ ,x ′ )iff there exists y∈Var Σ withL(y)⊆A,(x=y)∈last(h)and(y=x ′ )∈last(h ′ ). From Quasi-Model to ModelWe are first defining ourfirst-order data modelD= (D,I)for the restricted vocabularyV Σ : as announced, theset of ‘values’ Dis the quotient D:= (H×Var Σ )/≈=[h,x]:(h,x)∈H×Var Σ , where[h,x]denotes the equivalence class of(h,x)modulo≈, defined by [h,x]:=(h ′ ,x ′ )∈H×Var Σ :(h,x)≈(h ′ ,x ′ )(for any given pair(h,x)∈H×Var Σ ). The partial preorder⪅on pairs(h,x)∈H×Var Σ induces apartial order on the equivalence classes [h,x]∈D, which in its turn can be extended to sometotal order on D, that we will denote by≤ D . 10 Theinterpretation function Iwill mapn-ary functional symbolsF∈F unct Σ inton-ary functions I(F):D n →Dgiven by:I(F)([h,x 1 ],...,[h,x n ]):= [h,F(x 1 ,...,x n )]ifF(x 1 ,...,x n )∈Var Σ ; and I(f)([h,x 1 ],...,[h,x n ]):=⊥ D , otherwise; it will also mapn-ary predicate symbolsP∈Pred Σ \≤ inton-ary relationsI(P)⊆D n given by:I(P):=([h,x 1 ],...,[h,x n ])∈D n :h∈H, x= (x 1 ,...,x n )∈ Var n Σ s.t.P x∈last(h); while the interpretationI(≤)will be just the total order≤ D constructed above. 10 Though not unique, such a total order≤ D exists by the Order-Extension Principle, a well-known consequence of the Axiom of Choice. 110The Logic of Data Access and Data Exchanges The ModelFinally,our epistemic state modelM= (H,∼,•,•(•))is given by taking: as set of states, the setHof all histories; the indistinguishability relations∼ a ⊆H×Hare as defined above on histories 11 ; the valuation/assignment map•(•):H×(V Σ ∪Pro p Σ )→Dis given by putting:h(v):= [h,v]forv∈V Σ ; andh(p):=⊤ D iffp∈last(h)(-else,h(p):=⊥ D ) forp∈Pro p Σ . Lemma 5.18.(“Interpretation Lemma”) The interpretation I is well-defined, i.e. we have the following: 1.(h, x)≈(h ′ ,y)implies(h,F(x))≈(h ′ ,F(y)); 2.(h,x)≈(h ′ ,y)implies that:(Pxz)∈last(h)iff(Pyz)∈last(h ′ ); 3. I(E)is really the identity relation on D. Proof.Induction on the length of the non-redundant path fromhtoh ′ , using our conditions on types. Lemma 5.19.(“Preservation of Values”) If h∼ A h ′ and x∈Var Σ is s.t.L(x)⊆A, then[h,x] = [h ′ ,x]. Proof.This follows immediately from Corollary 5.16 and the definition of[h,x]. The next results use the following notation, forh∈H,x∈Var Σ ,φ∈ΣandA⊆A: Val h (x φ A ):=[h ′ ,x]∈D|h ′ ∼ A h,φ∈last(h ′ ) Lemma 5.20.(“Trivial-Minimum Lemma”) Ifμ N x φ A ∈Var Σ and h∈H are s.t. Val h (x φ A ) =/0, then [h,μ N x φ A ] =⊤ D . Proof.First, we prove an auxiliaryClaim:(K A ¬φ)∈last(h). To show this, suppose towards a contradic- tion that(K A ¬φ)̸∈last(h). This implies that⟨K A ⟩φ∈last(h)(given the closure conditions on types and the fact thatμ N x φ A ∈Var Σ implies⟨K A ⟩φ∈Σ). By the Diamond Lemma 5.13, there exists someh ′ ∼ A h withφ∈last(h ′ ), and thus[h ′ ,x]∈Val h (x φ A ). But this contradicts the assumption thatVal h (x φ A ) =/0. Using now the above Claim, and applying condition (14) on types, we obtain that(μ N x φ A =⊤)∈ last(h), i.e.[h,μ N x φ A ] =⊤ D , as desired. Lemma 5.21.(“Trivial-Value Lemma”) If[h,μ N x φ A ] =⊤ D , then Val h (x φ A )⊆⊤ D . Proof.From[h,μ N x φ A ] =⊤ D , we obtain that(h,μ N x φ A )≈(h,⊤). By the Path Lemma 5.15, we must have(μ N x φ A =⊤)∈last(h). Suppose now (towards a contradiction) thatVal h (x φ A )̸⊆⊤ D , i.e. there exists someh ′ ∼ A hwithφ,(x̸=⊤)∈last(h ′ ). By Lemma 5.11,h∼ A h ′ implies thatlast(h)∼ A last(h ′ ). From this, together with the fact that(μ N x φ A =⊤)∈last(h)and thatL(μ N x φ A =⊤) =A, = we derive that(μ N x φ A =⊤)∈last(h ′ )(by the definition of∼ A on types). Using condition 12 on types, we get that (⊤≤x)∈last(h ′ ), which together with conditions 8 and 6 on types, gives us that(x=⊤)∈last(h ′ ), contradicting the above assumption that(x̸=⊤)∈last(h ′ ). Lemma 5.22.(“Undefined-Minimum Lemma”) Letμ N x φ A ∈Var Σ be s.t.[h,μ N x φ A ] =⊥ D . Then we have either⊥ D ∈Val h (x φ A )or else|Val h (x φ A )|>N Proof.Assume towards a contradiction that[h,μ N x φ A ] =⊥ D , but⊥ D ̸∈Val h (x φ A ); i.e.:(μ N x φ A =⊥)∈ last(h), but(x̸=⊥)∈last(h ′ )for allh ′ ∼ A hwithφ∈last(h ′ ). By Corollary 5.14,K φ A (x̸=⊥)∈last(h). This, together withK A (μ N x φ A =⊥)∈last(h)(which follows from(μ N x φ A =⊥)∈last(h), by Proposition 5.4(2), and with the closure conditions onΣandL(μ N x φ A =⊥) =A), yieldK φ A (μ N x φ A ̸=x)∈last(h). To show that|Val h (x φ A )|>N, we will construct a sequence h 0 → A h 1 → A ...→ A h n → A ...→ A h N ,withh n ∼ A handφ∈last(h n )for alln, 11 Note that this is meant to be a (standard) model, so the group indistinguishability relations∼ A are just the intersections T a∈A ∼ a , thus coinciding with the general relations∼ A introduced above. A. Baltag, S. Smets111 together with a sequence ofN‘witnesses’y 1 ,...,y n ,...,y N ∈Var Σ ,withL(y n )⊆Afor alln. The construction is by recursion onn≤N. For the base step (n=0), note that(⟨K A ⟩φ)∈last(h) (since otherwise we’d have(μ N x φ A =⊤)∈last(h)by condition (14) on types, contradicting the fact that (μ N x φ A =⊥)∈last(h), given also condition (9) on types). By condition (**) on quasi-models, there exists ∆ 0 ∈Ss.t.last(h)∼ A ∆ 0 andφ∈∆ 0 . Take nowh 0 := (h,A,∆ 0 ), which fulfills the desired specifications. For the stepnof the induction (with 1≤n≤N, assuming givenh n−1 andy 1 ,...,y n−1 with the above properties), we first take then th witnessy n to be any term inVar Σ withL(y n )⊆Aand(x=y n )∈ last(h n−1 ), if such a term exists; and otherwise, we just puty n :=⊥. Next, we note that, by the induction hypothesis, we haveh n−1 ∼ A handφ∈last(h n−1 ), hencelast(h n−1 )∼ A last(h). Together with the fact thatK φ A (μ N x φ A ̸=x)∈last(h), this gives us thatφ,K φ A (μ N x φ A ̸=x)∈last(h). By condition (13) on types (applied toY:=y 1 ,...,y n , where note thatL(Y)⊆Aand|Y|≤N), we obtain⟨K φ A ⟩ V 1≤i≤n (x̸=y i )∈ last(h n−1 ). Using again clause (**) on quasi-models, there exists some∆ n ∈Ss.t.last(h n 1 )∼ A ∆ n and φ, V 1≤i≤n (x̸=y i )∈∆ n . Take nowh n := (h n−1 ,A,∆ n ), which obviously fulfills the desired specifications. Given this construction, it is clear that[h n ,x]∈Val h (x φ A )for all 0≤n≤N. We will prove thatall these N+1values are distinct(which immediately gives us that|Val h (x φ A )|>N, as desired): Let 1≤n≤N. It is enough to show that[h n ,x]̸= [h m ,x]for allm<n. Suppose not, i.e. assume towards a contradiction that we have(h n ,x)≈(h m ,x)for somem<n. Given that the non-redundant path fromh m toh n has the shapeh m → A h m+1 → A ...→ A h n , we can apply Corollary 5.17 to conclude that there exists somey∈Var Σ withL(y)⊆A,(y=x)∈last(h m )and(y=x)∈last(h n ). On the other hand, we also have by construction that(x=y m+1 )∈last(h m )and(x̸=y m+1 )∈last(h n )(sincem+1≤n). Putting all these together and using our conditions on equality, we obtain that(y=y m+1 )∈last(h m ) and(y̸=y m+1 )∈last(h n ). But this contradicts the fact thatlast(h m )∼ A last(h n )(sinceh m ∼ A h n by construction), given thatL(y=y m+1 )⊆A(and given the definition of the relation∼ A on types). Lemma 5.23.(“Least-of-N Values Lemma”) Ifμ N x φ A ∈Var Σ is s.t.[h,μ N x φ A ]̸=⊥ D ,⊤ D , then: 1.(|x| φ A ≤N)∈last(h); 2.|Val h (x φ A )|≤N; 3.[h,μ N x φ A ] =minVal h (x φ A ); i.e., there exists some history h 0 ∈H, satisfying: h 0 ∼ A h;φ∈last(h 0 ); and[h,μ N x φ A ] = [h 0 ,x]≤ D [h ′ ,x]for all[h ′ ,x]∈Val h (x φ A ). Proof.For part 1, from[h,μ N x φ A ]̸=⊥ D we obtain that(μ N x φ A ̸=⊥)∈last(h), so by condition (15) on types we have(|x| φ A ≤N)∈last(h), as desired. For part 2, we use part 1 and Lemma 5.12, to obtain that( W 1≤i≤n x=i N .x φ A )∈last(h ′ )holds for all [h ′ ,x]∈Val h (x φ A ); hence, for every[h ′ ,x]∈Val h (x φ A )there existsi∈1,...,Ns.t.[h ′ ,x] = [h ′ ,i N .x φ A ] = [h,i N .x φ A ](where the last equality follows by the Corollary 5.16 from the fact thatL(i N .x φ A ) =Atogether withh ′ ∼ A h). Thus, we have thatVal h (x φ A )⊆[h,i N .x φ A ]|1≤i≤N, which implies that|Val h (x φ A )|≤N. For part 3, we use the assumption that[h,μ N x φ A ]̸=⊤ D and Lemma 5.20 to obtainVal h (x φ A )̸=/0; i.e., there existsh 1 ∼ A hs.t.φ∈last(h 1 ). Putting this together with the fact that(|x| φ A ≤N)∈last(h 1 )(which follows from part 1 andh 1 ∼ A h, usingL(|x| φ A ≤N) =Aand Lemma 5.11), and applying condition (13) on types (withY:=Var N (x φ A ) =i N .x φ A : 1≤i≤N, while recalling that by definition|x| φ A ≤N:= K φ A (x∈Var N (x φ A )), we conclude that⟨K φ A ⟩(x=μ N x φ A )∈last(h 1 ). By the Diamond Lemma 5.13, there exists someh 0 ∼ A h 1 ∼ A hwithφ,(x=μ N x φ A )∈last(h 0 ), hence[h 0 ,x] = [h 0 ,μ N x φ A ] = [h,μ N x φ A ](with the last equality due toh 0 ∼ A handL(μ N x φ A ) =A, by Lemma 5.19). Finally, to prove that[h,μ N x φ A ] = minVal h (x φ A ), let[h ′ ,x]∈Val h (x φ A ), i.e.,h ′ ∼ A hwithφ∈last(h), and we need to show that[h,μ N x φ A ]≤ D [h ′ ,x]. By condition (12) on types, we have(μ N x φ A ≤x)∈last(h ′ ), hence[h ′ ,μ N x φ A ]≤ D [h ′ ,x]. Since h∼ A h ′ andL(μ N x φ A ) =A, Lemma 5.19 gives us that[h,μ N x φ A ] = [h ′ ,μ N x φ A ]≤ D [h ′ ,x], as desired. 112The Logic of Data Access and Data Exchanges Lemma 5.24.(“Truth Lemma”) For everyφ∈Σand x∈Var Σ , the following hold for all h∈H: 1. h|= M φiffφ∈last(h); 2. h (x) M = [h,x]. Proof.We prove 1.&2.for all expressionsα∈Σ∪Var Σ by induction on sub-expression complexity. (i)Predicative Atoms:φ=Px, withx= (x 1 ,...,x n ). ForP∈Pred\≤, we have the equiva- lences:h|=Pxiffh(x)∈I(P)iff (by the induction hypothesis for claim (2))([h,x 1 ],...,[h,x n ])∈I(P) iff∃h ′ ∈Hs.t.((h, x)≈(h ′ ,x)&(Px)∈last(h ′ ))iff(Px)∈last(h)(by Lemma 5.18). For≤, we have the equivalencies:h|=x≤yiff(h,x)≲(h,y)iff(h,x)⪅(h,y)iff[h,x]≤ D [h,y](by the Path Lemma). (i)Propositional atoms:p∈Pro p Σ . By definition,h|=piffh(p) =⊤ D iffp∈last(h). (i)Basic variables:v∈V Σ . By definition,h(v) M =h (v) = [h,v]. (iv)Boolean Case:φ→ψ. These is trivial, using conditions 1 and 2 on types. (v)K A -modal Case:(K A φ)∈Σ. Fromleft-to-right: assume (towards a contradiction) thath|=K A φ but(K A φ)̸∈last(h). By condition 1 on types, we have(⟨K A ⟩∼φ)∈last(h), and so by the property (**) of quasi-models, there exists a type∆ ′ ∈Ss.t.last(h)∼ A ∆ ′ and(∼φ)∈∆ ′ . Takeh ′ := (h,A,∆ ′ ): this is a well-defined history inH, satisfyingh∼ A h ′ andlast(h ′ ) =∆ ′ . Fromh|=K A φwe infer thath ′ |=φ, and so by the induction hypothesis we haveφ∈last(h ′ ) =∆ ′ , in contradiction to(∼φ)∈∆ ′ . For theright-to-leftdirection: we assume that(K A φ)∈last(h), and we have to prove thath|=K A φ. For this, leth ′ ∈Hbe s.t.h∼ A h ′ , and we need to show thath ′ |=φ. Fromh∼ A h ′ we obtain that last(h)∼ A last(h ′ )(by Lemma 5.11), which together withh|=K A φgives usφ∈last(h ′ )(by Proposition 5.2). Applying the induction hypothesis, we conclude thath ′ |=φ, as desired. (vi)Terms defined by casesφ→x|y. Given(φ→x|y)∈Σ, we haveφ∈Σ, so we have that either φ∈last(h), or else(∼φ)∈last(h). In the first case, we have(φ→x|y=x)∈last(h)(by condition 10 on types), hence[h,φ→x|y] = [h,x]; and on the other hand,φ∈last(h)yieldsh|=φ(by the induction hypothesis for Claim 1), so by definition we haveh (φ→x|y) M =h(x) M , and by the induction hypothesis for Claim 2 we haveh(x) M = [h,x], thus obtainingh(φ→x|y) M =h(x) M = [h,x] = [h,φ→x|y], as desired. The second case is similar: from(∼φ)∈last(h)we get(φ→x|y=y)∈last(h)(by condition 10 on types), hence[h,x| φ ] = [h,y]; and on the other hand,(∼φ)∈last(h)impliesφ̸∈last(h)(by the consistency of types), which by the induction hypothesis for Claim 1 yieldsh̸|=φ, so by definition we haveh (φ→x|y) M =h(y) M , and by the induction hypothesis for Claim 2 we haveh(y) M = [h,y], thus obtainingh(φ→x|y) M =h(y) M = [h,y] = [h,φ→x|y], as desired. (vii)Functional terms F(x)∈Var Σ for somex= (x 1 ,...,x n ). We assume by the induction hypothesis thath(x) M = [h,x], and using the semantics of functional terms and the definition ofI(F)in our history model, we obtainh (F(x)) M = (I(F))(h(x)) = (I(F))[h,x] = [h,F(x)], as desired. (viii)Least-value termsμ N x φ A ∈Var Σ . Using the notationVal h (x φ A ):=[h ′ ,x]∈D:h ′ ∼ A h,φ∈ last(h ′ )and the induction hypothesis for Claims (1) and (2), we haveVal h (x φ A ) =Val(x φ A ) h,M , where Val(x φ A ) h,M :=h ′ (x) M :h ′ ∼ A h,h ′ |= M φis the notation from Section 3. We distinguishthree subcases: Case 1:[h,μ N x φ A ] =⊤ D . By the Trivial-Value Lemma 5.21, we haveVal h (x φ A )⊆ ⊤ D , and hence min N Val h (x φ A ) =⊤ D (since by definition we havemin N /0=min N ⊤ D =⊤ D ). Given this, we obtain thath (μ N x φ A ) M =min N Val(x φ A ) h,M =min N Val h (x φ A ) =⊥ D = [h,μx φ A ], as desired. Case 2:[h,μ N x φ A ] =⊥ D . By the Undefined-Minimum Lemma 5.22, we have either⊥ D ∈Val h (x φ A )or else|Val h (x φ A )|>N.In both cases, we getmin N Val h (x φ A ) =⊥ D by definition, so we obtain h (μ N x φ A ) M =min N Val(x φ A ) h,M =min N Val h (x φ A ) =⊥ D = [h,μ N x φ A ], as desired. Case 3:[h,μ N x φ A ]̸=⊤ D ,⊥ D . By Lemma 5.23, we have both|Val h (x φ A )| ≤Nand[h,μ N x φ A ] = minVal h (x φ A ), i.e.,[h,μ N x φ A ] =min N Val h (x φ A ), thush (μ N x φ A ) M =min N Val(x φ A ) h,M =min N Val h (x φ A ) = [h,μ N x φ A ], as desired. A. Baltag, S. Smets113 Proof of Proposition 5.9: IfSis a quasi-model forφ 0 , then by applying claim 1 of the Truth Lemma 5.24 toφ 0 and to the historyh 0 := (∆ 0 ), we conclude thath 0 |=φ 0 in our history-based modelMabove. 6 Completeness and Decidability Proofs forLDAE In this section we prove Theorem 4.6. 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 expressionsA formulaθinLDAEis said to bereducibleif it is provably equivalent to a ’static’ formula; i.e., if there exists some formulaθ ′ in the static fragmentLDAs.t.⊢θ↔θ ′ is provable inLDAE. A termx∈Var LDAE isreducibleif it is provably equal to a static term; i.e., if there exists some x ′ ∈Var LDA s.t.⊢x=x ′ is provable inLDAE. Finally, an evente= (E,e)isreducibleif all preconditions pre f and all post-conditions of the forme (p)ore(v)are reducible (for allf∈E,p∈Pro pandv∈V). Lemma 6.1.(Replacement of Equivalents)Suppose that⊢φ↔φ ′ ,⊢θ↔θ ′ ,⊢x=x ′ ,⊢y=y ′ and ⊢x i =x ′ i (for all i=1,n) are provable inLDAE. Then the following are also provable inLDAE: 1.⊢φ→x|y=φ→x ′ |y ′ 2.⊢F(x 1 ,...,x n ) =F(x ′ 1 ,...,x ′ n ) 3.⊢μ N x φ A =μ N (x ′ ) φ ′ A 4.⊢Px 1 ...x n ↔Px ′ 1 ...x ′ n 5.⊢(φ→θ)↔(φ ′ →θ ′ ) 6.⊢K A φ↔K A φ ′ 7.⊢[e]φ↔[e]φ ′ 8.⊢e(x) =e(x ′ ) We first prove a preliminary “one-step reduction” result: Lemma 6.2.Letebe any reducible event. Then, for every ’static’ formulaθin LDA and every ’static’ term x∈Var LDA , the formula[e]θand the terme(x)are also reducible. Proof.Sincee= (E,e)is reducible, its preconditionpre e is also reducible. Let us fix some static formula ρs.t.⊢pre e ↔ρis provable inLDAE. We’l prove both claims simultaneously, by induction on sub- expression complexity (-and we’l make liberal use of Lemma 6.1, without explicitly mentioning it): Forθ:=p: sinceeis reducible, there exists some static formulaθ ′ s.t.⊢e (p)↔θ ′ . Using the Change of Facts axiom, we can see that[e]pis provably equivalent toρ→θ ′ . Forθ:=Px 1 ...x n : by the induction hypothesis, for alli=1,nwe have⊢e(x i ) =x ′ i for some static termsx ′ 1 ,...,x ′ n ∈Var LDA . Using also the Indiscernability axiom and the Property Change reduction axiom,[e]θis provably equivalent topre e →Px ′ 1 ...x ′ n , and hence also toρ→Px ′ 1 ...x ′ n . Forθ:=φ→ψis similar: by induction, there exist static formulasφ e andψ e s.t.⊢[e]φ↔φ ′ and ⊢[e]ψ↔ψ ′ are provable. Using the[e]-Distributivity axiom, we obtain⊢[e]θ↔(φ ′ →ψ ′ ). Forθ:=K A φ: by induction, for eachf∈Ethere exists some static formulaφ f s.t.⊢[f]φ↔φ f . Putting this together with the Knowledge Update axiom, we get⊢[e]θ↔ V ρ→K e (A) φ f :f∼ A e). Forx:=v(basic variable): sinceeis reducible, there exists some static termx ′ s.t.⊢e (v) =x ′ . Using this and the Value Change axiom, we obtain that⊢e(x) = (ρ→x ′ |⊤), soe(x)is reducible. Forx:=F(x 1 ,...,x n ): by the induction hypothesis, there exist static termsx ′ 1 ,...,x ′ n s.t.⊢e(x i ) =x ′ i for alli≤n. Using the Functional Change reduction axiom, we obtain⊢e(x) = (ρ→F(x ′ 1 ,...,x ′ n )). Forx:=φ→y|z: by the induction hypothesis, there exist static termsy ′ ,z ′ and static formulaφ ′ , s.t. ⊢e(y) =y ′ ,⊢e(z) =z ′ and⊢[e]φ↔φ ′ are provable. Using these, as well as the Case Change reduction axiom, we obtain⊢e(x) = (φ ′ →y ′ |z ′ ), and soe(x)is reducible. Forx:=μ N y φ A : first note that by definition, the reducibility ofe= (E,e)implies the reducibility of allf= (E,f)withf∈E. By the induction hypothesis and Proposition 4.5, for everyf∈Ethere exist a 114The Logic of Data Access and Data Exchanges static formulaφ f and a static termy f , s.t.⊢⟨f⟩φ↔φ f and⊢f(y) =y f . Thus, if we put η:=n N (y f ) φ f f (A) :f∼ A e,n≤N ♢ ≤N, then⊢η↔Val N e (x A φ) ♢ ≤Nis provable inLDAE. Using the Min. Val. Change axiom,e(μ N y φ A )is provably equal toρ→ η→minμ N (y f ) φ f f(A) :f∼ A e|⊥ . Using this, we can establish our full reduction result: Lemma 6.3.(Co-expressivity ofLDAEandLDA)All expressions (formulas, terms and events)αof LDAE are reducible. As a consequence, LDAE and LDA have the same expressive power. Proof.Induction on the subexpression-complexity of the expressionα. The base casesα:=p∈Pro p andα:=v∈Vare trivial. The casesα:=φ→x|y,α:=F( x),α:=μ N x φ A ,α:=P x,α:=φ→θand α:=K A φare straightforward: use the induction hypothesis and parts 1-6 of Lemma 6.1. Forα:= [e]φ: by induction,eandφare reducible, so there exists staticφ ′ s.t.⊢φ↔φ ′ . By Lemma 6.1.7,⊢α↔[e]φ ′ , and by Lemma 6.2[e]φ ′ is reducible (sinceeis reducible andφ ′ is static), so ⊢[e]φ ′ ↔φ ′ for some staticφ ′ . Using transitivity of equivalence, we get⊢α↔φ ′ , soαis reducible. Forα:=e(x): by induction,eandxare reducible, so there exists a static termx ′ s.t.⊢x=x ′ . By Lemma 6.1.8, we have⊢α=e(x ′ ), and by Lemma 6.2e(x ′ )is reducible (sinceeis reducible andx ′ is static), so⊢e(x ′ ) =x ′ for some static termx ′ . Using transitivity of equality, we obtain⊢α=x ′ . Finally, the caseα:=e= (E,e)is straightforward: for allf∈E,p∈Pro pandv∈V, the precondi- tionspre f and postconditionsf (p)andf(v)are<ein the subexpression complexity order, so they are all reducible (by the induction hypothesis), and henceeis also reducible (by definition). Proof of Theorem 4.6: Completeness follows immediately from Lemma 6.3, the soundness ofLDAE, and the completeness of the systemLDA(Theorem 4.2); decidability follows from the decidability of the static logicLDA(Theorem 4.2) and the co-expressivity ofLDAandLDAE(Lemma 6.3). 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 operatorsC A φ, but pre-encoding their dynamics requires a generalization to polyadic conditionalsC e A φ as in [11]. We leave this for a journal version, where we also plan to explore the relationships of our formalism with the Logic of Functional Dependence [13] and Graded (Multi)Modal Logic. Our axioms are somewhat complicated due to the fact that we didnotsucceed to prove FMP (Finite Model Property) for our logics. This would have allowed us to replace cutoff-minimizationμ N x φ A by plain minimizationmin x φ A (over allA-possiblex-values givenφ), which would greatly simplify our axioms. On the other hand, wedon’thave a counterexample to FMP, so this issue is still an open question. References [1] Thomas Agotnes & Yi N. Wang (2017):Resolving Distributed Knowledge.Artificial Intelligence252, p. 1–21, doi:10.1016/j.artint.2017.07.002. [2] Alexandru Baltag (2010):Presentation: “What is DEL good for?”. In:ESSLI Workshop on ‘Logic, Ra- tionality and Intelligent Interaction’ (organized by J. van Benthem and E. Pacuit). Available athttps: //cs.stanford.edu/~epacuit/lograt/wkshp-esslli2010.html. A. Baltag, S. Smets115 [3] Alexandru Baltag (2016):To Know is to Know the Value of a Variable. In:Advances in Modal Logic 2016, 11, College Publications, p. 135–155. ISBN:978-1-84890-201-5. [4] Alexandru Baltag, Rachel Boddy & Sonja Smets (2018):Group Knowledge in Interrogative Epistemology. In:Outstanding Contributions to Logic, 12, Springer, p. 131–164, doi:10.1007/978-3-319-62864-6_5. [5] Alexandru Baltag, Lawrence Moss & Slawomir Solecki (1998):The Logic of Public Announcements, Com- mon Knowledge, and Private Suspicions. In:Proceedings TARK 98, Morgan Kaufmann, p. 43–56. [6] Alexandru Baltag, Lawrence Moss & Slawomir Solecki (2023):Logics for epistemic actions: completeness, decidability, expressivity.Logics1(2), p. 97–147, doi:10.3390/logics1020006. [7] Alexandru Baltag & Lawrence S. Moss (2004):Logics for Epistemic Programs.Synthese139(2), p. 165– 224, doi:10.1023/B:SYNT.0000024912.56773.5e. [8] Alexandru Baltag, Lawrence S. Moss & Hans van Ditmarsch (2008):Epistemic Logic and Information Up- date. In P. Adriaans & J. van Benthem, editors:Philosophy of Information, part of series: Handbook of the Philosophy of Science, 8, Elsevier, p. 361–465, doi:10.1016/C2009-0-16481-4. [9] Alexandru Baltag & Bryan Renne (2016):Dynamic Epistemic Logic. In Edward N. Zalta, editor:The Stanford Encyclopedia of Philosophy, Winter 2016 edition, Metaphysics Research Lab, Stanford University. Available athttps://plato.stanford.edu/archives/win2016/entries/dynamic-epistemic/. [10] Alexandru Baltag & Sonja Smets (2020):Learning what Others Know. In L. Kovacs & E. Albert, editors: LPAR23 proceedings, EPiC Series in Computing, 73, p. 90–110, doi:10.48550/arXiv.2109.07255. [11] Alexandru Baltag & Sonja Smets (2024):Logics for Data Exchange and Communication. In:Advances in Modal Logic 2024, 15, College Publications, p. 147–169. ISBN:978-1-84890-467-5. [12] Alexandru Baltag & Sonja Smets (2025):Group Knowledge of Hypothetical Values. In:Electronic Proceed- ings in Theoretical Computer Science (TARK 2025), 437, p. 135–154, doi:10.4204/EPTCS.437.15. [13] Alexandru Baltag & Johan van Benthem (2021):A Simple Logic of Functional Dependence.Journal of Philosophical logic50, p. 939–1005, doi:10.1007/s10992-020-09588-z. [14] Johan van Benthem & ̧Stefan Minic ̆ a (2009):Toward a Dynamic Logic of Questions. In:LORI 2009 Proceed- ings, Lecture Notes in Computer Science, 5834, Springer, p. 27–41, doi:10.1007/978-3-642-04893-7_3. [15] Rachel Boddy (2014):Epistemic Issues and Group Knowledge. Master of logic thesis, mol-2014-03, Uni- versity of Amsterdam. Available athttps://eprints.illc.uva.nl/id/eprint/921/. [16] Yifeng Ding (2016):The axiomatization and complexity of Knowing-What-Logic on model class K, Epistemic Logic with Functional Dependency Operator.arXiv 1609.07684, doi:10.48550/arXiv.1609.07684. [17] Hans van Ditmarsch, Wiebe van der Hoek & Barteld Kooi (2008):Dynamic Epistemic Logic. 337, Springer, doi:10.1007/978-1-4020-5839-4. [18] Jan van Eijck, Malvin Gattinger & Yanjing Wang (2017):Knowing Values and Public Inspection. In:Lecture Notes in Computer Science, 10119, Springer, p. 77–90, doi:10.1007/978-3-662-54069-5_7. [19] Roosmarijn Goldbach (2015):Modelling Democratic Deliberation. Master of logic thesis, mol-2015-05, University of Amsterdam. Available athttps://eprints.illc.uva.nl/id/eprint/946/. [20] Tao Gu & Yanjing Wang (2016):“Knowing value” logic as a normal modal logic. In:Advances in Modal Logic, 11, College Pub., p. 362–381, doi:10.48550/arXiv.1604.08709. ISBN:978-1-84890-201-5. [21] Bo Hong (2023):Knowing the Value of a Predicate. In:Proceedings of LORI 2023, Lecture Notes in Computer Science, 14329, p. 149–166, doi:10.1007/978-3-031-45558-2_12. [22] Jan Plaza:Logics of Public Communication.Synthese158, p. 165–179, doi:10.1007/s11229-007-9168-7. Republication of J. Plaza (1989), Proceedings 4th International Symposium on Methodologies for Intelligent Systems, p.201-216. [23] Johan van Benthem (2011):Logical Dynamics of Information and Interaction. Cambridge University Press, UK, doi:10.1017/CBO9780511974533. 116The Logic of Data Access and Data Exchanges [24] Johan van Benthem & ̧Stefan Minic ̆ a (2012):Toward a Dynamic Logic of Questions.Journal of Philosophical Logic41, p. 633–669, doi:10.1007/s10992-012-9233-7. [25] Yanjing Wang (2018):Beyond Knowing That: A New Generation of Epistemic Logics. In:Outstanding Contributions to Logic, 12, Springer, p. 499–533, doi:10.1007/978-3-319-62864-6_21. [26] Yanjing Wang & Jie Fan (2013):Knowing that, Knowing what, and Public Communication: Public An- nouncement Logic with Kv Operators. In:Proceedings of IJCAI 2013, AAAI Press, p. 1147–1154, doi:10.5555/2540128.2540293. [27] Yanjing Wang & Jie Fan (2014):Conditionally knowing what. In:Advances in Modal Logic, 10, College Publications, p. 569–587. ISBN:978-1-84890-151-3.