The Modal Logic of Stepwise Removal
Johan van Benthem, Krzysztof Mierzewski, Francesca Zaffora Blando

Abstract:
We investigate the modal logic of stepwise removal of objects, both for its intrinsic interest as a logic of quantification without replacement, and as a pilot study to better understand the complexity jumps between dynamic epistemic logics of model trans- formations and logics of freely chosen graph changes that get registered in a growing memory. After introducing this logic (MLSR) and its corresponding removal modality, we analyze its expressive power and prove a bisimulation characterization theorem. We then provide a complete Hilbert-style axiomatization for the logic of stepwise removal in a hybrid language enriched with nominals and public announcement operators. The new method employed here may well work for a wide range of modal logics of graph change. Next, we show that model-checking for MLSR is PSPACE-complete, while its satisfiability problem is undecidable. Lastly, we consider an issue of fine-structure: the expressive power gained by adding the stepwise removal modality to fragments of first-order logic.