TAMING THE ‘ELSEWHERE’: ON EXPRESSIVITY OF TOPOLOGICAL LANGUAGES

Abstract

In topological modal logic, it is well known that the Cantor derivative is more expressive than the topological closure, and the ‘elsewhere’, or ‘difference’, operator is more expressive than the ‘somewhere’ operator. In 2014, Kudinov and Shehtman asked whether the combination of closure and elsewhere becomes strictly more expressive when adding the Cantor derivative. In this paper we give an affirmative answer: in fact, the Cantor derivative alone can define properties of topological spaces not expressible with closure and elsewhere. To prove this, we develop a novel theory of morphisms which preserve formulas with the elsewhere operator.

1 Introduction

Topology can be described as the qualitative study of space, and as such it is not surprising that it often serves as the foundation for spatial reasoning. One way to think about topological spaces is as pairs $(X,{\boldsymbol i})$ consisting of a set X and an operator ${\boldsymbol i} \colon \wp (X)\to \wp (X)$ satisfying ${\boldsymbol i} X = X$ , ${\boldsymbol i}(A\cap B) = {\boldsymbol i}A \cap {\boldsymbol i}B$ , and ${\boldsymbol i} A \subseteq A \cap {\boldsymbol i}{\boldsymbol i} A $ . The set ${\boldsymbol i} A$ is the interior of A, and the intuition is that it should not contain points on the boundary of A: if we think of A as an orange, we can think of ${\boldsymbol i}A$ as the same orange without its peel. If $A = {\boldsymbol i}A$ , we say that A is open; open sets are those that do not contain any of their boundary points. The interior operator admits a dual ‘closure’ operator, denoted, $\boldsymbol c$ , defined by ${\boldsymbol c}A = X\setminus {\boldsymbol i}(X\setminus A)$ ; if A is now the peeled orange, ${\boldsymbol c}A$ would be the original orange with its peel.

McKinsey and Tarski [14] already observed that the topological closure and interior could be used to provide semantics for modal logic. In this setting, a proposition $\varphi $ is interpreted as a region , and $\boxdot \varphi $ is interpreted as its interior (see Section 3 for formal definitions). If we moreover add a universal modality $\forall $ , where $\forall \varphi $ is true iff $\varphi $ covers the entire space X [15], then we obtain a modal framework in which all spatial relations of $\sf RCC8$ may be expressed [16]: for example, $\forall (p\to \boxdot q)$ states that the region is non-tangentially contained within the region .

However, the closure and universal modality are not the only primitive operations one can use for this style of spatial reasoning. McKinsey and Tarski [14] also noted that the Cantor derivative gives rise to an alternative interpretation of modal logic. For $A\subseteq X$ , we define ${\boldsymbol d}A$ to be the set of points $x\in X$ such that $x\in {\boldsymbol c}(A\setminus \{x\})$ ; ${\boldsymbol d}A$ is also called the set of limit points of A. Dually, we may define $x\in {\boldsymbol p}A $ if $x\in {\boldsymbol i}(A\cup \{x\}) $ : this is the set of points that have a punctured neighborhood contained in A. Modal logic based on the Cantor derivative does not validate the reflexivity property $\Box p\to p$ , making it an attractive model of belief, rather than knowledge. Logics of the Cantor derivative have been studied extensively (see e.g., [3, 4, 12]), particularly in the context of scattered spaces, which have applications to the logic of provability [1, 2, 5].

The universal modality also comes with a ‘punctured’ variant in the elsewhere, or difference, modality $[\neq ]$ [8], studied in a topological context in e.g., [7, 9]. Here, $[\neq ]\varphi $ holds on x if $\varphi $ is true in every point, aside from possibly x. There are some compelling reasons for considering the punctured variants as primitive, rather than the ‘unpunctured’ ones: for example, we may easily define $\forall \varphi := \varphi \wedge [\neq ]\varphi $ . In fact, the punctured variants are strictly more expressive.

Fig. 1 Order relations between different spatial languages: an arrow $\mathcal L\to \mathcal L'$ indicates that $\mathcal L < \mathcal L'$ . Our main result is that $\mathcal L_{\Box }\not \leq \mathcal L_{\boxdot \neq }$ , thus establishing that the diagram is complete: all reductions are already indicated in the figure.

To make this precise, note that each $M\subseteq \{\Box ,\boxdot ,[\neq ],\forall \}$ gives rise to a propositional modal language $\mathcal L_M $ . We omit set-brackets and also brackets around $\neq $ ; for example, $\mathcal L_{\Box \neq }$ denotes the language with modalities $\Box $ and $[\neq ]$ . All modalities are definable in terms of these, so it is rarely useful to consider more than two modalities at once. One question that arises when designing a language for formal topological reasoning is how the different combinations of modalities compare with respect to expressive strength.

A general analysis of the situation is given in [10] (see Section 3). In particular, it is known (and follows from the above discussion) that $\mathcal L_{\boxdot \neq }$ is reducible to $\mathcal L_{\Box \neq }$ , in the sense that any class of topologies definable in the former is already definable in the latter. Kudinov and Shehtman ask whether the reduction is strict, in the sense that converse fails. The aim of this paper is to give an affirmative answer to the latter. In fact, we show that already $\mathcal L_\Box $ cannot be reduced to $\mathcal L_{\boxdot \neq }$ .

We prove this by considering a variant of the local $1$ -componency property, which states that if $x\in U$ and U is open, then there is a neighborhood $N\subseteq U$ of x such that $N\setminus \{x\}$ is connected. This property holds on e.g., $\mathbb R^2$ but not on $\mathbb R$ , and it implies the validity of the formula ${\textrm {Kur}}:=\Box (\boxdot p\vee \boxdot \neg p)\to \Box p \vee \Box \neg p$ . Kudinov [9] showed that ${\textrm {Kur}}$ itself is definable in $\mathcal L_{\boxdot \neq }$ , in the sense that there is a formula ${\textrm {Kur}}_{\boxdot \neq } $ of this language such that for any topological space X, $X\models {\textrm {Kur}}$ if and only if $X\models {\textrm {Kur}}_{\boxdot \neq }$ . However, in Section 7 we also show that a mild variant of this property, $\Box {\textrm {Kur}}$ , is not definable in terms of $\boxdot $ and $[\neq ]$ . Intuitively, $\Box {\textrm {Kur}}$ states that local $1$ -componency may only fail on a discrete set of points. To prove that this formula is not expressible in $\mathcal L_{\boxdot \neq }$ , in Section 6 we first introduce a new notion of morphism for the difference modality.

A global variant of $1$ -componency can also be considered; the space X is globally $1$ -component if for any $x\in X$ , $X\setminus \{x\}$ is connected. Kudinov and Shehtman also exhibit a variant of $\rm Kur$ which holds on globally $1$ -connected spaces, and use it to separate the $\mathcal L_{\boxdot \neq }$ logics of the real line and the circle $\mathbb S^1$ . They also claim that every $\mathcal L_{\boxdot \forall }$ formula valid on the real line is valid on the circle, but this does not seem to follow immediately from their argument, so in Section 5 we provide a detailed proof. This completely settles all reducibility relations between the languages considered (see Figure 1).

2 Topological spaces

In this section we briefly recall some background from topology, particularly the notion of Cantor derivative on a topological space.

Definition 2.1 (topological space)

A topological space is a pair $(X,\tau )$ , where X is a set and $\tau $ is a subset of $\wp (X)$ that satisfies the following conditions:

• • $X,\varnothing \in \tau $ ;

• • if $U,V\in \tau $ , then $U\cap V\in \tau $ ;

• • if $\mathcal {U}\subseteq \tau $ , then $\bigcup \mathcal {U}\in \tau $ .

The elements of $\tau $ are called open sets, and the complement of an open set is called a closed set.

We will notationally identify X with $(X,\tau )$ , which in this paper will not lead to ambiguity as all topologies we consider come from the Euclidean spaces $\mathbb R^n$ or their subspaces. Perhaps the most familiar example of a topological space is the real line $\mathbb R$ , where $U\subseteq \mathbb R$ is open iff it is a (possibly infinite) union of intervals of the form $(a,b)$ . More generally, each space $\mathbb R^n$ comes with a topology where U is open iff whenever $x\in U$ , there is $\varepsilon>0$ such that $\|x-y\|<\varepsilon $ implies that $y \in U$ (where $\|\cdot \|$ is the standard Euclidean norm). Each space $\mathbb R^n$ is connected: recall that if X is a topological space and $C\subseteq X$ , we say that C is connected if whenever $C\subseteq A\cup B$ with $A,B$ disjoint and open, it follows that $C\cap A =\varnothing $ or $C\cap B = \varnothing $ .

If $X,Y$ are topological spaces, a function $f\colon X\to Y$ is continuous if $f^{-1}(B)$ is open whenever $B\subseteq Y$ is open, and open if $f (A)$ is open whenever $A\subseteq X$ is open. A continuous and open map is an interior map.

The fundamental operation on topological spaces we are interested in is the Cantor derivative.

Definition 2.2 (Cantor derivative)

Let $ (X,\tau )$ be a topological space. Given $S\subseteq X$ , the Cantor derivative ${\boldsymbol d} $ of S is the set ${\boldsymbol d} S $ of all limit points of S, i.e., $ x\in {\boldsymbol d} S $ if and only if, whenever $x\in U\in \tau $ , it follows that $ (U\cap S)\backslash \{x\}\neq \varnothing $ .

Given $A,B\subseteq X$ , it is not hard to check that the Cantor derivative satisfies ${\boldsymbol d} \varnothing =\varnothing $ , ${\boldsymbol d}(A\cup B)= {\boldsymbol d} A \cup {\boldsymbol d} B $ , and ${\boldsymbol d}{\boldsymbol d} A \subseteq A\cup {\boldsymbol d} A $ . The topological closure of $A\subseteq X$ can then be defined as ${\boldsymbol c}A = A \cup {\boldsymbol d}A$ , or, directly, as the intersection of all closed sets containing A. Both the Cantor derivative and topological closures admit duals, the punctured interior given by ${\boldsymbol p}A = X\setminus {\boldsymbol d}(X\setminus A)$ and the interior ${\boldsymbol i}A = X\setminus {\boldsymbol c}(X\setminus A)$ . The latter is also definable as the union of all open sets contained in A, while the former has the property that $x\in {\boldsymbol p}A$ iff there is some open set U such that $x\in U\subseteq A\cup \{x\}$ . We say that A contains a punctured neighborhood of x.

3 Topological languages and reducibility

All languages we consider will be subsets of the full topological language $\mathcal L_*$ given by the following syntax in Backus–Naur form:

$$ \begin{align*}\varphi,\psi :: = \ p \ \mid \ \neg \varphi \ \mid \ \varphi\wedge\psi \ \mid \ \Box \varphi\ \mid \ \boxdot \varphi \ \mid \ [{\neq}]\varphi\ \mid \ \forall \varphi.\end{align*} $$

Sublanguages are indicated with allowed modalities as subindices. We are mostly concerned with $\mathcal L_\Box $ and $\mathcal L_{\boxdot {\neq }}$ (we omit brackets around $\neq $ ). As usual, we use $\Diamond $ as a shorthand for $\neg \Box \neg $ , $\exists $ as a shorthand for $\neg \forall \neg $ , and $\langle \neq \rangle $ as a shorthand for $\neg [\neq ]\neg $ .

Definition 3.1. A topological model is a pair where X is a topological space and is a valuation function assigning a subset of X to each formula of $\mathcal L_*$ , satisfying the following recursive clauses:

• • ,

• • ,

• • ,

• • ,

• • ,

• • if , otherwise .

Equivalently, we can write ; in this way, it becomes evident that $[\neq ]$ is a ‘punctured’ version of $\forall $ , much as $ \boldsymbol p$ is a punctured version of $\boldsymbol i$ . Note that, dually, if and only if there is $x'\neq x$ such that . We write $(\mathfrak M,x)\models \varphi $ if , and $\mathfrak M\models \varphi $ if . Similarly, $X\models \varphi $ if for every valuation on X, and $(X,x)\models \varphi $ if for every valuation . We may write instead of when working with more than one topological space.

The general type of question we are concerned with is: Given $\mathcal L,\mathcal L'\subseteq \mathcal L_*$ , is $\mathcal L'$ reducible to $\mathcal L $ ? Intuitively, $\mathcal L'$ is reducible to $\mathcal L $ if every $\mathcal L'$ -definable class of spaces is also $\mathcal L$ -definable. Let us make this precise.

Definition 3.2. Given $\varphi \in \mathcal L_*$ , let $\mathcal C(\varphi )$ be the class of all topological spaces X such that $X\models \varphi $ . Say that a class of spaces $\Omega $ is definable in $\mathcal L \subseteq \mathcal L_*$ if there is $\varphi \in \mathcal L$ such that $\Omega = \mathcal C(\varphi )$ , and similarly, say that a formula $\psi $ is definable in $\mathcal L$ if there is $\psi '\in \mathcal L$ such that $\mathcal C(\psi ') = \mathcal C(\psi )$ .

Then, write $\mathcal L'\leq \mathcal L $ if every $\varphi \in \mathcal L'$ is definable in $\mathcal L $ , and $\mathcal L'<\mathcal L$ if $\mathcal L'\leq \mathcal L$ but $\mathcal L\not \leq \mathcal L'$ . In this case, we say that $\mathcal L'$ is (strictly) reducible to $\mathcal L$ .

Equivalently, $\mathcal L'\leq \mathcal L $ if every class that is definable in $\mathcal L'$ is also definable in $\mathcal L$ . Kudinov and Shehtman [10] give an overview of the known facts about reducibility between sublanguages of $\mathcal L_*$ . The general picture is represented in Figure 1. The non-strict inclusions all follow from the definability of $\boxdot $ as $\boxdot \varphi :=\varphi \wedge \Box \varphi $ , and $\forall $ as $\forall \varphi := \varphi \wedge [\neq ]\varphi $ . Languages obtained by adding $\forall $ to $\Box $ or $\boxdot $ are more expressive because e.g., $\forall $ is needed to define connectedness [15]. That no language with $\Box $ is reducible to one without $\Box $ follows from results in the current paper, but was already known for languages without $\neq $ since $\mathcal L_\boxdot $ cannot distinguish between $\mathbb R$ and $\mathbb R^2$ [14] but $\mathcal L_\Box $ can [10, 13].

4 Kuratowski formulas and $1$ -Componency

Classes of spaces that cannot be distinguished by the ‘reflexive’ modalities $\boxdot $ and $\forall $ can sometimes be disgintuished by variants of the Kuratowski formula. For example, the $\mathcal L_\Box $ -logics of $\mathbb R$ and $\mathbb R^2$ differ because $\mathcal L_\Box $ contains a formula valid on locally $1$ -component spaces. If X is a topological space, $x\in X$ is locally $1$ -component if for every neighborhood U of x there is a neighborhood $N \subseteq U$ of x such that $N\setminus \{x\}$ is connected. The space X is locally $1$ -component if every point of X is locally $1$ -component. It is well known and easy to see that $\mathbb R^2$ is locally $1$ -component, but $\mathbb R$ is not.

Locally $1$ -component spaces validate the Kuratowski formula

$$ \begin{align*}{\textrm{Kur}}:= \Box(\boxdot p\vee\boxdot \neg p) \to \Box p \vee\Box \neg p\end{align*} $$

[11]. This is also well known, but since this is an important element in our own results, we provide a proof.

Lemma 4.1. Let X be any topological space and $x\in X$ . Then, if x satisfies local $1$ -componency, it follows that $(X,x) \models \rm Kur$ .

Proof. Assume that x satisfies local $1$ -componency. To show that $(X,x) \models \rm Kur$ , assume moreover that is a valuation such that . Then, x has a neighborhood U such that ; by local $1$ -componency, we may assume that $U\setminus \{x\}$ is connected (otherwise, choose a suitable $U'\subseteq U$ ). Then, . Since these two sets are open and disjoint and $U\setminus \{x\}$ is connected, we either have that and , or and . Either way, .

Kudinov and Shehtman [10] use this example to show that Since $\mathbb R^2$ is locally $1$ -component, we obtain $\mathbb R^2\models \rm Kur$ . On the other hand, $\mathbb R\not \models \rm Kur$ , which can be seen by setting ; then, it is readily checked that $(\mathbb R,0)\models \Box (\boxdot p\vee \boxdot \neg p) $ but $(\mathbb R,0)\not \models \Box p $ because points to the left of $0$ do not satisfy p, while $(\mathbb R,0)\not \models \Box \neg p $ because points to the right do not satisfy $\neg p$ . Conversely, since there is a surjective, interior map $\pi \colon \mathbb R^2\to \mathbb R$ given by projecting onto the first component, it follows that every formula of $\mathcal L_\boxdot $ valid on $\mathbb R^2$ is also valid on $\mathbb R$ , and hence $\mathcal L_\boxdot <\mathcal L_\Box $ .

Kudinov and Shehtman also point out that $\mathcal L_{\boxdot \neq } \leq \mathcal L_{\Box \neq }$ , but leave open whether $\mathcal L_{\boxdot \neq }< \mathcal L_{\Box \neq }$ . One strategy that comes to mind is to show that the class of spaces validating $\rm Kur$ is not definable in $\mathcal L_{\boxdot \neq }$ . However, this idea would not quite work, since Kudinov [9] exhibits an $\mathcal L_{\boxdot \neq }$ -formula that is valid on the same class of spaces as $\rm Kur$ . Nevertheless, we will see in Section 7 that a slight modification of $\rm Kur$ will do the trick.

A global version of $1$ -componency can also be defined. We say that $x\in X$ is globally $1$ -component if $X\setminus \{x\}$ is connected, and say that X is globally $1$ -component if every $x\in X$ is globally $1$ -component. It is easy to see that the circle is globally $1$ -component but the real line is not. Globally $1$ -component spaces satisfy a version of the Kuratowsky formula, defined by

$$ \begin{align*}{\textrm{Kur}}_{\neq} : = [\neq](\boxdot p\vee\boxdot \neg p) \to [\neq] p \vee [\neq]\neg p.\end{align*} $$

The following is then verified along the lines of Lemma 4.1:

Lemma 4.2. Let X be any topological space and $x\in X$ . Then, if x satisfies global $1$ -componency, it follows that $(X,x) \models {\mathrm {Kur}}_{\neq }$ .

Since the circle $\mathbb S^1$ is globally $1$ -component, it follows that $\mathbb S^1\models {\mathrm {Kur}}_{\neq }$ . The same valuation we used for $\mathrm{Kur}$ shows that $\mathbb R\not \models {\mathrm {Kur}}_{\neq }$ , and thus the $\mathcal L_{\boxdot \neq }$ logic of the circle is different from that of the real line.

5 The circle and the line

Using the formula ${\mathrm {Kur}}_{\neq }$ , Kudinov and Shehtman [10] conclude that $\mathcal L_{\Box \forall }<\mathcal L_{\Box \neq } $ by claiming that every $\mathcal L_{\Box \forall }$ -formula satisfiable on $\mathbb R$ is also satisfiable on $\mathbb S^1$ . Their argument is that there is a surjective local homeomorphism $f\colon \mathbb R\to \mathbb S^1$ given by $f(x) = \big ({\cos (x)},{\sin (x)}\big )$ ; however, this fact alone only shows that every formula valid on the real line is valid on the circle. In this section we fill this gap by providing a detailed, if somewhat ad hoc, proof.

Our proof is based on the following observation about the topology on the real line. Given $x\in \mathbb R$ and $A\subseteq \mathbb R$ , say that x is a limit point of A from the left (or left limit of A for short) if for every $\varepsilon>0$ there is $a\in A$ such that $x-\varepsilon <a<x$ . Similarly, x is a right limit of A if for every $\varepsilon>0$ there is $a\in A$ such that $x <a<x+\varepsilon $ .

Lemma 5.1. If $A\subseteq \mathbb R$ is uncountable, then there is $x\in A$ such that x is both a left limit and a right limit of A.

Proof. First we note that there are only countably many elements of A which are not left limits, since for every such $a\in A$ we can find $\varepsilon>0$ with $A\cap (a-\varepsilon ,a) = \varnothing $ , hence using the density of the rationals we can choose $q_a\in \mathbb Q\cap (a-\varepsilon ,a)$ . The assignment $a\mapsto q_a$ is readily seen to be injective, and since $\mathbb Q$ is countable, we conclude that only countably many points of A can fail to be left limits. By the same argument, only countably many points of A can fail to be right limits, so that uncountably many points of A must be both left and right limit points of A.

Next we fix a finite set $ \Sigma \subseteq \mathcal L_{\Box \forall }$ closed under subformulas. Our goal is to show that any formula of $\Sigma $ that is satisfiable on the real line is also satisfiable on the circle. This would normally require a surjective interior map ¹ $\pi \colon \mathbb S^1\to \mathbb R$ , but no such map exists. Instead, we will use properties of the real line to ‘fudge’ the requirements on $\pi $ a bit.

Theorem 5.2. Any formula of $\mathcal L_{\Box \forall }$ satisfiable on $\mathbb R$ is also satisfiable on the circle.

Proof. Let $\varphi \in \mathcal L_{\Box \forall }$ and be any valuation on $\mathbb R$ such that . Let $\Sigma $ be the set of subformulas of $\varphi $ , and for $x\in X$ define .

Choose N large enough so that whenever $\psi \in \Sigma $ and , it follows that ; such an N exists since $\Sigma $ is finite. We claim that there is a set $\Sigma _\ell \subseteq \Sigma $ such that there are uncountably many $x<-N$ with $\Sigma (x) = \Sigma _\ell $ ; this follows readily from the fact that $\Sigma (x)$ can take only finitely many values and $(-\infty ,-N)$ is uncountable. Let $A_\ell = \{x<-N: \Sigma (x) = \Sigma _\ell \}$ . Using Lemma 5.1, choose $x_\ell \in A_\ell $ such that $x_\ell $ is both a left and right limit of $A_\ell $ . Similarly, choose $\Sigma _r$ such that $A_r := \{x>N: \Sigma (x) = \Sigma _r\}$ is uncountable, and let $x_r\in A_r$ be both a left and right limit of $A_r$ .

By scaling if necessary, we may assume that $x_\ell =-1 $ and $x_r= 1 $ (so that also ${N<1}$ ). We may also identify the circle $\mathbb S^1$ with $\{(x,y)\in \mathbb R^2:x^2+y^2=1\}$ , and define $\pi (x,y) = x$ . Finally, define .

We claim that for all $\psi \in \Sigma $ and $(x,y)\in \mathbb S^1$ , if and only if . This concludes the proof, given that there is $x\in [-N,N] $ with , so $\varphi $ is satisfiable on $\big (\mathbb S^1, (x,\sqrt {1-x^2}) \big )$ .

The claim follows by induction on the build of $\psi $ . The case for $\psi =p$ is immediate, as are the Boolean cases. Consider $\psi =\exists \theta $ . If , then there exists $z \in \mathbb R$ such that , and by our choice of N we may assume that $z\leq N$ . Thus the induction hypothesis yields and hence . Conversely, if , then there is , so that by the induction hypothesis.

The most interesting case is that for $\psi =\Diamond \theta $ . First assume that $|x|<1$ . Then, $\pi $ is a local homeomorphism near $(x,y)$ , and standard arguments show that if and only if . So we assume that $|x|=1$ (hence $y=0$ ). For simplicity we further assume that $x=1$ , with the case for $x=-1$ being symmetric.

If , we let U be any neighbourhood of $1$ . Then, $\pi ^{-1}[U]$ is a neighbourhood of $(1,0)$ , so that there is $(x',y') \in \pi ^{-1}[U]$ with . Note that $x'\neq 1$ (since $(1,y) \in \mathbb S^1 $ implies that $y=0$ ), and the induction hypothesis implies that . Since U was arbitrary, .

Conversely, assume that and let V be any neighbourhood of $(1,0)$ . By the geometry of the circle, there is $\varepsilon>0$ such that if $(x',y') \in \mathbb S^1$ and $ 1-\varepsilon <x'$ , then $(x',y') \in U$ . By assumption, we have that $ \Sigma (1) = \Sigma _ r $ , and $1 $ is a limit of $A_r$ from the left. Hence there is $x' \in A_r$ such that $1-\varepsilon <x'<1$ . Since $x'\in A_r$ , we have that $\Diamond \theta \in \Sigma (x')$ , i.e., . Since $(1-\varepsilon ,x')$ is a neighbourhood of $x' $ , there is $z\in (1-\varepsilon ,x')$ with . The induction hypothesis yields , and since $z>1-\varepsilon $ we have that $(z,\sqrt {1-z^2}) \in V$ . Moreover, $z<1$ , so $(z,\sqrt {1-z^2}) \neq (1,0)$ . Since V was arbitrary, we conclude that , as required.

We conclude that $\mathcal L_{\boxdot \neq } \not \leq \mathcal L_{\Box \forall }$ , and thus $\mathcal L_{\Box \forall } < \mathcal L_{\Box \neq }$ . Note that our argument relies heavily on properties of the circle and the real line. In contrast, the next section provides a rather general treatment for showing that validity for formulas with $\neq $ is preserved between topological spaces.

6 Morphisms for the difference modality

The semantic clauses for $\neq $ are preserved by bijections, in the following sense. Suppose that $f\colon X\to Y$ is a bijection and p is a variable, and , are valuations on the respective spaces satisfying . Then, given $x\in X$ , iff . In general, if f fails to be surjective it is easy to find counterexamples to the latter equivalence. However, if f is surjective but fails to be injective, the only way to have but is if $f(x)$ is the only point of Y satisfying p and, moreover, there is $x'\neq x$ such that $f(x') = f(x)$ . In this case we say that $f(x)$ is p-unique (and x is not). It suffices for f to be injective with respect to unique points for it to preserve the semantic conditions for $\langle \neq \rangle $ (and hence $[\neq ]$ ): below, we make this precise.

Definition 6.1. Let X, Y be topological spaces and $U\subseteq Y$ . Say that $f\colon X\to Y$ is U-injective if for each $u\in U$ , $f^{-1}(u)$ is a singleton. If f is interior, surjective and U-injective, we say that f is a U-morphism.

Let be a topo-model, $\Sigma $ a set of formulas. For a formula $\varphi $ , say that $y\in Y$ is $\varphi $ -unique if , and $\Sigma $ -unique if it is $\varphi $ -unique for some $\varphi \in \Sigma $ . Let ${\textrm {U}}(\Sigma )$ be the set of $\Sigma $ -unique points. We define a $\Sigma $ -morphism to be a ${\textrm {U}}(\Sigma )$ -morphism.

Recall that any function $f\colon X\to Y$ defines a valuation on X by setting and extending recursively to complex formulas.

Lemma 6.2. If $\Sigma \subseteq \mathcal L_{\boxdot \neq }$ is closed under subformulas and single negations and $f\colon X\to Y$ is a $\Sigma $ -morphism, then for every $\varphi \in \Sigma $ , .

Proof. Induction on formulas, with only the case for $[{\neq }]\varphi $ being non-standard. If , there is $y'\neq f(x)$ such that . Since f is surjective, $y'=f(x')$ for some $x'\in X$ , which since f is a function satisfies $x'\neq x$ . By the IH , so .

For the other direction, if , let ; we must prove that $x ' = x$ to conclude that . Note that if it follows that $f(x) = y$ , given that . By the induction hypothesis, , which by the above yields . Thus , and $f(x)$ is $\neg \varphi $ -unique. But, $f $ is $\Sigma $ -injective, so $f(x) = f(x')$ yields $x = x'$ , as required.

Note that if $\Sigma $ is finite, there can be only finitely many $\Sigma $ -unique points. This will allow us to give a criterion for when, given any valuation on Y, there is a $\Sigma $ -morphism $f\colon X\to Y$ . Below, we write $A \subseteq _{\textrm {fin}} B$ to indicate that A is a finite subset of B.

Definition 6.3. If $X,Y$ are topological spaces, we write $X\gg Y$ if for every $U \subseteq _{\textrm {fin}} Y$ there is a surjective, U-injective interior map $f\colon X\to Y$ .

It is easy to check that if $\Sigma $ is finite and $X\gg Y$ , then for any valuation on Y there is a $\Sigma $ -morphism $f\colon X\to Y$ . It follows that if $X\gg Y$ , then every $\mathcal L_{\boxdot \neq }$ -formula valid on X is valid on Y.

Lemma 6.4. Define

$$ \begin{align*} \mathbb X = \{(x,y) \in \mathbb R^2 : |y| \leq |\sin(x)|\}\end{align*} $$

(see Figure 2). Then, every formula of $\mathcal L_{\boxdot \neq }$ valid on $\mathbb X$ is valid on $\mathbb R$ .

Fig. 2 The space $\mathbb X$ looks like the shadow of an infinite braid.

Proof. It suffices to check that $\mathbb X\gg \mathbb R $ . Let $U\subseteq _{\textrm {fin}} \mathbb R$ . Without loss of generality, we may assume that U consists of multiples of $\pi $ ; otherwise, apply a homeomorphism g to $\mathbb R$ so that $g(U)$ consists of multiples of $\pi $ , which is possible since U is finite. Let $f\colon \mathbb X\to \mathbb R$ be given by $f(x,y) = x$ . Then f is clearly a surjective interior map, and it is U-injective because if $x \in U$ then x is a multiple of $\pi $ , so $\sin (x) = 0$ and $f^{-1} (x) = \{(x,0)\}$ . It follows that any $\mathcal L_{\Box \neq }$ -formula valid on $\mathbb X$ is valid on $\mathbb R$ .

Remark 6.5. Unlike other notions of topological morphisms, the relation $X\gg Y$ is not witnessed by a single map, but rather, the existence of a suitable map $f_U$ for each finite $U\subseteq Y$ . However, it is possible to gather these maps into a single object $(f_U)_{U\subseteq _{\textrm {fin}} Y}$ , and view the latter as a form of topological morphism tailored for logics with $\neq $ . We will call such collections of functions $\neq $ -morphisms.

7 A $\mathcal L_{\boxdot \neq }$ -undefinable property

Recall that $ {\mathrm {Kur}} = \Box (\boxdot p\vee \boxdot \neg p ) \to (\Box p \vee \Box \neg p) $ is the Kuratowski formula [11], and is valid on locally $1$ -component spaces by Lemma 4.1. Note that ${\mathrm {Kur}}$ is expressible in $\mathcal L_{\Box }$ , since $\boxdot $ is definable in terms of $\Box $ . Our space $\mathbb X$ does not validate $\mathrm{Kur}$ , but it does validate an approximate version.

Lemma 7.1. $\Box {\mathrm {Kur}}$ is valid on $\mathbb X$ but not on $\mathbb R$ .

Proof. Let be any valuation on $\mathbb X$ . To see that it validates $\Box {\mathrm {Kur}}$ , note that if $(x,y) \in \mathbb X$ , then any small-enough neighbourhood N of $(x,y)$ has the property that if $(x', y') \in N\setminus \{(x,y)\}$ , then $x'$ is not a multiple of $\pi $ . But it is easy to see that any small-enough punctured ball around $(x', y')$ is connected (see Figure 2), so , and thus N witnesses that .

To see that $\Box {\mathrm {Kur}}$ is not valid on $\mathbb R$ , let be such that

Then, any punctured neighborhood U of $0$ contains a point of the form $x = 2^{-2n-1 }$ for large-enough n. But $N = (2^{-2n-2 }, 2^{-2n })$ is a neighborhood of x, and all points in N to the right of x satisfy p, hence $\boxdot p$ , and all points in N to the left of x satisfy $\neg p$ , hence $\boxdot \neg p$ . Thus . However, neither nor , so . Since U was arbitrary, it follows that .

However, by Lemma 6.4, we have that any $\mathcal L_{\boxdot \neq }$ -formula valid on $\mathbb X$ is also valid on $\mathbb R$ , so no $\mathcal L_{\boxdot \neq }$ -formula defines the same class of spaces as $ \Box {\mathrm {Kur }}$ . We thus obtain the following.

Theorem 7.2. The language $\mathcal L_\Box $ is not reducible to $\mathcal L_{\boxdot \neq }$ .

As a corollary, we obtain that $\mathcal L_{\boxdot \neq }<\mathcal L_{\Box \neq }$ .

8 Concluding remarks

We have closed the most prominent question left open by [10] in the comparison of topological modal languages by establishing that $\mathcal L_{\boxdot \neq }<\mathcal L_{\Box \neq }$ : in fact, we showed that $\mathcal L_{\Box }\not \leq \mathcal L_{\boxdot \neq }$ . We also closed a gap in the proof that $\mathcal L_{\boxdot \neq } \not \leq \mathcal L_{\Box \forall }$ . However, our main contribution is arguably a notion of topological morphism which preserves formulas with the difference modality. Unlike related morphisms for similar languages, preservation of formulas with $[\neq ]$ requires not only one map, but a family of maps indexed by the finite subsets of the codomain.

One interesting line of inquiry opened by $\neq $ -morphisms is that of succinctness: Fernández-Duque and Iliev [6] show that despite being less expressive, $\mathcal L_\boxdot $ is more succinct than $\mathcal L_\Box $ for certain formulas. Similar results could hold for $\mathcal L_{\boxdot \neq }$ vs. $\mathcal L_{\Box \neq }$ , and would require a refined notion of $\neq $ -morphisms.

Finally, we remark that interior maps do not always preserve formulas with $\Box $ : more restrictive maps, sometimes called $\boldsymbol d$ -morphisms, are needed. By combining $\boldsymbol d$ -morphisms with $\neq $ -morphisms, it would be possible to exhibit classes of spaces which are not distinguished by $\mathcal L_{\Box \neq }$ , thus establishing non-trivial limitations for the expressive power of the full topological modal language.