  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.
