A Modal Logic of Definable Link Deletion
摘要
In this chapter, we develop a game played on graphs that can model a large range of social interactions with obstructive actions that keep changing the interaction environment, and provide a matching logic to reason about it, where links in models can be removed according to some explicit definitions. With respect to the logic, we first present the details of the logical design and offer some interesting validities, and then define suitable notions of first-order translation and bisimulations for the logic, which together lead to a characterization theorem for the expressive power of the logic proposed. Also, we relate our logic to hybrid logic, compare their expressiveness, and discuss the axiomatization of our logic in the extended setting with hybrid formulas, using the techniques of ‘recursion axioms’ developed for dynamic-epistemic logics. Finally, we show the inherent complexity of the logic, by proving the undecidability of the satisfiability problem for our logic.