On Modal Logics of Connectedness in Metric Spaces
January 01, 1970
Abstract
For a positive number \(a\), each metric space carries the relation \(D_a\) consisting of those pairs that are of distance less than \(a\) apart. A space \(X\) is said to be \(a\)-connected, if the graph \((X,D_a)\) is connected (that is, there is a \(D_a\)-path between every pair of points in \(X\)). We give a complete axiomatization of \(a\)-connected metric spaces in the language with a family of distance modalities and the universal modality. Then we give a complete axiomatization of the logic of connected (in the classical topological sense) metric spaces in the language with the topological modality, universal modality, and a single distance modality. We also show that these logics have the finite model property.
1 Introduction↩︎
Let \((X,d)\) be a metric space, which we usually refer to as simply \(X\). There is a natural way to associate a relational structure, or Kripke frame, with \(X\). For each real number \(r>0\) define a relation \(D_r\) on \(X\) by setting \[x\,D_r\, y\,\,\Leftrightarrow\,\, d(x,y)<r.\] This allows us to interpret in \(X\) modal formulas with the corresponding distance modalities \(\lozenge_r\). We can also consider the topological closure operation of \(X\), which allows us to interpret in \(X\) modal formulas with the closure modality \(\lozenge\).
The situation described is the general setting of [@Kutz-Sturm-Suzuki-Wolter-Zakharyaschev2002; @Kutz-Sturm-Suzuki-Wolter-Zakharyaschev2003; @Wolter2005; @KuruczWZ05; @Kutz2007]. In this series of papers, numerous results were established related to the axiomatizability and decidability of modal logics of metric spaces with different families of operators. For instance, the axiomatization of the logic of all metric spaces with distance modalities \(\lozenge_r\) for each \(r>0\) is given by the family of axioms for all \(r,s>0\) [@Wolter2005]:
\(p\,\to\,\lozenge_r p\)
\(p\,\to\,\Box_r\lozenge_rp\)
\(\lozenge_r\lozenge_s p\to\,\lozenge_{r+s} p\)
The first axiom says that for a subset \(P\) of a metric space, we have \(P\) is contained in the set of points of distance less than \(r\) from \(P\); the second expresses the symmetry of the metric; and the third comes from the triangle inequality.
In this paper, we are interested in modal logics of connected metric spaces. More precisely, we consider two forms of connectedness: in the usual topological sense, and in a weaker sense of connectedness of the graph \((X,D_a)\) for some fixed positive \(a\). We address the latter property as \(a\)-connectedness, which means that there is a \(D_a\)-path between every pair of points in \(X\).
It is known that connectedness of a topological space is expressed in the language with the closure and universal modalities by the formula \[\label{eq:intro-conn} \exists p \wedge \exists\neg p \to\exists(\lozenge p\wedge \lozenge\neg p)\tag{1}\] and moreover, a complete axiomatization of the class of all connected spaces is the logic \(\mathrm{S4UC}\), the extension of \(\mathrm{S4}\) with the axioms of universal modality and the above formula [@Shehtman99]. The axiomatization of connected metric spaces in the language of the topological closure \(\lozenge\), universal modality, and distance modalities is an open problem [@Wolter2005; @KuruczWZ05]. We make partial progress in this direction, providing the following two completeness results.
For a given positive \(a\), we identify an axiomatization of \(a\)-connectedness in the language without topological closure, with the universal modality, and with any set of distance modalities \(\lozenge_r\) containing \(\lozenge_a\).
We give an axiomatization of topological connectedness in the language of closure \(\lozenge\), universal modality, and a single distance modality \(\lozenge_r\).
We also show that these logics have the finite model property and, in the case of a finite language, are decidable.
The paper is organized as follows. Syntactic and semantic conventions are given in Section 2. In Section 3, we prove the finite model property theorem, one of the ingredients of the completeness proofs. In Section 4, we give the axiomatization of \(a\)-connected spaces, and the result for topological connectedness is given in Section 5.
2 Logics and models↩︎
2.1 Language↩︎
Let \({\mathrm A}\) be a set of positive real numbers (parameters), which will also be considered as indices of modalities. An \({\mathrm A}\)-logic is a normal modal logic with modalities \(\{\lozenge_a\mid a\in{\mathrm A}\}\cup\{\exists\}\), and an \(({\mathrm A},\lozenge)\)-logic is a logic in this language endowed with \(\lozenge\), where \(\exists\) and \(\lozenge\) are two fresh symbols. We write \(\forall\) for the abbreviation \(\neg\, \exists\, \neg\). In relational or topological spaces, \(\exists\) will be interpreted as “somewhere”, that is, formally, via the universal relation. In topological spaces, \(\lozenge\) will be interpreted as the operation of closure.
For a logic \(L\) and a formula \(\varphi\), the smallest logic containing \(L\cup\{\varphi\}\) is denoted as \(L+\varphi\).
2.2 Axioms↩︎
Let \({\vec{r}}=(r_1,\ldots,r_m)\) be a tuple of parameters. We write \(\lozenge_{{{\vec{r}}}}\) for the compound modality \(\lozenge_{r_1}\ldots \lozenge_{r_m}\), and \(\oplus{{\vec{r}}}\) for \(r_1+\ldots+r_m\). We put \(\oplus{{\vec{r}}}=0\) for the empty \({\vec{r}}\).
Definition 1. We define \(\mathrm{Metr}{({\mathrm A})}\) as the smallest normal \({\mathrm A}\)-logic that, for each \(r\in {\mathrm A}\), contains the formulas
(i) \(p\to\forall\exists p\), \(p\to\exists p\), \(\exists\exists p \to\exists p\), and \(\lozenge_r p\to\exists p\);
(ii) \(p\to\Box_r \lozenge_r p\);
(iii) \(\lozenge_{{{\vec{r}}}} p\to\lozenge_{r} p\) for each tuple \({{\vec{r}}}\) over \({\mathrm A}\) with \(\oplus{{\vec{r}}}\leq r\).
Then set \(\mathrm{Metr}{({\mathrm A},\lozenge)}\) to be the smallest normal \(({\mathrm A},\lozenge)\)-logic that contains \(\mathrm{Metr}{({\mathrm A})}\) and the formulas
(i) \(p\to\lozenge p\), \(\lozenge\lozenge p\to\lozenge p\), \(\lozenge p\to\exists p\), and
(ii) \(\lozenge_r\lozenge p \to\lozenge_r p\) for each \(r\in {\mathrm A}\).
Note that \(\lozenge p\to\exists p\) follows from other axioms, provided that \({\mathrm A}\) is non-empty. For the empty \({\mathrm A}\), this logic is known as \(\mathrm{S4U}\), the logic of all (finite) preorders endowed with the universal relation [@Goranko-Passy].
2.3 Semantics↩︎
In the following, we recall that our language includes a fixed set \(A\) of positive real numbers as parameters.
Definition 2. Let \(S=(X,d)\) be a metric space. For \(r\in A\), let \(D_{r}\) be the binary relation on \(X\) given by \((x,y)\in D_{r}\) iff \(d(x,y) < r\). The metric \({\mathrm A}\)-frame of \((X,d)\) is the relational structure \((X,(D_{r})_{r\in {\mathrm A}},X\times X)\). Let \(\mathop{\mathrm{Log}}{F_{\mathrm A}(S)}\) denote the set of all \({\mathrm A}\)-formulas that are valid in the metric \(A\)-frame of \(S\). The \({\mathrm A}\)-logic of a class \(\mathcal{K}\) of metric spaces is defined as \(\bigcap\{\mathop{\mathrm{Log}}{F_{\mathrm A}(S)}\mid S\in \mathcal{K}\}\). To define the \(({\mathrm A},\lozenge)\)-logic of \(\mathcal{K}\), we additionally interpret \(\lozenge\) as the topological closure.
In [@Wolter2005], it was shown that \(\mathrm{Metr}{({\mathrm A},\lozenge)}\) is the \(({\mathrm A},\lozenge)\)-logic of the class of all metric spaces.
In [@Wolter2005], the axiom system was formally different, since extra conditions were assumed for the set of parameters. The difference is minor.
2.4 Expressing connectedness↩︎
A unimodal frame \(F=(X,R)\) is connected, if for any points \(x,y\) in \(X\), there is a non-oriented \(R\)-path from \(x\) to \(y\), that is: there are \(n<\omega\) and points \(x_0=x, x_1, \ldots, x_n=y\) such that for each \(k<n\), \(x_k \,R\, x_{k+1}\) or \(x_{k+1}\, R\, x_{k}\). A frame \(F=(X,(R_i)_{I})\) is \(a\)-connected for \(a\in I\), if \((X,R_a)\) is connected.
The property of \(a\)-connectedness is expressed by the formula \[\label{eq:conn-general} \exists p \wedge \exists\neg p \to\exists((p\wedge \lozenge_a \neg p)\vee (\neg p\wedge \lozenge_a p))\tag{2}\] Here \(\exists\) is interpreted as the modality of the universal relation \(X\times X\). That is, we have: \[(X,(R_i)_{I}) \text{ is a-connected} \text{ iff } \text{\mathrm{Con}_a is valid in (X,(R_i)_{I},X\times X).}\] The proof is straightforward.
For a symmetric \(R_a\), 2 simplifies to \[\exists p \wedge \exists\neg p \to\exists(p\wedge \lozenge_a \neg p).\] This formula will be denoted by \(\mathrm{Con}_a\).
For the case when \(R_a\) is reflexive, 2 simplifies to \[\label{eq:conn-top} \exists p \wedge \exists\neg p \to\exists(\lozenge_a p\wedge \lozenge_a \neg p).\tag{3}\]
If the modality is interpreted as the closure in a topological space, 3 expresses topological connectedness [@Shehtman99]; in this case, we denote this formula as \(\mathrm{Con}_\lozenge\).1
For the empty \({\mathrm A}\), the logic \(\mathrm{Metr}{({\mathrm A},\lozenge)}+\mathrm{Con}_\lozenge\) is known as \(\mathrm{S4UC}\). By [@Shehtman99], this logic has the finite model property: it is characterized by the class of finite connected preorders endowed with the universal relation. Moreover, \(\mathrm{S4UC}\) is the logic of all connected topological spaces, and in fact is characterized by any connected dense-in-itself separable metric space (i.e., any connected metric space with more than one point) [@Shehtman99].
3 The finite model property of logics of connectedness↩︎
In this section, we consider logics in an abstract setting, and their models are not assumed to be related to any geometric spaces – they are just relational structures.
3.1 Filtration lemma↩︎
In this subsection, we consider models, formulas, and logics in a fixed modal alphabet.
For a set of formulas \(\Gamma\), let \(\mathop{\mathrm{Sub}}\Gamma\) be the set of subformulas of formulas occurring in \(\Gamma\). If \(\Gamma=\mathop{\mathrm{Sub}}\Gamma\), then \(\Gamma\) is said to be \(\mathop{\mathrm{Sub}}\)-closed. For a model \(M\) and a set \(\Gamma\) of formulas, let \(\sim_\Gamma\) be the equivalence on \(M\) induced by \(\Gamma\):
\(x\sim_{\Gamma} y\) iff \(\forall \psi\in\Gamma\; (M,x\models \psi \text{ iff } M,y\models \psi)\).
We next recall the definition of the minimal and maximal filtrations of a relation.
Definition 3.
Suppose \(\Gamma\) is a \(\mathop{\mathrm{Sub}}\)-closed set of formulas, \(M=(X,(R_a)_{\mathrm A},v)\) is a model, and \(\sim\) is an equivalence relation that refines \(\sim_\Gamma\). Set \(\widehat{X}=X/{\sim}\). For a relation \(R\) corresponding to a modality \(\lozenge\), we define the minimal filtered relation \(R_{\sim}\) and the maximal filtered relation \(R^{\Gamma}_\sim\) on \(\hat{X}\) by setting \[\begin{align} \,\,\,\,[x]\,{R}_{\sim}\,[y]\,\, & \quad \text{ iff }\quad there exist x'\sim x and y'\sim y withx'\,R\,y'\\ [x]\,R^{\Gamma}_\sim\,[y]\,\, &\quad \text{ iff } \quad for all \psi with \lozenge\psi\in \Gamma, if M,y\models \psi then M,x\models \lozenge\psi. \end{align}\]
It is easy to check that \(R_{\sim}\) is contained in \(R^{\Gamma}_\sim\).
Definition 4. A filtration of \(M\) through \(\Gamma\) is a model \(\widehat{M}=(\widehat{X},(\widehat{R}_a)_{\mathrm A},\widehat{v})\) such that
(i) \(\widehat{X}=X/{\sim}\) for an equivalence relation \(\sim\), which refines \(\sim_\Gamma\);
(ii) \(\widehat{v}(p)=\{[x]\in \widehat{X} \mid x \in v(p)\}\) for all variables \(p\in \Gamma\);
(iii) For each \(a\in {\mathrm A}\), \(R_{a,\sim} \subseteq \widehat{R}_a \subseteq R^{\Gamma}_{{a},\sim}\).
The following fact is standard.
Lemma 1 (Filtration lemma). Suppose that \(\Gamma\) is a \(\mathop{\mathrm{Sub}}\)-closed set of formulas and \(\widehat{M}\) is a \(\Gamma\)-filtration of a model \(M\). Then, for all points \(x\) in \(M\) and all formulas \({\psi \in\Gamma}\), we have:
\({M,x\models \psi}\quad\) iff \(\quad{\widehat{M},[x]\models\psi}\).
Proof. Induction on \(\psi\). ◻
For a relation \(R\) on \(X\), let \(R^+\) be its transitive closure \(\bigcup_{0<i<\omega}R^i\). The following is well known.
Lemma 2. ([@Seg1968-S4.1])Let \(M\vDash\lozenge_a \lozenge_a \psi \to\lozenge_a \psi\) for each formula \(\psi\), and let \(\sim\) be the equivalence induced by a \(\mathop{\mathrm{Sub}}\)-closed \(\Gamma\) on \(M\). Then \((R_{a,\sim})^+\) is contained in the maximal filtered relation \(R^{\Gamma}_{{a},\sim}\).
Proof. By induction on \(n\), we show \((R_{a,\sim})^n\subseteq R^{\Gamma}_{{a},\sim}\) for all \(n>0\). Basis is trivial, since the \(a\)-th minimal filtered relation is contained in the \(a\)-th maximal. For the step, suppose \(\lozenge_a \psi \in \Gamma\), \(M,y\vDash\psi\), and \([x] (R_{a,\sim})^{(n+1)} [y]\). Then \([x] R_{a,\sim} [z] (R_{a,\sim})^n [y]\) for some \(z\). By the hypothesis, \(M,z\vDash\lozenge_a \psi\). We have \(x'R_a z'\) for some \(x'\sim x\) and \(z'\sim z\), and since \(\lozenge_a\psi \in \Gamma\), \(M,z'\vDash\lozenge_a\psi\). Thus, \(M,x'\vDash\lozenge_a\lozenge_a\psi\). The formula \(\lozenge_a\lozenge_a\psi\to\lozenge_a\psi\) is true in \(M\), hence \(M,x'\vDash\lozenge_a\psi\). So \(M,x\vDash\lozenge_a\psi\), as required. ◻
3.2 Metric closure operations on frames↩︎
The formula \(\lozenge_c\lozenge p \to\lozenge_c p\) expresses the property \(R_c\circ R \subseteq R_c\). The following construction will be used to build filtrations with this property. Let \(R,D\) be relations on \(X\). We define recursively a relation \(S\) called the \(R\)-closure of \(D\) as follows: \[\begin{align} S^{(0)} &=& D\cup D^{-1},\\ S^{(n+1)} &=& (S^{(n)} \circ R) \cup (S^{(n)}\circ R) ^{-1}, \\ S &=& \bigcup\nolimits_{\omega} S^{(n)}. \end{align}\] The relation \(S^{(n)}\) is called the \(n\)-th grade of the closure \(S\).
Lemma 3. \(S\) is symmetric and \(S\circ R \subseteq S\).
Proof. Each \(S^{(n)}\) is symmetric, so is \(S\). Assume \((x,y)\in S\circ R\). Then \((x,y)\in S^{(n)}\circ R\) for some \(n\), and so \((x,y)\in S^{(n+1)}\subseteq S\). ◻
For a non-empty tuple \({{\vec{r}}}=(r_1,\ldots,r_m)\) of parameters and a frame \((X, (S_r)_{\mathrm A})\), put \(S_{\vec{r}}=S_{r_1}\circ \ldots \circ S_{r_m}\). For the empty \({\vec{r}}\), define \(S_{\vec{r}}\) as the diagonal \(\{(x,x)\mid x\in X\}\).
Definition 5. The \({\mathrm A}\)-closure of a frame \((X, (S_r)_{\mathrm A})\) is the frame \((X, (H_r)_{\mathrm A})\) such that \[H_{r}=\bigcup\{S_{\vec{r}}\mid \text{{\vec{r}} is a tuple of parameters with \oplus{{\vec{r}}}\leq r}\}.\]
Lemma 4. The \({\mathrm A}\)-closure \((X, (H_r)_{\mathrm A})\) of any frame \((X,(S_r)_{\mathrm A})\) validates the formulas \(\lozenge_{{{\vec{r}}}} p\to\lozenge_{r} p\) for each tuple \({{\vec{r}}}\) over \({\mathrm A}\) and \(r\in {\mathrm A}\) with \(\oplus{{\vec{r}}}\leq r\).
Proof. Let \((x,y)\in H_{{\vec{r}}}\) for \({{\vec{r}}}=(r_1,\ldots,r_m)\). Then we have \((x,y) \in S_{{\vec{s}}_1}\circ \ldots \circ S_{{\vec{s}}_m}\) for some \({\vec{s}}_i\) with \(\oplus{{\vec{s}}}_i\leq r_i\). Then \((x,y) \in S_{\vec{s}}\), where \({\vec{s}}\) is the concatenation \({\vec{s}}_1{\vec{s}}_2\ldots {\vec{s}}_m\). Hence \(\oplus{{\vec{s}}}\leq r\). By the definition of \(H_r\), we have \((x,y)\in H_r\), as desired. ◻
Definition 6. The \(({\mathrm A},\lozenge)\)-closure of a frame \(F=(X, R, (D_r)_{\mathrm A})\) is the frame \(G=(X,\preceq, (H_r)_{\mathrm A},X\times X)\) defined as follows:
(i) \(\preceq\) is the transitive closure of \(R\);
(ii) \((X,(H_r)_{\mathrm A})\) is the \({\mathrm A}\)-closure of \((X,(S_r)_{\mathrm A})\), where \(S_r\) is the \(\preceq\)-closure of \(D_r\).
Lemma 5. For a frame \(F=(X, R, (D_r)_{\mathrm A})\) with all relations reflexive, its \(({\mathrm A},\lozenge)\)-closure validates the logic \(\mathrm{Metr}{({\mathrm A},\lozenge)}\).
Proof. Let \(G=(X,\preceq, (H_r)_{\mathrm A}, X\times X)\) be this closure. The axioms for the modality \(\exists\) hold trivially. Since \(R\) is reflexive, \(\preceq\) is a preorder. That the \(\lozenge_{{{\vec{r}}}}\, p\to\lozenge_{r} p\) are valid follows from Lemma 4. All \(S_r\) are symmetric by Lemma 3, hence each \(H_{r}\) is the union of compositions of symmetric relations, and so is symmetric as well.
Let us check the validity of \(\lozenge_r\lozenge p\to\lozenge_r p\). For this, we show that \(H_r\, \circ \preceq \;\subseteq\; H_r\). In turn, it is enough to show that for a tuple of parameters \(\vec{r}\) with \(\oplus\,\vec{r}\leq r\) we have \(S_{\vec{r}}\,\circ\preceq\,\,\subseteq\, H_r\). For any \(t\in A\) we have \(S_t\circ{\preceq}\) included in \(S_t\) by Lemma 3, and \(S_t\) included in \(S_t\circ {\preceq}\) due to reflexivity of \(\preceq\). So we have for any non-empty \({\vec{r}}={\vec{s}}t\): \[S_{\vec{r}}\circ {\preceq}\;=\;(S_{\vec{s}}\circ S_t)\circ {\preceq}\; = \; S_{\vec{s}}\circ (S_t \circ {\preceq})\;=\; S_{\vec{s}}\circ S_t\;=\; S_{\vec{r}}.\] Thus when \({\vec{r}}\) is non-empty, \(S_{\vec{r}}\;\circ\preceq\;\subseteq H_r\). When \(\vec{r}\) is empty, \(S_{\vec{r}}\) is by definition the identity relation, so we must show \(\preceq\;\subseteq H_r\). Since \(D_r\) is reflexive, so is \(S_r\), hence \(\preceq\;\subseteq S_r\,\circ\preceq\). Thus by Lemma 3 used again, \(\preceq\;\subseteq S_r\), and clearly \(S_r\subseteq H_r\). ◻
3.3 The filtration↩︎
The following is a corollary of [@Shehtman99] and [@ChromoWallic].
Lemma 6. Consider a model \(M=(X,(R_i)_I,X\times X,v)\) and let \(\widehat{X}= X{/}{\sim_\Delta}\) for a finite \(\mathop{\mathrm{Sub}}\)-closed set of formulas \(\Delta\). Let \(a\in I\), and assume that a relation \(\widehat{R}\) on \(\widehat{X}\) includes the minimal filtered relation \(R_{a,\sim_\Delta}\). Assume \(M\vDash L\) for an \({\mathrm A}\)-logic \(L\), and \(L\) contains the formula \(\exists p \wedge \exists\neg p \to\exists(\lozenge_a p\wedge \lozenge_a \neg p)\) or the formula \(\exists p \wedge \exists\neg p \to\exists(p\wedge \lozenge_a \neg p)\). Then the frame \((\widehat{X},\widehat{R})\) is connected.
Proof. Assume that \(\widehat{X}=\widehat{Y}\cup\widehat{Z}\) for disjoint non-empty \(\widehat{Y}\) and \(\widehat{Z}\), \(Y=\bigcup \widehat{Y}\), \(Z=\bigcup \widehat{Z}\). We aim to show that \[\label{eq:conn-lemma} \exists y\in Y\; \exists z\in Z \;([y]\, \widehat{R}\, [z] \text{ or }[z]\, \widehat{R}\, [y]).\tag{4}\]
Since \(\widehat{Y}\) consists of \(\sim_\Delta\)-classes, for some Boolean combination \(\gamma\) of formulas in \(\Delta\) we have for all \(y\in X\): \[M,y\vDash\gamma \quad \text{iff} \quad y\in Y.\]
Assume that \(L\) contains the formula \(\exists p \wedge \exists\neg p \to\exists(\lozenge_a p\wedge \lozenge_a \neg p)\). Then it also contains its substitution instance \(\exists\gamma \wedge \exists\neg \gamma \to\exists(\lozenge_a \gamma\wedge \lozenge_a \neg \gamma)\). Since both \(Y\) and \(Z\) are non-empty, there are points \(x_1\), \(x_2\), and \(x_3\) such that \(x_1Rx_2\), \(x_1Rx_3\), \(M,x_2\vDash\gamma\), and \(M,x_3\vDash\neg \gamma\). Hence, \(x_2\in Y\) and \(x_3\in Z\). If \(x_1\in Y\), put \(y=x_1\) and \(z=x_3\); otherwise, put \(y=x_2\) and \(z=x_1\). In either case, we have 4 according to the definition of minimal filtration.
Now assume that \(L\) contains \(\exists p \wedge \exists\neg p \to\exists(p\wedge \lozenge_a \neg p)\). Similar reasoning shows that there are points \(y,z\) such that \(yRz\), \(M,y\vDash\gamma\), and \(M,z\vDash\neg \gamma\), and so \(y\in Y\) and \(z\in Z\).
Hence, we have 4 , and so \((\widehat{X},\widehat{R})\) is connected. ◻
Lemma 7. Assume \({\mathrm A}\) is finite. Let \(L=\mathrm{Metr}{({\mathrm A})}+\mathrm{Con}_a\) for some \(a\in{\mathrm A}\), or \(L=\mathrm{Metr}{({\mathrm A},\lozenge)}+\mathrm{Con}_a\) for some \(a\in{\mathrm A}\cup \{\lozenge\}\). Then \(L\) has the finite model property.
Proof. The proof for the case when \(\lozenge\) is in the language is more general, so we consider this case.
In the case \({\mathrm A}=\varnothing\), \(L\) is the logic \(\mathrm{S4UC}\), whose fmp is known [@Shehtman99]. Assume \({\mathrm A}\neq \varnothing\).
The proof is technical, and we first outline the strategy. Assume that \(\varphi\) is \(L\)-consistent. To establish the result, we find a finite model of \(L\) in which \(\varphi\) is satisfiable. (A) Begin with a certain model \(M\) of \(L\) in which \(\varphi\) is satisfiable. (B) Take \(\Gamma=\mathop{\mathrm{Sub}}\varphi\) and \(\Delta\) to be a certain finite set of formulas constructed from \(\Gamma\). Then form the minimal filtration of \(M\) over \(\sim_\Delta\). (C) Take the \((A,\lozenge)\)-closure of this filtration \(\widehat{F}\). By Lemma 5, \(\widehat{F}\) validates \(\mathrm{Metr}{({\mathrm A},\lozenge)}\). The details of our setup allow us to use Lemma 6 to obtain that \(\widehat{F}\) validates \(\mathrm{Con}_a\). Since \(\Delta\) is finite, the minimal filtration is finite, hence \(\widehat{F}\) is finite. (D) Define a valuation to construct a model \(\widehat{M}\) from \(\widehat{F}\). Then show \(\widehat{M}\) is a filtration of \(M\) through \(\Gamma\), hence by the filtration lemma \(\varphi\) is satisfible in \(\widehat{F}\).
Assume \(\varphi\) is \(L\)-consistent. Then \(\varphi\in x_0\) for some \(x_0\) in the canonical model of \(L\). Let \(M=(X,R, (D_r)_{{\mathrm A}},R_\exists,v)\) be the submodel of the canonical model of \(L\) generated by \(x_0\); here \(R\) interprets \(\lozenge\), \(R_\exists\) interprets the modality \(\exists\). The logic \(\mathrm{Metr}{({\mathrm A},\lozenge)}\) is canonical since its axioms are Sahlquist formulas. Hence, we have: \(R\) is a preorder, all \(D_r\) are symmetric and reflexive, and for all \(r\in {\mathrm A}\) \[\label{eq:poly:closure-canonGen} D_r\circ R\subseteq D_r.\tag{5}\] Since \(M\) is point-generated, we have \(R_\exists=X\times X\).
Let \(\Gamma=\mathop{\mathrm{Sub}}\varphi\) and let \(V\) be the set of tuples \(\vec{r}\) of parameters with \(\oplus\vec{r}\leq r\) for some \(r\in A\). Define \[\begin{align} \Delta &=& \{\lozenge_{\vec{r}}\,\psi, \lozenge\lozenge_{\vec{r}}\psi \mid {\vec{r}}\in V , \psi \in \Gamma\}. \end{align}\] Note that the empty string \(\vec{r}\) has \(\oplus\vec{r}=0\), so belongs to \(V\), and in this case \(\lozenge_{\vec{r}}\psi\) is \(\psi\) for any formula. Thus \(\Gamma\;\subseteq\;\Delta\). Put \(\widehat{X}=X/{\sim}\) for the equivalence \(\sim\;=\;\sim_\Delta\) induced by \(\Delta\). Then \(\sim\) refines \(\sim_\Gamma\). Let \(R_\sim\) be the minimal filtered relation induced by \(R\) on \(\widehat{X}\), and let \(E_r\) denote the minimal filtered relation \(D_{r,\sim}\).
Let \(\widehat{F}=(\widehat{X},\preceq, (H_r)_{\mathrm A},\widehat{X}\times \widehat{X})\) be the \(({\mathrm A},\lozenge)\)-closure of \((\widehat{X},R_\sim, (E_r)_{\mathrm A})\). Since \(R\) and the \(D_r\) are reflexive, so are their minimal filtrations \(R_\sim\) and the \(E_r\), and so by Lemma 5, \(\widehat{F}\) validates \(\mathrm{Metr}{({\mathrm A},\lozenge)}\). Since \(L\) contains \(\mathrm{Con}_a\), \(\widehat{F}\) validates \(\mathrm{Con}_a\) by Lemma 6. Hence, \(\widehat{F}\) validates \(L\).
Define \(\widehat{M}=(\widehat{F},\widehat{v})\), where \(\widehat{v}(p)=\{[x]\in \widehat{X} \mid x \in v(p)\}\) for variables \(p\in \Gamma\). Our aim is to show the following: \[\widehat{M}=(\widehat{X},\preceq, (H_r)_{\mathrm A},\widehat{X}\times \widehat{X},\widehat{v}) is a filtration of M=(X,R, (D_r)_{{\mathrm A}},R_\exists,v) through \Gamma.\]
By definition, \(\widehat{X}=X/\sim\), and as noted in Step (B), \(\sim\) refines \(\sim_\Gamma\). The valuation \(\widehat{v}\) is defined to match the criterion set in Definition 4. It remains to show that each relation of \(\widehat{M}\) lies between the minimal and maximal filtered relations. Trivially, \(\widehat{X}\times \widehat{X}\) is the minimal filtered relation of \(R_\exists=X\times X\). By definition of the \((A,\lozenge)\)-closure, \(\preceq\) is the transitive closure of \(R_\sim\). So clearly \(\preceq\) contains the minimal filtered relation \(R_\sim\). Since \(L\) contains \(\lozenge\lozenge p\to \lozenge p\) and \(M\vDash L\), we have \(M\models \lozenge\lozenge\psi\to\lozenge\psi\) for any formula \(\psi\), so by Lemma 2, \[\text{ \preceq is contained in R_\sim^{(\Delta)}.}\] But \(\Gamma\subseteq\Delta\) gives \(R_\sim^\Delta\subseteq R_\sim^\Gamma\).
It remains to show that for each \(r\in A\), the relation \(H_r\) lies between the minimal and maximal \(\sim\)-filtrations of \(D_r\). Recall that \(D_{r,\sim}\) is written \(E_r\) and \(H_r\) is constructed by first taking the \(\preceq\)-closure \(S_r\) of \(E_r\) as given before Lemma 3, then obtaining \(H_r\) from the family \((S_r)_{\mathrm A}\) as in Definition 5. Note that \(S_r\) contains \(D_{r,\sim}\) and \(S_r\subseteq H_r\) is immediate from the definition of \(H_r\). Thus \(H_r\) contains the minimal \(\sim\)-filtration of \(D_r\). To show that it is contained in the maximal filtration \(D_{r,\sim}^\Gamma\) we must show \[\label{eq:32John} \text{If \lozenge_r\psi\in \Gamma, [x]\, H_r\, [y], and M,y\vDash\psi, then M,x\vDash\lozenge_r\,\psi.}\tag{6}\] We establish this through a series of results.
We first claim that for \([x]\preceq [y]\): \[\begin{align} \tag{7} &&\text{ if \lozenge\psi\in \Delta and M,y\vDash\lozenge\psi}, \text{ then M,x\vDash\lozenge\psi;}\\ \tag{8} &&\text{ if \lozenge_r\psi\in \Delta and M,x\vDash\lozenge_r\psi}, \text{ then M,y\vDash\lozenge_r\psi. } \end{align}\]
We have 7 as a corollary of the fact that \(\preceq\;\subseteq\;R_\sim^\Delta\). Indeed, if \(M,y\vDash\lozenge\psi\), then \(M,z\vDash\psi\) for some \(z\) with \(yRz\). Now \([x] \preceq [z]\), so \([x]\,R_\sim^\Delta\,[z]\), giving \(M,x\vDash\lozenge\psi\).
Let us check 8 . By induction on \(n\), we show that 8 holds for \([x] (R_\sim)^n [y]\) for all \(n\geq 0\). The basis \(n=0\) is trivial, since \(x\sim y\) in this case, meaning that \(M,x\models\psi\) iff \(M,y\models\psi\) for every formula \(\psi\) in \(\Delta\) and we assumed \(\lozenge_r\psi\in \Delta\). Let \(n>0\). We have \([x]\, R_{\sim}\, [z]\, (R_{\sim})^{n-1} [y]\) for some \(z\), and \(x'R\, z'\) for some \(x'\sim x\) and \(z'\sim z\). Then \(M,x'\vDash\lozenge_r\psi\), and we have \(M,u\vDash\psi\) for some \(u\) with \(x' D_r\, u\). Since \(D_r\) is symmetric, we have \(u\,D_r\, x'\), and so \(u\, D_r\circ R\, z'\). So \(u\, D_r\, z'\) by 5 . Hence, \(z' D_r\, u\), and so \(M,z'\vDash\lozenge_r \psi\). We have \([z'] (R_{\sim})^{n-1} [y]\), and \(M,y\vDash\lozenge_r \psi\) now follows from the induction hypothesis. This completes the proof of 8 .
Now by induction on \(n\), we show that for the \(n\)-grade \(S_r^{(n)}\) of \(S_r\), we have \[\begin{align} \label{eq:poly:closureMaxGenJohn} &&\text{ if \lozenge_r \psi\in \Delta, [x]\, S_r^{(n)}\, [y], and M,y\vDash\lozenge\psi}, \text{ then M,x\vDash\lozenge_r\psi.} \end{align}\tag{9}\]
First, observe that \(\lozenge_r \psi\in \Delta\) gives \(\lozenge\psi\in \Delta\). Indeed, if \(\lozenge_r\psi\in \Delta\), then \(\lozenge_r\psi\) has the form \(\lozenge_r\lozenge_{\vec{s}}\,\chi\) for some \(\chi\in \Gamma\) and \({\vec{s}}\in V\). Then \(\lozenge\lozenge_{\vec{s}}\,\chi\in \Delta\).
Let \([x]\, S_r^{(0)}\,[y]\). We have \(S_r^{(0)}=E_r \cup E_r^{-1}\). Since \(E_r\) is symmetric, \(S^{(0)}=E_r=D_{r,\sim}\). The assumptions of 9 give some \(x'\sim x\), \(y'\sim y\) with \(x' D_r\, y'\), and since \(\lozenge\psi\in \Delta\), we have \(M,y'\vDash\lozenge\psi\). Hence, \(M,x'\vDash\lozenge_r\lozenge\psi\), and so \(M,x'\vDash\lozenge_r \psi\), since \(\lozenge_r\lozenge\psi\to\lozenge_r\psi\) is true in \(M\). Thus, \(M,x\vDash\lozenge_r \psi\).
Now let \([x]\, S_r^{(n+1)}\,[y]\) and \(M,y\models\lozenge\psi\). Consider two cases. First, assume that \([x]\, S_r^{(n)} \circ {\preceq}\, [y]\). Then we have that \([x]\, S_r^{(n)} [z] \; {\preceq}\; [y]\) for some \([z]\). So by 7 we have \(M,z\vDash\lozenge\psi\). By induction hypothesis, we have \(M,x\vDash\lozenge_r \psi\). Now assume that \([x]\, (S_r^{(n)} \circ {\preceq})^{-1}\, [y]\), that is \([y]\, S_r^{(n)} [z] \preceq [x]\) for some \(z\). Since \(S_r^{(n)}\) is symmetric, we have \([z]\, S_r^{(n)}\, [y]\), and so \(M,z\vDash\lozenge_r\psi\) by the induction hypothesis. Now 8 implies that \(M,x\vDash\lozenge_r\psi\). This completes the proof of 9 .
Using 9 , now we show: \[\begin{align} \label{eq:poly:closureMaxGen1John} &&\text{ If \lozenge_r \psi\in \Delta, [x]\, S_r\, [y], and M,y\vDash\psi}, \text{ then M,x\vDash\lozenge_r\psi}. \end{align}\tag{10}\] Since \(M,y\vDash\psi\) and \(R\) is reflexive, \(M,y\vDash\lozenge\psi\). We have \([x]\, S_r^{(n)}\, [y]\) for some \(n\), and by 9 , \(M,x\vDash\lozenge_r\psi\), as desired.
Now we claim that for \({\vec{r}}\in V\), we have: \[\label{eq:poly:filtrGenJohn} \text{If \psi\in \Gamma, [x]\, S_{\vec{r}}\, [y], and M,y\vDash\psi, then M,x\vDash\lozenge_{\vec{r}}\,\psi.}\tag{11}\] By induction on the length of \({\vec{r}}\). If \({\vec{r}}\) is empty, \(S_{\vec{r}}\) is the diagonal, so \([x]=[y]\); also, \(\lozenge_{\vec{r}}\,\psi\) is just \(\psi\); now 11 holds because \(\psi\in \Gamma\subseteq\Delta\). For the inductive step, suppose that \({\vec{r}}\) is the concatenation \(r{\vec{s}}\) for a parameter \(r\) and a tuple of parameters \({\vec{s}}\). We have \([x]\,S_{r}\, [z]\, S_{\vec{s}}\,[y]\) for some \(z\). Notice that \({\vec{s}}\in V\), so by the induction hypothesis, we have \(M,z \vDash\lozenge_{\vec{s}}\,\psi\). We have \(\lozenge_r\lozenge_{\vec{s}}\,\psi\in \Delta\), and by 10 , we get \(M,x\vDash\lozenge_{\vec{r}}\, \psi\). This completes the proof of 11 .
To establish 6 , assume that \(\lozenge_r\psi \in \Gamma\), \([x]\, H_r\, [y]\), and \(M,y\vDash\psi\). We have \([x]\, S_{\vec{r}}\, [y]\) for some tuple of parameters \({\vec{r}}\) with \(\oplus{{\vec{r}}}\leq r\). Also, since \(\Gamma\) is Sub-closed, \(\psi\in \Gamma\). By 11 , \(M,x\vDash\lozenge_{{{\vec{r}}}}\, \psi\). We have \(\oplus{{\vec{r}}}\leq r\), so the formula \(\lozenge_{{{\vec{r}}}} \, p\to\lozenge_{r} p\) is in \(L\). So \(\lozenge_{{{\vec{r}}}}\, \psi\,\to\lozenge_{r} \psi\) is true in \(M\). Thus, \(M,x\vDash\lozenge_r\psi\), and establishing 6 .
We have established that \(\widehat{M}\) is a filtration of \(M\) through \(\Gamma\). It then follows by the filtration lemma that \(\varphi\) is satisfiable in \(\widehat{F}\), completing the proof. ◻
4 The logic of graph-connected spaces↩︎
Theorem 1. Let \({\mathrm A}\) be a set of positive real numbers, \(a\in {\mathrm A}\). The \({\mathrm A}\)-logic of the class of all \(a\)-connected metric spaces, and also of all finite \(a\)-connected metric spaces, is \(\mathrm{Metr}{({\mathrm A})}+\mathrm{Con}_a\).
The proof of this theorem is based on two ingredients. The first one is Kripke completeness of the logic, which follows from the finite model property established earlier. The second ingredient is the following lemma, which in fact follows from [@Kutz-Sturm-Suzuki-Wolter-Zakharyaschev2003; @Kutz2007].
Lemma 8 (Corollary of [@Kutz-Sturm-Suzuki-Wolter-Zakharyaschev2003; @Kutz2007]). Assume that \({\mathrm A}\) is finite. Let \(F=(X, (R_l)_{l\in {\mathrm A}},X\times X)\) be a \(\mathrm{Metr}{({\mathrm A})}\)-frame, and assume that the frame \((X, (R_l)_{l\in {\mathrm A}})\) is point-generated. Then there exists a metric \(d\) on \(X\) such that \(F\) is the \({\mathrm A}\)-metric frame of \((X,d)\), and \(\inf\{d(a,b)\mid a\neq b and a,b\in X\}>0\).
This statement is only a slight modification of known facts; for the sake of rigor, we provide its proof in the Appendix.
Proof of theorem 1.. Soundness is straightforward.
To prove the other inclusion, assume that a formula \(\varphi\) is consistent with the logic \(\mathrm{Metr}{({\mathrm A})}+\mathrm{Con}_a\). Let \({\mathrm B}\) be the set consisting of \(a\) and the parameters occurring in \(\varphi\), and let \(L=\mathrm{Metr}{({\mathrm B})}+\mathrm{Con}_a\). Then \(\varphi\) is consistent with the logic \(L\). Due to Lemma 7, \(L\) has the finite model property and so is Kripke complete. Hence, \(\varphi\) is satisfiable in a (finite) Kripke frame \(F=(X, (R_l)_{l\in {\mathrm B}},X\times X)\), which validates \(L\). Due to \(a\)-connectedness, the frame \((X, (R_l)_{l\in {\mathrm B}})\) is point-generated. By Lemma 8, \(F\) is the \({\mathrm B}\)-metric frame of a metric space \((X,d)\). Clearly, this space is \(a\)-connected. Now consider the expansion \(F_{\mathrm A}(X,d)\) of \(F\). The formula \(\varphi\) is satisfiable in \(F_{\mathrm A}(X,d)\), which completes the proof. ◻
Theorem 1 generalizes the finite model property of the logic of \(a\)-connectedness (Lemma 7) for the case of infinite alphabets: indeed, finite metric spaces correspond to finite Kripke frames.
Theorem 1 does not apply (at least, directly) to the case of topological connectedness due to the following observation. If the closure modality is interpreted via a preorder in a Kripke frame, the corresponding topological space need not even be \(T_1\). And hence, this topological closure is not induced by any metric. This motivates our next section.
5 The logic of connected spaces↩︎
In this section, we consider the language with the topological modality, universal modality, and a single distance modality. Our aim is to axiomatize the logic of all connected metric spaces in this language.
In the next subsection, we list the axioms of the logic, which we denote \(\mathrm{S4UC_{<1}}\). We then discuss three preliminary constructions – relational and topological (introduced earlier in [@Shehtman99]), as well as metric; they are given in subsections 5.2, 5.3, and 5.4. Then, for a given \(\mathrm{S4UC_{<1}}\)-consistent formula \(\varphi\), we construct a connected space where \(\varphi\) is satisfiable. This part of the proof is given in the two final subsections: we first construct a certain connected subspace \(X\) of \(\mathbb{R}^3\); then, preserving its connectedness, we alter its metric to ensure satisfiability of \(\varphi\).
5.1 The logic↩︎
We assume that the alphabet \({\mathrm A}\) of distance modalities is a singleton. Without loss of generality, we assume that \({\mathrm A}=\{1\}\). Let \[\mathrm{S4UC_{<1}}=\mathrm{Metr}{(\{1\},\lozenge)}+\mathrm{Con}_\lozenge.\] According to Definition 1, the explicit set of axioms defining \(\mathrm{S4UC_{<1}}\) is the following: \[\begin{align} &&p\to\forall\exists p,~p\to\exists p,~\exists\exists p \to\exists p, \text{ and } \lozenge_1 p\to\exists p;\\ \tag{12} &&p\to\Box_1 \lozenge_1 p;\\ &&p\to\lozenge_{1} p;\\ &&p\to\lozenge p,~\lozenge\lozenge p\to\lozenge p; \\ \tag{13} &&\lozenge_1\lozenge p \to\lozenge_1 p;\\ &&\exists p \wedge \exists\neg p \to\exists(\lozenge p\wedge \lozenge\neg p), \text{ that is } \mathrm{Con}_\lozenge. \end{align}\]
As we mentioned earlier, the counterpart of \(\mathrm{S4UC_{<1}}\) for the empty \({\mathrm A}\) is the logic \(\mathrm{S4UC}\).
5.2 Quasiparks and suitable frames↩︎
As usual, a preorder \((W,\preceq)\) is a set with a transitive reflexive relation. We use the following notation: for \(a\in W\) set \({\uparrow}a=\{b\mid a\preceq b\}\) and for \(U\subseteq W\), set \({\uparrow}U =\bigcup_{a\in U}{\uparrow}a\). Likewise for downsets \({\downarrow}a\) and \({\downarrow}U\). A rooted poset \((P,\leq)\) is a (transitive) tree, if \({\downarrow}a\) is a finite chain for all \(a\) in \(P\). A preorder \((W,\preceq)\) is a quasitree, if its skeleton (the associated partial order) is a tree.
Let \((W,\preceq, S, W\times W)\) be an \(\mathrm{S4UC_{<1}}\)-frame. We have:
\(\preceq\) is included in \(S\);
For \(a\in W\), \({\uparrow}a\) is an \(S\)-clique, that is \({\uparrow}a\times {\uparrow}a\subseteq S\);
If \(a \preceq a'\), \(b \preceq b'\), and \(aSb\), then \(a'S b'\).
Proof. Axioms 12 – 13 give that \(\preceq\) is a quasi-order, \(S\) is reflexive and symmetric, and \(S\,\circ\preceq\;\subseteq S\). So clearly we have (1) \(\preceq\;\subseteq S\). For (2) suppose \(a\preceq b,c\). Then \(b\,S\,a\,\preceq\,c\), so \((b,c)\in S\,\circ\preceq\;\subseteq S\). For (3) assume \(a\;\preceq\;a'\), \(b\;\preceq\;b'\) and \(a\,S\,b\). Then \(b\,S\,a\,\preceq\,a'\), so \(b\,S\,a'\), and then \(a'\,S\,b\). Then \(a'\,S\,b\,\preceq\,b'\) gives \(a'\,S\,b'\). ◻
Definition 7. [@Shehtman99] In a poset \((P,\leq)\), let \(\lessdot\) denote the immediate successor relation: \(x\, \lessdot\, y\) iff \(x<y\) but \(x <z< y\) for no \(z\). A non-trivial loop in \((P,\leq)\) is a non-oriented \(\lessdot\,\)-path \((x_1,\ldots ,x_n,x_1)\) (in other words, with \(x_i\, \lessdot\; x_{i+1}\) or \(x_{i+1}\, \lessdot\; x_i\) for each \(i\leq n\)) with \(n\geq 3\) and all \(x_1,\ldots x_n\) distinct.
A finite preorder \((W,\preceq)\) is called a quasipark, if:
(i) the skeleton of \((W,\preceq)\) has no non-trivial loops, and
(ii) one can order the minimal clusters of \((W,\preceq)\) as \(C_1,\ldots,C_n\) so that \[\label{eq:quasipark} {\uparrow}C_i\cap {\uparrow}C_{j}\neq\varnothing\text{ iff }|i-j|\leq 1.\tag{14}\]
The following is straightforward from the definition.
In a quasipark \(Q=(W,\preceq)\), for each \(a,b\in W\) we have:
The restriction of \(Q\) to \({\uparrow}a\) is a quasitree;
If \({\uparrow}a\cap {\uparrow}b\) is non-empty, then the restriction of \(Q\) to this set is a quasitree.
Definition 8. An \(\mathrm{S4UC_{<1}}\)-frame \((W,\preceq, S, W\times W)\) is said to be suitable, if \((W,\preceq)\) is a quasipark.
It is known that \(\mathrm{S4UC}\) is characterized by quasiparks (endowed with the universal relation) [@Shehtman99]. Together with the finite model property of \(\mathrm{S4UC_{<1}}\), this results in the following fact.
Corollary 1. \(\mathrm{S4UC_{<1}}\) is the logic of suitable frames.
Proof. According to the finite model property of \(\mathrm{S4UC_{<1}}\) (Lemma 7), it is enough to show that any finite \(\mathrm{S4UC_{<1}}\)-frame \(F=(X,\sqsubseteq, T, X\times X)\) is a p-morphic image of a suitable \(G\).
In view of [@Shehtman99], there is a quasipark \((W,\preceq)\) and a p-morphism \(f: (W,\preceq) \twoheadrightarrow(X,\sqsubseteq)\). Set \(S=\{(a,b)\in W\times W\mid f(a) T f(b)\}\), \(G=(W,\preceq, S, W\times W)\). It is immediate that \(f:G\twoheadrightarrow F\). Also, it is straightforward that \(G\) is an \(\mathrm{S4UC_{<1}}\)-frame. In particular, the formula \(\lozenge_1\lozenge p \to\lozenge_1 p\) holds there. For this, assume that we have \(a S b \preceq c\). Then \(f(a)Tf(b)\sqsubseteq f(c)\), and hence \(f(a) T f(c)\). By the definition of \(S\), \(aS c\). ◻
5.3 Morphisms from topological spaces to preorders↩︎
In a topological space \((X,\tau)\), for \(Y\subseteq X\), let \(\mathrm{c}{Y}\) denote the closure of \(Y\).
Definition 9. [@Shehtman99] Let \((X,\tau)\) be a topological space, \((W,\preceq)\) a preorder. A surjective \(f:X\to W\) is called a cp-morphism, if for each \(a\in W\) we have \[\mathrm{c}f^{-1}(a)\;=\;f^{-1}[{\downarrow}a]\] (equivalently, \(f\) is an interior map from \((X,\tau)\) onto \((W,\tau_\preceq)\), where \(\tau_\preceq\) is the topology of upsets in \((W,\preceq)\).)
The next statement is a corollary of [@McKinsey-Tarski-1944]; in explicit form, it is given in [@Shehtman99].
Lemma 9. If \(X\) is a connected dense-in-itself separable metric space and \(F\) is a finite quasitree, then \(f:X\twoheadrightarrow F\) for a cp-morphism \(f\).
5.4 Jumps↩︎
Here we introduce a notion of jumps – a geometric tool to produce from a metric space \((X,d)\) a new metric space \((X,d_J)\) that is topologically equivalent, but reduces distances by making “wormholes” in space.
Definition 10. Let \((X,d)\) be a metric space, \(E\subseteq X\times X\), and \(J:E\to\mathbb{R}_{>0}\) a map that is symmetric in that if \((x,y)\in E\), then \((y,x)\in E\) and \(J(x,y)=J(y,x)\). Call \(J(x,y)\) the jump between \(x\) and \(y\). For \(x,y\in X\), define the weight of \((x,y)\): if \((x,y)\in E\) and \(J(x,y)<d(x,y)\), put \(w(x,y)=J(x,y)\); otherwise, put \(w(x,y)=d(x,y)\). A path in \(X\) from \(x\) to \(y\) is a finite non-empty tuple \(\tau=(x_0,\ldots,x_m)\) of elements of \(X\) with \(x_0=x\) and \(x_m=y\). Put \(w(\tau)=\sum_{i<m} w(x_i,x_{i+1})\). For \(x,y \in X\), define \[\label{eq:distance-for-jumps} d_{J}(x,y)=\inf\{w(\tau) \mid \tau\text{ is a path from x to y}\}.\tag{15}\]
Lemma 10. If \(\inf\{J(x,y)\mid (x,y)\in E\}>0\), then \(d_J\) is a metric on \(X\) and the topologies on \(X\) induced by \(d\) and \(d_{J}\) are equal.
Proof. It is easy to see that \(d_{J}\) is a metric on \(X\); in particular, the triangle inequality is straightforward from 15 . Also, open balls of radii less than this infimum form bases of both these topologies. ◻
5.5 Constructing a connected space for \(\varphi\)↩︎
Assume that a formula \(\varphi\) is \(\mathrm{S4UC_{<1}}\)-satisfiable. By Corollary 1, \(\varphi\) is satisfiable in a suitable frame \[F=(W,\preceq, S, W\times W).\] Our goal is to show that \(\varphi\) is satisfiable in a connected metric space.
First, we name parts of \(F\). Let \(C_i\), \(1\leq i\leq n\) be the minimal clusters of \(W\) in the order satisfying 14 . We denote \({\uparrow}C_i\) as \(W_i\), and the restriction of \((W,\preceq)\) to \(W_i\) as \(F_i\). Put \(V_i=W_i\cap W_{i+1}\) (here \(1\leq i<n\)). By Proposition [prop:quasipark-basic], each \(V_i\) has a least cluster \(D_i\). Let \(d_i\) be some point in \(D_i\). Finally, let \(Q_i\) be the restriction of \((W,\preceq)\) to \({\uparrow}D_i\).
Now we construct a subspace \(X\) of \(\mathbb{R}^3\).
Fix a number \(L>2\). Let \(1\leq i\leq n\). In the plane \(x= Li\), consider a closed disk \(X_i\) centered at \((Li,0,0)\) of radius \(\frac{1}{L}\), and let \(\tau_i\) be the standard topology on \(X_i\). Fix a cp-morphism \(f_i:(X_i,\tau_i)\twoheadrightarrow F_i\); the existence of \(f_i\) follows from Lemma 9.
Choose \(y_i\) in the \(f_i\)-preimage of \(d_i\), and \(z_i\) in the \(f_{i+1}\)-preimage of \(d_i\). Define the \(i\)-th handle \(H_i\) as the open interval between between \(y_i\) and \(z_{i}\) on the line through these two points; the standard topology on \(H_i\) is denoted as \(\rho_i\). Fix a cp-morphism \(g_i:(H_i,\rho_i)\twoheadrightarrow Q_i\) (we use [@Shehtman99] again).
Let \(X\) be the (disjoint, in fact) union of these disks and handles, \(\tau\) the standard topology on \(X\). Observe that \((X,\tau)\) is connected. Now let \(f \; =\; f_1\cup g_1\cup f_2\cup \ldots \cup g_{n-1}\cup f_n\).
\(f: (X,\tau)\twoheadrightarrow(W,\preceq)\) is a cp-morphism.
Proof. Clearly \(f\) is onto. Note that any set closed in \(X_i\) is closed in \(X\) and any set closed in \(H_i\) and containing its endpoints is closed in \(X\). So for any \(a\in W\) we have that \(f^{-1}[{\downarrow}a]\) is a finite union of closed sets of \(X\), so is closed in \(X\). Thus \(\mathrm{c}f^{-1}(a)\subseteq f^{-1}[{\downarrow}a]\). Conversely, suppose \(x\in f^{-1}[{\downarrow}a]\) and consider two cases. Case (i) \(x\in X_i\). Then \(f(x)\in W_i\), and since \(W_i\) is an upset, \(a\in W_i\). Then \(x\) is in the closure of \(f_i^{-1}(a)\) in \(X_i\), hence it is in the closure of \(f^{-1}(a)\) in \(X\). Case (ii) \(x\in H_i\). Then \(a\in Q_i\), and \(x\) is in the closure of \(g_i^{-1}(a)\) in \(H_i\), hence in the closure of \(f^{-1}(a)\) in \(X\). ◻
We say that two points \(x,y\) in \(X\) are neighbours, if \(d(x,y)<L\).
Let \(x,y\) be neighbours. Then:
\({\downarrow}f(x)\,\cap \,{\downarrow}f(y)\neq \varnothing\);
\(f(x)\,S\, f(y)\);
\(\mathrm{c}{f^{-1}(f(x))}\,\cap\, \mathrm{c}{f^{-1}(f(y))}\neq \varnothing\).
Proof. Due to the construction, a pair of adjacent handles, as well as a pair of adjacent handle and a disk, is mapped to a quasitree. Hence, if \(d(x,y)<L\), then \(f(x)\) and \(f(y)\) belong to the same quasitree \(F_i\). That \(f(x)S f(y)\) follows from the fact that \(F_i\) is an \(S\)-clique by Proposition [prop:prop-of-suit].
The third statement follows from the first, since \(f\) is a cp-morphism. ◻
5.6 Altering the metric↩︎
Let \(d\) denote the Euclidean distance in \(\mathbb{R}^3\). Our goal is to define jumps \(J\) in \(X\) in such a way that \(\varphi\) is satisfiable in \((X,d_{J})\).
Let \(B(x,\delta)\) denote the open ball in \(X\) centered at \(x\) of radius \(\delta\) (w.r.t. the Euclidean distance).
Let \(x\in X\). We put \[\label{eq:delta-x} \delta(x)=\sup\{\delta<\frac{1}{L}\mid B(x,\delta)\subseteq f^{-1}[{\uparrow}f(x)]\}.\tag{16}\] Since \(f^{-1}[{\uparrow}f(x)]\) is open, \(\delta(x)>0\).
For \(b\in W\), we define \(y_b\) and \(\delta(b)\). Let \(i\) be the least such that \(b \in W_i\). Take \(y_b\) in \(f_i^{-1}(b)\), which is not a limit of a handle (notice that if \(y\in f_i^{-1}(b)\) is a limit of a handle, then \(b=d_i\) or \(b=d_{i-1}\); in both cases, \({\downarrow}b\cap W_i\) contains the minimal points in \(W_i\), which are distinct from \(b\); we have \(\mathrm{c}f_i^{-1}(b)=f_i^{-1}[{\downarrow}b\cap W_i]\neq f_i^{-1}(b)\), so \(f_i^{-1}(b)\) is infinite.)
Let \(\delta(b)\) be the supremum of \(\delta\) such that \(\delta<\delta(y_b)\) and \(B(y_b,\delta)\) does not contain limits of handles. Let \(\delta_F= \frac{1}{2}\min\{\delta(b)\mid b\in W\}\). So we have \[\label{eq:delta-y} f[B(y_b,\delta_F)]\subseteq {\uparrow}b\tag{17}\] Also, notice that \(B(y_b,\delta_F)\) and \(B(y_c,\delta_F)\) are disjoint for distinct \(b,c\in W\).
Assume that for \(x\in X\) we have \(f(x)\, S\, b\). If \(d(x,y_b)\geq 1\), then we add the jump \[J(x,y_b)=1-\frac{1}{2}{\min\{\delta(x),\delta_F\}}.\] Notice that \(J(x,y_b)>\frac{1}{2}\).
Now consider the metric space \((X,d_{J})\).
\((X,d_{J})\) is connected.
Proof. Follows from Lemma 10 immediately. ◻
\(f:(X,d_{J})\twoheadrightarrow(W,\preceq)\) is a cp-morphism.
Proof. Follows from Lemma 10 and Proposition [prop:cpmorphBasic] immediately. ◻
Now consider the distance relation on \((X,d_{J})\): \[x\,S^{(J)}\, y\,\,\Leftrightarrow\,\, d_{J}(x,y)<1.\]
\(f:(X,S^{(J)})\twoheadrightarrow(W,S)\) is a p-morphism.
Proof. That \(f\) satisfies the back property of \(p\)-morphism is immediate from the definition of \(J\): if \(f(x)\,S\,b\) and \(d(x,y_b)\geq 1\), we added the jump \(J(x,y_b)\).
To check the relational homomorphism property, assume \(d_{J}(x,y)<1\). We aim to show that \(f(x)Sf(y)\).
Let \(w\) be the weighting function induced by \(J\) on \((X,d)\) (Definition 10). Then for some path \(\tau=(x_0,\ldots,x_m)\) from \(x\) to \(y\) we have \(\sum_{i<m} w(x_i,x_{i+1})<1\).
Clearly, this path has at most one jump, since any jump value is greater than \(\frac{1}{2}\).
If there are no jumps, then \(d(x,y)<1\), and hence \(x\) and \(y\) are neighbours, and the claim follows from Proposition [prop:neighbours].
Assume that \(\tau\) has one jump \((x_k,x_{k+1})\). Then \(x_{k+1}\) (or \(x_{k}\)) is \(y_b\) for some \(b\). It follows that both \(\sum_{i<k} w(x_i,x_{i+1})\) and \(\sum_{k+1\leq i<m} w(x_i,x_{i+1})\) are less than \({\min\{\delta(x_k),\delta_F\}}\). At the same time, these initial and final parts of \(\tau\) have no jumps, and we have \(d(x,x_k)\leq \sum_{i<k} w(x_i,x_{i+1})\) and \(d(x_{k+1},y)\leq \sum_{k+1\leq i<m} w(x_i,x_{i+1})\).
Now it follows from 16 and 17 that \(f(x_k) \preceq f(x)\) and \(f(x_{k+1}) \preceq f(y)\). We also have \(f(x_k)Sf(x_{k+1})\) due to the construction of jumps. By Proposition [prop:prop-of-suit][item3:prop:prop-of-suit], it follows that \(f(x)S f(y)\). ◻
From the p-morphism lemma [@BDV] and cp-morphism lemma [@Shehtman99], it follows that \(\varphi\) is satisfiable in \((X,d_J)\). Hence, we have
Theorem 2. In the language with the topological modality, universal modality, and a single distance modality, the logic of all connected, and also of all connected and compact metric spaces is \(\mathrm{S4UC_{<1}}\).
6 Concluding remarks↩︎
The construction given in the previous section does not seem to be applicable to the case of more than one metric modality. The main (and the only) problem is the relational homomorphism condition in the proof of Proposition [prop:jump-p-morph]: our argument that any path was augmented with at most one jump does not extend to the case of several distance relations. Hence, the problem of axiomatization of connected metric spaces ([@Wolter2005; @KuruczWZ05]) in the language of the topological closure \(\lozenge\), universal modality, and multiple metric modalities remains open.
Another natural question is the axiomatization of metric spaces that are \(a\)-connected for all positive \(a\). Such spaces are said to be well-chained [@TopologicalAnalysis-Whyburn]. We conjecture that for any set \({\mathrm A}\) of parameters, the \({\mathrm A}\)-logic of the class of all well-chained metric spaces is \(\mathrm{Metr}{({\mathrm A})}+\{\mathrm{Con}_a\mid a\in {\mathrm A}\}\).
These are only two of many open problems related to modal axiomatization of metric spaces. Of particular interest are distance logics of Euclidean spaces. Even the unimodal language with a single distance modality turns out to be surprisingly expressive: for example, it distinguishes between different dimensions and between the rational and real lines [@RTG-DistanceLogics]. However, no complete axiomatizations are known for the corresponding logics.
Acknowledgements↩︎
We are grateful to anonymous reviewers for their helpful comments on an earlier version of this text.
This work was supported by NSF Grant DMS - 2231414.
Appendix↩︎
Proof of Lemma 8. Very close to the argument in the proof of [@Kutz2007].
The case \({\mathrm A}=\varnothing\) is trivial. Assume \({\mathrm A}\neq \varnothing\). Let \(R=\bigcup_{l\in {\mathrm A}} R_l\). Since \((X, (R_l)_{l\in {\mathrm A}})\) is point-generated, \((X,R)\) is connected.
Let \[k=\frac{\max{{\mathrm A}}+1}{\min{{\mathrm A}}},\] and let \({\mathrm A}^{<2k}\) be the set of tuples over \({\mathrm A}\) whose length is less than \(2k\). Consider the set \[S=\{\oplus{{\vec{r}}}-l\mid \text{{{\vec{r}}}\in A^{<2k}, l\in {\mathrm A}, and \oplus{{\vec{r}}}> l}\}.\] Clearly, \(S\) is a finite set of positive numbers. Let \[\label{eq:epsilon} \varepsilon=\frac{\min (S\cup {\mathrm A})}{2k}.\tag{18}\] Since \(k>1\) and \(\min (S\cup {\mathrm A})\leq \min A\), we have \[\label{eq:metr:eps-small} \varepsilon<\frac{\min {\mathrm A}}{2}.\tag{19}\]
Let \(e=(a,b) \in R\), \(a\neq b\). Define the index \(\mathrm{ind}(e)\) of \(e\) as \(\min\{l\in {\mathrm A}\mid e\in R_l\}\), and its weight \(w(e)\) as \(\mathrm{ind}(e)-\varepsilon.\) By the definition, we put \(w(a,a)=0\).
For an \(R\)-path \(\tau=(a_0,\ldots,a_m)\), put \(w(\tau)=\sum_{i<m} w(a_i,a_{i+1})\).
Finally, for \(a,b \in X\), we define \[\label{eq:distance-for-postgraph} d(a,b)=\inf\{w(\tau) \mid \tau \text{ is an R-path from a to b}\}.\tag{20}\]
It is easy to see that \(d\) is a metric on \(X\). In particular, since \((X,R)\) is connected, \(d(a,b)\) is defined for all \(a,b\in X\). That \(d(a,b)=d(b,a)\) is immediate from the symmetry of relations. The triangle inequality is straightforward from 20 . It is also clear from the definition of \(w\) that \(d(a,b)\geq \min {\mathrm A}-\varepsilon\) for distinct \(a,b\).
It remains to show that for \(l\in {\mathrm A}\), \[\label{eq:metr-induced} aR_l b \text{ iff } d(a,b)<l.\tag{21}\]
The ‘only if’ follows from 20 and the definition of weight.
For the ‘if’ direction, assume that \(\displaystyle d(a,b)<l\in{\mathrm A}\). Then \(a\) and \(b\) are connected by an \(R\)-path \(\tau=(a_0,\ldots,a_m)\) with \(w(\tau)<l\). The case \(a=b\) is trivial, so let us assume that \(m>0\). We can also assume that \(\tau\) is simple, that is all \(a_i\) are distinct. For \(i<m\), put \(l_i=\mathrm{ind}(a_i,a_{i+1})\), and consider \({{\vec{r}}}=(l_0,\ldots, l_{m-1})\). We have \[\label{eq:metr:weight-eps} w(\tau)=\sum_{i<m}{(l_i-\varepsilon)}=\oplus{{\vec{r}}}-m\varepsilon<l.\tag{22}\]
We claim that \(m<2k\). Indeed, in view of 19 , we have \[m\frac{\min {\mathrm A}}{2}<m(\min {\mathrm A}-\varepsilon)\leq \oplus{{\vec{r}}}-m\varepsilon=w(\tau)< l\leq \max {\mathrm A},\] and hence we have \(m<2\frac{\max{{\mathrm A}}}{\min{{\mathrm A}}}<2k\).
Now we claim that \[\label{xscvikfd} \oplus{{\vec{r}}}\leq l.\tag{23}\] For the sake of contradiction, assume \(\oplus{{\vec{r}}}> l\). We have \(\oplus{{\vec{r}}}-l\in S\), and hence \[\oplus{{\vec{r}}}-l\geq \min S\geq \min (S\cup A)=2k\varepsilon>m\varepsilon,\] so \(\oplus{{\vec{r}}}-m\varepsilon> l\). This contradicts 22 , which proves [eq:metr:main].
We have \((a,b)\in R_{{{\vec{r}}}}\). Since \(F\) is a \(\mathrm{Metr}{({\mathrm A})}\)-frame and in view of [eq:metr:main], \((a,b)\in R_{l}\). This completes the proof of 21 . ◻
More ways to represent topological connectedness in propositional languages are discussed in [@RCC-2008; @RCC-2010].↩︎