A New Look at the Modal Logic of Stepwise Removal
摘要
This article is a follow-up study on the modal logic of stepwise removal of objects, MLSR, which was first introduced by van Benthem et al. [13]. We recapitulate the main results from [13] and also provide some new results. After introducing 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 in a hybrid language enriched with nominals and public announcement operators. Next, we show that model-checking for MLSR is PSPACE-complete, that MLSR lacks the finite model property, and that its satisfiability problem is undecidable—even when we forbid the nesting of removal operators by restricting the removal operator to formulas in the basic modal language. Then, we consider an issue of fine-structure: the expressive power gained by adding the stepwise removal modality to various fragments of first-order logic. Lastly, to conclude our investigation of the complexity threshold from decidable to undecidable, we propose a decidable protocol variant of MLSR.