A Propositional Dynamic Logic for Instantial Neighborhood Semantics
Johan van Benthem, Nick Bezhanishvili, Sebastian Enqvist · Studia Logica · 2018
We propose a new perspective on logics of computation by combining instantial neighborhood logic $$\mathsf {INL}$$ with bisimulation safe operations adapted from $$\mathsf {PDL}$$ . $$\mathsf {INL}$$ is a recent modal logic, based on an extended neighborhood semantics which permits quantification over individual neighborhoods plus their contents. This system has a natural interpretation as a logic of computation in open systems. Motivated by this interpretation, we show that a number of familiar program constructors can be adapted to instantial neighborhood semantics to preserve invariance for instantial neighborhood bisimulations, the appropriate bisimulation concept for $$\mathsf {INL}$$ . We also prove that our extended logic $$\mathsf {IPDL}$$ is a conservative extension of dual-free game logic, and its semantics generalizes the monotone neighborhood semantics of game logic. Finally, we provide a sound and complete system of axioms for $$\mathsf {IPDL}$$ , and establish its finite model property and decidability.