# The Modal Logic of Stepwise Removal

arXiv: https://arxiv.org/abs/2103.05117 · HTML: https://mlsanity.com/paper/2103.05117/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 8 Mar 2021.

## Built on by (most cited first, 2 of 2)

- [Permissible Knowledge Pooling](https://mlsanity.com/paper/2404.03418/) (2024)
- [Interleaving Logic and Counting](https://mlsanity.com/paper/2507.05219/) (2025)

## Abstract (arXiv)

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 (textsfMLSR) 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 textsfMLSR 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.