1 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
$\mathcal {M}$
, look at what is true in other models
$\mathcal {N}$
, related to
$\mathcal {M}$
via some relevant cross-model relation. These dynamic logics come in a wide range of expressive power and computational complexity (Aucher, van Benthem, Grossi, Reference Aucher, van Benthem and Grossi2018). 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
$!\varphi $
of reliable public information that
$\varphi $
is the case changes a current pointed model
$(\mathcal {M}, s)$
to the definable sub-model
$(\mathcal {M}| \varphi , s)$
, whose domain is the set of all points in
$\mathcal {M}$
that satisfy
$\varphi $
. Likewise, an event where all agents publicly lose all uncertainty about
$\varphi $
takes
$(\mathcal {M}, s)$
to a model
$(\mathcal {M} \backslash\varphi , s)$
, where the domain stays the same, but the epistemic accessibility relation
$\sim $
of
$\mathcal {M}$
gets replaced by the refinement
$s \sim _\varphi t$
: i.e.,
$s \sim t$
and, also,
$\mathcal {M}, t\models \varphi $
if and only if
$\mathcal {M}, s\models \varphi $
. These and many other model transformations F have matching modalities
${[F]}\psi $
in dynamic epistemic logics, whose key axioms for
${[F]}\psi $
give a recursive analysis of when the postconditions
$\psi $
hold in terms of what was true before the F-update (see the survey by van Benthem, Reference van Benthem2011). 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 (Reference van Benthem, Hutter and Stephan2005), 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., Reference Aucher, van Benthem and Grossi2018) and (van Benthem & Liu, Reference van Benthem, Liu, Liu, Ono and Yu2020)).
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 sabotage-type 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.
A stepwise update modality. Consider the standard language of basic modal logic, augmented with a dynamic modality
$\langle - {\varphi }\rangle \psi $
that has the following semantics.
Definition 1.1. Given a relational model
$\mathcal {M}=(W, R, V)$
, with
$R\subseteq W\times W$
and V a valuation, the satisfaction clause for
$\langle - {\varphi }\rangle \psi $
reads
$$\begin{align*}\mathcal{M}, s\models \langle-\varphi\rangle\psi \text{ iff there is a point } t \neq s \text{ in } \mathcal{M} \text{ with } \mathcal{M}, t \models \varphi \text{ and } \mathcal{M}-\{t\}, s\models\psi, \end{align*}$$
where
$\mathcal {M}-\{t\}$
is the submodel of
$\mathcal {M}$
having just the point t removed from its domain. More generally, given
$D\subseteq W$
,
$\mathcal {M}-D$
denotes the submodel of
$\mathcal {M}$
with domain
$W\setminus D$
.
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
$\varphi $
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, Reference de Lavalette, Condoravdi and de Lavalette2001). 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
$\exists x\, \varphi (x) \cdot \psi (x)$
in first-order logic (FOL). One searches for an object d satisfying
$\varphi $
and then checks whether d also satisfies
$\psi $
. In this second stage, the model has not changed: the witness d is still in the domain and it influences the evaluation of
$\psi $
. Call this process “quantification with replacement”. Now, it has been claimed (Hintikka & Sandu, Reference Hintikka, Sandu, ter Meulen and van Benthem1997) 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, Reference Gabbay and Gabbay2013):
$\exists x (\varphi |\psi )$
says that there is an object (or, in a natural polyadic version
$\exists \overline {x} (\varphi |\psi )$
, a tuple of objects) that satisfies
$\varphi $
in the current model
$\mathcal {M}$
, while
$\psi $
holds in the sub-model
$\mathcal {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,
$\neg $
,
$\vee $
,
$\Diamond $
, plus the additional modality
$\langle -\varphi \rangle \psi $
, whose semantics was given above (Definition 1.1). Occasionally, we will also use this language extended with a “public announcement,” or relativization, modality
$\langle !\varphi \rangle \psi $
describing what is true in restrictions to definable subdomains:
$$\begin{align*}\mathcal{M}, s\models \langle!\varphi\rangle\psi \;\; \text{ iff } \; \; \mathcal{M}, s\models\varphi \text{ and }\mathcal{M}|\varphi, s \models \psi, \end{align*}$$
with
$\mathcal {M}|\varphi $
the submodel of
$\mathcal {M}$
consisting of all and only the points in
$\mathcal {M}$
where
$\varphi $
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 PSPACE-complete. This analysis uses a reduction technique from Löding & Rohde (Reference Löding, Rohde, Rovan and Vojtas2003) 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, Reference Marx, Blackburn, van Benthem and Wolter2006; Areces, Fervari, & Hoffmann, Reference Areces, Fervari and Hoffmann2015). 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
$\langle -\varphi \rangle \psi $
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.
2 Basics of expressive power
We start with the formal language to be used in most of this paper.Footnote 1
Definition 2.1. The syntax of MLSR is given by
$$\begin{align*}\varphi:= p\,|\,\neg\varphi\,|\,(\varphi\vee\varphi)\,|\,\Diamond\varphi\,|\,\langle-\varphi\rangle\varphi , \end{align*}$$
with
$p\in {\mathsf{PROP}}$
. Dual modal operators
$\Box , {[-\varphi ]}$
are defined as usual.
Some definable notions. The language of MLSR can define various modal operators from hybrid logic (Areces & ten Cate, Reference Areces, ten Cate, Blackburn, van Benthem and Wolter2006) that go beyond the basic modal language. For instance, the difference modality
$\mathsf {D}\varphi $
(‘
$\varphi $
is true at some different point’) can be defined as
$\langle -\varphi \rangle \top $
, and this, in turn, allows to define the existential modality
$\mathsf {E}\varphi $
as
$\varphi \vee \mathsf {D}\varphi $
. MLSR can also count all finite cardinalities, using suitably iterated formulas
$$\begin{align*}\underbrace{\langle-\top\rangle\cdots\langle-\top\rangle}_{k \text{ times}}\top, \end{align*}$$
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
$\rho _{2}$
be the formula defining domain size 2, and let
$\mathsf {U}$
be the universal modality (i.e.,
$\mathsf {U}\varphi = \varphi \wedge {[-\neg \varphi ]}\bot )$
. The following observation requires an easy exercise in understanding what our language can express.
Fact 2.2. The
MLSR
-formula
$\rho _{2} \wedge \mathsf {U}\langle -\top \rangle \Box \bot \wedge \Diamond \Diamond \top $
defines a two-point irreflexive loop.
However, not every finite graph is definable, as we shall soon see.
SR-bisimulation. The semantic invariance matching this language is as follows.
Definition 2.3. A relation Z between a set of pointed relational models is an
SR
-bisimulation if it is a modal bisimulation in the ordinary sense, where the back and forth clauses stay inside the same models
$\mathcal {M}, \mathcal {N}$
, while, in addition,
-
(a) if
$(\mathcal {M}, s) Z (\mathcal {N}, t)$
and
$u \in \mathcal {M}$
with
$u \neq s$
, then there is a
$v \in \mathcal {N}$
such that
$v \neq t$
,
$(\mathcal {M},u) Z (\mathcal {N}, v)$
, and
$(\mathcal {M}-\{u\},s) Z (\mathcal {N}-\{v\}, t)$
, -
(b) the analogous clause in the converse direction.
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.
Fact 2.4. MLSR -formulas are invariant for SR -bisimulations.
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.
$\forall y (Rxy\vee Ryx)$
is not
MLSR
-definable.
Proof. Consider the model
$\mathcal {M}$
consisting of two isolated reflexive points and the model
$\mathcal {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
$(\mathcal {M}, x)$
and
$(\mathcal {N}, y)$
plus all links between the 1-point pointed sub-models of
$\mathcal {M}$
and
$\mathcal {N}$
is an SR-bisimulation. But, clearly, connectedness holds in
$\mathcal {N}$
, but not in
$\mathcal {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
$\tau (\varphi , y, X)$
from MLSR-formulas
$\varphi $
to first-order formulas, where y is a free variable and X a finite set of variables:
$$ \begin{align*} \tau(p, y, X) &= Py,\\ \tau(\neg\varphi, y, X) &= \neg\tau(\varphi, y, X),\\ \tau(\varphi\vee\psi, y, X) &= \tau(\varphi , y, X) \vee \tau(\psi, y, X),\\ \tau(\Diamond\varphi, y, X) &= \exists z \bigg(Ryz \wedge \bigwedge_{x\in X}\neg(z = x) \wedge \tau(\varphi, z, X)\bigg),\\ \tau(\langle-\varphi\rangle\psi, y, X) &= \exists z \bigg(\neg(z=y) \wedge \bigwedge_{x\in X}\neg(z = x) \wedge \tau(\varphi, z, X) \wedge \tau(\psi, y, X \cup \{z\})\bigg). \end{align*} $$
Let
$(\mathcal {M}, s)$
be any pointed model and
$D = \{d_1,..., d_k\}$
a finite set of points in
$\mathcal {M}$
of size k. The following equivalence is shown by a straightforward induction on MLSR-formulas
$\varphi $
and sets of variables
$X = \{x_1,..., x_k\}$
of size k:
$$\begin{align*}\mathcal{M}- D, s \models \varphi \text{ iff } \mathcal{M}, a[y/s, X/D] \models \tau(\varphi, y, X), \end{align*}$$
where
$a[y/s, X/D]$
is the variant of the variable assignment a such that
$a[y/s, X/D](y)=s$
and
$a[y/s, X/D](x_i) = d_i$
for
$1\leq i\leq k$
. As a special case, there is an equivalence for MLSR-formulas in ordinary relational models
$\mathcal {M}$
with
$D = \varnothing $
.
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, de Rijke, & Venema, Reference Blackburn, de Rijke and Venema2011)) yields the following result.
Theorem 2.8. The following assertions are equivalent for all first-order formulas
$\varphi (x)$
in the signature of our models, with one free variable:
-
(a)
$\varphi (x)$
is invariant for
SR
-bisimulation; -
(b)
$\varphi (x)$
is equivalent to the translation of some
MLSR
-formula.
Proof. We merely outline the points that need attention in the nontrivial direction from (a) to (b). Let
$\mathcal {S}\mathcal {R}$
denote the
$\mathsf {MLSR}$
-fragment of first-order logic (that is, all first-order formulas equivalent to translations of
$\mathsf {MLSR}$
formulas via the translation
$\tau $
from Fact 2.6). As usual, one shows that
$\varphi (x)$
is a semantic consequence of the set
$\mathcal {C}_{x}(\varphi )$
of its
$\mathcal {S}\mathcal {R}$
-consequences and then applies Compactness to get an
$\mathcal {S}\mathcal {R}$
-equivalent. We thus need to show that
$\mathcal {C}_{x}(\varphi ) \models \varphi (x)$
. Suppose
$\mathcal {M}, s\models \mathcal {C}_{x}(\varphi )$
. A standard compactness argument shows that there is a model
$\mathcal {N}$
and
$t\in \mathcal {N}$
such that
$(\mathcal {M}, s)$
and
$(\mathcal {N}, t)$
are
$\mathcal {S}\mathcal {R}$
-equivalent, while
$\mathcal {N}, t \models \varphi (x)$
. These models are then extended to
$\omega $
-saturated elementary extensions
$(\mathcal {M}^+, s)$
and
$(\mathcal {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
$(\mathcal {M}^+-D, u)$
and
$(\mathcal {N}^+-E, v)$
, with
$E, D$
of the same finite size, which holds if
$(\mathcal {M}^+-D, u)$
and
$(\mathcal {N}^+-E, v)$
satisfy the same
$\mathcal {S}\mathcal {R}$
-formulas. Using saturation, it can be shown that Z is an SR-bisimulation, where the argument for the modality
$\Diamond \varphi $
is standard, while the one for
$\langle -\varphi \rangle \psi $
in terms of removing single objects goes as follows. Take
$(\mathcal {M}^+-D, u)$
and
$w \neq u$
. Now, let
$$ \begin{align*} \Gamma(y) &:= \big\{\gamma(y)\in\mathcal{S}\mathcal{R}\,\big|\, \mathcal{M}^{+}-D, w\models \gamma\big\} \\ \Delta(x) &:= \big\{\delta(x)\in\mathcal{S}\mathcal{R}\,\big|\, \mathcal{M}^{+}-(D\cup\{w\}), u\models\delta\} \end{align*} $$
and consider the set of first-order formulas
$$\begin{align*}p(x,y) :=\{\neg(y = x)\} \cup \Gamma(y)\cup \Delta(x) \end{align*}$$
This set is finitely satisfiable in
$(\mathcal {M}^+-D, u, w)$
(interpreting x as u and y as w). For each of its finite subsets
$\{\neg (y = x)\} \cup \Gamma ^{\prime }(y)\cup \Delta ^{\prime }(x)$
, we have
$$\begin{align*}\mathcal{M}^+-D, u, w\models \neg(y = x)\wedge \bigwedge \Gamma^{\prime}(y) \wedge \bigwedge \Delta^{\prime}(x), \end{align*}$$
which means that
$$\begin{align*}\mathcal{M}^+-D, u\models\exists y\Big( \neg(y = x)\wedge \bigwedge \Gamma^{\prime}(y) \wedge \bigwedge \Delta^{\prime}(x)\Big), \end{align*}$$
and this formula is in
$\mathcal {S}\mathcal {R}$
(it is equivalent to the translation of a
$\langle -\varphi \rangle \psi $
formula). This means that the formula also holds in
$(\mathcal {N}^+-E, v)$
. Thus, every finite subset of
$p(x,y)$
is satisfiable in
$(\mathcal {N}^+-E, v)$
(interpreting x as v). In other words, expanding the language with a new constant symbol
$\mathbf {c}$
, the 1-type
$p(\mathbf {c},y)$
is finitely satisfiable in
$(\mathcal {N}^+-E, v)$
(fixing the interpretation of
$\mathbf {c}$
as v). Then, by saturation, the type is realized in
$(\mathcal {N}^+-E, v)$
: we can thus find an object in
$\mathcal {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,\downarrow )$
(Areces & ten Cate, Reference Areces, ten Cate, Blackburn, van Benthem and Wolter2006). The key translation clause here reads, for each formula of the form
$\langle - {\varphi }\rangle \psi $
and sequence of nominals
$\overline {\mathbf {n}}=(\mathsf {n}_{1},...,\mathsf {n}_{\ell })$
:
$$\begin{align*}\sigma(\langle - {\varphi}\rangle\psi)^{\overline{\mathbf{n}}} = \downarrow_{\mathsf{m}}. \mathsf{E}\downarrow_{\mathsf{k}}. \bigg(\neg \mathsf{m} \wedge\bigwedge^{\ell}_{i=1}\neg\mathsf{n}_{i} \wedge \sigma(\varphi)^{\overline{\mathbf{n}}}\wedge @_{\mathsf{m}}\sigma(\psi)^{\overline{\mathbf{n}}, \mathsf{k}}\bigg) \end{align*}$$
Further connections of MLSR with hybrid logics will be discussed in §7 below.
3 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
$\langle -\varphi \rangle \psi $
distributes over disjunction in both of its arguments:
Fact 3.1. The following formulas are both valid:
$$ \begin{align*} \langle -\psi\rangle (\varphi_{1}\vee\varphi_{2}) &\leftrightarrow \big(\langle -\psi\rangle\varphi_{1} \vee \langle -\psi\rangle\varphi_{2}\big) \\ \langle -(\varphi_{1}\vee\varphi_{2})\rangle\psi &\leftrightarrow \big(\langle -\varphi_{1}\rangle\psi \vee \langle -\varphi_{2}\rangle\psi\big) \end{align*} $$
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
$\langle !\varphi \rangle \psi $
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
$\langle - {\varphi }\rangle \langle ! {\alpha }\rangle \psi $
or
$\langle ! {\alpha }\rangle \langle - {\varphi }\rangle \psi $
. For example,
$\langle ! {\alpha }\rangle \langle - {\varphi }\rangle \psi $
is not equivalent to
$\alpha \wedge \langle - {\langle ! {\alpha }\rangle \varphi }\rangle \langle ! {\alpha }\rangle \psi $
(consider, for instance, the case where
$\alpha =\Diamond p$
,
$\varphi =\Box \bot $
and
$\psi = \top $
). 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:
$$\begin{align*}(\exists x (\varphi|\psi))^{\alpha(\cdot)} (x) \, \leftrightarrow \, \alpha(x) \wedge \exists y(\alpha(y)\wedge y\neq x \wedge \varphi^{\alpha(\cdot)}(y) \wedge (\psi)^{\alpha(\cdot)\wedge\, \cdot\,\neq (y)}(x))\end{align*}$$
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
$$\begin{align*}\varphi:= p\,|\,\mathsf{n}\,|\,\top\,|\,\neg\varphi\,|\,(\varphi\vee\varphi)\,|\,\Diamond\varphi\,|\,\langle!\varphi\rangle\varphi\,|\,\langle-\varphi\rangle\varphi\,|\,\mathsf{E}\varphi, \end{align*}$$
with
$p\in {\mathsf{PROP}}$
,
$\mathsf{n}\in {\mathsf{NOM}}$
. Dual modal operators
$\Box , [!\varphi ], [-\varphi ]$
and
$\mathsf {U}$
are defined as usual.
Note that it is not necessary to add the
$@_{\mathsf {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,
$@_{\mathsf {n}}\varphi $
is simply a shorthand for
$\textsf {U}(\mathsf {n}\rightarrow \varphi )$
.Footnote
2
The following proof system may look somewhat complex, but its components just follow the formal syntax just introduced.
The Hilbert-style proof system for MLSR.
Definition 3.4. The logic MLSR (see Figure 1 ) consists of:
-
• the rule of Replacement of Provable Equivalents,Footnote 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., Reference Blackburn, de Rijke and Venema2011 ;
-
• the Name Rule and the Paste Rule from hybrid logic (Areces & ten Cate, Reference Areces, ten Cate, Blackburn, van Benthem and Wolter2006), with the latter slightly adapted to our setting;
-
• the axiom
$\mathsf {E} (\mathsf {n}\wedge \varphi )\rightarrow \mathsf {U}(\mathsf {n}\rightarrow \varphi )$
, which we denote by (H); -
• the usual reduction axioms of public announcement logic
$\mathsf {PAL}$
for atoms (including nominals), the existential base modality, the global existential modality, and the announcement modality (van Benthem, Reference van Benthem2011),Footnote
4
as well as the Truth Axiom
$\langle !\top \rangle \varphi \leftrightarrow \varphi $
; -
• the following two principles connecting the stepwise removal modality with the public announcement modality:
-
(Mix Axiom)
$(\mathsf {E}(\mathsf {n} \wedge \alpha ) \wedge \langle !\neg \mathsf {n} \rangle \varphi ) \rightarrow \langle - \alpha \rangle \varphi $
; -
(Mix Rule) If
$\,\vdash\ \mathsf {E}(\mathsf {n}\land \langle ! {\varphi }\rangle \mathsf {E}(\mathsf {k}\land \alpha ) \land \langle ! {\varphi }\rangle \langle ! {\neg \mathsf {k}}\rangle \psi )\rightarrow \sigma $
,then
$\,\vdash\ \mathsf {E}(\mathsf {n}\land \langle ! {\varphi }\rangle \langle -\alpha \rangle \psi )\rightarrow \sigma $
, where
$\mathsf {k}\notin \sigma ,\varphi ,\alpha ,\psi $
.
-
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
$\mathsf {n}$
, the formula
$\neg \mathsf {E}\mathsf {n}$
holds. Connected to this, the equivalence
$\mathsf {E}(\mathsf {n} \land \neg \varphi ) \leftrightarrow \neg \mathsf {E}(\mathsf {n} \land \varphi )$
underpinning the common hybrid notation
$@_{\mathsf {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:
-
•
$\mathsf {E}(\mathsf {n} \land \neg \varphi ) \leftrightarrow (\mathsf {E}\mathsf {n} \land \neg \mathsf {E}(\mathsf {n} \land \varphi ))$
-
•
$\mathsf {n} \rightarrow (\mathsf {E}(\mathsf {n}\land \varphi )\leftrightarrow \varphi )$
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
$\mathsf {n}\rightarrow \neg \langle - {\mathsf {n}}\rangle \top $
is an
$\mathsf {MLSR}$
theorem for any
$\mathsf {n}\in \mathsf {NOM}$
.
Proof. Take
$\varphi , \psi = \top $
,
$\sigma = \bot $
,
$\alpha = \mathsf {n}$
. Then the antecedent formula in the Mix Rule reads
$$\begin{align*}\mathsf{E}(\mathsf{n} \land \langle!\top\rangle \mathsf{E}(\mathsf{k}\land \mathsf{n}) \land \langle!\top\rangle\langle!\neg \mathsf{k}\rangle\top) \rightarrow \bot \end{align*}$$
This is derivable in
$\mathsf {MLSR}$
. Using Replacement of Equivalents,Footnote
5
and appealing to (i) a simple analysis of
$\langle !\top \rangle \mathsf {E}(\mathsf {k}\land \mathsf {n})$
using the
$\mathsf {PAL}$
reduction axioms for
$\mathsf {E}$
and nominals, and (ii) the implication from
$\langle !\neg \mathsf {k}\rangle \top $
to
$\neg \mathsf {k}$
which is one half of the
$\mathsf {PAL}$
reduction axiom for
$\top $
, the antecedent of the above formula derives
$\mathsf {E}(\mathsf {k}\wedge \neg \mathsf {k})$
. It then suffices to note that the S5 axioms for quantifiers allow to derive
$\mathsf {E}(\mathsf {k}\wedge \neg \mathsf {k})\rightarrow \bot $
.
Therefore, the consequent formula is provable using the Mix Rule:
$$\begin{align*}\mathsf{E}(\mathsf{n} \land \langle!\top\rangle\langle -\mathsf{n}\rangle\top) \rightarrow \bot.\end{align*}$$
Using the Truth Axiom and the S5 axioms for quantifiers, this is equivalent in
$\mathsf {MLSR}$
to
$\mathsf {U}(\mathsf {n}\rightarrow \neg \langle - {\mathsf {n}}\rangle \top )$
, which implies the desired
$\mathsf {n}\rightarrow \neg \langle - {\mathsf {n}}\rangle \top $
.
To increase familiarity with the proof system, we explore
$\mathsf {MLSR}$
a bit further.
-
(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
$\mathsf {n}$
, and using propositional logic, derive
$(\mathsf {n} \land \langle ! {\varphi }\rangle (\mathsf {E}(\mathsf {k}\wedge \alpha )\wedge \langle ! {\neg \mathsf {k}}\rangle \psi ))\rightarrow \sigma $
. Given the facts derived in Remark 3.6, this is equivalent to
$(\mathsf {n} \land \mathsf {E}(\mathsf {n} \land \langle ! {\varphi }\rangle (\mathsf {E}(\mathsf {k}\wedge \alpha )\wedge \langle ! {\neg \mathsf {k}}\rangle \psi )))\rightarrow \sigma $
. Again by propositional logic, this yields
$\mathsf {E}(\mathsf {n} \land \langle ! {\varphi }\rangle (\mathsf {E}(\mathsf {k}\wedge \alpha )\wedge \langle ! {\neg \mathsf {k}}\rangle \psi ))) \rightarrow (\mathsf {n} \rightarrow \sigma )$
. Here, since
$\mathsf {n}$
was fresh, the nominal
$\mathsf {k}$
still satisfies the conditions of the Mix Rule. Therefore, we can conclude
$\mathsf {E}(\mathsf {n} \land \langle ! {\varphi }\rangle \langle -\alpha \rangle \psi )\rightarrow (\mathsf {n} \rightarrow \sigma )$
. From this, using propositional logic,
$(\mathsf {n} \land \mathsf {E}(\mathsf {n} \land \langle ! {\varphi }\rangle \langle -\alpha \rangle \psi ))\rightarrow \sigma $
. Then using Remark 3.6 once more, we get
$(\mathsf {n} \land \langle ! {\varphi }\rangle \langle -\alpha \rangle \psi )\rightarrow \sigma $
, and with propositional logic,
$\mathsf {n} \rightarrow (\langle ! {\varphi }\rangle \langle -\alpha \rangle \psi )\rightarrow \sigma )$
. Finally, using the Name Rule of the hybrid logic component of
$\mathsf {MLSR}$
, the conclusion
$\langle ! {\varphi }\rangle \langle -\alpha \rangle \psi \rightarrow \sigma $
follows.Taking the special case of
$\varphi = \top $
, and using the Truth Axiom of
$\mathsf {MLSR}$
(which was not used in the preceding derivations), the Stripped Mix Rule reduces to: -
(b) 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.
Proposition 3.9. The following are
$\mathsf {MLSR}$
-provable validities:
-
(i)
$\langle !\varphi \rangle \alpha \rightarrow \varphi $
(announced formulas are always true); -
(ii)
$\langle -(\varphi _{1}\vee \varphi _{2})\rangle \psi \leftrightarrow \big (\langle -\varphi _{1}\rangle \psi \vee \langle -\varphi _{2}\rangle \psi \big )$
(distributivity over disjunction, cf. Fact 3.1); -
(iii)
$\mathsf {E}\alpha \leftrightarrow (\alpha \vee \langle -\alpha \rangle \top )$
(the removal modality captures quantifiers).
Proof. (i) This follows since
$\langle !\varphi \rangle \alpha \rightarrow \langle !\varphi \rangle \top $
is provable by principles of the minimal logic
$\mathsf {K}$
for the modality
$\langle !\varphi \rangle $
, while the
$\mathsf {PAL}$
reduction axiom for the atom
$\top $
gives
$\langle !\varphi \rangle \top \leftrightarrow \varphi $
.
(ii) With the Basic Mix Rule in hand, it is straightforward to derive this nontrivial distribution law. We sketch the left-to-right direction, appealing to the Basic Mix Rule with
$\alpha = \varphi _{1}\vee \varphi _{2}$
and
$\sigma =\langle - {\varphi _{1}}\rangle \psi \,\vee \langle - {\varphi _{2}}\rangle \psi $
. For
$\mathsf {k}$
a fresh nominal,
$\mathsf {E} (\mathsf {k} \land (\varphi _{1}\vee \varphi _{2})) \land \langle !\neg \mathsf {k}\rangle \rangle \psi )$
provably implies
$\langle - {\varphi _{1}}\rangle \psi \,\vee \langle - {\varphi _{2}}\rangle \psi $
: this can be shown using the standard distribution of the
$\mathsf {E}$
modality over disjunctions, after which the Mix Axiom gives the required result.
(iii) For the left-to-right direction, let
$\mathsf {k}$
be a fresh nominal not appearing in
$\alpha $
. Note that, by the (H) Axiom,
$\mathsf {E}(\mathsf {k}\wedge \alpha )\rightarrow \mathsf {U}(\neg \alpha \rightarrow \neg \mathsf {k})$
is derivable. Then, since
$$ \begin{align*} &\vdash (\mathsf{E}(\mathsf{k}\wedge\alpha) \wedge\neg\alpha)\rightarrow (\mathsf{E}(\mathsf{k}\wedge\alpha) \wedge\neg\mathsf{k}),\\ &\vdash (\mathsf{E}(\mathsf{k}\wedge\alpha) \wedge\neg\mathsf{k})\rightarrow (\mathsf{E}(\mathsf{k}\wedge\alpha) \wedge\langle ! {\neg\mathsf{k}}\rangle\top),\text{ and}\\ &\vdash (\mathsf{E}(\mathsf{k}\wedge\alpha) \wedge\langle ! {\neg\mathsf{k}}\rangle\top)\rightarrow \langle-\alpha\rangle\top \,\,\,(\text{by the Mix Axiom}), \end{align*} $$
we have that
$\vdash (\mathsf {E}(\mathsf {k}\wedge \alpha ) \wedge \neg \alpha )\rightarrow \langle -\alpha \rangle \top $
. 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
$\langle -\alpha \rangle \top \rightarrow \mathsf {E}\alpha $
. Let
$\mathsf {k}$
be a fresh nominal not appearing in
$\alpha $
. Since
$(\mathsf {E}(\mathsf {k}\wedge \alpha )\wedge \langle ! {\neg \mathsf {k}}\rangle \top )\rightarrow \mathsf {E}\alpha $
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
$\mathsf {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:
$$\begin{align*}\langle ! {\top}\rangle\varphi \leftrightarrow \varphi.\end{align*}$$
In public announcement logic
$\mathsf {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
$\varphi $
. The base cases for atoms (proposition letters, nominals and
$\top $
), as well as the inductive steps for negations, disjunctions, and the two existential modalities are immediate from the corresponding reduction axioms in
$\mathsf {PAL}$
.
However, in the setting of
$\,\mathsf {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
$\langle ! {\top }\rangle \langle -\alpha \rangle \psi \rightarrow \langle -\alpha \rangle \psi $
, it suffices to derive, for some fresh nominal
$\mathsf {k}$
, the implication
$\langle ! {\top }\rangle (\mathsf {E}(\mathsf {k} \land \alpha ) \land \langle ! {\neg \mathsf {k}}\rangle \psi ) \rightarrow \langle -\alpha \rangle \psi $
. And here, distributing the modality
$\langle ! {\top }\rangle $
inside by appealing to the
$\mathsf {PAL}$
axioms of
$\mathsf {MLSR}$
, and using the inductive hypothesis that
$\langle ! {\top }\rangle \alpha \leftrightarrow \alpha $
is derivable already, the antecedent is provably equivalent to
$\mathsf {E}(\mathsf {k} \land \alpha ) \land \langle ! {\neg \mathsf {k}}\rangle \psi $
, which implies
$\langle -\alpha \rangle \psi $
by the Mix Axiom.
A similar analysis in the opposite direction would derive
$\langle -\alpha \rangle \psi \rightarrow \langle ! {\top }\rangle \langle -\alpha \rangle \psi $
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 nonredundant presentation of
$\mathsf {MLSR}$
as an open problem (see also the final point in §4 about the need for the
$\mathsf {PAL}$
component). Even so, as shown in this section,
$\mathsf {MLSR}$
is quite a workable proof system, whose fine-structure deserves further exploration.
4 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., Reference Blackburn, de Rijke and Venema2011), 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
$\Gamma $
is
-
• named if it contains a nominal;
-
•
$\Diamond $
-pasted if
$\mathsf {E}(\mathsf {n}\land \Diamond \varphi )\in \Gamma $
implies that there is some nominal
$\mathsf {m}$
such that the formula
$\mathsf {E}(\mathsf {n}\land \Diamond \mathsf {m})\wedge \mathsf {E}(\mathsf {m}\land \varphi )\in \Gamma $
; -
•
$\mathsf {E}$
-pasted if
$\mathsf {E}(\mathsf {n}\land \mathsf {E}\varphi )\in \Gamma $
implies that there is some nominal
$\mathsf {m}$
such that the formula
$\mathsf {E}(\mathsf {n}\land \mathsf {E}\mathsf {m})\wedge \mathsf {E}(\mathsf {m}\land \varphi )\in \Gamma $
; -
• mixed if
$\langle ! {\varphi }\rangle \langle -\alpha \rangle \psi \in \Gamma $
implies that there is some nominal
$\mathsf {n}$
such that the formula
$\langle ! {\varphi }\rangle \mathsf {E}(\mathsf {n}\wedge \alpha )\wedge \langle ! {\varphi }\rangle \langle !\neg \mathsf {n}\rangle \psi \in \Gamma $
; -
•
$\mathsf {E}$
-mixed if, whenever
$\mathsf {E}(\mathsf {n}\wedge \langle ! {\varphi }\rangle \langle - {\alpha }\rangle \psi )\in \Gamma $
, then there is some nominal
$\mathsf {k}$
such that
$\mathsf {E}\big (\mathsf {n}\wedge \langle ! {\varphi }\rangle (\mathsf {E}(\mathsf {k}\wedge \alpha )\wedge \langle ! {\neg \mathsf {k}}\rangle \psi )\big )\in \Gamma $
.
A set
$\Gamma $
of MLSR-formulas will be said to be pasted if it is both
$\Diamond $
-pasted and
$\mathsf {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
$\Gamma $
contains some nominal
$\mathsf {n}$
naming it, then
$\mathsf {E}$
-mixing implies plain mixing. For, in that case, as was shown in Remark 3.6, modulo
$\Gamma $
, any formula
$\psi $
will be provably equivalent to
$\mathsf {E}(\mathsf {n} \land \psi $
).
Remark 4.3. As will be seen below, the Mix Rule of
$\mathsf {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
$\langle !\varphi \rangle $
. But this implies the Mix Rule for arbitrary finite sequences of updates. First, the special case of
$\langle !\top \rangle \psi $
gives the case of single formulas
$\psi $
, as the two are equivalent in
MLSR
. But also, longer sequences of updates are covered, as is easy to see using the
$\mathsf {PAL}$
axiom
$\langle ! {\varphi }\rangle \langle ! {\psi }\rangle \alpha \leftrightarrow \langle ! {(\varphi \wedge [!\varphi ]\psi )}\rangle \alpha $
compressing two nested update modalities to a single one.
It follows that if a deductively closed set
$\Gamma $
is mixed, then it also witnesses sequences of announcement modalities
$\langle ! {\overline {\varphi }}\rangle $
, where
$\langle ! {\overline {\varphi }}\rangle :=\langle ! {\varphi _{1}}\rangle ...\langle ! {\varphi _{k}}\rangle $
for a sequence of formulas
. For instance, with simple mixing: if
$\langle ! {\overline {\varphi }}\rangle \langle -\alpha \rangle \psi \in \Gamma $
, then there is a nominal
$\mathsf {n}$
such that
$\langle ! {\overline {\varphi }}\rangle \mathsf {E}(\mathsf {n}\wedge \alpha )\wedge \langle ! {\overline {\varphi }}\rangle \langle !\neg \mathsf {n}\rangle \psi \in \Gamma $
.Footnote
6
Lemma 4.4 (Lindenbaum Lemma)
Every MLSR -consistent set of formulas can be extended to an MLSR maximal consistent set that is named, pasted, as well as mixed in both senses.
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
$\mathsf {E}$
-mixing. We have to ensure that, throughout the inductive construction, whenever we consistently add a formula of the form
$\mathsf {E}(\mathsf {n} \land \langle ! {\varphi }\rangle \langle -\alpha \rangle \psi )$
to a consistent, named set of formulas
$\Sigma $
, the formula
$\mathsf {E}(\mathsf {n}\land \langle ! {\varphi }\rangle (\mathsf {E}(\mathsf {k} \land \alpha ) \land \langle !\neg \mathsf {k} \rangle \psi ))$
is also added to
$\Sigma $
—where
$\mathsf {k}$
is the first nominal in the enumeration of nominals used in our construction that occurs in neither
$\Sigma $
nor
$\langle ! {\varphi }\rangle \langle -\alpha \rangle \psi $
. Crucially, for such a
$\mathsf {k}$
, the set
$\Sigma \cup \{\mathsf {E}(\mathsf {n}\land \langle ! {\varphi }\rangle (\mathsf {E}(\mathsf {k} \land \alpha ) \land \langle !\neg \mathsf {k} \rangle \psi ))\}$
is consistent, given that
$\Sigma $
is consistent. For if not, then for some conjunction
$\sigma $
of formulas from
$\Sigma $
, the implication
$\mathsf {E}(\mathsf {n}\land \langle ! {\varphi }\rangle (\mathsf {E}(\mathsf {k} \land \alpha ) \land \langle !\neg \mathsf {k} \rangle \psi )) \rightarrow \neg \sigma $
would be provable. But then, by the Mix Rule, the implication
$\mathsf {E}(\mathsf {n} \land \langle ! {\varphi }\rangle \langle -\alpha \rangle \psi ) \rightarrow \neg \sigma $
is provable from
$\Sigma $
, contradicting our initial assumption that
$\Sigma \cup \{\mathsf {E}(\mathsf {n}\wedge \langle ! {\varphi }\rangle \langle -\alpha \rangle \psi )\}$
is consistent.
For the remainder of this proof, fix a maximal consistent set
$\Gamma $
of MLSR-formulas (an
$\textsf {MLSR}$
-MCS, for short) that is named, pasted, and mixed in all the senses of Definition 4.2. Next, for all nominals
$\mathsf {n}$
with
$\mathsf {E}\mathsf {n} \in \Gamma $
define the set
$\Delta _{\mathsf {n}}:=\{\varphi \in \mathsf {MLSR}\,|\, \mathsf {E}(\mathsf {n}\land \varphi ) \in \Gamma \}$
. Let
$$\begin{align*}\mathcal{W}= \{\Gamma\}\cup \{\Delta_{\mathsf{n}}\,|\,\mathsf{n}\in\mathsf{NOM},\,\mathsf{E}\mathsf{n}\in\Gamma \}.\end{align*}$$
Over this universe, accessibility relations are defined as follows:
$$ \begin{align*} \mathcal{R}_{\Diamond}(\Delta_{\mathsf{n}}, \Delta_{\mathsf{m}}) \, &\text { iff}\ \mathsf{E}(\mathsf{n} \land \Diamond\mathsf{m}) \in \Gamma \\ \mathcal{R}_{\mathsf{E}}(\Delta_{\mathsf{n}}, \Delta_{\mathsf{m}}) \, &\text { iff } \mathsf{E}(\mathsf{n} \land \mathsf{E}\mathsf{m}) \in \Gamma. \end{align*}$$
In this definition, the set
$\Gamma $
is thought of as containing all information about the whole universe
$\mathcal {W}$
. This includes information about
$\Gamma $
itself, since, by an earlier observation,
$\Gamma = \Delta _{\mathsf {n}}$
for any nominal
$\mathsf {n}\in \Gamma $
, and such nominals exist since
$\Gamma $
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, ...$
Footnote
7
We now define an initial structure toward finding a model for our consistent set.
Definition 4.5 (Upper Henkin Model)
The upper Henkin model
$\mathcal {M}$
generated by
$\Gamma $
is defined as the structure
$(W, R_{\Diamond }, R_{\mathsf {E}}, V)$
, where
-
•
$W:= [\Gamma ]_{\mathcal {R}_{\mathsf {E}}}$
, the equivalence class of
$\Gamma $
in
$\mathcal {W}$
under
$\mathcal {R}_{\mathsf {E}}$
; -
• the relations
$R_{\Diamond }$
and
$R_{\mathsf {E}}$
are, respectively,
$\mathcal {R}_{\Diamond }$
and
$\mathcal {R}_{\mathsf {E}}$
restricted to W; -
• the valuation V is given by
$V(p) = \{w\in W\,|\,p\in w\}$
for all proposition letters p and, for all nominals
$\mathsf {n}, V(\mathsf {n}) = \{\Delta _{\mathsf {n}}\} \, \text {if }\, \mathsf {En}\in \Gamma ,\text {and } V(\mathsf {n}) = \varnothing \,\, \text {otherwise.} $
Setting the domain to be the equivalence class of
$\Gamma $
under
$\mathcal {R}_{\mathsf {E}}$
ensures that
$R_{\mathsf {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.
Lemma 4.6 (Existence Lemma)
Let
$\Gamma $
be a named, pasted and
$\mathsf {E}$
-mixed
MLSR
-MCS and
$\mathcal {M}= (W, R_\Diamond , R_{\mathsf {E}}, V)$
the upper Henkin model yielded by
$\Gamma $
.
-
• All sets
$\Delta _{\mathsf {n}}$
are
MLSR
-MCSs; -
• If
$u\in W$
and
$\Diamond \varphi \in u$
, then there is an object
$v\in W$
such that
$R_\Diamond uv$
and
$\varphi \in v$
. -
• If
$u\in W$
and
$\mathsf {E}\varphi \in u$
, then there is some
$v\in W$
such that
$R_{\mathsf {E}}uv$
and
$\varphi \in v$
. -
• All sets
$\Delta _{\mathsf {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
$\mathsf {E}$
-Mixing properties of the original set
$\Gamma $
, using principles available in
$\mathsf {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
$\mathcal {M}$
. Recall that, given a sequence
, the notation
$\langle ! {\overline {\varphi }}\rangle $
stands for
$\langle ! {\varphi _{1}}\rangle \cdots \langle ! {\varphi _{k}}\rangle $
.
Definition 4.7 (Derived Henkin Model)
For each finite sequence of
$\mathsf {MLSR}$
-formulas
, the derived Henkin model
$\mathcal {M}:\overline {\varphi }$
is the structure
$(W^{\overline {\varphi }}, R_\Diamond ^{\overline {\varphi }}, R^{\overline {\varphi }}_{\mathsf {E}}, V^{\overline {\varphi }})$
, where
-
•
$W_{\overline {\varphi }}:=\{(w,\overline {\varphi })\,|\, w\in W \text { and } \langle ! {\varphi _{1}}\rangle \cdots \langle ! {\varphi _{k}}\rangle \top \in w \}$
; -
• for
$(w, \overline {\varphi }), (v, \overline {\varphi }) \in W_{\overline {\varphi }}$
,
$R_\Diamond ^{\overline {\varphi }}\big ((w,\overline {\varphi }) , (v,\overline {\varphi })\big )$
(resp.,
$R^{\overline {\varphi }}_{\mathsf {E}}\big ((w,\overline {\varphi }) , (v,\overline {\varphi })\big )$
) if and only if
$R_{\Diamond }wv$
(resp.,
$R_{\mathsf {E}}wv$
) in the upper Henkin model
$\mathcal {M}$
; -
•
$V^{\overline {\varphi }}(p):= \{(w,\overline {\varphi })\,|\, p\in w\} $
for
$p\,{\in }\,\mathsf {PROP}$
and
$V^{\overline {\varphi }}(\mathsf {n}):= \{(w,\overline {\varphi })\,|\, \mathsf {n}\in w\} $
for
$\mathsf {n}\,{\in}\, \mathsf {NOM}$
.
Points in the derived Henkin model
$\mathcal {M}:\overline {\varphi }$
are sequences
, where w is a MCS in the upper Henkin model that contains the pre-condition formula
Footnote
8
$$\begin{align*}\mathsf{pre}(\overline{\varphi}) = \langle ! {\overline{\varphi}}\rangle\top = \langle !\varphi_{1} \rangle \cdots\langle !\varphi_{k}\rangle \top \end{align*}$$
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.
In derived Henkin models, all points are still named by nominals, but some nominals may fail to denote. This explains the modified hybrid base logic for MLSR (Remark 3.6).
Now, to each point
in the derived Henkin model
$\mathcal {M}:\overline {\varphi }$
, we associate the following set of formulas
$$\begin{align*}\Phi(\mathcal{M}, \overline{\varphi},w):=\{\alpha\,|\, \langle ! {\varphi_{1}}\rangle\cdots\langle ! {\varphi_{k}}\rangle\alpha\in w \}.\end{align*}$$
These sets record what the upper Henkin model ‘claims’ is true after the update with
$\overline {\varphi }$
. 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:
$$ \begin{align} \begin{aligned} \vdash_{\textsf{MLSR}} \langle!\varphi_1\rangle\cdots\langle!\varphi_k\rangle\top &\leftrightarrow\varphi_1\wedge \langle!\varphi_1\rangle\varphi_2 \wedge\langle!\varphi_1\rangle\langle!\varphi_2\rangle\varphi_3\wedge\cdots\wedge \langle!\varphi_1\rangle\cdots\langle!\varphi_{k-1}\rangle\varphi_k\\ &\leftrightarrow \bigwedge_{i=1}^k\langle!\varphi_1\rangle\cdots\langle!\varphi_{i-1}\rangle\varphi_i\\[-24pt] \end{aligned}\end{align} $$
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, Reference van Benthem2011).
Our second observation analyses when atomic formulas are true after iterated updates:
$$ \begin{align} \vdash_{\textsf{MLSR}} \langle!\overline{\varphi}\rangle p \leftrightarrow (\mathsf{pre}(\overline{\varphi})\wedge p) \end{align} $$
The preceding theorem also applies to nominals. A similar pattern occurs with negations:Footnote 9
$$ \begin{align} \vdash_{\textsf{MLSR}} \langle!\overline{\varphi}\rangle \neg\alpha \leftrightarrow (\mathsf{pre}(\overline{\varphi})\wedge \neg\langle!\overline{\varphi}\rangle\alpha) \end{align} $$
For conjunctions, it is easy to see that
$$ \begin{align} \vdash_{\textsf{MLSR}} \langle!\overline{\varphi}\rangle (\alpha \wedge \beta) \leftrightarrow (\langle!\overline{\varphi}\rangle\alpha \wedge \langle!\overline{\varphi}\rangle\beta) \end{align} $$
Finally, consider the diamond modality. Here we have:
$$ \begin{align} \vdash_{\textsf{MLSR}} \langle!\overline{\varphi}\rangle\Diamond\alpha \leftrightarrow (\mathsf{pre}(\overline{\varphi})\wedge \Diamond\langle!\overline{\varphi}\rangle\alpha) \end{align} $$
A similar principle holds for global existential modalities of the form E
$ \alpha $
.Footnote
10
Intuitively, the models
$\mathcal {M}:\overline {\varphi }$
are meant to be isomorphic to submodels of
$\mathcal {M}$
after the sequence of consecutive semantic updates
$ \overline {\varphi }$
, 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.Footnote
11
Now comes the main point of our construction so far.
Lemma 4.8 (Truth Lemma)
For all formulas
$\psi $
, finite sequences
$\overline {\varphi }$
and points w,
$$\begin{align*}\mathcal{M}:\overline{\varphi}, (w, \overline{\varphi}) \models \psi \,\,\, \text{if and only if } \,\,\, \psi \in \Phi(\mathcal{M}, \overline{\varphi}, w) \end{align*}$$
Proof. The proof is by induction on the formulas
$\psi $
. For convenience, when the context is clear, we write w instead of
$(w, \overline {\varphi })$
, 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, \overline {\varphi })$
in
$\mathcal {M}:\overline {\varphi }$
assumes that the precondition
$\mathsf {pre}(\overline {\varphi })$
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 \in \Phi (\mathcal {M}, \overline {\varphi }, w)$
iff
$\langle !\overline {\varphi } \rangle p \in w $
iff (by the above-noted fact (R2))
$ \mathsf {pre}(\overline {\varphi }) \land p \in 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.
(b) For negations, we have
$\neg \psi \in \Phi (\mathcal {M}, \overline {\varphi }, w)$
iff
$\langle !\overline {\varphi } \rangle \neg \psi \in w $
, which, by (R3), is provably equivalent to
$\mathsf {pre}(\overline {\varphi }) \in w$
and
$\neg \langle !\overline {\varphi } \rangle \psi \in w $
. Given that
$ \mathsf {pre}(\overline {\varphi }) \in w$
, we have that
$\langle !\overline {\varphi } \rangle \neg \psi \in w $
iff
$\langle !\overline {\varphi } \rangle \psi \notin w $
. The latter statement is equivalent to
$\psi \not \in \Phi (\mathcal {M},\overline {\varphi }, w)$
, which, by the inductive hypothesis for
$\psi $
, holds if and only if
$\mathcal {M}:\overline {\varphi },w\models \neg \psi $
.
(c) The inductive step for conjunctions
$\psi _{1} \wedge \psi _{2}$
is straightforward, using the above distribution principle (R4) of
$\langle !\overline {\varphi } \rangle $
modalities over conjunctions, as well as the fact that maximally consistent sets decompose conjunctions into components.
(d) Next, we consider the basic modality
$\Diamond \psi $
, relying on the above principle (R5).
-
• If
$\mathcal {M}:\overline {\varphi }, w \models \Diamond \psi $
, then, for some v with
$R_\Diamond ^{\overline {\varphi }}wv$
,
$\mathcal {M}:\overline {\varphi }, v \models \psi $
. So, by the inductive hypothesis,
$\psi \in \Phi (\mathcal {M}, \overline {\varphi }, v)$
. Hence, in the upper Henkin model
$\mathcal {M}$
, we have that
$\langle ! {\overline {\varphi }}\rangle \psi \in v$
and also
$R_\Diamond wv$
. This entails that, in
$\mathcal {M}$
,
$\Diamond \langle ! \overline {\varphi }\rangle \psi \in w$
. Now, using (R5) and the fact that
$\mathsf {pre}(\overline {\varphi }) \in w$
,
$\langle ! {\overline {\varphi }}\rangle \Diamond \psi \in w$
. By the definition of
$\Phi $
, then
$\Diamond \psi \in \Phi (\mathcal {M}, \overline {\varphi }, w)$
. -
• Conversely:
$\Diamond \psi \in \Phi (\mathcal {M}, \overline {\varphi }, w)$
entails that
$\langle ! {\overline {\varphi }}\rangle \Diamond \psi \in w$
in the upper Henkin model
$\mathcal {M}$
. From (R5) we obtain
$\Diamond \langle ! \overline {\varphi }\rangle \psi \in w$
. Therefore, by the Existence Lemma 4.6, there is some
$v\in \mathcal {M}$
with
$R_\Diamond wv$
and
$\langle ! {\overline {\varphi }}\rangle \psi \in v$
. Now obviously
$\vdash _{\mathsf {MLSR}}\langle ! {\overline {\varphi }}\rangle \psi \rightarrow \langle ! {\overline {\varphi }}\rangle \top = \mathsf {pre}(\overline {\varphi })$
, and so it follows that
$\mathsf {pre}(\overline {\varphi })\in v$
. Hence, v is in the derived Henkin model under consideration here. So, we have that
$\psi \in \Phi (\mathcal {M}, \overline {\varphi }, v)$
and, by the inductive hypothesis, we get
$\mathcal {M}:\overline {\varphi }, v\models \psi $
. Since
$R_\Diamond wv$
, we have
$R_\Diamond ^{\overline {\varphi }}wv$
, and so
$\mathcal {M}:\overline {\varphi }, w \models \Diamond \psi $
.
(e) The reasoning for the existential modality
$\mathsf {E}\psi $
is just like the preceding argument.
(f) The analysis for PAL modalities
$\langle ! {\alpha }\rangle \psi $
proceeds as follows.
First note that, by the inductive hypothesis, the truth of
$\alpha $
at any point
$(v, \overline {\varphi })$
is equivalent to
$\alpha $
belonging to
$ \Phi (\mathcal {M}, \overline {\varphi }, v)$
. Hence, restricting the model
$ \mathcal {M}:\overline {\varphi }$
to
$ (\mathcal {M}:\overline {\varphi })|\alpha $
in the usual semantic sense yields exactly the derived Henkin model
$ \mathcal {M}:(\overline {\varphi }^{\frown }\alpha )$
.Footnote
12
We then have the following equivalences:
$$ \begin{align*} \hspace{12pt}\mathcal{M}:\overline{\varphi}, w\models \langle ! {\alpha}\rangle\psi \quad &\text{ iff } \mathcal{M}:\overline{\varphi}, w\models\alpha \text{ and } (\mathcal{M}:\overline{\varphi}) |\alpha, w\models \psi & \\ &\text{ iff } \mathcal{M}:(\overline{\varphi}^{\frown}\alpha), w\models \psi &\\ &\text{ iff } \psi\in\Phi(\mathcal{M}, \overline{\varphi}^{\frown}\alpha , w) \hspace{26.5pt}\text{(by the inductive hypothesis)}\\ & \text{ iff } \langle ! {\alpha}\rangle\psi\in \Phi(\mathcal{M},\overline{\varphi}, w) \hspace{23.5pt}\text{(since } \langle ! {\overline{\varphi}^{\frown}\alpha}\rangle\psi = \langle ! {\overline{\varphi}}\rangle\langle ! {\alpha}\rangle\psi) \end{align*} $$
(g) Finally, the MLSR deletion modality
$\langle - {\alpha }\rangle \psi $
is analyzed as follows.
-
• If
$\mathcal {M}:\overline {\varphi }, w \models \langle - {\alpha }\rangle \psi $
, then, by the truth definition, for some
$v\neq w$
, (i)
$\mathcal {M}:\overline {\varphi }, v \models \alpha $
and (ii)
$(\mathcal {M}:\overline {\varphi })~-~\{v\}, w\models ~ \psi $
. Next, since all states in the upper Henkin model are named (see Definition 4.2), there exists a nominal
$\mathsf {n}$
denoting v, and this nominal is still available for denoting v’s descendant in the derived Henkin model
$\mathcal {M}:\overline {\varphi }$
.First consider conjunct (i). By the inductive hypothesis,
$\alpha \in \Phi (\mathcal {M}, \overline {\varphi }, v)$
, while also, for our nominal
$\mathsf {n}$
, we have
$\mathsf {n}\in \Phi (\mathcal {M}, \overline {\varphi }, v)$
. Therefore, in the upper Henkin model
$\mathcal {M}$
,
$ \langle ! {\overline {\varphi }}\rangle (\mathsf {n}\wedge \alpha )\in v $
. Now, the relation
$R_{\mathsf {E}}$
is universal in the upper Henkin model, and so, in particular,
$R_{\mathsf {E}}wv$
, which entails that
$\mathsf {E} \langle ! {\overline {\varphi }}\rangle (\mathsf {n}\wedge \alpha )\in w$
. Next, by our earlier observations about provable generalized reduction axioms in MLSR: (‡)
$$ \begin{align} \vdash_{\mathsf{MLSR}} \langle ! {\overline{\varphi}}\rangle\mathsf{E}(\mathsf{n}\wedge \alpha)\leftrightarrow \big(\mathsf{pre}(\overline{\varphi})\wedge \mathsf{E} \langle ! {\overline{\varphi}}\rangle (\mathsf{n}\wedge \alpha) \big). \end{align} $$
Together with the fact that
$\mathsf {pre}(\overline {\varphi }) \in w$
, it follows that
$\langle ! {\overline {\varphi }}\rangle \mathsf {E}(\mathsf {n}\wedge \alpha )\in w$
.Next, consider conjunct (ii) in our initial assumption. It is easy to see that the model
$(\mathcal {M}:\overline {\varphi })~-~\{v\}$
equals the updated model
$(\mathcal {M}:\overline {\varphi })| \neg \mathsf {n}$
, using the fact that each nominal belongs to at most one world in
$\mathcal {M}$
. Thus (ii) implies that
$(\mathcal {M}:\overline {\varphi })| \neg \mathsf {n}, w \models \psi $
. Moreover, it can be seen that the latter model in turn equals
$\mathcal {M}:~(\overline {\varphi } ^ \frown \neg \mathsf {n})$
.Footnote
13
Therefore, we also have
$\mathcal {M}:~(\overline {\varphi } ^ \frown \neg \mathsf {n}), w\models \psi $
. But then, by the inductive hypothesis, we have that
$\psi \in \Phi (\mathcal {M}, \overline {\varphi }^{\frown }\neg \mathsf {n}, w)$
, i.e.,
$\langle ! {\overline {\varphi }}\rangle \langle !\neg \mathsf {n} \rangle \psi \in w $
.It now remains to apply the Mix Axiom. As stated in the definition of the system MLSR, this says that the conjunction
$\mathsf {E}(\mathsf {n}\wedge \alpha )\wedge \langle ! {\neg \mathsf {n}}\rangle \psi $
implies
$\langle - {\alpha }\rangle \psi $
. Now in the upper Henkin model, we only have the antecedent for this in the set w under the prefix
$\langle !\overline {\varphi }\rangle $
. But then the modalized conclusion
$\langle !\overline {\varphi }\rangle \langle - {\alpha }\rangle \psi $
is derivable using the K axioms for the
$\langle ! {\varphi }\rangle $
modalities, and hence it, too, is in w. In other words,
$ \langle - {\alpha }\rangle \psi \in \Phi (\mathcal {M}, \overline {\varphi }, w)$
. -
• Next suppose that
$\langle - {\alpha }\rangle \psi \in \Phi (\mathcal {M}, \overline {\varphi },w )$
: i.e.,
$\langle ! {\overline {\varphi }}\rangle \langle - {\alpha }\rangle \psi \in w$
. Since w is mixed by the Existence Lemma 4.6, there exists some nominal
$\mathsf {n}$
such that (i)
$\langle ! {\overline {\varphi }}\rangle \mathsf {E}(\mathsf {n}\wedge \alpha ) \in w$
, and (ii)
$ \langle ! {\overline {\varphi }}\rangle \langle ! {\neg \mathsf {n}}\rangle \psi \in w$
. Using the earlier equivalence (‡) once more, from (i), we get
$\mathsf {E} \langle ! {\overline {\varphi }}\rangle (\mathsf {n}\wedge \alpha )\in w$
. By the Existence Lemma 4.6 once more, this means that there is some
$v\in \mathcal {M}$
with
$\langle ! {\overline {\varphi }}\rangle (\mathsf {n}\wedge \alpha )\in v$
. So,
$\mathsf {n} \wedge \alpha \in \Phi (\mathcal {M}, \overline {\varphi },v )$
. By the inductive hypothesis, this entails that
$\mathcal {M}:\overline {\varphi }, v\models \alpha $
.Next, turning to (ii), using the straightforward observation that
$\vdash _{\mathsf {MLSR}} \langle ! {\overline {\varphi }}\rangle \neg \mathsf {n} \rightarrow \neg \mathsf {n} $
, we get
$ \mathsf {n}\not \in w$
, while
$\langle ! {\overline {\varphi }}\rangle (\mathsf {n}\wedge \alpha )\in v$
entails
$\mathsf {n}\in v$
, so
$w\neq v$
.Lastly,
$ \langle ! {\overline {\varphi }}\rangle \langle ! {\neg \mathsf {n}}\rangle \psi \in w$
means
$\langle ! {\neg \mathsf {n}}\rangle \psi \in \Phi (\mathcal {M}, \overline {\varphi },w )$
. This is equivalent to
$\psi \in \Phi (\mathcal {M}, \overline {\varphi }^{\frown }\neg \mathsf {n},w )$
, which, by the inductive hypothesis, yields that
$\mathcal {M}:\overline {\varphi }^{\frown }\neg \mathsf {n}, w\models \psi $
. Next, as already noted in the argument for the converse direction,
$\mathcal {M}:(\overline {\varphi }^{\frown }\neg \mathsf {n}) = (\mathcal {M}:\overline {\varphi })|\neg \mathsf {n}$
, and hence we get
$(\mathcal {M}:\overline {\varphi })|\neg \mathsf {n}, w\models \psi $
. Moreover, we had
$(\mathcal {M}:\overline {\varphi })|\neg \mathsf {n}= (\mathcal {M}:\overline {\varphi })-\{v\}$
, and so we also have
$(\mathcal {M}:\overline {\varphi })-\{v\}, w\models \psi $
.Taking these three facts together, it can be concluded that
$\mathcal {M}:\overline {\varphi }, w\models \langle - {\alpha }\rangle \psi $
.
This concludes the proof of the Truth Lemma, and thus, the consistent set
$\Gamma $
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.Footnote 14
5 Complexity and undecidability
Having analyzed expressive power and axiomatization, we now turn to matters of computational complexity for the core notions of our system
$\mathsf {MLSR}$
as defined in §2.
5.1 Model checking
We begin by showing that model checking for
$\mathsf {MLSR}$
is PSPACE-complete. We do so by providing a reduction from the quantified Boolean formula problem (QBF) (Stockmeyer & Meyer, Reference Stockmeyer and Meyer1973), in the style of Rohde (Reference Rohde2005) and Löding & Rohde (Reference Löding, Rohde, Rovan and Vojtas2003).
Theorem 5.1. Model checking for
$\mathsf {MLSR}$
is PSPACE-complete.
The shape of the initial module (a) does not depend on which quantifier
$\varphi $
begins with. In (b), (c) and (d), the top nodes labeled by
$x_j$
and
$\neg x_j$
are the end nodes of the previous module. In (d), each clause vertex
$c_{i}$
has an outgoing edge to a vertex labeled by a literal
$\pm x_{j}$
exactly if the dual literal
$\mp x_{j}$
makes clause
$C_{i}$
true.
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
$\varphi $
: that is, a formula of the form
$$\begin{align*}Q_{1}x_{1}\,\cdots\,Q_{n}x_{n} \bigwedge_{1\leq i\leq k} C_{i}, \end{align*}$$
where
$Q_{j}\in \{\exists , \forall \}$
, and each
$C_{i}$
is a disjunction of literals
$\pm x_{j}$
(here, without loss of generality, we can assume that the quantifiers alternate between
$\exists $
and
$\forall $
).
Given such a formula
$\varphi $
, we construct a finite pointed model
$(\mathcal {M}_{\varphi }, s)$
and an MLSR formula
$\gamma _{\varphi }$
such that
$\varphi $
is true if and only if
$(\mathcal {M}_{\varphi }, s)\models \gamma _{\varphi }$
. The construction will ensure that the model
$\mathcal {M}_{\varphi }$
and the formula
$\gamma _{\varphi }$
both have a size that grows linearly in the number of quantifiers and clauses of
$\varphi $
, which gives the desired reduction from QBF.
To increase intuitive understanding, in what follows the model
$(\mathcal {M}_{\varphi }, s)$
is constructed so that the truth of
$\varphi $
can be captured by a traveling game on the model between two players: Traveler and Demon. The formula
$\varphi $
is true if and only if Traveler has a winning strategy in the traveling game on
$(\mathcal {M}_{\varphi }, s)$
, while the MLSR formula
$\gamma _{\varphi }$
states the existence of a winning strategy for Traveler.
$(\mathcal {M}_{\varphi }, s)$
consists of
$n+1$
vertically concatenated ‘modules’: one initial module for the first quantifier in
$\varphi $
, 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
$\mathcal {M}_{\varphi }$
is as follows: starting with the initial module, we concatenate successive
$\forall x_{i}$
- and
$\exists x_{j}$
-modules corresponding to the order of quantifiers in
$\varphi $
(we treat the top nodes labeled by
$x_j$
and
$\neg 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.
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
$\varphi $
starts with
$\exists $
, Traveler goes first. If
$\varphi $
starts with
$\forall $
, 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
$\forall 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.
An example. The proposition letter g marks the goal points. Each
$\forall $
-module forces Traveler to the literal
$\pm x_{j}$
point chosen by Demon, while each
$\exists $
-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
$\pm x_{j}$
that makes such clause true, Traveler can then go to the node labeled by dual literal
$\mp x_{j}$
above.
The game adequately captures the truth of
$\varphi $
:
Observation 5.2. Traveler has a winning strategy for the game on
$(\mathcal {M}_{\varphi }, s)$
if and only if the initial QBF formula
$\varphi $
is true.
Proof. Each travel path to the verification module yields a valuation. Say that a truth value is selected for
$x_{i}$
if Traveler’s path passes through the node labeled
$x_{i}$
. At
$\forall x_{i}$
modules, Demon selects a truth value for
$x_{i}$
. At
$\exists x_{j}$
modules, Traveler selects a truth value for
$x_{j}$
. Once Traveler reaches a clause node, an assignment has thus been chosen for all variables. Here, the design of the above modules guarantees the following two key facts at that stage: (i) the deleted goal points are all and only those seen by the visited vertices, and also, (ii) all unvisited
$\pm x_{i}$
vertices still have two adjacent goal points.
If
$\varphi $
is true, then the assignment chosen in this manner (with Demon controlling
$\forall $
and Traveler controlling
$\exists $
) makes all (disjunctive) clauses true. So, for every clause
$C_{i}$
, there is some visited
$\pm x_{j}$
node, for some
$\pm x_{j}$
that entails
$C_{i}$
. By design of the final clause module, no matter which clause Traveler is at, there is some unvisited vertex labeled
$\mp x_{j}$
accessible from this clause vertex. Traveler can then travel to this vertex, where she sees two goal points. Demon can remove at most one of them at her next move, and Traveler therefore wins. Conversely, if
$\varphi $
is false, the final assignment makes at least one clause false. Demon forces Traveler to the corresponding clause vertex: because the current assignment makes the disjunctive clause false, all the accessible
$\pm x_{j}$
vertices have already been visited and, thus, do not see any goal points. Demon therefore wins.
Lastly, to conclude the proof of Theorem 5.1, we make sure that MLSR can express the existence of a winning strategy for Traveler. When
$\varphi $
starts with
$\forall $
and has n quantifiers and k clauses, the general form of the corresponding MLSR formula
$\gamma _{\varphi }$
is
$$\begin{align*}\big([-\alpha_{j}]\Diamond\big)^{f(n)}[\delta]^{k-1}\Diamond^{2} [-\top]\Diamond g \end{align*}$$
Here,
$f(n)$
is a function counting the total number of rounds played in the game up to the final module: f is linear in n (it is in fact easy to see that
$f(n)\leq 3n$
). The symbol
$\alpha _{j}$
denotes
$p_{j}$
whenever Traveler sees a
$p_{j}$
-point in the corresponding
$\forall x_{j}$
-module; it stands for
$\top $
otherwise. The formula
$\delta $
, on the other hand, is a Boolean combination of
$c_{i}$
’s expressing that exactly one of the clauses is true. The repeated modalities capture exactly the structure of the game and the restrictions on the players’ moves. The game goes on for
$f(n)$
rounds until the penultimate stage is reached. The
${[-p_{j}]}$
modalities force Demon to remove only
$p_{j}$
-points during the middle round played on a
$\forall x_{j}$
-module. Then,
${[\delta ]}^{k-1}$
quantifies over all ways in which Demon can remove
$k-1$
clauses (all but one). The formula
$\gamma _{\varphi }$
expresses that Traveler can ensure that such a sequence of moves results in reaching a goal point, and thus holds exactly if Traveler has a winning strategy: equivalently, it holds if and only if the initial QBF formula
$\varphi $
is true.Footnote
15
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 & Liu, Reference van Benthem, Liu, Liu, Ono and Yu2020). 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.
5.2 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., Reference Blackburn, de Rijke and Venema2011; Marx, Reference Marx, Blackburn, van Benthem and Wolter2006), 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
$\mathcal {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
$\varphi _{\mathcal {T}}$
such that the following holds:
$$ \begin{align*} \varphi _{\mathcal {T}} \text{ is satisfiable if and only if } \mathcal {T} \text{ tiles the discrete quadrant } \mathbb {N}\times \mathbb {N}.\end{align*} $$
The formula
$\varphi _{\mathcal {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:
$$ \begin{align*} ({Func}) &&& \mathsf{U}\langle-\top \rangle (\Box_{u}\bot \wedge \Diamond_{r}\top) \\ &&& \mathsf{U}\langle-\top \rangle (\Box_{r}\bot \wedge \Diamond_{u}\top) \\ ({Conf}) &&& \mathsf{U}\langle-\top \rangle (\Diamond_{r}\Box_{u}\bot \wedge \Diamond_{u}\Box_{r}\bot ) \\ ({Unique}) &&& \mathsf{U}\Bigg(\bigvee_{1\leq i\leq n} t_i\wedge\bigwedge_{1\leq i<j\leq n} (t_i\rightarrow\neg t_j)\Bigg)\\ ({Vert}) &&& \mathsf{U}\bigwedge_{1\leq i\leq n}\Bigg(t_i\rightarrow\Diamond_u\bigvee_{1\leq j\leq n, u(T_i) = d(T_j)} t_j\Bigg)\\ ({Horiz}) &&& \mathsf{U}\bigwedge_{1\leq i\leq n}\Bigg(t_i\rightarrow \Diamond_r\bigvee_{1\leq j\leq n, r(T_i) = l(T_j)} t_j\Bigg) \end{align*} $$
(
$\Leftarrow $
) It is easy to see that any tiling of
$\mathbb {N}\times \mathbb {N}$
induces a model for
$\varphi _{\mathcal {T}}$
.
(
$\Rightarrow $
) For the other direction, suppose that
$\mathcal {M}, w\models \varphi _{\mathcal {T}}$
, for some
$\mathsf {LSR}$
-model
$\mathcal {M}=(W, R_u, R_r, V)$
and
$w\in 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]\neq 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}\circ R_{r} = R_{r}\circ R_{u}$
. This ensures the existence of an embedding
$f:\mathbb {N}^{2}\rightarrow W$
that preserves the structure of vertical and horizontal successors: that is, for all
$(n,m)\in \mathbb {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
$\mathbb {N}^{2}$
with tile
$T_{i}$
exactly if
$\mathcal {M}, f(n,m) \models 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 & Wolter, Reference Kracht and Wolter1999), 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, Mierzewski, & Areces, Reference Zaffora Blando, Mierzewski, Areces, Liu, Ono and Yu2020.
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
$\mathcal {M}$
,
$\mathcal {N}$
, it is easy to find an EXPSPACE upper bound. One considers the space of all models arising from
$\mathcal {M}$
,
$\mathcal {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 & Smolka, Reference Kanellakis and Smolka1983), one can probably do better.
6 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
$\langle - {\varphi }\rangle \psi $
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.
Theorem 6.1.
$\mathsf {MLSR(MFOL)}=\mathsf {MFOL}_{=}^{x}$
.
Proof. Fix finitely many unary predicates
$P_{1},\dots , P_{k}$
. We define standard normal forms for the whole language
$\mathsf {MFOL}_{=}$
. Local state descriptions
$sd$
are conjunctions of
$\pm P_{i}$
with
$1\leq i \leq 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
$\bigwedge _{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}$
.
Definition 6.2. An enumerative normal form is a disjunction of conjunctions
$NF$
, each consisting of (a) local state descriptions for each of the variables
$x_{i}$
plus a complete set of equalities and inequalities for all pairs of variables from
$x_{1}, ..., x_{m}$
, plus (b) a global state description that is consistent with (a) in an obvious syntactic sense.
Claim. Each formula in
$\mathsf {MFOL}_{=}$
of quantifier depth N and m free variables
$x_{1}, ..., x_{m} $
is equivalent to an enumerative normal form.
This can be proved by induction on formulas via a syntactic argument.Footnote 16
Claim.
$\mathsf {MFOL}_{=}$
is closed under the modality
$\langle - {\varphi }\rangle \psi $
.
Proof of Claim
Using the disjunction axioms for existential modalities and
$\langle - {\varphi }\rangle \psi $
stated in Section 3, in proving closure, one can restrict attention to conjunctive forms
$NF$
and special removal modalities
$\langle - {sd\wedge SD}\rangle NF$
. Closure can be shown here by a simple argument, driven by the following two key facts:
-
• the equivalence
$\langle - {sd\wedge SD}\rangle NF\leftrightarrow (SD\wedge \langle - {sd}\rangle NF)$
is valid,Footnote
17
-
• the formula
$\langle - {sd_{i}}\rangle (sd' \wedge SD$
) is equivalent to
$sd' \wedge SD[i:=i+1]$
,
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
$\mathsf {MLSR}$
to the language of modal
$\mathsf {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
$\mathsf {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?
7 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.Footnote 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.
Among the issues still to be addressed is the complexity problem for SR-bisimulation (Section 5), as well as the expressive closure problem for
$\mathsf {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
$\langle -(\varphi _1,...,\varphi _k)\rangle \psi $
or with truly polyadic operators
$\langle -\overline {\varphi }\rangle \psi $
, where the formulas
$\overline {\varphi }$
can be evaluated in a tuple of indices. These modalities seem undefinable as iterations of our unary
$\langle -\varphi \rangle \psi $
. 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., Reference Areces, Figueira, Figueira, Mera, Hodges and de Queiroz2008). 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
$\langle -\overline {\varphi }\rangle \psi $
to various first-order fragments with the natural hierarchy offered by the memory-logic perspective.Footnote
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., Reference Aucher, van Benthem and Grossi2018). Does our axiomatization technique for MLSR employing added dynamic epistemic modalities work for these logics, as well?Footnote 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, Reference Li2020). 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., Reference Andréka, Bezhanishvili, van Benthem, Németi, Alonso, Manzano and Sain2016). 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 first-order 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 (Reference Immerman1999).
Acknowledgments
We thank audiences in Amsterdam, Beijing, Gothenburg and Stanford for their comments on versions of this work, while Dazhu Li and the referee provided further useful corrections. We thank, especially, Alexandru Baltag for giving us the crucial hint toward our completeness theorem. But most of all, we are indebted to Carlos Areces for a very inspiring and pleasant collaboration during his 2018 spring stay at Stanford. Johan van Benthem was supported by the Tsinghua University Initiative Scientific Research Program, No. 2017THZWYX08.
