June 30, 2026
The topological semantics of modal logic has been an active area of research ever since their introduction in the 1940s, with attention shifting in recent years from standard unimodal logic to more expressive frameworks. In particular, an Until-like path-reachability modality has recently been studied in Bezhanishvili et al. (2024) in polyhedral semantics; this paper investigates its topological counterpart. Focusing on the language combining said modality with the classical Cantor derivative modality, we exhibit an axiomatic system sound and complete both for the class of \(T_1\) topologies and for the class of all metric spaces, and establish its decidability. We also axiomatize the logic of all topological models in a weaker language obtained by substituting the closure modality for the Cantor derivative. To prove our results, we introduce an equivalent neighborhood-like semantics allowing for the finite model property.
Topological semantics provide ways of interpreting modal formulas in spatial terms, by viewing propositions as regions of a topological space and modal operators as expressing some spatial transformations. Two classical variants of topological semantics, both introduced by McKinsey and Tarski [@MT44], are the c-semantics and the d-semantics. In the c-semantics, the modal operators \(\Diamond\) and \(\Box\) are interpreted as closure and interior, respectively. The logic of all topological spaces then coincides with \(\mathbf{S4}\). Moreover, \(\mathbf{S4}\) is the logic of any dense-in-itself metric space [@MT44; @BB07]. In the more expressive d-semantics, the \(\Diamond\) modality is interpreted as the Cantor derivative, which maps a region to the set of its limit points. The logic of all topologies is \(\mathbf{wK4}\) [@BB07]. The separation axiom \(T_D\) is modally definable by \(\Box p \to \Box^2 p\), and \(\mathbf{K4}=\mathbf{wK4}+\Box p \to \Box^2 p\) is the logic of metrizable Stone spaces [@BEG10].
An Until-like binary modality \(\gamma\) for path-reachability was introduced in [@BCGGLM22] in the context of so-called polyhedral models. The formula \(\gamma(\varphi,\psi)\) is defined to be true at a point \(x\) iff there exists a continuous path beginning at \(x\), with all intermediate points validating \(\varphi\), and the end point validating \(\psi\). In [@BBCFG24], the logic of polyhedral models as well as the logic of Alexandroff spaces with this modality were axiomatized and shown to be decidable. In polyhedral and Alexandroff models, \(\gamma(\varphi,\top)\) defines the closure of the set defined by \(\varphi\), thus \(\gamma\)-semantics subsumes c-semantics [@BBCFG24]. This is not necessarily the case in an arbitrary topology, e.g., in any non-trivial totally path-disconnected space.
In this paper, we study logics related to \(\gamma\) in a general topological setting. In the language combining \(\gamma\) with c-semantics, we axiomatize the logic of all topologies and show that it coincides with the logic of metric spaces. In the language combining \(\gamma\) with d-semantics, we exhibit a formula defining the separation axiom \(T_1\), axiomatize the logic of all \(T_1\) topologies, and show that it is complete for the class of metric spaces. Thus, both logics are also characterized by the class of Hausdorff spaces, by the class of regular Hausdorff spaces, etc. Further, we establish that these logics are decidable.
In proving our results, we introduce an equivalent neighborhood-like semantics (cf. [@Pacuit]) for \(\gamma\), where the set of intermediate points of a path is treated as a “neighborhood” of the path’s original point. Then we establish the finite model property in this semantics by constructing an appropriate filtration of the canonical neighborhood-like model. In Sections 2–6, we obtain our result for the d-semantics, while their c-semantical counterparts are derived in Section 7.
In this section we establish some of the notation we will use. The powerset of \(X\) is denoted \(\mathcal{P}(X)\). For a transitive binary relation \(R\) on a set \(X\), we write \(R(x) := \left\{ y \in X \,:\, x\mathrel{R}y \right\}\), and call \(U \subseteq X\) an \(R\)-upset if \(R(x) \subseteq U\) for all \(x \in U\).
Topology. We use the following standard notions from general topology; see e.g. [@Engelking] for definitions: topological space; open, closed, discrete, and connected subsets; continuous map; metric space and its induced topology. A topological space \(\langle X,\tau\rangle\) is called \(T_1\) if for all distinct \(x,y \in X\) there exists an open set \(U\) with \(x \in U\) and \(y \not\in U\). Note that all metric spaces induce \(T_1\) topologies [@Engelking].
When a subset of \(\mathbb{R}\) is mentioned (e.g., \([0,1]\) or \(\mathbb{Q}\)), the usual metric given by \(d(x,y):=|x-y|\) and its induced topology are implicit. A path in a topological space \(\langle X,\tau\rangle\) is a continuous map \([0,1] \to X\).
Miscellaneous. For a map \(\pi:[0,1] \to X\) and \(a,b \in [0,1]\), denote by \(\pi \restriction [a,b]\) the map \([0,1]\to X\) given by \(t \mapsto \pi(bt-at+a)\). Observe that if a topology on \(X\) is given and \(\pi\) is a path, then \(\pi \restriction [a,b]\) is also a path. Note that we allow \(b<a\); in particular, \(\pi \restriction [1,0]\) is the “reverse” of \(\pi\).
For a set \(X\) and \(x,y \in X\), denote by \(\iota_{x,y}\) the map \([0,1] \to X\) given by \(\iota_{x,y}(0)=x\) and \(\iota_{x,y}(t)=y\) for \(t \in (0,1]\). In particular, \(\iota_{x,x}\) is constant. Note that \(\iota_{x,y}\) may or may not be continuous when some topology on \(X\) is given.
Language. Fix a countably infinite set of propositional variables \(\mathrm{Prop}\). Denote by \(\mathcal{L}\) the language built from \(\mathrm{Prop}\) and \(\bot\) using the unary connective \({\mathop{\square}}\) and binary connectives \(\to\) and \(\gamma\). For a formula \(\varphi\in\mathcal{L}\), denote by \(\mathop{\mathrm{Sub}}\varphi\) the set of its subformulas.
Semantics. We interpret \(\Box\) as in the usual topological \(d\)-semantics [@BB07; @BEG10], and \(\gamma\) as the reachability modality from [@BBCFG24; @BCGGLM22]. Formally, a topological model is a triple \(\mathfrak{M}=\langle X,\tau,\llbracket \cdot \rrbracket\rangle\), where \(\langle X, \tau\rangle\) is a topological space, and \(\llbracket \cdot \rrbracket : \mathrm{Prop}\to \mathcal{P}(X)\). The map \(\llbracket \cdot \rrbracket\) is extended to \(\mathcal{L}\) as follows:
\(\llbracket \bot \rrbracket=\varnothing\);
\(\llbracket \varphi\to \psi \rrbracket = (X \setminus \llbracket \varphi \rrbracket) \cup \llbracket \psi \rrbracket\);
\(x \in \llbracket {\mathop{\square}}\varphi \rrbracket\) iff there exists \(U \in \tau\) such that \(x \in U\) and \(U \setminus \{x\} \subseteq \llbracket \varphi \rrbracket\);
\(x \in \llbracket \gamma(\varphi,\psi) \rrbracket\) iff there exists a path \(\pi\) with \(\pi(0) = x\), \(\pi[(0,1)] \subseteq \llbracket \varphi \rrbracket\), and \(\pi(1) \in \llbracket \psi \rrbracket\).
We write \(\mathfrak{M} \models \varphi\) iff \(\llbracket \varphi \rrbracket=X\).
Abbreviations. We use standard abbreviations \(\top\), \(\neg\), \(\vee\), and \(\wedge\). We also abbreviate \({\mathpalette\dotop@{\square}}\varphi:= \varphi\wedge {\mathop{\square}}\varphi\) and \(\widehat\gamma(\varphi,\psi) := \varphi\wedge \gamma(\varphi,\varphi\wedge\psi)\). Note that in a topological model:
\(\llbracket {\mathpalette\dotop@{\square}}\varphi \rrbracket\) is the interior of \(\llbracket \varphi \rrbracket\). In particular, all \(\llbracket {\mathpalette\dotop@{\square}}\varphi \rrbracket\) are open sets;
\(x \in \llbracket \widehat\gamma(\varphi,\psi) \rrbracket\) iff there exists a path \(\pi\) with \(\pi(0)=x\), \({\pi[[0,1]] \subseteq \llbracket \varphi \rrbracket}\), and \(\pi(1) \in \llbracket \psi \rrbracket\).
In this section, we present an \(\mathcal{L}\)-formula defining the separation axiom \(T_1\). We also exhibit an axiomatic system \(\mathbf{TLR}\) and verify its soundness for \(T_1\) topologies.
A topological space \(\langle X,\tau\rangle\) is \(T_1\) if and only if \(\gamma(p\wedge {\mathop{\square}}\neg p, \top) \to p\) is valid in all topological models based on \(\langle X,\tau\rangle\).
Proof. Suppose \(\langle X,\tau\rangle\) is not \(T_1\), i.e., there exist distinct \(x,y\in X\) such that every open neighborhood of \(x\) contains \(y\), and thus \(\iota_{x,y}\) is continuous. Take \(\llbracket p \rrbracket := \{y\}\). Now \(y \in \llbracket {\mathop{\square}}\neg p \rrbracket\), whence \(\iota_{x,y}\) witnesses \(x \in \llbracket \gamma(p\wedge {\mathop{\square}}\neg p,\top) \rrbracket\). However, \(x \not\in \llbracket p \rrbracket\).
Conversely, suppose \(\langle X,\tau\rangle\) is \(T_1\). Consider a valuation \(\llbracket \cdot \rrbracket\) and a point \(x\) with \(x \in \llbracket \gamma(p\wedge{\mathop{\square}}\neg p,\top) \rrbracket\) witnessed by some path \(\pi\). The set \(\llbracket p\wedge {\mathop{\square}}\neg p \rrbracket\) is discrete, whence its connected subset \(\pi[(0,1)]\) is some singleton \(\{y\}\). Now, \(\pi\) is continuous with \(\pi(0)=x\) and \(\pi[(0,1)]=y\), thus every open neighborhood of \(x\) contains \(y\), hence \(x=y \in \llbracket p \rrbracket\). ◻
Definition 1. The logic \(\mathbf{TLR}\) is defined by all axioms and rules of \(\mathbf{K4}\) for \({\mathop{\square}}\) together with the following:
\(\gamma(\varphi, \psi_1 \vee \psi_2) \to \gamma(\varphi, \psi_1) \vee\gamma(\varphi,\psi_2)\);
\(\gamma(\varphi, \varphi\wedge \gamma(\varphi,\psi)) \to \gamma(\varphi,\psi)\);
\(\varphi\to \gamma(\varphi,\varphi)\);
\(\neg \gamma(\bot,\top)\);
\(\gamma (\varphi, \neg \gamma(\varphi,\psi)) \to \neg \psi\);
\(\gamma(\varphi, \psi) \to \gamma(\varphi\wedge \gamma(\varphi,\psi),\psi)\);
\({\mathpalette\dotop@{\square}}\psi \wedge \gamma(\varphi,\chi) \to \gamma(\varphi\wedge{\mathpalette\dotop@{\square}}\psi, (\varphi\wedge \neg {\mathpalette\dotop@{\square}}\psi) \vee\chi)\);
\(\widehat\gamma\big(\chi\wedge ({\mathpalette\dotop@{\square}}\varphi_1\vee{\mathpalette\dotop@{\square}}\varphi_2)\wedge(\widehat\gamma(\chi\wedge{\mathpalette\dotop@{\square}}\varphi_1,\psi)\vee \widehat\gamma(\chi\wedge{\mathpalette\dotop@{\square}}\varphi_2,\psi)\to\psi), \psi\big) \to \psi\);
\(\gamma(\varphi\wedge {\mathop{\square}}\neg \varphi, \top) \to \varphi\);
\(\begin{array}{r} \varphi\to\varphi' \quad \psi\to\psi' \\ \cline{1-1} \gamma(\varphi,\psi)\to\gamma(\varphi',\psi')\\ \end{array}\).
Now we verify soundness using some natural properties of paths in a topology; e.g., (A1) expresses that a concatenation of two paths is also a path, (A2) signifies the existence of constant paths, etc.
The logic \(\mathbf{TLR}\) is sound for the class of \(T_1\) topologies. Moreover, (A0)–(A7) and (Mon) are valid in all topologies.
Proof. Consider a topological model \(\mathfrak{M}=\langle X, \tau,\llbracket \cdot \rrbracket\rangle\) and a point \(x \in X\).
(A0): If \(x \in\llbracket \gamma(\varphi,\psi_1\vee\psi_2) \rrbracket\) is witnessed by a path \(\pi\), then \(\pi(1) \in \llbracket \psi_1 \vee \psi_2 \rrbracket\), hence \(\pi(1) \in \llbracket \psi_i \rrbracket\) for some \(i \in \{1,2\}\), whence \(\pi\) witnesses \(x \in\llbracket \gamma(\varphi,\psi_i) \rrbracket\).
(A1): Suppose \(x \in \llbracket \gamma(\varphi,\varphi\wedge \gamma(\varphi,\psi)) \rrbracket\) is witnessed by \(\pi_1\), and \(\pi_1(1) \in\llbracket \gamma(\varphi,\psi) \rrbracket\) is witnessed by \(\pi_2\). Now the path \(\pi\) given by \(\pi \restriction [0,\frac{1}{2}]=\pi_1\) and \(\pi \restriction [\frac{1}{2},1]=\pi_2\) witnesses \(x \in \llbracket \gamma(\varphi,\psi) \rrbracket\).
(A2): If \(x \in \llbracket \varphi \rrbracket\), then \(\iota_{x,x}\) witnesses \(x \in \llbracket \gamma(\varphi,\varphi) \rrbracket\).
(A3) is valid since \(\pi[(0,1)] \neq\varnothing\) for every path \(\pi\).
(A4): Suppose \(x \in \llbracket \gamma(\varphi,\neg\gamma(\varphi,\psi)) \rrbracket\) is witnessed by a path \(\pi\), and assume \(x \in\llbracket \psi \rrbracket\). Then \(\pi \restriction [1,0]\) witnesses that \(\pi(1) \in \llbracket \gamma(\varphi,\psi) \rrbracket\), which is a contradiction.
(A5): Suppose \(x \in \llbracket \gamma(\varphi, \psi) \rrbracket\) is witnessed by a path \(\pi\). Then for every \(t \in (0,1)\), the path \(\pi \restriction [t,1]\) witnesses \(\pi(t) \in \llbracket \gamma(\varphi,\psi) \rrbracket\). Therefore, \(\pi\) witnesses \(x \in \llbracket \gamma(\varphi\wedge \gamma(\varphi,\psi), \psi) \rrbracket\).
(A6): Suppose \(x \in\llbracket {\mathpalette\dotop@{\square}}\psi \rrbracket\) and \(x \in \llbracket \gamma(\varphi,\chi) \rrbracket\) is witnessed by a path \(\pi\). If \(\pi[(0,1)] \subseteq \llbracket {\mathpalette\dotop@{\square}}\psi \rrbracket\), then \(\pi\) witnesses \(x \in \llbracket \gamma(\varphi\wedge {\mathpalette\dotop@{\square}}\psi, \chi) \rrbracket\). Otherwise, denote by \(t\) the least element of the closed set \(\pi^{-1}[\llbracket \neg {\mathpalette\dotop@{\square}}\psi \rrbracket]\). As \(0<t<1\), the path \(\pi \restriction [0,t]\) witnesses that \(x \in \llbracket \gamma(\varphi\wedge {\mathpalette\dotop@{\square}}\psi, \varphi\wedge \neg {\mathpalette\dotop@{\square}}\psi) \rrbracket\).
(A7): Suppose \(x \in \llbracket \widehat\gamma(\chi\wedge ({\mathpalette\dotop@{\square}}\varphi_1\vee{\mathpalette\dotop@{\square}}\varphi_2)\wedge(\widehat\gamma(\chi\wedge{\mathpalette\dotop@{\square}}\varphi_1,\psi)\vee \widehat\gamma(\chi\wedge{\mathpalette\dotop@{\square}}\varphi_2,\psi)\to\psi), \psi) \rrbracket\) is witnessed by a path \(\pi\), and assume \(x \not\in\llbracket \psi \rrbracket\). Denote by \(t\) the supremum of \(\pi^{-1}[\llbracket \neg\psi \rrbracket]\). Fix \(i \in \{1,2\}\) such that \(\pi(t) \in \llbracket {\mathpalette\dotop@{\square}}\varphi_i \rrbracket\) and \(\varepsilon>0\) such that \([\max\{t-\varepsilon,0\},\min\{t+\varepsilon,1\}] \subseteq \pi^{-1}[\llbracket {\mathpalette\dotop@{\square}}\varphi_i \rrbracket]\). Now \(\pi \restriction [t,\min\{t+\varepsilon,1\}]\) witnesses that \(\pi(t) \in \llbracket \widehat\gamma(\chi\wedge{\mathpalette\dotop@{\square}}\varphi_i, \psi) \rrbracket\). As \(\pi[[0,1]] \subseteq \llbracket \widehat\gamma(\chi\wedge {\mathpalette\dotop@{\square}}\varphi_i, \psi) \to \psi \rrbracket\), we conclude that \(\pi(t) \in \llbracket \psi \rrbracket\). By the choice of \(t\), there exists \(t' \in \pi^{-1}[\llbracket \neg \psi \rrbracket] \cap [t-\varepsilon,t]\), thus \(\pi \restriction [t',t]\) witnesses \(\pi(t') \in \llbracket \widehat\gamma(\chi\wedge {\mathpalette\dotop@{\square}}\varphi_i,\psi) \rrbracket\), hence \(\pi(t') \in \llbracket \psi \rrbracket\), which is a contradiction.
(Mon): If \(\llbracket \varphi \rrbracket\subseteq \llbracket \varphi' \rrbracket\) and \(\llbracket \psi \rrbracket\subseteq\llbracket \psi' \rrbracket\), then \(\llbracket \gamma(\varphi,\psi) \rrbracket\subseteq\llbracket \gamma(\varphi',\psi') \rrbracket\).
If \(\langle X,\tau\rangle\) is \(T_1\), then the validity of (A8) follows from Proposition [P:t1Characterization], and the validity of \(\mathbf{K4}\) is well-known [@BB07]. ◻
In this section, we define an alternative semantics for \(\mathcal{L}\) (flanked Kripke frames) and a certain class of finite frames in it (suitable frames). In the following sections, we will establish our results by proving that \(\mathbf{TLR}\) is complete for suitable frames (Section 5) and that suitable frames define the same logic as \(T_1\) topologies (Section 6).
Definition 2. A flanked Kripke frame* is a triple \(\langle X, R, P \rangle\), where:*
\(R \subseteq X \times X\) is transitive;
\(P \subseteq X \times \mathcal{P}(X) \times X\) is monotone, i.e., if \(\langle x, S,y\rangle \in P\) and \(S \subseteq S' \subseteq X\), then \(\langle x,S',y\rangle\in P\).
A flanked Kripke model* is a flanked Kripke frame equipped with a valuation \(\llbracket \cdot \rrbracket : \mathrm{Prop}\to \mathcal{P}(X)\), which is extended to \(\mathcal{L}\) as follows:*
\(\llbracket \bot \rrbracket = \varnothing\);
\(\llbracket \varphi\to\psi \rrbracket = (X \setminus \llbracket \varphi \rrbracket) \cup \llbracket \psi \rrbracket\);
\(x \in\llbracket {\mathop{\square}}\varphi \rrbracket\) iff \(R(x) \subseteq \llbracket \varphi \rrbracket\);
\(x \in \llbracket \gamma(\varphi,\psi) \rrbracket\) iff there exists \(y \in \llbracket \psi \rrbracket\) satisfying \(\langle x,\llbracket \varphi \rrbracket,y \rangle \in P\).
This semantics combines a Kripke structure \(R\) for \(\Box\) and and a “flanked” structure \(P\) for \(\gamma\). The former is natural to consider as \(\mathbf{K4}\) is the logic of \(T_1\) topologies [@BB07]. To motivate the latter, note that the topological interpretation of \(\gamma\) may be rewritten as follows: \(x \in \llbracket \gamma(\varphi,\psi) \rrbracket\) iff there exists \(y \in \llbracket \psi \rrbracket\) with \(\langle x,\llbracket \varphi \rrbracket,y\rangle \in P\), where \(P\) is a monotone set defined as follows: \[P := \left\{ \langle x, S,y\rangle \in X \times \mathcal{P}(X) \times X \,:\, \text{there exists a path \pi with \pi(0)=x, \pi[(0,1)]\subseteq S, and \pi(1)=y} \right\}.\]
This “flanked” semantics for \(\gamma\) is similar to the monotone neighborhood semantics used for non-normal modal logics such as \(\mathbf{EM}\) (cf. [@Pacuit]).
We now list the frame properties that roughly correspond to the axioms (A1)–(A8).
Definition 3. A flanked Kripke frame \(\langle X,R,P\rangle\) is suitable* if it is finite and has the following 8 properties:*
if \(\langle x, S,z\rangle \in P\), \(\langle z,S,y\rangle \in P\), and \(z \in S\), then \(\langle x, S,y\rangle \in P\);
\(\langle x, \{x\}, x \rangle \in P\) for all \(x \in X\);
and for all \(\langle x,S,y\rangle \in P\):
\(S \neq \varnothing\);
\(\langle y,S,x\rangle \in P\);
for each \(z \in S\), either \(\langle x, S \setminus \{z\}, y \rangle \in P\) or \(\langle z, S, y\rangle \in P\);
for every \(R\)-upset \(U\) with \(x \in U\), there exists \(z \in (S \setminus U) \cup \{y\}\) with \(\langle x,S \cap U, z\rangle \in P\);
if \(x,y\in S\), then, for all \(R\)-upsets \(U_1\) and \(U_2\) with \(S \subseteq U_1 \cup U_2\), there exists an \(\langle S,U_1,U_2,x,y\rangle\)-sequence. Here an \(\langle S,U_1,U_2,x,y\rangle\)-sequence* is a sequence \(x_0,\dotsc,x_k\) with \(k \geq 0\), \(x_0=x\), and \(x_k=y\) such that for each \(i<k\) there exists \(j_i \in \{1,2\}\) satisfying \(x_i,x_{i+1} \in S \cap U_{j_i}\) and \(\langle x_i, S \cap U_{j_i}, x_{i+1} \rangle \in P\);*
if \(S=\{y\}\), then either \(x = y\) or \(yRy\).
In the remainder of this section, we briefly motivate properties (F1)–(F8) and exhibit some illustrative examples.
Note that \(R\)-upsets form an Alexandroff topology on \(X\) (cf. [@BB07]). Given a topological space, the set \(P\) from Remark [R:semanticMotivation] satisfies (F1)–(F5), as well as (F6) and (F7) if we substitute “open set” for “\(R\)-upset.” One can verify this similarly to the proof of Proposition [P:soundness], invoking the same topological properties.
All axioms and rules of \(\mathbf{K4}\), axiom (A0), and rule (Mon) are valid in all flanked Kripke frames. One can check that (F1)–(F4) and (F6)–(F7) are precisely the frame properties corresponding to (A1)–(A4) and (A6)–(A7). However, (F5) is defined by (A5) only over finite frames, and (F8) is defined by (A8) only over frames satisfying (F3)–(F6). We employ (F5) and (F8) merely for convenience.
Example 1. Take \(X=\{a,b,c\}\), \(R=(\{b,c\} \times X) \cup \{\langle a,a\rangle\}\), and \(\langle x,S,y\rangle\in P\) iff (i) \(x=y \in S\), (ii) \(S=X\), or (iii) \(a \in S\) and \(x,y \in \{a,b\}\). A direct inspection shows that \(\langle X,R,P\rangle\) is suitable. If we omit \(\langle a,a\rangle\) from \(R\), the resulting frame refutes (F8) since \(\langle b,\{a\},a\rangle \in P\), but (F1)–(F7) are unaffected. If we omit (iii) from \(P\), the resulting frame satisfies (F1)–(F5), (F7), and (F8), but not (F6).
Example 2. Take \(X = \{a,b,c,d,e,f\}\), \(R = \{a,b\}^2 \cup \{c,d\}^2 \cup (X \times \{e,f\})\), and \(\langle x,S,y\rangle \in P\) iff (i) \(x=y \in S\), (ii) \(x,y \in \{a,c,e\}\) and \(e \in S\), (iii) \(x,y \in \{b,d,f\}\) and \(f \in S\), or (iv) \(S=X\). This \(\langle X,R,P\rangle\) refutes (F7) since \(\langle a,X,f\rangle \in P\) but there are no \(\langle X,\{a,b,e,f\}, \{c,d,e,f\}, a,f\rangle\)-sequences. However, one can verify (F1)–(F6) and (F8).
Example 3. The axiomatic system obtained from \(\mathbf{TLR}\) by dropping (A8) is sound but not complete for the class of \(T_D\) spaces. Indeed, one can verify that \(\varphi:= \gamma(p\wedge \Box\neg p\wedge \gamma(q,\top), \top) \to \gamma(q,\top)\) is valid in all topological models. Now take \(X=\{a,b,c\}\), \(R=\{\langle a,b\rangle, \langle b,c\rangle, \langle a,c\rangle\}\), and \(\langle x,S,y\rangle \in P\) iff (i) \(x=y \in S\), (ii) \(x,y \in \{a,b\}\) and \(b \in S\), (iii) \(x,y \in \{b,c\}\) and \(c \in S\), or (iv) \(x,y \in \{a,b,c\}\) and \(\{b,c\}\subseteq S\). As seen by inspection, \(\langle X,R,P\rangle\) satisfies (F1)–(F7) and thus validates said axiomatic system. Taking \(\llbracket p \rrbracket := \{b\}\) and \(\llbracket q \rrbracket := \{c\}\), we obtain \(a \not\in \llbracket \varphi \rrbracket\), whence \(\varphi\) is not derivable.
In this section, we verify that \(\mathbf{TLR}\) has the finite model property in the flanked Kripke semantics, i.e., that \(\mathbf{TLR}\) is complete for the class of suitable frames (Proposition [P:flankedFMP]). First, we define the canonical flanked Kripke model, similarly to canonical models in monotone neighborhood semantics (cf. [@Pacuit]). Then we construct a suitable filtration.
Definition 4. A set \(\Gamma \subseteq \mathcal{L}\) is \(\mathbf{TLR}\)-consistent* if there exists no finite \(\Gamma' \subseteq \Gamma\) with \(\mathbf{TLR} \vdash \bigwedge \Gamma' \to \bot\). The canonical flanked Kripke model is \(\mathfrak{M}_c = \langle X_c, R_c, P_c, \llbracket \cdot \rrbracket_c\rangle\), where:*
\(X_c\) is the class of all maximal \(\mathbf{TLR}\)-consistent sets;
\(\Gamma \mathrel{R_c} \Delta\) iff for all \({\mathop{\square}}\varphi\in \Gamma\) we have \(\varphi\in \Delta\);
\(\langle \Gamma, S, \Delta\rangle \in P_c\) iff for all \(\varphi\in \bigcap S\) and \(\psi \in \Delta\) we have \(\gamma(\varphi,\psi) \in \Gamma\);
\(\Gamma \in \llbracket p \rrbracket_c\) iff \(p \in \Gamma\).
Lemma 1. \(\mathfrak{M}_c\) is indeed a flanked Kripke model.
Proof. Since \(\mathbf{TLR} \vdash {\mathop{\square}}\varphi\to{\mathop{\square}}^2\varphi\), the relation \(R_c\) is transitive. It should be clear that \(P_c\) is monotone. ◻
As for the usual neighborhood semantics of [@Pacuit], we have the following:
Lemma 2. For all \(\Gamma\in X_c\) and \(\chi \in \mathcal{L}\), we have \(\Gamma \in \llbracket \chi \rrbracket_c\) iff \(\chi \in \Gamma\).
Proof. By induction on \(\chi\). The base case and the step for \(\chi=\varphi\to\psi\) or \(\chi={\mathop{\square}}\varphi\) are as in the standard canonical Kripke model construction for modal logic (cf. [@CZbook]); we only consider \(\chi=\gamma(\varphi,\psi)\). If \(\Gamma \in \llbracket \gamma(\varphi,\psi) \rrbracket_c\), then \(\langle \Gamma, \llbracket \varphi \rrbracket_c, \Delta\rangle \in P_c\) for some \(\Delta \in \llbracket \psi \rrbracket_c\), whence \(\varphi\in \bigcap \llbracket \varphi \rrbracket_c\) and \(\psi \in \Delta\) by the induction hypothesis, hence \(\gamma(\varphi,\psi)\in \Gamma\) by definition of \(P_c\).
Conversely, suppose \(\gamma(\varphi,\psi) \in \Gamma\). Assume \(\Delta_0 := \{\psi\} \cup \left\{ \neg\psi' \,:\, \gamma(\varphi,\psi') \not\in \Gamma \right\}\) is not \(\mathbf{TLR}\)-consistent, witnessed by \(\vdash \psi \to \bigvee_{i=1}^k \psi'_i\). If \(k>0\), it follows by (Mon) and (A0) that \(\vdash \gamma(\varphi,\psi) \to \bigvee_{i=1}^k \gamma(\varphi, \psi'_i)\), which is a contradiction. If \(k=0\), i.e., \(\vdash \neg\psi\), then \(\vdash \psi \to \neg\gamma(\varphi,\top)\) and \(\vdash \gamma(\varphi,\neg\gamma(\varphi,\top))\to \bot\) by (A4), hence \(\vdash \gamma(\varphi,\psi)\to\bot\) by (Mon), which is also a contradiction. Therefore, \(\Delta_0\) is \(\mathbf{TLR}\)-consistent. Fix some \(\Delta \in X_c\) extending \(\Delta_0\). Now for every \(\varphi' \in \bigcap \llbracket \varphi \rrbracket_c\) and \(\psi' \in \Delta\) we have \(\vdash \varphi\to \varphi'\) and \(\gamma(\varphi,\psi') \in \Gamma\), thus \(\gamma(\varphi',\psi')\in\Gamma\) by (Mon). Therefore, \(\langle \Gamma,\llbracket \varphi \rrbracket_c,\Delta \rangle \in P_c\) witnesses \(\Gamma \in \llbracket \gamma(\varphi,\psi) \rrbracket_c\). ◻
For the remainder of this section, fix a formula \(\varphi_0 \in \mathcal{L}\). To establish the finite model property, we take the “closure under concatenations” (i.e., under (F1)) of the “minimal \(\varphi_0\)-filtration.” We first verify that it admits a “filtration lemma” (Lemma 3). Then we show that it is a suitable frame, by establishing that the “minimal \(\varphi_0\)-filtration” itself satisfies (F2)–(F8) (Lemma 4) and that said “closure under concatenations” preserves (F2)–(F8) (Lemma 5).
This line of reasoning resembles e.g. a classical proof of the Kripke finite model property of \(\mathbf{S4}\) by showing that the transitive closure of the minimal filtration is a filtration, that the minimal filtration itself is reflexive, and that transitive closure preserves reflexivity (cf. [@CZbook]).
Definition 5. Set \(\mathfrak{M}^+ := \langle X_c/\mathord{\sim}, R, P^+, \llbracket \cdot \rrbracket \rangle\), where:
\(\Gamma \sim \Delta\) iff \(\Gamma \in \llbracket \varphi \rrbracket_c \Longleftrightarrow\Delta \in\llbracket \varphi \rrbracket_c\) for all \(\varphi\in \mathop{\mathrm{Sub}}\varphi_0\). Denote the projection \(X_c \to X_c/\mathord{\sim}\) by \(g\);
\(R\) is the transitive closure of \(\left\{ \langle g(x), g(y)\rangle \,:\, x\mathrel{R_c}y \right\}\);
\(P := \left\{ \langle g(\Gamma), g[S], g(\Delta)\rangle \,:\, \langle \Gamma,S,\Delta\rangle \in P_c \right\}\);
\(P^+\) is the smallest set extending \(P\) and satisfying (F1);
\(\llbracket p \rrbracket := g[\llbracket p \rrbracket_c]\) for all \(p \in \mathrm{Prop}\).
Observe that \(\langle x,S,y\rangle \in P^+\) iff there exists a sequence \(x_0,\dotsc,x_k\) with \(k\geq 1\), \(x_0=x\), \(x_k=y\), and \(x_1,\dotsc,x_{k-1} \in S\) such that \(\langle x_i, S,x_{i+1}\rangle \in P\) for each \(i=0,\dotsc,k-1\).
Lemma 3. For every \(\chi \in \mathop{\mathrm{Sub}}\varphi_0\) we have \(\llbracket \chi \rrbracket_c = g^{-1}[\llbracket \chi \rrbracket]\).
Proof. By induction on \(\chi\). The base case and the step for \(\chi=\varphi\to\psi\) or \(\chi={\mathop{\square}}\varphi\) are as in the standard filtration construction for \(\mathbf{K4}\) (cf. [@CZbook]); we only consider \(\chi=\gamma(\varphi,\psi)\). If \(\Gamma \in \llbracket \gamma(\varphi,\psi) \rrbracket_c\) is witnessed by \(\langle \Gamma, \llbracket \varphi \rrbracket_c, \Delta\rangle \in P_c\), then \(\langle g(\Gamma), \llbracket \varphi \rrbracket, g(\Delta)\rangle \in P \subseteq P^+\) witnesses \(g(\Gamma) \in \llbracket \gamma(\varphi,\psi) \rrbracket\).
Conversely, suppose \(g(\Gamma) \in \llbracket \gamma(\varphi,\psi) \rrbracket\) is witnessed by \(\langle g(\Gamma),\llbracket \varphi \rrbracket, y\rangle \in P^+\), and fix a corresponding sequence \(x_0,\dotsc,x_k\) as in Remark [R:concat]. For each \(i<k\), fix also \(\Gamma_i \in g^{-1}(x_i)\) and \(\Gamma'_{i+1} \in g^{-1}(x_{i+1})\) with \(\langle \Gamma_i, \llbracket \varphi \rrbracket_c, \Gamma_{i+1}'\rangle \in P_c\). Let us show by descending induction on \(i=k-1,\dotsc,0\) that \(\Gamma_i \in \llbracket \gamma(\varphi,\psi) \rrbracket_c\). For \(i=k-1\), it suffices to note that \(\langle \Gamma_{k-1},\llbracket \varphi \rrbracket_c, \Gamma_k'\rangle \in P_c\) and \(\Gamma_k' \in g^{-1}(y) \subseteq g^{-1}[\llbracket \psi \rrbracket] = \llbracket \psi \rrbracket_c\). Now consider \(i<k-1\) and suppose \(\Gamma_{i+1} \in \llbracket \gamma(\varphi,\psi) \rrbracket_c\). As \(\Gamma_{i+1},\Gamma_{i+1}' \in g^{-1}(x_{i+1})\), we have \(\Gamma_{i+1}\sim\Gamma_{i+1}'\), thus \(\Gamma_{i+1}' \in \llbracket \gamma(\varphi,\psi) \rrbracket_c\), hence \(\Gamma_i \in \llbracket \gamma(\varphi,\varphi\wedge\gamma(\varphi,\psi)) \rrbracket_c\). By Lemma 2 we have \(\mathfrak{M}_c \models \mathbf{TLR}\), thus \(\llbracket \gamma(\varphi,\varphi\wedge\gamma(\varphi,\psi)) \rrbracket_c \subseteq \llbracket \gamma(\varphi,\psi) \rrbracket_c\) by (A1), hence \(\Gamma_i \in \llbracket \gamma(\varphi,\psi) \rrbracket_c\). We conclude that \(\Gamma_0 \in \llbracket \gamma(\varphi,\psi) \rrbracket_c\). Since \(\Gamma,\Gamma_0 \in g^{-1}(x_0)\), we have \(\Gamma \sim\Gamma_0\), hence \(\Gamma \in \llbracket \gamma(\varphi,\psi) \rrbracket_c\). ◻
Lemma 4. The flanked Kripke frame \(\langle X_c/\mathord{\sim}, R, P\rangle\) satisfies (F2)–(F8).
Proof. First note that:
All instances of (A2)–(A8) are valid in \(\mathfrak{M}_c\). Indeed, \(\mathfrak{M}_c \models \mathbf{TLR}\) by Lemma 2.
For every \(T \subseteq X_c/\mathord{\sim}\) there exists a formula \(\varphi\in \mathcal{L}\) with \(g^{-1}[T]=\llbracket \varphi \rrbracket_c\). Moreover, if \(T\) is an \(R\)-upset, then \(\llbracket \varphi \rrbracket_c = \llbracket {\mathpalette\dotop@{\square}}\varphi \rrbracket_c\). Indeed, an appropriate \(\varphi\) may be built as a Boolean combination of \(\mathop{\mathrm{Sub}}\varphi_0\). If \(T\) is an \(R\)-upset and \(\Gamma \in \llbracket \varphi \rrbracket_c\), then for every \(\Delta \in R_c(\Gamma)\) we have \(g(\Gamma) \mathrel{R} g(\Delta)\) and \(g(\Gamma) \in T\), thus \(g(\Delta) \in T\), whence \(\Delta \in \llbracket \varphi \rrbracket_c\), hence \(\Gamma \in \llbracket {\mathpalette\dotop@{\square}}\varphi \rrbracket_c\).
Now we check each of the requisite properties.
(F2): Consider \(x \in X_c/\mathord{\sim}\). Fix some \(\Gamma \in g^{-1}(x)\) and \(\varphi\) such that \(\llbracket \varphi \rrbracket_c = g^{-1}(x)\). We have \(\Gamma \in \llbracket \varphi \rrbracket_c \subseteq \llbracket \gamma(\varphi,\varphi) \rrbracket_c\) by (A2), whence \(\langle \Gamma, \llbracket \varphi \rrbracket_c,\Gamma' \rangle \in P_c\) for some \(\Gamma' \in \llbracket \varphi \rrbracket_c\), hence \(\langle x, \{x\},x \rangle \in P\).
For (F3)–(F8), consider \(\langle x, S, y \rangle \in P\), and fix \(\Gamma \in g^{-1}(x)\) and \(\Delta \in g^{-1}(y)\) such that \(\langle \Gamma, g^{-1}[S], \Delta\rangle \in P_c\).
(F3): Note that \(\Gamma\not\in\llbracket \gamma(\bot,\top) \rrbracket_c\) by (A3), thus \(g^{-1}[S] \neq \varnothing\), hence \(S \neq \varnothing\).
(F4): Fix \(\varphi\) and \(\psi\) such that \(\llbracket \varphi \rrbracket_c = g^{-1}[S]\) and \(\llbracket \psi \rrbracket_c=g^{-1}(x)\). We have \(\Gamma \in \llbracket \psi \rrbracket_c\), thus \(\Gamma \not\in\llbracket \gamma(\varphi,\neg\gamma(\varphi,\psi)) \rrbracket_c\) by (A4), whence \(\Delta\not\in\llbracket \neg \gamma(\varphi,\psi) \rrbracket_c\), hence \(\langle \Delta, \llbracket \varphi \rrbracket_c, \Gamma'\rangle \in P_c\) for some \(\Gamma' \in \llbracket \psi \rrbracket_c\), thus \(\langle y,S,x\rangle \in P\).
(F5): Consider \(z \in S\) and fix \(\varphi, \psi\) with \(\llbracket \varphi \rrbracket_c = g^{-1}[S]\) and \(\llbracket \psi \rrbracket_c = g^{-1}(y)\). If there exists \(\Theta \in g^{-1}(z) \cap \llbracket \gamma(\varphi,\psi) \rrbracket_c\), then \(\langle \Theta, \llbracket \varphi \rrbracket_c, \Delta'\rangle \in P_c\) for some \(\Delta' \in \llbracket \psi \rrbracket_c\), whence \(\langle z, S,y \rangle \in P\). Now suppose \(g^{-1}(z) \cap \llbracket \gamma(\varphi,\psi) \rrbracket_c = \varnothing\). We have \(\Gamma \in\llbracket \gamma(\varphi,\psi) \rrbracket_c \subseteq \llbracket \gamma(\varphi\wedge \gamma(\varphi,\psi),\psi) \rrbracket_c\) by (A5), whence \(\langle \Gamma, g^{-1}[S] \cap \llbracket \gamma(\varphi,\psi) \rrbracket_c, \Delta'\rangle \in P_c\) for some \(\Delta' \in g^{-1}(y)\), thus \(\langle \Gamma, g^{-1}[S \setminus \{z\}], \Delta'\rangle \in P_c\), hence \(\langle x, S \setminus \{z\}, y \rangle \in P\).
(F6): Consider an \(R\)-upset \(U\) with \(x \in U\). Fix \(\varphi\), \(\psi\), and \(\chi\) such that \(\llbracket \varphi \rrbracket_c = g^{-1}[S]\), \(\llbracket {\mathpalette\dotop@{\square}}\psi \rrbracket_c = \llbracket \psi \rrbracket_c = g^{-1}[U]\), and \(\llbracket \chi \rrbracket_c = g^{-1}(y)\). Now \(\Gamma \in {\llbracket {\mathpalette\dotop@{\square}}\psi\wedge \gamma(\varphi,\chi) \rrbracket_c} \subseteq \llbracket \gamma(\varphi\wedge{\mathpalette\dotop@{\square}}\psi, (\varphi\wedge\neg{\mathpalette\dotop@{\square}}\psi)\vee\chi) \rrbracket_c\) by (A6), whence \(\langle \Gamma, \llbracket \varphi\wedge {\mathpalette\dotop@{\square}}\psi \rrbracket_c, \Theta\rangle \in P_c\) for some \(\Theta \in \llbracket (\varphi\wedge \neg{\mathpalette\dotop@{\square}}\psi)\vee \chi \rrbracket_c\), hence \(\langle x, {S \cap U}, g(\Theta)\rangle \in P\) and \(g(\Theta) \in (S \setminus U) \cup \{y\}\).
(F7): Consider \(R\)-upsets \(U_1\) and \(U_2\) with \(x,y \in S \subseteq U_1 \cup U_2\). Denote by \(T\) the set of all \(s \in S\) for which there exists an \(\langle S,U_1,U_2,s,y\rangle\)-sequence. Fix \(\varphi_1\), \(\varphi_2\), \(\psi\), and \(\chi\) such that \(\llbracket {\mathpalette\dotop@{\square}}\varphi_i \rrbracket_c=\llbracket \varphi_i \rrbracket_c= g^{-1}[U_i]\), \(\llbracket \psi \rrbracket_c = g^{-1}[T]\), and \(\llbracket \chi \rrbracket_c = g^{-1}[S]\). It suffices to show that \(\langle \Gamma, g^{-1}[S], \Delta\rangle \in P_c\) witnesses \(\Gamma \in \llbracket \widehat\gamma(\chi\wedge ({\mathpalette\dotop@{\square}}\varphi_1\vee{\mathpalette\dotop@{\square}}\varphi_2)\wedge(\widehat\gamma(\chi\wedge{\mathpalette\dotop@{\square}}\varphi_1,\psi)\vee \widehat\gamma(\chi\wedge{\mathpalette\dotop@{\square}}\varphi_2,\psi)\to\psi), \psi) \rrbracket_c\), for then \(\Gamma \in \llbracket \psi \rrbracket_c\) by (A7) and thus \({x \in T}\). Since \(y \in T\), we have \(\Delta \in \llbracket \psi \rrbracket_c\). It is immediate that \(\Gamma,\Delta \in g^{-1}[S]= \llbracket \chi\wedge ({\mathpalette\dotop@{\square}}\varphi_1\vee{\mathpalette\dotop@{\square}}\varphi_2) \rrbracket_c\). Now it remains to verify that \(\llbracket \widehat\gamma(\chi\wedge{\mathpalette\dotop@{\square}}\varphi_i,\psi)\to \psi \rrbracket_c=X_c\) for \(i=1,2\). Suppose \(\Theta \in \widehat\gamma(\chi\wedge{\mathpalette\dotop@{\square}}\varphi_i,\psi)\). Then \(\Theta \in \llbracket \chi\wedge {\mathpalette\dotop@{\square}}\varphi_i \rrbracket_c\) and \(\langle \Theta, \llbracket \chi\wedge{\mathpalette\dotop@{\square}}\varphi_i \rrbracket_c,\Theta'\rangle \in P_c\) for some \(\Theta' \in \llbracket \chi\wedge{\mathpalette\dotop@{\square}}\varphi_i\wedge \psi \rrbracket_c\), thus \(g(\Theta) \in S \cap U_i\) and \(g(\Theta') \in S \cap U_i \cap T\). Now there exists an \(\langle S,U_1,U_2,g(\Theta'), y\rangle\)-sequence, and appending \(g(\Theta)\) to its beginning we obtain an \(\langle S,U_1,U_2,g(\Theta),y\rangle\)-sequence, whence \(g(\Theta) \in T\), hence \(\Theta \in \llbracket \psi \rrbracket_c\).
(F8): Suppose \(S=\{y\}\). Fix \(\varphi\) with \(\llbracket \varphi \rrbracket_c = g^{-1}(y)\). If \(\llbracket \varphi \rrbracket_c = \llbracket \varphi\wedge {\mathop{\square}}\neg\varphi \rrbracket_c\), then \(\langle \Gamma,g^{-1}(y),\Delta\rangle \in P_c\) witnesses \(\Gamma \in \llbracket \gamma(\varphi\wedge{\mathop{\square}}\neg\varphi,\top) \rrbracket_c\), whence \(\Gamma \in \llbracket \varphi \rrbracket_c\) by (A8), hence \(x=g(\Gamma)=y\). Otherwise, fix \(\Theta \in {\llbracket \varphi\wedge \neg {\mathop{\square}}\neg\varphi \rrbracket_c}\). The set \(\{\varphi\} \cup \left\{ \psi \,:\, {\mathop{\square}}\psi \in \Theta \right\}\) is \(\mathbf{TLR}\)-consistent, for if \(\vdash \bigwedge \psi_i \to \neg \varphi\) then \(\vdash \bigwedge {\mathop{\square}}\psi_i \to {\mathop{\square}}\neg \varphi\). Fix some \(\Theta' \in \llbracket \varphi \rrbracket_c \cap \bigcap_{{\mathop{\square}}\psi\in\Theta} \llbracket \psi \rrbracket_c\). Now \(\Theta \mathrel{R_c} \Theta'\), whence \(y\mathrel{R}y\). ◻
Lemma 5. The frame \(\langle X_c/\mathord{\sim}, R, P^+\rangle\) is suitable.
Proof. The frame is clearly finite and satisfies (F1). Property (F2) holds for \(P^+\) since it holds for \(P\) by Lemma 4 and \(P \subseteq P^+\). By Lemma 4, \(P\) also satisfies (F3)–(F8), hence \(P^+\) satisfies (F3)–(F8) for all triples \(\langle x,S,y\rangle\) that are in \(P\). Now it suffices to check that the set of triples for which \(P^+\) satisfies (F3)–(F8) is closed under (F1), i.e., that if \(P^+\) satisfies (F3)–(F8) for some \(\langle x,S,w\rangle \in P^+\) and \(\langle w,S,y\rangle \in P^+\), with \(w \in S\), then \(P^+\) also satisfies (F3)–(F8) for \(\langle x,S,y\rangle\). We do this for each of these properties separately.
(F3): We have \(w \in S\), thus \(S \neq \varnothing\).
(F4): Since (F4) holds for \(\langle x,S,w\rangle\) and \(\langle w,S,y\rangle\), we have \(\langle y,S,w\rangle, \langle w,S,x\rangle \in P^+\), hence \(\langle y,S,x\rangle \in P^+\) by (F1).
(F5): Consider \(z \in S\). If \(z = w\) or \(\langle z,S,y\rangle \in P^+\), there is nothing to prove. If \(\langle z,S,w\rangle \in P^+\), then \(\langle z,S,y\rangle \in P^+\) by (F1) since \(\langle w,S,y\rangle \in P^+\). In all other cases, \(\langle x,S \setminus \{z\},w\rangle \in P^+\) by (F5) for \(\langle x,S,w\rangle\), \(\langle w,S\setminus \{z\},y\rangle \in P^+\) by (F5) for \(\langle w,S,y\rangle\), and \(w \in S \setminus \{z\}\), hence \(\langle x, S \setminus \{z\},y\rangle \in P^+\) by (F1).
(F6): Consider an \(R\)-upset \(U\) with \(x \in U\). By (F6) applied to \(\langle x,S,w\rangle\) we have \(\langle x,S\cap U,z\rangle \in P^+\) for some \(z \in (S \setminus U) \cup \{w\}\). If \(z \in S \setminus U\), there is nothing to prove. Otherwise, \(z=w \in U\). Now, (F6) applied to \(\langle w,S,y\rangle\) yields \(\langle w,S\cap U,z'\rangle \in P^+\) for some \(z' \in (S\setminus U) \cup \{y\}\). Since \(\langle x,S\cap U,w\rangle \in P^+\) and \(w \in U\), we obtain \(\langle x,S\cap U,z'\rangle \in P\) by (F1).
(F7): Consider \(R\)-upsets \(U_1\) and \(U_2\) with \(x,y \in S \subseteq U_1\cup U_2\). By (F7) for \(\langle x,S,w\rangle\) and \(\langle w,S,y\rangle\) there exist an \(\langle S,U_1,U_2,x,w\rangle\)-sequence and an \(\langle S,U_1,U_2,w,y\rangle\)-sequence; concatenating them we obtain an \(\langle S,U_1,U_2,x,y\rangle\)-sequence.
(F8): If \(S \neq \{y\}\), there is nothing to prove. If \(S=\{y\}\), then \(w \in S\) implies \(y=w\), hence (F8) for \(\langle x,S,w\rangle\) implies (F8) for \(\langle x,S,y\rangle\). ◻
Summarizing this section, we have:
If \(\mathbf{TLR}\nvdash \varphi_0\), then \(\varphi_0\) is refuted in a suitable frame of size at most \(2^{|\mathop{\mathrm{Sub}}\varphi_0|}\).
Proof. The flanked Kripke frame \(\langle X_c/\mathord{\sim}, R, P^+\rangle\) is suitable by Lemma 5. Clearly, \(|X_c/\mathord{\sim}| \leq 2^{|\mathop{\mathrm{Sub}}\varphi_0|}\). If \(\mathbf{TLR}\nvdash \varphi_0\), then \(\mathfrak{M}_c \not\models \varphi_0\) by Lemma 2, whence \(\mathfrak{M}^+ \not\models \varphi_0\) by Lemma 3. ◻
In this section, we show that every formula refuted in a suitable frame is also refuted in a metric space. First, we introduce path-morphisms that preserve the validity of \(\mathcal{L}\)-formulas (cf. [@BBCFG24]). Then, given a suitable frame \(X\), it will suffice to produce a path-morphism \(f: T \to X\) from some metric space \(T\).
Definition 6. For a topological space \(\langle T,\tau\rangle\) and a flanked Kripke frame \(\langle X,R,P\rangle\), a map \(f: T \to X\) is a path-morphism* if:*
every \(a \in T\) has a neighborhood \(U \in \tau\) with \(f[U \setminus \{a\}] \subseteq R(f(a))\);
if \(f(a) R y\) and \(a \in U \in \tau\), then there exists \(b \in U \setminus \{a\}\) with \(f(b)=y\);
if \(\delta\) is a path in \(\langle T,\tau\rangle\), then \(\langle f(\delta(0)), f[\delta[(0,1)]], f(\delta(1))\rangle \in P\); and
if \(\langle f(a),S,y\rangle \in P\), then there exists a path \(\delta\) in \(\langle T,\tau\rangle\) with \(\delta(0)=a\), \(f[\delta[(0,1)]] \subseteq S\), and \(f(\delta(1)) = y\).
Lemma 6. Let \(f : \langle T,\tau\rangle \to \langle X,R,P\rangle\) be a path-morphism and \(\llbracket \cdot \rrbracket : X \to \mathrm{Prop}\). Put \(\llbracket p \rrbracket_T := f^{-1}[\llbracket p \rrbracket]\) for all \(p \in \mathrm{Prop}\). Then \(a \in \llbracket \chi \rrbracket_T \Longleftrightarrow f(a) \in \llbracket \chi \rrbracket\) for all \(\chi \in \mathcal{L}\) and \(a \in T\).
Proof. By induction on \(\chi\). The step for \(\chi=\varphi\to\psi\) is trivial.
Consider \(\chi={\mathop{\square}}\varphi\). If \(f(a) \in \llbracket {\mathop{\square}}\varphi \rrbracket\), then \(R(f(a)) \subseteq \llbracket \varphi \rrbracket\), whence \(f^{-1}[R(f(a))] \subseteq\llbracket \varphi \rrbracket_T\) by the induction hypothesis for \(\varphi\), hence the set \(U\) given by (\(\Diamond\)-forth) witnesses \(a \in \llbracket \Box\varphi \rrbracket_T\). Conversely, suppose \(a\in \llbracket {\mathop{\square}}\varphi \rrbracket_T\), i.e., there exists \(U \in \tau\) with \(a \in U\) and \(U \setminus \{a\} \subseteq \llbracket \varphi \rrbracket_T\). By (\(\Diamond\)-back), for every \(y \in R(f(a))\) there exists \(b \in U \setminus \{a\} \subseteq \llbracket \varphi \rrbracket_T\) with \(f(b)=y\), whence \(y \in \llbracket \varphi \rrbracket\) by the induction hypothesis for \(\varphi\). Therefore, \(R(f(a)) \subseteq \llbracket \varphi \rrbracket\), i.e., \(f(a) \in \llbracket {\mathop{\square}}\varphi \rrbracket\).
Consider \(\chi=\gamma(\varphi,\psi)\). If \(a \in \llbracket \gamma(\varphi,\psi) \rrbracket_T\) is witnessed by a path \(\delta\), then \(\langle f(a), f[\delta[(0,1)]], f(\delta(1))\rangle \in P\) by (\(\gamma\)-forth), hence \(f(a) \in \llbracket \gamma(\varphi,\psi) \rrbracket\). Conversely, if \(f(a) \in \llbracket \gamma(\varphi,\psi) \rrbracket\) is witnessed by \(\langle f(a),\llbracket \varphi \rrbracket,y\rangle \in P\), then by (\(\gamma\)-back) there exists a path \(\delta\) in \(\langle T,\tau\rangle\) witnessing \(a \in \llbracket \gamma(\varphi,\psi) \rrbracket_T\). ◻
Example 4. Take \(\langle X,R,P\rangle\) from Example 1. Consider the Cantor set \(\mathcal{C} \subseteq [0,1]\) and present \([0,1] \setminus \mathcal{C}\) as a union of pairwise-disjoint intervals \(\bigcup_{i \in \mathbb{Q}} (\alpha_i,\beta_i)\). Now consider \(\pi:[0,1] \to X\) given by \(\pi[[0,1] \setminus \bigcup_{i \in \mathbb{Q}} [\alpha_i,\beta_i]] = \{c\}\) and \(\pi \restriction [\alpha_i,\beta_i] = \pi'\) for every \(i\), where \(\pi'(0)=\pi'(1) := b\) and \(\pi'[(0,1)] := \{a\}\). A direct inspection shows that \(\pi\) is a path-morphism with respect to the usual topology on \([0,1]\). By Lemma 6, it follows that all \(\mathcal{L}\)-formulas refuted in \(\langle X,R,P\rangle\) are also refuted in \([0,1]\).
In general, given a suitable frame \(X\), we will construct a metric tree-like structure \(T\) whose “edges” are isomorphic copies of \([0,1]\), and a path-morphism \(f: T \to X\) will be defined in terms of its restrictions to individual “edges.” For \(f\) to satisfy (\(\Diamond\)-forth) and (\(\gamma\)-forth), it is necessary that said restrictions themselves satisfy (\(\Diamond\)-forth) and (\(\gamma\)-forth), i.e., that they are maps of the following form:
Definition 7. A good path* in a suitable frame \(\langle X,R,P\rangle\) is a map \([0,1]\to X\) satisfying (\(\Diamond\)-forth) and:*
It easily follows from (F1) and (F4) that (G) is equivalent to (\(\gamma\)-forth). A map \([0,1]\to X\) satisfies (\({\mathop{\lozenge}}\)-forth) iff preimages of \(R\)-upsets are open and preimages of irreflexive singletons are discrete. In particular, \(\iota_{x,x}\) is a good path iff \(x \mathrel{R} x\).
Definition 8. A map \(\pi: [0,1] \to X\) matches* a triple \(\langle x, S, y\rangle \in X \times \mathcal{P}(X) \times X\) if \(\pi(0)=x\), \(\pi[(0,1)] \subseteq S\), and \(\pi(1)=y\).*
We claim that each “non-constant” triple in \(P\) is matched either by a good path or by a constant (Lemma 8). This will provide us a sufficient supply of good paths to define a path-morphism \(f: T \to X\) (Proposition [P:networkTree]).
Example 5. Each triple in \(P\) from Examples 1 and 4 is matched by one of the following good paths: \(\iota_{a,a}\), \(\iota_{b,b}\), \(\iota_{c,c}\), \(\iota_{b,a}\), \(\iota_{b,a}\restriction [1,0]\), \(\pi'\), the map given by \(\delta(0):=c\) and \(\delta(t):=\pi(t)\) for \(t>0\), the map given by \(\delta'(1):=c\) and \(\delta'(t):=\pi(t)\) for \(t<1\), the concatenation of \(\iota_{a,b}\) with \(\delta'\), or the concatenation of \(\delta\) with \(\iota_{a,b}\restriction [1,0]\).
We will construct the requisite good paths from “simpler” good paths using several specific operations (among them are concatenation, reversion, the way \(\pi\) is constructed from \(\pi'\) in Example 4, etc.). The following lemma, informally speaking, states that all elements of \(P\) can be “constructed” from “simpler” elements of \(P\) using the corresponding set of operations on triples.
Lemma 7. Let \(\langle X, R, P \rangle\) be a suitable frame. Then there exists a strict partial order \(\vartriangleleft\) on \(P\) such that for every \(\langle x, S,y\rangle \in P\) one of the following holds:
\(x=y \in S\);
\(\langle y,S,x\rangle \vartriangleleft \langle x,S,y\rangle\);
there is a sequence \(x_0,\dotsc,x_k\) with \(k \geq 1\), \(x=x_0\), \(x_k=y\), and \(x_1,\dotsc,x_{k-1} \in S\), such that for each \(i<k\) there exists \(S_i' \subseteq S\) with \(P \owns \langle x_i, S_i',x_{i+1}\rangle \vartriangleleft \langle x,S,y\rangle\);
we have:
\(x \neq y \in S \subseteq R(x)\);
\(P \owns \langle z,S,w\rangle \vartriangleleft \langle x,S,y\rangle\) for all \(z,w \in S\); and
\(\langle x,S,z\rangle \in P\) for all \(z \in S\);
there exists \(U \subseteq X\) such that:
\(x,y\in S \setminus U\);
\((S \setminus U) \times S \subseteq R\);
for every \(z \in S\cap U\) there exists \(w_z \in S \setminus U\) with \(P \owns \langle z, S \cap U,w_z\rangle \vartriangleleft \langle x,S,y\rangle\); and
\(\langle z,S,w\rangle \in P\) for all \(z,w \in S\).
Proof. For \(z \in X\), put \(\widehat{R}(z) := \{z\} \cup R(z)\); note that \(\widehat{R}(z)\) is an \(R\)-upset. Put \(\langle x,S,y\rangle \vartriangleleft \langle x',S',y'\rangle\) iff one of the following holds:
\(S\subsetneq S'\);
\(S=S'\) and \(y \in S \not \owns y'\);
\(S=S'\), \(x \in S \not\owns x'\), and either \(y,y' \in S\) or \(y,y'\not\in S\);
\(x,y,x',y'\in S=S'\) and \(\widehat{R}(y) \supsetneq \widehat{R}(y')\);
\(x,y,x',y' \in S=S'\), \(\widehat{R}(y)=\widehat{R}(y')\), and \(\widehat{R}(x) \supsetneq \widehat{R}(x')\).
Observe that \(\vartriangleleft\) is a strict partial order. Now consider \(\langle x,S,y\rangle \in P\) and suppose that (C1), (C2), and (C3) do not hold. Then:
For all \(S' \subsetneq S\) we have \(\langle x, S' , y\rangle \not\in P\). Indeed, otherwise (C3) is true with \(k=1\).
For every \(z \in S\) we have \(\langle x, S, z\rangle \in P\) and \(\langle z,S,y\rangle \in P\). Indeed, \(\langle x,S\setminus \{z\}, y\rangle \not \in P\) by (i); it remains to apply (F5) together with (F4).
If \(y \in S\), then \(\langle z,S,w\rangle \in P\) for all \(z,w \in S\). Indeed, \(\langle z,S,y\rangle, \langle y, S, w\rangle \in P\) by (ii) and (F4), hence \(\langle z,S,w\rangle \in P\) by (F1).
If an \(R\)-upset \(U\) satisfies \(S \not\subseteq U\) and \(x \in U\), then there exists \(z \in S\setminus U\) with \(\langle z,S,y\rangle \ntriangleleft \langle x,S,y\rangle\). Indeed, by (F6) we have \(\langle x, S \cap U, z \rangle \in P\) for some \(z \in (S \setminus U) \cup \{y\}\). By (i), \(z\neq y\). Now we have \(z \in S\), \(P \owns \langle x,S \cap U, z\rangle \vartriangleleft \langle x,S,y\rangle\) by (L1), and \(\langle z,S,y\rangle \in P\) by (ii). Therefore, \(\langle z,S,y\rangle \ntriangleleft \langle x,S,y\rangle\), for otherwise (C3) holds with \(k=2\) and \(x_1=z\).
Now, to show that either (C4) or (C5) holds for \(\langle x,S,y\rangle\), consider two cases.
Case 1: \(x \not \in S\). Let us establish (C4). By (F3) we have \(S \neq \varnothing\); fix some \(z' \in S\). If \(y \not \in S\), we have \(P \owns \langle x,S,z'\rangle \vartriangleleft \langle x,S,y\rangle\) by (ii) and (L2), and \(P \owns \langle z',S,y\rangle \vartriangleleft \langle x,S,y\rangle\) by (ii) and (L3), hence (C3) holds with \(k=2\). Therefore, \(y \in S\).
By (L3) we have \(\langle z,S,y\rangle \vartriangleleft \langle x,S,y\rangle\) for all \(z \in S\), thus by (iv) applied to \(U:=\widehat{R}(x)\) we obtain \(S\subseteq \widehat{R}(x)\), hence \(S \subseteq R(x)\), i.e., (C4a) is true. Condition (C4b) follows from (iii) and (L3), and (C4c) holds by (ii).
Case 2: \(x\in S\). If \(y \not \in S\), then \(\langle y,S,x\rangle \vartriangleleft\langle x,S,y\rangle\) by (L2), whence (C2) holds. Therefore, \(y \in S\).
Fix an \(R\)-upset \(U\) which is maximal with respect to \(U \subsetneq \widehat{R}[S]\). (Note that \(U\) may be empty.) Since \(\widehat{R}[S] \not\subseteq U\), we have \(S \not\subseteq U\). Let us show that (C5) is true for \(U\).
First we claim that every \(z \in S \setminus U\) satisfies \(\widehat{R}(z)=\widehat{R}[S]\). Indeed, by maximality of \(U\) we have \(U \cup \widehat{R}(z) = \widehat{R}[S]\). Using (F7), fix an \(\langle S, U,\widehat{R}(z),x,y\rangle\)-sequence \(x_0,\dotsc,x_k\). Since (C1) does not hold, we have \(x \neq y\) and thus \(k>0\). Since (C3) does not hold, there exists \(i<k\) with \(\langle x_i, S \cap U, x_{i+1}\rangle \ntriangleleft \langle x,S,y\rangle\) or \(\langle x_i, S \cap \widehat{R}(z), x_{i+1}\rangle \ntriangleleft \langle x,S,y\rangle\). As (L1) does not apply, it follows that \(S \cap U=S\) or \(S \cap \widehat{R}(z) =S\). Since \(S \not\subseteq U\), we conclude that \(S \subseteq \widehat{R}(z)\) and thus \(\widehat{R}(z) = \widehat{R}[S]\).
To verify (C5a), first assume \(x \in U\). Since \(S\not\subseteq U\), by (iv) there exists \(z \in S \setminus U\) with \(\langle z,S,y\rangle \ntriangleleft \langle x,S,y\rangle\). But \(x,y,z \in S\) and \(\widehat{R}(x) \subseteq U \subsetneq \widehat{R}[S] = \widehat{R}(z)\), thus \(\langle z,S,y\rangle \vartriangleleft \langle x,S,y\rangle\) by (L5), which is a contradiction. Now assume \(x \in S \setminus U\) and \(y \in U\). Then \(\widehat{R}(y) \subsetneq \widehat{R}[S] =\widehat{R}(x)\), thus \(\langle y,S,x\rangle \vartriangleleft \langle x,S,y\rangle\) by (L4), hence (C2) holds. Therefore, \(x,y \in S \setminus U\).
To verify (C5b), recall that \(S \subseteq \widehat{R}[S] = \widehat{R}(z)\) for all \(z \in S \setminus U\). It remains to note that \(\widehat{R}\) is total on \(S \setminus U\) and \(x,y \in S \setminus U\) are distinct, thus all \(z \in S \setminus U\) are \(R\)-reflexive.
To check (C5c), consider \(z \in S \cap U\). By (ii) we have \(\langle z, S,y\rangle \in P\), thus by (F6) there exists \(w_z \in S \setminus U \cup \{y\} = S \setminus U\) satisfying \(\langle z, S \cap U, w_z \rangle \in P\).
Condition (C5d) follows from (iii). ◻
Lemma 8. Let \(\langle X, R, P \rangle\) be a suitable frame. Then, for every triple \(\langle x,S,y\rangle \in P\), either \(x=y \in S\) or there exists a good path matching \(\langle x,S,y\rangle\).
Proof. Fix a strict partial order \(\vartriangleleft\) as in Lemma 7. Since \(X\) and \(P\) are finite, this \(\vartriangleleft\) is well-founded. The proof proceeds by \(\vartriangleleft\)-induction on \(P\).
Case (C1). Since \(x=y \in S\), there is nothing to prove.
Case (C2). Since \(\langle y,S,x\rangle \vartriangleleft \langle x,S,y\rangle\), we have \(x\neq y\). By the induction hypothesis, some good path \(\pi\) matches \(\langle y,S,x\rangle\). Now, \(\pi \restriction [1,0]\) matches \(\langle x,S,y\rangle\); it is a good path by (F4).
Case (C3). Consider a requisite sequence \(x_0,\dotsc,x_k\). Without loss of generality, either \(x_0\neq x_1 \neq \dotso \neq x_k\) or \(k=1\), for we can omit duplicate adjacent \(x_i\)’s. If \(k=1\) and \(x=y \in S_0'\), then \(x=y\in S\). Otherwise, for each \(i<k\) the induction hypothesis yields a good path \(\pi_i\) matching \(\langle x_i,S_i',x_{i+1}\rangle\). Now the map \(\pi:[0,1]\to X\) given by \(\pi \restriction [\frac{i}{n}, \frac{i+1}{n}] = \pi_i\) matches \(\langle x,S,y\rangle\). Since each \(\pi_i\) satisfies (\(\Diamond\)-forth), \(\pi\) also satisfies (\(\Diamond\)-forth). Since each \(\pi_i\) satisfies (G), \(\pi\) also satisfies (G) by (F1).
Case (C4) with \(S=\{y\}\). The map \(\iota_{x,y}\) matches \(\langle x,S,y\rangle\). We have \(x \mathrel{R} y\) by (C4a) and \(y \mathrel{R} y\) by (F8), hence \(\iota_{x,y}\) satisfies (\(\Diamond\)-forth). By (F2) we have \(\langle y,\{y\},y\rangle \in P\), thus \(\iota_{x,y}\) satisfies (G).
Case (C4) with \(\{y\} \subsetneq S\). Denote by \(z_0,\dotsc,z_{k-1}\) an enumeration of \(S\) such that \(z_0=y\), and put \(z_k = z_0\). For each \(i<k\) we have \(P \owns \langle z_{i+1}, S,z_{i}\rangle \vartriangleleft \langle x,S,y\rangle\) by (C4b) and \(z_{i+1} \neq z_i\), thus the induction hypothesis yields a good path \(\pi_i\) matching \(\langle z_{i+1}, S, z_{i}\rangle\). Consider \(\pi:[0,1]\to X\) given by \(\pi(0)=x\) and \(\pi \restriction [\frac{1}{i+2}, \frac{1}{i+1}] = \pi_{i \bmod k}\) for all \(i \geq 0\). Clearly, \(\pi\) matches \(\langle x, S, y\rangle\). This \(\pi\) satisfies (\({\mathop{\lozenge}}\)-forth) at every \(t \in (0,1]\) since \(\pi_i\)’s satisfy (\({\mathop{\lozenge}}\)-forth), and at \(t=0\) since \(\pi[(0,1)]=S \subseteq R(x)\) by (C4a). For all \(u \in (0,1]\) we have \(\langle \pi(0), \pi[(0,u)],\pi(u)\rangle = \langle x,S,\pi(u) \rangle \in P\) by (C4c). Condition (G) for \(0<t<u\leq 1\) follows easily by (F1) from the fact that \(\pi_i\)’s satisfy (G).
Case (C5). For every \(z \in S\cap U\), we claim that there exists a good path \(\pi_z\) with \(z \in \pi_z[(0,1)] \subseteq S\) and \(\pi_z(0)=\pi_z(1) \in S \setminus U\). Indeed, by (C5c) and the induction hypothesis, there exists a good path \(\pi_z'\) matching \(\langle z, S\cap U, w_z\rangle\) for some \(w_z \in S \setminus U\). Take \(\pi_z\) with \(\pi_z \restriction [0,\frac{1}{2}] = \pi_z' \restriction [1,0]\) and \(\pi_z \restriction [\frac{1}{2},1] = \pi_z'\).
As in Example 4, denote by \(\mathcal{C} \subseteq [0,1]\) the standard Cantor set, and present \([0,1] \setminus \mathcal{C}\) as a union of pairwise-disjoint intervals \(\bigcup_{i \in \mathbb{Q}} (\alpha_i,\beta_i)\), with \(i<j \Longleftrightarrow\alpha_i<\alpha_j\). Fix \(f: \mathbb{Q} \to S\) such that \(f^{-1}(z)\) is dense in \(\mathbb{Q}\) for every \(z \in S\). Define \(\pi:[0,1]\to X\) as follows:
\(\pi \restriction [\alpha_i,\beta_i] = \pi_{f(i)}\) if \(f(i) \in S\cap U\) and \(\pi\restriction [\alpha_i,\beta_i]=\iota_{f(i),f(i)}\) if \(f(i) \in S \setminus U\);
\(\pi(t)=x\) for all \(t \in [0,1) \setminus \bigcup_{i \in \mathbb{Q}} [\alpha_i,\beta_i]\), and \(\pi(1)=y\).
Clearly, \(\pi\) matches \(\langle x, S, y\rangle\). Consider \(t \in [0,1]\). If \(\pi(t)\in S\setminus U\), then \(R(\pi(t))\supseteq S=\pi[[0,1]]\) by (C5a) and (C5b). Otherwise, some \(i \in\mathbb{Q}\) satisfies \(t \in (\alpha_i,\beta_i)\) and \(\pi \restriction [\alpha_i,\beta_i]\) satisfies (\(\Diamond\)-forth). Therefore, \(\pi\) satisfies (\(\Diamond\)-forth). Towards (G), consider \(0\leq t<u\leq 1\). If \([t,u] \subseteq [\alpha_i,\beta_i]\) for some \(i\) with \(f(i) \in S\cap U\), it suffices to apply (G) for \(\pi_{f(i)}\). If \([t,u]\subseteq [\alpha_i,\beta_i]\) with \(f(i) \in S\setminus U\), apply (F2). Finally, suppose \([t,u]\) is not contained in any of the intervals \([\alpha_i,\beta_i]\). Then \([t,u]\) intersects at least two of those intervals, say \([\alpha_i,\beta_i]\) and \([\alpha_j,\beta_j]\) with \(i<j\). But now for every \(z \in S\) there exists \(k \in f^{-1}(z) \cap (i,j)\), thus \(z \in \pi [ [\alpha_k,\beta_k] ] \subseteq \pi[(t,u)]\). Therefore, \(\pi[(t,u)]=S\), hence \(\langle \pi(t),\pi[(t,u)],\pi(u)\rangle=\langle \pi(t), S, \pi(u)\rangle \in P\) by (C5d). ◻
Now, given a suitable frame \(\langle X,R, P\rangle\), we employ Lemma 8 to produce a metric “tree” \(T\) and a path-morphism \(f:T \to X\). Let us first outline our construction. To assure (\({\mathop{\lozenge}}\)-back) and (\(\gamma\)-back), it suffices to define \(T\) as the closure of \(\{a_0\}\) with \(f(a_0) := x_0\) under the following two operations:
if \(a \in T\) and \(f(a) \mathrel{R} y\), isometrically glue \(\{0\} \cup \left\{ \frac{1}{n} \,:\, n\geq 1 \right\}\) to \(T\) with \(a \sim 0\), taking \(f(\frac{1}{n}):=y\) for all \(n\geq 1\);
if \(a \in T\) and \(\langle f(a),S,y\rangle \in P\), isometrically glue a real interval \([0,1]\) to \(T\) with \(a \sim 0\), taking \(f \restriction [0,1] := \pi\), where \(\pi:[0,1]\to X\) is a good path matching \(\langle f(a), S,y\rangle\). We need not do this operation if \(f(a) = y \in S\) (because in this case (\(\gamma\)-forth) is already witnessed by \(\delta := \iota_{a,a}\)); otherwise a requisite good path exists by Lemma 8.
For this construction, we will show that properties (\(\Diamond\)-forth) and (\(\gamma\)-forth) transfer from individual good paths to the whole map \(f\).
The metric space \(T\) we construct is similar to a real tree (as defined e.g. in [@Janson]), except that in addition to “edges” isomorphic to \([0,1]\) we also have those isomorphic to \(\{0\} \cup \left\{ \frac{1}{n} \,:\, n \geq 1 \right\}\). We define the metric in terms of a height function \(h\) and a meet-semilattice \(\wedge\) of “least common ancestors” in our “tree”; this is reminiscent of [@Janson]. In a real tree, every path passes through all the points on the unique arc between its ends (cf. e.g. [@Janson]); we essentially make a similar observation on our metric to verify (\(\gamma\)-forth).
If \(\langle X,R,P\rangle\) is a suitable frame and \(x_0 \in X\), then there exists a metrizable topological space \(\langle T,\tau\rangle\) and a path-morphism \(f: T \to X\) with \(x_0 \in f[T]\).
Proof. In this proof, \(a {}^\smallfrown b\) denotes the concatenation of tuples \(a\) and \(b\).
Using Lemma 8, fix a set \(\Gamma\) containing one good path matching each triple \(\langle x,S,y\rangle \in P\), except those with \(x=y \in S\). Denote by \(T\) the set consisting of the empty tuple \(\varnothing\) and all tuples \(\langle \pi_1,u_1,\dotsc,\pi_k,u_k\rangle\) such that:
for each \(i=1,\dotsc,k\), either:
\(\pi_i\) is an element of \(\Gamma\) and \(u_i \in (0,1]\); or
\(\pi_i = \iota_{x,y}\) for some \(x,y \in X\) with \(x \mathrel{R} y\), and \(u_i = \frac{1}{n}\) for some integer \(n>0\); and
\(\pi_1(0)=x_0\) and \(\pi_{i}(0)=\pi_{i-1}(u_{i-1})\) for each \(i=2,\dotsc,k\).
(Note that \(\iota_{x,y}\) may or may not be in \(\Gamma\). If \(\pi_i =\iota_{x,y} \in \Gamma\), we allow any \(u_i \in (0,1]\).)
For \(a, b \in T\), put \(a \prec b\) iff \(b\) has a prefix \(c {}^\smallfrown \langle \pi,u\rangle\) such that either \(a =c\) or \(a=c {}^\smallfrown \langle \pi,u'\rangle\) for some \(u'< u\). Observe that \(\prec\) is a partial order on \(T\).
We claim that \(\langle T,\prec\rangle\) is a meet-semilattice (i.e., that any two elements of the “tree” \(\langle T,\prec\rangle\) have a least common ancestor). Indeed, consider \(\prec\)-incomparable \(a,b \in T\). There are unique prefixes \(c {}^\smallfrown \langle \pi_a,u_a\rangle\) and \(c {}^\smallfrown\langle \pi_b,u_b\rangle\) of \(a\) and \(b\), respectively, with \(\langle \pi_a,u_a\rangle\neq\langle\pi_b,u_b\rangle\). If \(\pi_a=\pi_b\), then \(c {}^\smallfrown \langle \pi_a, \min\{u_a,u_b\}\rangle\) is the meet of \(a\) and \(b\). Otherwise, \(c\) is the meet of \(a\) and \(b\). We denote \(\prec\)-meets by \(\wedge\).
Put \(h(\langle \pi_1,u_1,\dotsc,\pi_k,u_k\rangle):=u_1+\dotsc+u_k\), \(h(\varnothing):=0\), and \(d(a,b) := h(a)+h(b)-2h(a\wedge b)\) for \(a,b \in T\). We claim that \(d\) is a metric on \(T\). Indeed, \(d\) is clearly symmetric. Since \(h\) is \(\prec\)-monotone, \(d\) is positive. For all \(a,b,c\in T\) we have \(h(b) \geq \max\{h(a\wedge b),h(b\wedge c)\}\) and \(h(a\wedge c) \geq \min\{h(a\wedge b), h(b\wedge c)\}\), thus \(h(b)+h(a\wedge c)\geq h(a\wedge b)+h(b\wedge c)\), hence \(d(a,b)+d(b,c)\geq d(a,c)\).
Denote by \(\tau\) the topology on \(T\) induced by \(d\). Put \(f(a^\smallfrown \langle \pi,u\rangle) := \pi(u)\) and \(f(\varnothing) := x_0\). Now we verify that \(f\) is a path-morphism from \(\langle T,\tau\rangle\) to \(\langle X,R,P\rangle\).
Condition (\(\Diamond\)-back). Consider \(a \in T\), \(y \in R(f(a))\), and \(U \in \tau\) with \(a\in U\). For every \(n>0\), we have \(b_{n} := a {}^\smallfrown \langle \iota_{f(a),y}, \frac{1}{n}\rangle \in T\) and \(d(a,b_{n}) = \frac{1}{n}\). Therefore, \(b_{n} \in U \setminus \{a\}\) for a sufficiently big \(n\).
Condition (\(\gamma\)-back). Consider \(a \in T\) and \(\langle f(a), S,y\rangle \in P\). If \(f(a)=y \in S\), it suffices to take \(\delta := \iota_{a,a}\). Otherwise, fix \(\pi \in \Gamma\) that matches \(\langle f(a),S,y\rangle\), put \(\delta(0) := a\) and \(\delta(u):=a{}^\smallfrown \langle\pi,u\rangle\) for \(u\in (0,1]\), and observe that \(\delta\) is isometric and thus continuous.
Condition (\(\Diamond\)-forth). Consider \(a \in T\). If \(a \neq \varnothing\), present \(a\) as \(a=a' {}^\smallfrown \langle \pi_a,u_a\rangle\). Since \(\Gamma\) is finite and all its elements satisfy (\(\Diamond\)-forth), we can fix a sufficiently small \(\varepsilon>0\) such that:
for every \(\pi \in \Gamma\), we have \(\pi[(0,\varepsilon)] \subseteq R(f(\pi(0)))\);
if \(a\neq\varnothing\) and \(\pi_a \in \Gamma\), then \(\varepsilon<u_a\) and \(\pi_a[(u_a-\varepsilon,\min\{u_a+\varepsilon,1\}) \setminus \{u_a\}] \subseteq R(f(a))\);
if \(a \neq \varnothing\) and \(\pi_a \not\in \Gamma\), then \(\varepsilon<u_a\) and \((u_a - \varepsilon, u_a) \cup (u_a,u_a+\varepsilon)\) is disjoint from \(\left\{ \frac{1}{n} \,:\, n\geq 1 \right\}\).
Consider \(b \in T\) with \(d(a,b)<\varepsilon\); it suffices to show that \(b=a\) or \(f(a) \mathrel{R} f(b)\). As \(d(a,{a\wedge b}) \leq d(a,b) < \varepsilon\), we have either \(a=\varnothing\) or \(a\wedge b = a' {}^\smallfrown \langle \pi_a,u\rangle\) for some \(u \in (u_a-\varepsilon, u_a]\). Present \(b\) as \(c {}^\smallfrown \langle \pi_1,u_1,\dotsc,\pi_k,u_k\rangle\) with \(k\geq 0\), where \(c = \varnothing\) if \(a=\varnothing\) and \(c = a' {}^\smallfrown \langle \pi_a,u'\rangle\) for some \(u'\geq u\) otherwise. In the latter case, \(0\leq u'-u \leq d(a \wedge b,b)<\varepsilon\), whence \(u' \in (u_a-\varepsilon,u_a+\varepsilon)\), hence either \(c=a\) (if \(u'=u_a\)) or \(f(a) \mathrel{R} f(c)\) (otherwise). If \(k=0\), there is now nothing to prove. Otherwise, for each \(i<k\) with \(\pi_i \in \Gamma\) we have \(u_i \leq d(a\wedge b,b)<\varepsilon\), whence \(\pi_i(0) \mathrel{R} \pi_i(u_i)\) by definition of \(\varepsilon\). For each \(i<k\) with \(\pi_i \not\in \Gamma\), we have \(\pi_i=\iota_{x,y}\) for some \(x \mathrel{R} y\), thus also \(\pi_i(0) \mathrel{R} \pi_i(u_i)\). By transitivity of \(R\), it follows that \(f(c) \mathrel{R} f(b)\). Since \(c=a\) or \(f(a) \mathrel{R} f(c)\), we conclude that \(f(a) \mathrel{R} f(b)\).
Condition (\(\gamma\)-forth). Consider a path \(\delta\) in \(\langle T,\tau\rangle\). First observe the following for every \(a^* \in T\):
the set \(T \setminus \{a^*\}\) is the disjoint union of the following open sets:
\(\left\{ b \in T \,:\, a^* \not\preceq b \right\}\);
\(\left\{ b \in T \,:\, \text{a^* {}^\smallfrown \langle \pi\rangle is a prefix of b} \right\}\), for some \(\pi\);
\(\left\{ b \in T \,:\, \text{a^* = a' {}^\smallfrown \langle \pi,u'\rangle and a' {}^\smallfrown \langle \pi,u\rangle is a prefix of b for some u>u'} \right\}\);
thus, by connectedness of \([0,1]\), either \(a^* \in \delta[[0,1]]\) or \(\delta[[0,1]]\) is a subset of one of these sets.
if \(a^* = a' {}^\smallfrown \langle \pi,u'\rangle\) with \(\pi \not\in \Gamma\), then \(\left\{ b \in T \,:\, a^* \preceq b \right\}\) is open. Hence \(\delta[[0,1]]\) is a subset either of said set or of its complement, by connectedness of \([0,1]\).
Now, to establish (\(\gamma\)-forth) for \(\delta\), consider 5 cases:
Case 1A: \(\delta(1) = a{}^\smallfrown \langle \pi,u\rangle\) and either \(\delta(0)=a{}^\smallfrown \langle \pi,u'\rangle\) with \(u'<u\) or \(\delta(0)=a\). If \(\delta(0)=a\), put \(u' := 0\). Since \(\delta(0) \prec \delta(1)\), by (ii) applied to \(a^* := \delta(1)\) we have \(\pi \in \Gamma\), thus by (G) \(\langle \pi(u'),\pi[(u',u)],\pi(u)\rangle \in P\). For every \(u'' \in (u',u)\), we have \(\delta(0) \prec a {}^\smallfrown \langle \pi,u''\rangle \prec\delta(1)\), hence \(a {}^\smallfrown \langle \pi,u''\rangle \in \delta[(0,1)]\) by (i), whence \(\pi(u'') = f(a {}^\smallfrown \langle \pi,u''\rangle) \in f[\delta[(0,1)]]\). Therefore, \(\pi[(u',u)] \subseteq f[\delta[(0,1)]]\). As \(P\) is monotone, we obtain \(\langle f(\delta(0)), f[\delta[(0,1)]], f(\delta(1))\rangle \in P\).
Case 1: \(\delta(0) \prec\delta(1)\). By induction on the length of \(\delta(1)\). Present \(\delta(1)\) as \(a {}^\smallfrown \langle \pi,u\rangle\). If Case 1A does not apply, we have \(\delta(0)\prec a\). By (i) for \(a^* := a\), we obtain \(a =\delta(t)\) for some \(t\in (0,1)\). It remains to apply the induction hypothesis to \(\delta \restriction [0,t]\) and Case 1A to \(\delta \restriction [t,1]\), and use (F1).
Case 2: \(\delta(1) \prec\delta(0)\). Apply Case 1 to \(\delta \restriction [1,0]\) and use (F4).
Case 3: \(\delta(0) \not\prec\delta(1)\), \(\delta(1) \not\prec\delta(0)\), and \(\delta(0)\neq\delta(1)\). Applying (i) to \(a^* := \delta(0) \wedge \delta(1)\), we obtain \(\delta(t)=\delta(0)\wedge \delta(1)\) for some \(t \in (0,1)\). Now apply Case 2 to \(\delta \restriction [0,t]\) and Case 1 to \(\delta\restriction [t,1]\), and use (F1).
Case 4: \(\delta(0) = \delta(1)\). If \(\delta\) is constant, it suffices to use (F2). Otherwise, fix some \(t \in (0,1)\) with \(\delta(t) \neq\delta(0)\), apply previous cases to \(\delta \restriction [0,t]\) and \(\delta \restriction [t,1]\), and use (F1).
◻
Summarizing this and the preceding sections, we have the following:
Theorem 1. For a formula \(\varphi\in \mathcal{L}\), the following are equivalent:
\(\varphi\) is valid over the class of \(T_1\) topological spaces;
\(\varphi\) is valid over the class of metric spaces;
\(\varphi\) is valid over the class of suitable frames of size at most \(2^{|\mathop{\mathrm{Sub}}\varphi|}\);
\(\mathbf{TLR} \vdash \varphi\).
The set of formulas with these properties is decidable.
Proof. (1) implies (2) since all metric spaces are \(T_1\); (2) implies (3) by Lemma 6 and Proposition [P:networkTree]; (3) implies (4) by Proposition [P:flankedFMP]; (4) implies (1) by Proposition [P:soundness]. Decidability follows from (3). ◻
In this section, we axiomatize the c-semantical fragment of \(\mathbf{TLR}\) and observe that it is sound for the class of all topologies. Denote by \(\mathcal{L}_c\subseteq \mathcal{L}\) the set of formulas that may be written in terms of \(\bot\), \(\to\), \(\gamma\), and \({\mathpalette\dotop@{\square}}\), without explicit occurrences of \({\mathop{\square}}\).
Definition 9. Denote by \(\mathbf{TLR_c}\) the \(\mathcal{L}_c\)-calculus consisting of:
all axioms and rules of \(\mathbf{S4}\) for \({\mathpalette\dotop@{\square}}\);
axioms (A0)–(A7) and rule (Mon).
Lemma 9. For \(\xi \in \mathcal{L}\), denote by \(\xi^\# \in \mathcal{L}_c\) the result of substituting each \(\Box\) with \({\mathpalette\dotop@{\square}}\).
1) If \(\xi \in \mathcal{L}_c\), then \(\mathbf{TLR_c} \vdash \xi \leftrightarrow \xi^\#\).
2) If \(\mathbf{TLR}\vdash\xi\), then \(\mathbf{TLR_c}\vdash \xi^\#\).
Proof. 1) Since \(\xi^\#\) is obtained from \(\xi\) by substituting each occurrence of \({\mathpalette\dotop@{\square}}\varphi=\varphi\wedge\Box\varphi\) with \(\varphi\wedge {\mathpalette\dotop@{\square}}\varphi\), it suffices to note that \(\mathbf{S4} \vdash \varphi\wedge{\mathpalette\dotop@{\square}}\varphi\leftrightarrow {\mathpalette\dotop@{\square}}\varphi\).
) By induction on the derivation of \(\mathbf{TLR}\vdash\xi\). If \(\xi\) is an axiom of \(\mathbf{K4}\) or is obtained by a rule of \(\mathbf{K4}\) or is obtained by (Mon), it suffices to note that those axioms and rules are also among the axioms and rules of \(\mathbf{TLR_c}\) with \({\mathpalette\dotop@{\square}}\) substituted for \(\Box\). If \(\xi=\gamma(\varphi\wedge{\mathop{\square}}\neg\varphi,\top)\to\varphi\) is an instance of (A8), then \(\mathbf{S4} \vdash \varphi^\#\wedge{\mathpalette\dotop@{\square}}\neg\varphi^\#\to\bot\) and \(\mathbf{TLR_c} \vdash \gamma(\bot,\top)\to\varphi^\#\) by (A3), hence \(\mathbf{TLR_c} \vdash \gamma(\varphi^\# \wedge {\mathpalette\dotop@{\square}}\neg\varphi^\#, \top)\to\varphi^\#\) by (Mon). Now suppose \(\xi\) is an instance of (A0)–(A7). Since \(\Box\) does not occur in those axioms (except as \({\mathpalette\dotop@{\square}}\)), we can present \(\xi\) as \(\chi[p_1/\psi_1,\dotsc,p_k/\psi_k]\), where \(\chi \in \mathcal{L}_c\) is itself an occurrence of (A0)–(A7). Since \(\mathbf{TLR_c} \vdash \chi\), we have \(\mathbf{TLR_c} \vdash \chi^\#\) by (1), hence \(\mathbf{TLR_c} \vdash \chi^\#[p_1/\psi_1^\#,\dotsc,p_k/\psi_k^\#]=\xi^\#\). ◻
Theorem 2. The logic \(\mathbf{TLR_c}\) is decidable, sound for the class of all topological spaces, and complete for the class of metric spaces.
Proof. Soundness of \(\mathbf{S4}\) is well-known [@BB07]. Soundness of (A0)–(A7) and (Mon) follows from Proposition [P:soundness]. If \(\xi \in \mathcal{L}_c\) is valid over the class of metric spaces, then \(\mathbf{TLR} \vdash \xi\) by Theorem 1, whence \(\mathbf{TLR_c} \vdash \xi\) by Lemma 9. Decidability follows by Theorem 1. ◻
In this paper we axiomatized the logic of all topological spaces in the language with path-reachability \(\gamma\) and the interior modality, but in the language enriched by the Cantor derivative we only addressed \(T_1\) spaces. As illustrated in Example 3, the interaction of Cantor derivative with \(\gamma\) in non-\(T_1\) spaces has extra phenomena not caught by the axioms of this paper. To establish completeness for all spaces, it might be useful to enrich the tree-like construction of Proposition [P:networkTree] with “jump” edges isomorphic to the 2-point Sierpiński space. Another problem, already mentioned in [@BBCFG24], is to axiomatize the \(\gamma\)-logic of the Euclidean plane.
Acknowledgments. The research on which this publication is based received financial support from project grant PID2023-149556NB-I00 and CEX2021-001169-M, funded by MICIU/AEI/10.13039/501100011033. The work of the first author was supported by University of Barcelona collaboration grant, call 2025.4.FF.1.
[@*]