Group Knowledge of Hypothetical Values
Alexandru Baltag, Sonja Smets
TL;DR
This paper develops DLKV, a dynamic epistemic logic for knowledge of variable values under semi-public data-exchange events. It augments standard knowledge with hypothetical values $x_A^\varphi$ and group/conditional operators like $K_A x$, $C_{\mathfrak A}^\theta$, and their reductions, and provides complete axiomatizations for static and dynamic fragments. The authors prove completeness and decidability by constructing finite quasi-models for the static logic and by showing co-expressivity with the static fragment for the dynamic logic, using reduction lemmas. They illustrate the framework with a numbers-game puzzle to demonstrate complex knowledge propagation and common-knowledge properties. The work lays a foundation for formal reasoning about data sharing and knowledge of data values in multi-agent systems, with plans to extend to arbitrary data-exchange events.
Abstract
In recent years, epistemic logics have been extended with operators K_ax for knowledge of (the value of) a variable x (by an agent a). We study dynamic versions of these logics, enriched with modalities for semi-public data-exchange events (e.g., public announcements, data-sharing within a subgroup, or changing the value of a variable). To obtain a complete axiomatization of data-exchange events, in the presence of equality x = y and K_ax, one needs to extend the logic further: first, with an operator for distributed knowledge K_Ax of the value (by a group of agents A); next, with a conditional version of this: distributed knowledge K^P_A x (of the value by a group) given some hypothetical condition (expressed by some proposition P); then, with definite descriptions x^P_A , denoting the 'hypothetical' value of x according to A's (distributed) knowledge given condition P. In order to deal with common knowledge in the presence of semi-public data exchanges, we also need to add a novel conditional version of the recent concept of common distributed knowledge. We investigate the resulting logic, giving examples and presenting a complete axiomatization and a decidability proof.