The Modal Logic of Stepwise Removal

TL;DR

This paper introduces and analyzes the modal logic MLSR, which models stepwise removal of objects, exploring its expressive power, axiomatization, and computational complexity, revealing undecidability in satisfiability and PSPACE-completeness in model-checking.

Contribution

It provides the first formal analysis of the logic of stepwise removal, including axiomatization, bisimulation characterization, and complexity results.

Findings

Model-checking for MLSR is PSPACE-complete.

Satisfiability for MLSR is undecidable.

The logic's expressive power increases with the removal modality.

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 transformations and logics of freely chosen graph changes that get registered in a growing memory. After introducing this logic ($\textsf{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. Next, we show that model-checking for $\textsf{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.