The Modal Logic of Stepwise Removal

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.


Model change and quantification
Logical systems describing model change come up when reasoning about forms of semantic interpretation that affect a current model, varieties of information update, or more general actions changing a local environment. A typical feature of such systems is the use of dynamic modalities that, when evaluated in a current model M, look at what is true in other models N , related to M via some relevant cross-model relation. These dynamic logics come in a wide range of expressive power and computational complexity [Aucher et al., 2018]. Our aim in this small pilot study is to explore a significant border line, where the complexity of the satisfiability problem jumps from decidable to undecidable. In the process, we highlight some further issues, as well as some new proof techniques, as will be explained below.

Dynamic epistemic logics of information update.
Here is one recent genre of dynamic logics that can describe model change. When modeling the effects of new information, a natural format changes a current epistemic model to a new one, suitably modified. For instance, an event !ϕ of reliable public information that ϕ is the case changes a current pointed model (M, s) to the definable sub-model (M|ϕ, s), whose domain is the set of all points in M that satisfy ϕ. Likewise, an event where all agents publicly lose all uncertainty about ϕ takes (M, s) to a model (M\ϕ, s), where the domain stays the same, but the epistemic accessibility relation ∼ of M gets replaced by the refinement s ∼ ϕ t: i.e., s ∼ t and, also, M, t |= ϕ if and only if M, s |= ϕ. These and many other model transformations F have matching modalities [F ]ψ in dynamic epistemic logics, whose key axioms for [F ]ψ give a recursive analysis of when the postconditions ψ hold in terms of what was true before the F -update (see the survey by van Benthem [2011]). Dynamic epistemic logics are usually decidable if their underlying static logics are: the recursion axioms reduce out the dynamic modalities, at least on full standard universes of epistemic models.

Sabotage-style graph logics.
Here is a second natural genre of modal logics for describing model change. In the sabotage game of van Benthem [2005], arbitrary links in a graph are cut, one by one, by a Demon opposing a Traveler, who, in turn, moves across the graph along still available links. The winning positions of the Demon and the Traveler can be analyzed using standard modalities, together with additional modalities describing what holds in a pointed model after one link has been removed from the current accessibility relation. However, validity in modal logics for various graph games of this sort can be undecidable, and the resulting model theory is quite complex (see [Aucher et al., 2018] and [van Benthem and Liu, 2020]). This difference in complexity calls for an explanation. The present paper locates its source in the contrast between, on the one hand, the simultaneous removal of points or links in dynamic epistemic logics and, on the other, the stepwise modifications captured by logics for sabotage and related graph games. In doing so, we explore the border between two system designs: dynamic epistemic logics of graph change that reduce effectively to a decidable static base language-and, hence, to what is true in the initial model, which already 'pre-encodes' the effects of changes-and, on the other hand, undecidable sabotagetype logics of graph change operations, whose effects are not pre-encoded in the original model, but rather depend on a growing 'memory' of previous changes.
To make this concrete, here is a simplest dynamic epistemic logic turned 'stepwise'. For simplicity, we focus on point deletion, rather than link deletion.
This system of what may be called stepwise point removal (MLSR) will be studied here as an intermediate case between the simplest dynamic epistemic logic of public announcements, where all points satisfying ϕ are removed simultaneously during an update, and a simple sabotage modal logic for stepwise graph change.
Quantification without replacement. The language introduced here has various further interpretations. For instance, it can be seen as a medium for describing 'interventions' that minimally change some given model to make some specified new properties true [Renardel de Lavalette, 2001]. But the system has an even more general logical motivation, which is not tied to information updates or any other specific application.
Consider the evaluation of restricted existential quantifiers ∃x ϕ(x) · ψ(x) in first-order logic (FOL). One searches for an object d satisfying ϕ and then checks whether d also satisfies ψ. In this second stage, the model has not changed: the witness d is still in the domain and it influences the evaluation of ψ. Call this process "quantification with replacement". Now, it has been claimed [Hintikka and Sandu, 1997] that quantifiers in natural language can also behave differently: witness, for instance, the natural sense in which the distrust in "John distrusted everyone" does not apply to John himself. Even though this may be an idiosyncrasy of natural language, it clearly makes sense to explore quantification without replacement as a model for evaluation procedures that change domains [Gabbay, 2013]: ∃x(ϕ|ψ) says that there is an object (or, in a natural polyadic version ∃x(ϕ|ψ), a tuple of objects) that satisfies ϕ in the current model M, while ψ holds in the sub-model M − {s} where that object (or all those objects) has been removed.
This quantifier form is clearly definable in FOL with identity, but, taken by itself, it suggests its own model theory and proof theory. Moreover, as we shall see, adding quantification without replacement to weaker fragments of the first-order language, such as monadic predicate logic or basic modal logic, produces much less simple effects.
The system MLSR. The system MLSR of stepwise object removal studied in this paper provides a simple modal setting for bringing all of this out. Its syntax is that of the basic modal language with proposition letters, ¬, ∨, , plus the additional modality −ϕ ψ, whose semantics was given above (Definition 1.1). Occasionally, we will also use this language extended with a "public announcement", or relativization, modality !ϕ ψ describing what is true in restrictions to definable subdomains: with M|ϕ the submodel of M consisting of all and only the points in M where ϕ is true.
Outline of the paper. In this paper, we study the essential features of this modal system. In §2, we analyze the expressive power of MLSR by providing a first-order translation and a semantic characterization in terms of bisimulation invariance. This mainly requires straightforward adaptations of known techniques. §3 and §4 present a complete axiomatization for MLSR, based on a new idea of mixing standard relativization with stepwise removal, which may very well be applicable to many other logics of graph change, for which Hilbert-style axiomatizations have long been an open problem. In §5, we first analyze the computational complexity of model checking for MLSR, which turns out to be PSPACEcomplete. This analysis uses a reduction technique from Löding and Rohde [2003] which deserves to be better known in modal logic. Next, we prove that the satisfiability problem for MLSR is undecidable using a tiling argument familiar from the modal logic literature [Marx, 2006;Areces et al., 2015]. In §6, we then raise a more general definability issue: namely, what the addition of quantification without replacement does to various fragments of first-order logic. In particular, we show that, when added to monadic first-order logic, the modality −ϕ ψ essentially allows us to count, boosting the expressive power of monadic first-order logic to that of monadic first-order logic with identity.
In summary, we locate the threshold of complexity in the stepwise character of the modality for point removal, leading to the need for a computational device for maintaining a memory of deleted points, whose complexity equals that of arbitrary tiling problems and computations of Turing machines. In the process, we also raise new types of questions about modal logics of graph change, and we advertise and introduce some techniques that deserve to be better known among modal logicians.

Basics of expressive power
We start with the formal language to be used in most of this paper. 1 Definition 2.1. The syntax of MLSR is given by with p ∈ PROP. Dual modal operators , [−ϕ] are defined as usual.
Some definable notions. The language of MLSR can define various modal operators from hybrid logic [Areces and ten Cate, 2006] that go beyond the basic modal language. For instance, the difference modality Dϕ ('ϕ is true at some different point') can be defined as −ϕ ⊤, and this, in turn, allows to define the existential modality Eϕ as ϕ ∨ Dϕ. MLSR can also count all finite cardinalities, using suitably iterated formulas which express that a model has at least k objects different from the current point of evaluation. In addition, MLSR can define quite a few finite relational graphs up to isomorphism. For instance, let ρ 2 be the formula defining domain size 2, and let U be the universal modality (i.e., Uϕ = ϕ ∧ [−¬ϕ]⊥). The following observation requires an easy exercise in understanding what our language can express.
However, not every finite graph is definable, as we shall soon see.

SR-bisimulation.
The semantic invariance matching this language is as follows.
1 This language will be extended slightly with nominals in §3 and §4, which deal with proof systems. Note that this definition imposes some minimal closure conditions on the set of models involved in the above clauses that are easy to spell out. The following property is proved by a standard induction on formulas. Now we can give an example of two finite graphs that are not definable up to isomorphism and, in line with this, a first-order formula that is not in MLSR.

Fact 2.5. ∀y(Rxy ∨ Ryx) is not MLSR-definable.
Proof. Consider the model M consisting of two isolated reflexive points and the model N consisting of two points with the universal relation, plus all their submodels. By checking all clauses, one sees that the universal relation Z between all pairs (M, x) and (N , y) plus all links between the 1-point pointed sub-models of M and N is an SR-bisimulation. But, clearly, connectedness holds in N , but not in M. This new logical system still lies inside standard first-order logic.
Fact 2.6. There is an effective meaning-preserving translation from MLSR into FOL.
Proof. We define the following compositional translation τ (ϕ, y, X) from MLSR-formulas ϕ to first-order formulas, where y is a free variable and X a finite set of variables: τ (p, y, X) = P y, τ (¬ϕ, y, X) = ¬τ (ϕ, y, X), τ (ϕ ∨ ψ, y, X) = τ (ϕ, y, X) ∨ τ (ψ, y, X), Remark 2.7. The set X in this translation serves as a finite memory storing the points that have already been deleted. This is an essential difference with first-order translations for standard modal languages, which usually lie inside fixed finite-variable fragments.
A simple adaptation of a well-known model-theoretic argument for standard modal logic (cf. [Blackburn et al., 2011]) yields the following result.
Theorem 2.8. The following assertions are equivalent for all first-order formulas ϕ(x) in the signature of our models, with one free variable: Proof. We merely outline the points that need attention in the non-trivial direction from (a) to (b). Let SR denote the MLSR-fragment of first-order logic (that is, all first-order formulas equivalent to translations of MLSR formulas via the translation τ from Fact 2.6). As usual, one shows that ϕ(x) is a semantic consequence of the set C x (ϕ) of its SRconsequences and then applies Compactness to get an SR-equivalent. We thus need to show that C x (ϕ) |= ϕ(x). Suppose M, s |= C x (ϕ). A standard compactness argument shows that there is a model N and t ∈ N such that (M, s) and (N , t) are SR-equivalent, while N , t |= ϕ(x). These models are then extended to ω-saturated elementary extensions (M + , s) and (N + , t). We use first-order saturation allowing finite sets of parameters consisting of designated objects in the models; in turn, the finitely satisfiable sets of first-order formulas to be saturated can have a finite set of free variables (not just one, as in the argument for basic modal logic). This is needed for the saturation argument to follow. Now we define a relation Z between pointed models (M + −D, u) and (N + −E, v), with E, D of the same finite size, which holds if (M + − D, u) and (N + − E, v) satisfy the same SR-formulas. Using saturation, it can be shown that Z is an SR-bisimulation, where the argument for the modality ϕ is standard, while the one for −ϕ ψ in terms of removing single objects goes as follows. Take which means that and this formula is in SR (it is equivalent to the translation of a −ϕ ψ formula). This means that the formula also holds in (N + − E, v). Thus, every finite subset of p(x, y) is satisfiable in (N + −E, v) (interpreting x as v). In other words, expanding the language with a new constant symbol c, the 1-type p(c, y) is finitely satisfiable in (N + − E, v) (fixing the interpretation of c as v). Then, by saturation, the type is realized in (N + − E, v): we can thus find an object in N + −E matching the given w, as required for an SR-bisimulation.
Remark 2.9. The first-order translation for MLSR can also be phrased in terms of the hybrid language H(E, ↓), [Areces and ten Cate, 2006]. The key translation clause here reads, for each formula of the form −ϕ ψ and sequence of nominals n = (n 1 , ..., n ℓ ): Further connections of MLSR with hybrid logics will be discussed in §7 below.

Axiomatization
Thanks to the first-order translation, the valid formulas of MLSR are effectively axiomatizable. But more immediate information comes from explicit modal laws. For instance, the removal modality −ϕ ψ distributes over disjunction in both of its arguments: Fact 3.1. The following formulas are both valid: To obtain an explicit modal axiomatization, we extend the language of MLSR with a countable set NOM of nominals, each standing for either a unique point in the model, or not denoting at all (this small technical deviation from hybrid logic will be helpful later on.) We also add standard public announcement modalities !ϕ ψ from dynamic epistemic logic, whose interpretation was given in §1. This will turn out to be useful, even though the axiom system to follow features no recursion axioms in the usual dynamic epistemic style for the removal modality. For simplicity, we retain the name MLSR for this logic.

Remark 3.2. There seem to be no modal recursion axioms inverting the operator order for combinations
This feature of the modal language may be contrasted with how first-order logic augmented with an explicit syntactic operator of relativization would write this recursion: We now extend the language of Definition 2.1 with nominals, public announcement operators, as well as the existential modality.

Definition 3.3. MLSR with nominals (for short still to be called MLSR) has the syntax
Note that it is not necessary to add the @ n operator from hybrid logic as a primitive symbol, for it can be defined using the universal modality: in our setting with (possibly non-referring) nominals, @ n ϕ is simply a shorthand for U(n → ϕ). 2 The following proof system may look somewhat complex, but its components just follow the formal syntax just introduced.
Definition 3.4. The logic MLSR (see Figure 1) consists of: • the rule of Replacement of Provable Equivalents, 3 • the axioms and rules of classical propositional logic; • the axioms and rules of the minimal normal modal logic for all the universal box modalities of the language (static or dynamic), plus the standard axioms and rules for the global universal modality [Blackburn et al., 2011]; • the Name Rule and the Paste Rule from hybrid logic [Areces and ten Cate, 2006], with the latter slightly adapted to our setting; • the axiom E(n ∧ ϕ) → U(n → ϕ), which we denote by (H); • the usual reduction axioms of public announcement logic PAL for atoms (including nominals), the existential base modality, the global existential modality, and the announcement modality [van Benthem, 2011], 4 as well as the Truth Axiom !⊤ ϕ ↔ ϕ; • the following two principles connecting the stepwise removal modality with the public announcement modality: Fact 3.5. The Mix Axiom is valid, and the Mix Rule is semantically sound.
Remark 3.6. The system MLSR does not include all the usual axioms for the basic hybrid language because nominals can fail to denote in our models after an update. In particular, after the deletion of a state named by n, the formula ¬En holds. Connected to this, the equivalence E(n ∧ ¬ϕ) ↔ ¬E(n ∧ ϕ) underpinning the common hybrid notation @ n is no longer valid. However, the proof principles of MLSR guarantee all the properties of nominals that we need in what follows. In particular, the following useful facts are provable: The System MLSR • The rule of Replacement of Equivalents: Hybrid inference rules: • Axiom for the removal modality: Inference rule for the removal modality: Figure 1: The Hilbert-style proof system for MLSR.
The language of MLSR captures various global properties of our semantics, such as the fact that nominals hold at one state at most. Deriving this shows the Mix Rule at work.
Observation 3.7. The formula n → ¬ −n ⊤ is an MLSR theorem for any n ∈ NOM.
Proof. Take ϕ, ψ = ⊤, σ = ⊥, α = n. Then the antecedent formula in the Mix Rule reads This is derivable in MLSR. Using Replacement of Equivalents, 5 and appealing to (i) a simple analysis of !⊤ E(k ∧ n) using the PAL reduction axioms for E and nominals, and (ii) the implication from !¬k ⊤ to ¬k which is one half of the PAL reduction axiom for ⊤, the antecedent of the above formula derives E(k ∧ ¬k). It then suffices to note that the S5 axioms for quantifiers allow to derive E(k ∧ ¬k) → ⊥.
Therefore, the consequent formula is provable using the Mix Rule: Using the Truth Axiom and the S5 axioms for quantifiers, this is equivalent in MLSR to U(n → ¬ −n ⊤), which implies the desired n → ¬ −n ⊤.
To increase familiarity with the proof system, we explore MLSR a bit further.

Remark 3.8. (a)
Here is a more elaborate derivation showing the interplay of the two dynamic modalities. The premise of the above Mix Rule uses antecedents prefixed by an existential modality. However, we can also derive the following 'bare' variant: To see this, assume the premise. Take a fresh nominal n, and using propositional logic, derive (n∧ !ϕ (E(k∧ α)∧ !¬k ψ)) → σ. Given the facts derived in Remark 3.6, this is equivalent to Here, since n was fresh, the nominal k still satisfies the conditions of the Mix Rule. Therefore, we can conclude E(n∧ !ϕ −α ψ) → (n → σ). From this, using propositional logic, (n∧E(n∧ !ϕ −α ψ)) → σ. Then using Remark 3.6 once more, we get (n ∧ !ϕ −α ψ) → σ, and with propositional logic, n → ( !ϕ −α ψ) → σ). Finally, using the Name Rule of the hybrid logic component of MLSR, the conclusion !ϕ −α ψ → σ follows.
Taking the special case of ϕ = ⊤, and using the Truth Axiom of MLSR (which was not used in the preceding derivations), the Stripped Mix Rule reduces to: MLSR also admits the following simple variant of the Paste Rule: The Basic Paste Rule is derivable by the preceding method, starting with the premise: We now use our observations to derive some simple but useful validities.

the removal modality captures quantifiers).
Proof. (i) This follows since !ϕ α → !ϕ ⊤ is provable by principles of the minimal logic K for the modality !ϕ , while the PAL reduction axiom for the atom ⊤ gives !ϕ ⊤ ↔ ϕ.
(ii) With the Basic Mix Rule in hand, it is straightforward to derive this non-trivial distribution law. We sketch the left-to-right direction, appealing to the Basic Mix Rule with α = ϕ 1 ∨ ϕ 2 and σ = −ϕ 1 ψ ∨ −ϕ 2 ψ. For k a fresh nominal, E(k ∧ (ϕ 1 ∨ ϕ 2 )) ∧ !¬k ψ) provably implies −ϕ 1 ψ ∨ −ϕ 2 ψ: this can be shown using the standard distribution of the E modality over disjunctions, after which the Mix Axiom gives the required result.
(iii) For the left-to-right direction, let k be a fresh nominal not appearing in α. Note that, by the (H) Axiom, The following instance of the Basic Paste Rule then gives us the desired conclusion: For the right-to-left direction, we have to show that −α ⊤ → Eα. Let k be a fresh nominal not appearing in α. Since (E(k ∧ α) ∧ !¬k ⊤) → Eα is clearly derivable, this follows from the instance of the Basic Mix Rule displayed here: Many of the formal proof routines illustrated in this section will be assumed without further explanation in the completeness proof of our next section. The above axiom system, though matching our later completeness proof, may have some redundancies in its formulation. There is more power to the PAL reduction axioms than meets the eye, and the same is true of the Mix Rule.
Remark 3.10. Consider the Truth Axiom, a modest, but useful principle: In public announcement logic PAL with nominals and global modalities, the Truth Axiom is redundant, as all its instances are derivable. This can be shown by a straightforward induction on the formula ϕ. The base cases for atoms (proposition letters, nominals and ⊤), as well as the inductive steps for negations, disjunctions, and the two existential modalities are immediate from the corresponding reduction axioms in PAL.
However, in the setting of MLSR, we must also consider the inductive step for the removal modality. As it happens, one direction presents no difficulties. By the Stripped Mix Rule, to prove !⊤ −α ψ → −α ψ, it suffices to derive, for some fresh nominal k, the implication !⊤ (E(k ∧ α) ∧ !¬k ψ) → −α ψ. And here, distributing the modality !⊤ inside by appealing to the PAL axioms of MLSR, and using the inductive hypothesis that !⊤ α ↔ α is derivable already, the antecedent is provably equivalent to E(k ∧ α) ∧ !¬k ψ, which implies −α ψ by the Mix Axiom.
A similar analysis in the opposite direction would derive −α ψ → !⊤ −α ψ using the earlier Basic Mix Rule. However, showing the validity of that rule involved an appeal to the Truth Axiom, and it is not clear whether we can do without.
We leave finding a more minimal and provably non-redundant presentation of MLSR as an open problem (see also the final point in §4 about the need for the PAL component). Even so, as shown in this section, MLSR is quite a workable proof system, whose finestructure deserves further exploration.

Completeness
We now proceed to prove (strong) completeness of our deductive calculus.
Theorem 4.1. The system MLSR is complete for validity in the given semantics.
Soundness of the given axioms and rules follows from a straightforward inspection. The Henkin-style completeness proof follows standard modal and hybrid lines [Blackburn et al., 2011], but there are some interesting new features that will be highlighted in what follows. We begin with a preliminary definition toward a Lindenbaum Lemma.

Definition 4.2 (Named, Pasted, Mixed). A set of MLSR-formulas Γ is
• named if it contains a nominal; A set Γ of MLSR-formulas will be said to be pasted if it is both -pasted and E-pasted. The technical reason for having two mixing principles instead of one will become clear later on. But it may be noted here already that if a deductively closed set Γ contains some nominal n naming it, then E-mixing implies plain mixing. For, in that case, as was shown in Remark 3.6, modulo Γ, any formula ψ will be provably equivalent to E(n ∧ ψ). Remark 4.3. As will be seen below, the Mix Rule of MLSR supports the preceding 'mixing': i.e., witnessing the removal modality by introducing a new nominal for the point to be removed. As stated, the rule does this only under one-step update modalities !ϕ . But this implies the Mix Rule for arbitrary finite sequences of updates. First, the special case of !⊤ ψ gives the case of single formulas ψ, as the two are equivalent in MLSR. But also, longer sequences of updates are covered, as is easy to see using the PAL axiom !ϕ !ψ α ↔ !(ϕ ∧ [!ϕ]ψ) α compressing two nested update modalities to a single one.
Proof. Naming and pasting work in exactly the same way as in the completeness proof for the basic hybrid logic. As for mixing, given the above observation, we only consider the case of E-mixing. We have to ensure that, throughout the inductive construction, whenever we consistently add a formula of the form E(n ∧ !ϕ −α ψ) to a consistent, named set of formulas Σ, the formula E(n ∧ !ϕ (E(k ∧ α) ∧ !¬k ψ)) is also added to Σ-where k is the first nominal in the enumeration of nominals used in our construction that occurs in neither Σ nor !ϕ −α ψ. Crucially, for such a k, the set Σ ∪ {E(n ∧ !ϕ (E(k ∧ α) ∧ !¬k ψ))} is consistent, given that Σ is consistent. For if not, then for some conjunction σ of formulas from Σ, the implication E(n ∧ !ϕ (E(k ∧ α) ∧ !¬k ψ)) → ¬σ would be provable. But then, by the Mix Rule, the implication E(n ∧ !ϕ −α ψ) → ¬σ is provable from Σ, contradicting our initial assumption that Σ ∪ {E(n ∧ !ϕ −α ψ)} is consistent.
Over this universe, accessibility relations are defined as follows: In this definition, the set Γ is thought of as containing all information about the whole universe W. This includes information about Γ itself, since, by an earlier observation, Γ = ∆ n for any nominal n ∈ Γ, and such nominals exist since Γ is named by our Lindenbaum construction. One could continue the completeness argument in this style, but in what follows we consider all sets introduced here on a par, as 'worlds' or 'states' in a modal model, for which we will use the standard notation w, v, ... 7 We now define an initial structure toward finding a model for our consistent set. • the relations R and R E are, respectively, R and R E restricted to W ; • the valuation V is given by V (p) = {w ∈ W | p ∈ w} for all proposition letters p and, for all nominals n, V (n) = {∆ n } if En ∈ Γ, and V (n) = ∅ otherwise.
Setting the domain to be the equivalence class of Γ under R E ensures that R E is the universal relation in the model. It is also easy to show that the valuation is well-defined for nominals. This construction has some important properties, listed in the next result. • All sets ∆ n are MLSR-MCSs; • If u ∈ W and ϕ ∈ u, then there is an object v ∈ W such that R uv and ϕ ∈ v.
• If u ∈ W and Eϕ ∈ u, then there is some v ∈ W such that R E uv and ϕ ∈ v. 7 The above accessibility relations could also be defined equivalently in a standard modal manner: for any w, v ∈ W, we have R (w, v) if and only if for all ϕ, if ϕ ∈ v then ϕ ∈ w, and similarly for R E .

• All sets ∆ n are mixed in the first sense listed in Definition 4.2.
The proof of all these assertions is by reference to the Pasting and E-Mixing properties of the original set Γ, using principles available in MLSR that were identified earlier.
Next, we define a family of derived structures which capture the effects of finite sequences of updates on the upper Henkin model M. Recall that, given a sequence ϕ = (ϕ 1 , . . . , ϕ k ), the notation !ϕ stands for !ϕ 1 ... !ϕ k .  ϕ) ) if and only if R wv (resp., R E wv) in the upper Henkin model M; Points in the derived Henkin model M : ϕ are sequences (w, ϕ 1 , . . . , ϕ k ), where w is a MCS in the upper Henkin model that contains the pre-condition formula 8 The accessibility relations stay as they were for the initial points of the sequences in the upper Henkin model. Likewise, the valuation for proposition letters at each sequence stays the same as that for its initial point in the upper Henkin model.
These sets record what the upper Henkin model 'claims' is true after the update with ϕ. Our task is to analyze how this matches up with truth in the updated models.
To do so, we first note some useful theorems of MLSR concerning the effects of finite sequences of successive updates. The first of these computes preconditions explicitly: The derivation of (R1) and the following principles of MLSR are obtained by straightforward iteration of the principles of public announcement logic PAL [van Benthem, 2011]. Our second observation analyses when atomic formulas are true after iterated updates: The preceding theorem also applies to nominals. A similar pattern occurs with negations: 9 For conjunctions, it is easy to see that Finally, consider the diamond modality. Here we have: A similar principle holds for global existential modalities of the form Eα. 10 Intuitively, the models M : ϕ are meant to be isomorphic to submodels of M after the sequence of consecutive semantic updates ϕ, but the precise sense in which this is true will become clear in the following key property of the construction of initial and derived Henkin models. 11 Now comes the main point of our construction so far.

Lemma 4.8 (Truth Lemma). For all formulas ψ, finite sequences ϕ and points w,
Proof. The proof is by induction on the formulas ψ. For convenience, when the context is clear, we write w instead of (w, ϕ), reflecting the fact that derived Henkin models represent submodels arising from iterated PAL updates. Also note that, by the earlier definitions, the existence of the state (w, ϕ) in M : ϕ assumes that the precondition pre(ϕ) of the relevant update sequence belongs to w. This fact will be used repeatedly in what follows.
(a) For the equivalence of truth and membership for atoms p, it suffices to observe that p ∈ Φ(M, ϕ, w) iff !ϕ p ∈ w iff (by the above-noted fact (R2)) pre(ϕ) ∧ p ∈ w. But then, by the definition of the valuation in derived Henkin models, this means that p is true at the initial w and all its descendants under update. The same argument applies to nominals.
(c) The inductive step for conjunctions ψ 1 ∧ ψ 2 is straightforward, using the above distribution principle (R4) of !ϕ modalities over conjunctions, as well as the fact that maximally consistent sets decompose conjunctions into components.
(d) Next, we consider the basic modality ψ, relying on the above principle (R5).
(e) The reasoning for the existential modality Eψ is just like the preceding argument.
(f) The analysis for PAL modalities !α ψ proceeds as follows.
First note that, by the inductive hypothesis, the truth of α at any point (v, ϕ) is equivalent to α belonging to Φ (M, ϕ, v). Hence, restricting the model M : ϕ to (M : ϕ)|α in the usual semantic sense yields exactly the derived Henkin model M : (ϕ ⌢ α). 12 We then have the following equivalences: (g) Finally, the MLSR deletion modality −α ψ is analyzed as follows. First consider conjunct (i). By the inductive hypothesis, α ∈ Φ(M, ϕ, v), while also, for our nominal n, we have n ∈ Φ(M, ϕ, v). Therefore, in the upper Henkin model M, !ϕ (n ∧ α) ∈ v. Now, the relation R E is universal in the upper Henkin model, and so, in particular, R E wv, which entails that E !ϕ (n ∧ α) ∈ w. Next, by our earlier observations about provable generalized reduction axioms in MLSR: Together with the fact that pre(ϕ) ∈ w, it follows that !ϕ E(n ∧ α) ∈ w.
Next, consider conjunct (ii) in our initial assumption. It is easy to see that the model (M : ϕ) − {v} equals the updated model (M : ϕ)|¬n, using the fact that each nominal belongs to at most one world in M. Thus (ii) implies that (M : ϕ)|¬n, w |= ψ. Moreover, it can be seen that the latter model in turn equals M : (ϕ ⌢ ¬n). 13 Therefore, we also have M : (ϕ ⌢ ¬n), w |= ψ. But then, by the inductive hypothesis, we have that ψ ∈ Φ(M, ϕ ⌢ ¬n, w), i.e., !ϕ !¬n ψ ∈ w.
It now remains to apply the Mix Axiom. As stated in the definition of the system MLSR, this says that the conjunction E(n ∧ α) ∧ !¬n ψ implies −α ψ. Now in the upper Henkin model, we only have the antecedent for this in the set w under the prefix !ϕ . But then the modalized conclusion !ϕ −α ψ is derivable using the K axioms for the !ϕ modalities, and hence it, too, is in w. In other words, −α ψ ∈ Φ(M, ϕ, w).
This concludes the proof of the Truth Lemma, and thus, the consistent set Γ at the start of the construction has a model. This establishes the completeness of the system MLSR.

Remark 4.9. One way of understanding the mechanics of this modal completeness proof is doing a parallel standard Henkin-style completeness proof for a first-order language with explicit operations of quantification without replacement and definable relativization.
Finally, a natural question is if our expanded language with nominals and PAL modalities is really needed. We leave the existence of a 'pure' axiomatization of MLSR open here. 14

Complexity and undecidability
Having analyzed expressive power and axiomatization, we now turn to matters of computational complexity for the core notions of our system MLSR as defined in §2.

Model checking
We begin by showing that model checking for MLSR is PSPACE-complete. We do so by providing a reduction from the quantified Boolean formula problem (QBF) [Stockmeyer and Meyer, 1973], in the style of Rohde [2005] and Löding and Rohde [2003].
Proof. An upper bound is established as follows. The translation into first-order logic given earlier (Fact 2.6) only has a polynomial size increase, and it is known that model checking for first-order logic is in PSPACE.
The lower bound is demonstrated by a reduction from QBF into model checking for MLSR. Take any QBF formula ϕ: that is, a formula of the form where Q j ∈ {∃, ∀}, and each C i is a disjunction of literals ±x j (here, without loss of generality, we can assume that the quantifiers alternate between ∃ and ∀).
Given such a formula ϕ, we construct a finite pointed model (M ϕ , s) and an MLSR formula γ ϕ such that ϕ is true if and only if (M ϕ , s) |= γ ϕ . The construction will ensure that the model M ϕ and the formula γ ϕ both have a size that grows linearly in the number of quantifiers and clauses of ϕ, which gives the desired reduction from QBF.
To increase intuitive understanding, in what follows the model (M ϕ , s) is constructed so that the truth of ϕ can be captured by a traveling game on the model between two players: Traveler and Demon. The formula ϕ is true if and only if Traveler has a winning strategy in the traveling game on (M ϕ , s), while the MLSR formula γ ϕ states the existence of a winning strategy for Traveler. (M ϕ , s) consists of n + 1 vertically concatenated 'modules': one initial module for the first quantifier in ϕ, one module for each of the remaining n − 1 quantifiers, plus one final verification module. Each of these modules is depicted in Figure  2. More in detail, the construction of M ϕ is as follows: starting with the initial module, we concatenate successive ∀x i -and ∃x j -modules corresponding to the order of quantifiers in ϕ (we treat the top nodes labeled by x j and ¬x j as the end nodes of the previous module). The goal points are those to which the valuation assigns the proposition letter g (as depicted in Figure 2). Once all n quantifier modules have been added, we append the final verification module. For each clause C i , we use a distinct proposition letter c i , which holds at exactly one node in the verification module, called a clause vertex. Each clause vertex c i has an outgoing edge to all and only the duals of literals that make C i true. x j−1 ¬x j−1 g g g g . . .  Now, the traveling game proceeds in the following manner. At the beginning, Traveler is positioned at the starting vertex s. When Demon plays, she deletes a node in the graph. When Traveler plays, she can travel along one of the remaining edges to an adjacent vertex. Traveler wins if she manages to reach a goal point, marked with the proposition letter g. Demon wins otherwise. More in detail, if ϕ starts with ∃, Traveler goes first. If ϕ starts with ∀, Demon goes first: in the first move, she can only delete a vertex marked by p 1 -that is, she can only delete a point adjacent to the starting vertex. From then on, Traveler and Demon alternate their turns, with turns being either traveling one edge further or deleting one node, respectively, where the Demon's second move at each ∀x j -module is restricted to nodes marked with p j (see Figure 2). This continues in this manner until Traveler reaches a node that sees a clause node. At this point, Demon has k − 1 moves, which she must use to delete all but one clause node. Then, we allow Traveler two successive moves (once Demon has restricted her choices to one clause node). Then, Demon and Traveler once again alternate single moves until the game is resolved. See Figure 3 for an example.
The game adequately captures the truth of ϕ: Observation 5.2. Traveler has a winning strategy for the game on (M ϕ , s) if and only if the initial QBF formula ϕ is true.
g g x 2 ¬x 2 g g p 3 p 3 g g x 3 ¬x 3 g g c 2 c 1 c 3 Figure 3: An example. The proposition letter g marks the goal points. Each ∀-module forces Traveler to the literal ±x j point chosen by Demon, while each ∃-module leaves the choice to Traveler. The letters p 1 , ..., p k are level markers that restrict Demon's moves. In the final module, Demon forces Traveler into some clause. For each literal ±x j that makes such clause true, Traveler can then go to the node labeled by dual literal ∓x j above.
Note on game perspectives. While not strictly necessary for the proof of Theorem 4.1, the above traveling game with point removal over the initial structure is independently appealing, and it suggests links with the graph games that motivate sabotage logics and related logics for graph change mentioned in §1 [van Benthem and Liu, 2020]. As a further perspective, the above traveling game is virtually identical to the standard logical evaluation game for the crucial quantified Boolean formula in the above proof. Making these game perspectives precise is left as an open problem here.

Satisfiability
Next, we show that, despite the recursive axiomatizability shown in §3, stepwise removal has a complex theory. The satisfiability problem for the logic MLSR is undecidable, which we establish by a reduction from the tiling problem, a standard technique in modal logic (cf. [Blackburn et al., 2011;Marx, 2006], to which we refer for details).
Theorem 5.3. The satisfiability problem for MLSR with two binary accessibility relations R u and R r is undecidable.
Proof. Let T = {T 1 , ..., T n } be a finite set of tile types. Given a tile type T i , u(T i ), r(T i ), d(T i ) and l(T i ) will represent the colors of the upper, right, lower and left edges of T i , respectively. For each tile type T i , we fix a proposition letter t i that is going to encode T i . We will now define an MLSR formula ϕ T such that the following holds: ϕ T is satisfiable if and only if T tiles the discrete quadrant N × N.
The formula ϕ T is the conjunction of the following MLSR formulas. The first three describe the relational structure of a grid, the last three encode the behavior of a tiling of the grid: It is easy to see that any tiling of N × N induces a model for ϕ T .
(⇒) For the other direction, suppose that M, w |= ϕ T , for some LSR-model M = (W, R u , R r , V ) and w ∈ W . The formula (Func) ensures that the relations R u and R r are functions, and that for every point x, that R u [x] R r [x] (the R u and R r -images of x are different). The formula (Conf ) then guarantees that the functions commute: R u • R r = R r • R u . This ensures the existence of an embedding f : N 2 → W that preserves the structure of vertical and horizontal successors: that is, for all (n, m) ∈ N 2 , we have R u (f (n, m), f (n, m + 1)) and R r (f (n, m), f (n + 1, m)). Now, tile the point (n, m) in N 2 with tile T i exactly if M, f (n, m) |= t i . This gives a tiling of the discrete quadrant of the plane.
The two standard modalities used in this proof can be reduced to one using standard techniques [Kracht and Wolter, 1999], but we forego details here because of the syntactic cost involved in writing the formulas.
The above undecidability argument applies a fortiori to the richer language of §3 with nominals and PAL modlities. But it will also work with languages that are less expressive than MLSR. In particular, one can replace the universal modality by an extra standard modality that can survey the domain by employing the well-known 'spypoint technique' from hybrid logic. A detailed syntactic construction of this sort for modal logics of graph games can be found in [Zaffora Blando et al., 2020].
Having determined the complexity of model checking and satisfiability, one task would remain, concerning definability and expressive power. However, we leave this open here.

Open problem. What is the complexity of testing for SR-bisimulation?
Given any two finite models M, N , it is easy to find an EXPSPACE upper bound. One considers the space of all models arising from M, N by deleting finite sequences of different points, and then tests for ordinary modal bisimulation over this space with respect to MLSR, now viewed as a standard bimodal language. But, just as with standard modal bisimulation [Kanellakis and Smolka, 1983], one can probably do better.

Stepwise removal over first-order fragments
Having established the complexity of adding quantification without replacement to the basic modal language, we can also consider other fragments of first-order logic. Perhaps the simplest case is adding the removal modality −ϕ ψ to monadic first-order logic MFOL. As it turns out, this yields exactly the formulas in MFOL x = : that is, all formulas with one free variable x in monadic first-order logic with identity. Proof. Fix finitely many unary predicates P 1 , . . . , P k . We define standard normal forms for the whole language MFOL = . Local state descriptions sd are conjunctions of ±P i with 1 ≤ i ≤ k. There are 2 k of these, and they can be applied to arbitrary variables. Global state descriptions SD of depth N are then conjunctions j SD j where, for each local state description sd j , SD j is either the statement that exactly m j objects satisfy sd j , where we have m j < N , or the statement that at least N objects satisfy sd j . Claim. MFOL = is closed under the modality −ϕ ψ.
Proof of Claim. Using the disjunction axioms for existential modalities and −ϕ ψ stated in §3, in proving closure, one can restrict attention to conjunctive forms N F and special removal modalities −sd ∧ SD N F . Closure can be shown here by a simple argument, driven by the following two key facts: where SD[i := i + 1] replaces the quantification in the i-th conjunct of SD by a quantifier stating the existence of one more point satisfying the relevant local state description.
Arguments like this are available for other languages that admit of simple normal forms of modal depth 1. Here is one obvious question.

Open problem. What fragment of first-order logic results from adding the dynamic operators of MLSR to the language of modal S5?
We have some initial results, but the combinatorics get considerably more complex, since the logic can now also distinguish between different equivalence classes in S5 models.
The general question suggested by the specific case analyzed in Theorem 6.1 is the following: what is the boost in expressive power when we close fragments of first-order logic under various model-changing modalities?

Conclusion and further directions
The logic of stepwise removal of objects lies in between modal logics of definable model change and logics for graph games with arbitrary moves, and it may well be the most intuitive example of a modal system that crosses the line from decidable to undecidable. 18 We have established its main properties, proving a bisimulation characterization theorem and other results on expressive power, a completeness theorem, and two basic complexity results. Most of the techniques that we used are well-known, others less so, and we also introduced a new technique for proving completeness. The resulting style of thinking can be applied to a wide range of modal systems of this sort. 16 Alternatively, N F describes a model M in such a way that, for any model N that satisfies N F , Duplicator has a winning strategy in the Ehrenfeucht game over N rounds between M and N starting with the partial isomorphism between the objects on both sides satisfying the atomic diagram (a). 17 Here is a general useful principle that is easy to state in first-order syntax. When we take out a point satisfying ϕ(x) ∧ ψ, where x does not occur free in ψ, then we can just put ψ outside in a conjunction.
18 Another contender is the 'modal fact change logic' of Thompson [2020].
Among the issues still to be addressed is the complexity problem for SR-bisimulation ( §5), as well as the expressive closure problem for S5. Moreover, all of our questions return for some obvious extensions and variations.
Simultaneous versions of MLSR. It is natural to add a modality for removing a fixed finite number of points, either in a conjunctive unary version −(ϕ 1 , ..., ϕ k ) ψ or with truly polyadic operators −ϕ ψ, where the formulas ϕ can be evaluated in a tuple of indices. These modalities seem undefinable as iterations of our unary −ϕ ψ. Even so, we conjecture that all of our results go through.
Another immediate question concerns other extended modal logics.
Connections with hybrid logic. MLSR seems closely related to hybrid modal formalisms such as 'memory logics' that have been used to detect jumps to undecidability for fragments of FOL in an illuminating manner, [Areces et al., 2008]. Given that MLSR translates into a fragment of the first-order language, cf. Fact 2.5, it may be of interest to compare the fragments that arise by adding the removal modality −ϕ ψ to various first-order fragments with the natural hierarchy offered by the memory-logic perspective. 19 Then, there is the question of the scope of our methods.
Axiomatizing logics of graph games. It is a long-standing open problem how to axiomatize the validities of sabotage-style modal logics and related ones [Aucher et al., 2018]. Does our axiomatization technique for MLSR employing added dynamic epistemic modalities work for these logics, as well? 20 Next, returning to the issue of undecidability, a few questions arise naturally.
Other sources of undecidability. In addition to the undecidability induced by stepwise removal, there is the undecidability induced by local link-cutting or local definable point removal, taking place only at the current point of evaluation [Li, 2020]. Both modifications of dynamic-epistemic logics block the usual recursion axioms, both allow for tiling encodings, but the connection remains to be clarified.
But there are also other perspectives on complexity that we have found.
Lowering the complexity of MLSR. Can MLSR be shifted back into the decidable modal fold? For many logical systems, one can lower the complexity by a Henkin-style change in the semantics [Andréka et al., 2016]. In particular, one could restrict the removal of points to those that are accessible from the current point in some global relation Axy and, if this does not suffice for decidability, one might use further guarding, so that the earlier firstorder translations of MLSR formulas (from §2) end up inside guarded, or loosely guarded, fragments of FOL.
Yet, moves like this make most sense when connected to a principled view of computation. We believe that modal logics like MLSR, but also hybrid memory logics or related systems, offer an interesting alternative take on the sources of computational complexity.
In the usual automata hierarchy, Turing machine power arises when we have an active memory that can be rewritten. In our logics, however, a simple device that merely stores the set of deleted or visited points suffices. The reason must be the interplay of memory and expressiveness of the language for constructing models around that memory, suggesting a sort of descriptive complexity theory complementary to that of Immerman [1999].