A small workshop on (dynamic) epistemic logic

Oct 18 (Sun), Room 3109, Department of Philosophy, Peking University

Confirmed speakers (alphabetically):

Malvin Gattinger (University of Amsterdam), Hongyi Wang (Peking University), Yu Wei (East China Normal University), Yuchen Wu (Hebei University)

Organizers：Yanjing Wang, Rujing Wang

Tentative program:

9:00-9:45 Malvin Gattinger: Symbolic Epistemic Model Checking for DEL with S5, K and
S4, now what about know-wh?

9:45-10:30 Hongyi Wang: Knowing Value Logic with Background Theories

10:30-10:45 break

10:45-11:30 Yu Wei: Knowing who in groups: A murder, a robot, and a dog

11:30-12:15 Yuchen Wu: On the Axiomatization of Knowing-Value Logic with De Re Dynamics

12:15-12:30 Discussions

Lunch @ Shaoyuan Resturant

---

Abstracts:

Symbolic Epistemic Model Checking for DEL with S5, K and
S4, now what about know-wh?

Malvin Gattinger
Symbolic Model Checking is a collection of techniques to tackle the state explosion problems: Kripke models are often exponentially large even if their informational content is small. Symbolic representation thus tries to encode them using less memory while still allowing us to evaluate formulas on that encoding. We have theoretical frameworks and implementations for symbolic model checking of standard DEL, including S5 and K. Recently this framework has been generalized to also cover S4
and topological epistemic models for evidence-based (group) belief and knowledge. What has not been studied systematically is how these techniques can be applied to the various knowing-wh logics. In this talk I will summarize the existing framework and then speculate about new methods for the knowing-wh logics.

Knowing Value Logic with Background Theories

Hongyi Wang

Knowing value logic has a close and natural connection with mathematical theories such as arithmetic, which is evident in the classic “sum and product” puzzle. Motivated by this connection, we extend knowing value logic with a first-order signature containing rigid function, predicate, and constant symbols. This allows us to formalize knowing the value of a term. For a universal first-order theory T in this signature, we consider two modal semantics. The first ranges over Kripke models based on arbitrary first-order structures satisfying T. The second ranges over models based on a fixed structure whose universal theory is axiomatized by T. We give a uniform axiomatization and prove strong completeness for the first semantics. For the fixed-structure semantics, a finite-world model property yields weak completeness, and we characterize exactly when strong completeness holds. Finally, we briefly discuss the extension of this study to epistemic logic with assignment operators, a setting that is more complicated. Overall, this approach provides a novel framework for combining philosophical logic with background mathematical theories.

Knowing who in groups: A murder, a robot, and a dog

Yu Wei

Abstract: Recent years witnessed a growing interest in formalizing group knowledge with intensional groups whose members may not be known explicitly. In this work, we propose a logical framework where various de re/de dicto group knowledge can be expressed, e.g., one knows all the logicians coming to the workshop know that modal logic S4 is decidable, without knowing who will come to the workshop. The framework is a group knowledge extension of the quantifier-free term-modal logic with the second-order assignment operator that plays an important role in capturing de re group knowledge. Despite the technical complications introduced by the second-order variables and their assignments, we give a sound and strongly complete axiomatization of the logic over S5 models with a constant domain by applying a step-by-step Henkin construction of the canonical model. (joint work with Yanjing Wang)

On the Axiomatization of Knowing-Value Logic with De Re Dynamics

Yuchen Wu

Standard epistemic logic provides a well-established account of de dicto knowledge, or “knowing that”. Its de re counterpart, “knowing what”, has also received considerable attention in recent years. A similar move from “announcing that” to “announcing what” leads to public inspection: the formula [c]φ says that φ holds after the actual value of c is publicly revealed. However, capturing the interaction of public inspection with other operators is difficult. The operator cannot in general be eliminated by reduction axioms in the underlying static language, and the usual no-miracles principle is invalid for it. Previous approaches have either focused on restricted fragments or encoded value announcements within more expressive languages.

In this talk, we present a non-reduction method for treating these interactions directly. We first resolve the axiomatization problem for PILKvʳ, which combines propositional knowledge, conditional knowing value, and public inspection. We give sound and complete axiomatizations over S5 frames, and explain the intuitions behind several of the axioms. Inspired by the work of Yanjing Wang and his collaborators, we introduce an equivalent auxiliary semantics in which public inspections are represented by labelled state transitions, allowing [c] to be interpreted as an ordinary modal operator. We then combine PILKvʳ with public announcement logic (PAL) . We give sound and complete axiomatizations of versions with conditional and unconditional knowing-value operators, and show that these versions are equally expressive. This yields a single framework in which “knowing that”, “knowing what”, “announcing that”, and “announcing what” are represented directly and their complex interactions can be studied together.

Finally, we discuss how this method might extend to de re event models, covering semi-public and private value announcements, changes in the values of names. We also discuss other possible extensions.