The McKinsey-Tarski Theorem for Topological Evidence Logics

Abstract

We prove an analogue of the McKinsey and Tarski theorem for the recently introduced dense-interior semantics of topological evidence logics. In particular, we show that in this semantics the modal logic $\mathsf {S4.2}$ is sound and complete for any dense-in-itself metrizable space. As a result $\mathsf {S4.2}$ is complete with respect to the real line $\mathbb {R}$, the rational line $\mathbb {Q}$, the Baire space $\mathfrak {B}$, the Cantor space $\mathfrak {C}$, etc. We also show that an extension of this logic with the universal modality is sound and complete for any idempotent dense-in-itself metrizable space, obtaining as a result that this logic is sound and complete with respect to $\mathbb {Q}$, $\mathfrak {B}$, $\mathfrak {C}$, etc.

A Appendices

1.1 A.1 Proof of Theorem 2.8

Let us take a finite rooted preorder $\mathfrak {F}= (W,\le )$ and a dense-in-itself metrizable space $(X,\tau )$ and construct a dense-interior onto map $\bar{f}:(X,\tau )\twoheadrightarrow (W,\le )$.¹⁴ For this construction, we will use the following two lemmas. Their proofs¹⁵ can be found respectively in [5, Lemmas 4.13 and 4.22] and [10, Thm. 41].

Lemma A.1

• (i) If $\mathfrak {F}=(W,\le )$ is a finite rooted preorder, and $(G,\tau )$ is a dense-in-itself metrizable space, there exists a continuous, open and surjective map .

• (ii) (Partition Lemma) Let X be a dense-in-itself metrizable space and $n\ge 1$. Then there is a partition $\{G,U_1,...,U_n\}$ of X such that G is a dense-in-itself closed subspace of X with dense complement and each $U_i$ is an open set.

Lemma A.2

Given a dense-in-itself metrizable space X and $n\ge 1$, X can be partitioned in n dense sets.

Note that $\mathfrak {F}$ has a final cluster, i.e., a set $A\subseteq W$ with the property that $w\le a$ for all $w\in W$ and all $a\in A$. Indeed, let $r\in W$ be the root and let $x,y\in W$ be any two maximal elements (which exist, on account that $\mathfrak {F}$ is finite). Since $r\le x$ and $r\le y$, by weak directedness, there is a z such that $x, y\le z$. But by maximality of x and y, we have that $z\le x$ and $z\le y$, hence, by transitivity, $x\le y$ and $y\le x$: the maximal elements of $\mathfrak {F}$ form a final cluster. Let this cluster be $A=\{a_1,...,a_n\}$.

If $W=A$, then we simply partition X in n dense sets $\{A_1,...,A_n\}$ as per Lemma A.2 and we take $\bar{f}$ to map each $x\in A_i$ to $a_i$. It is a straightforward check that $\bar{f}$ is dense-open (the image of a dense open set is W) and dense-continuous (the preimage of a nonempty upset is X). Otherwise, let us call $B:=W\setminus A$, which is a finite rooted preorder. Let $\{G,U_1,...,U_n\}$ be a partition of X as given by the Partition Lemma. Since G is a dense-in-itself metrizable space and B is a finite rooted preorder, by Lemma A.1(i), there exists an onto interior map (with respect to the subspace topology of G) $f: G\twoheadrightarrow B$. We extend this map to $\bar{f}:X\twoheadrightarrow W$ by mapping each $x\in U_i$ to $a_i$.

We now show that $\bar{f}$ is the desired map. It is surjective by construction. It is dense-open, for given a nonempty dense open set $U\subseteq X$, we have that $U\cap G$ is an open set in the subspace topology of G and therefore $\bar{f}[U\cap G]=f[U\cap G]$ is an upset in B. On the other hand, $U\setminus G=U\cap (X\setminus G)$ is the intersection of two dense open sets and therefore is dense open, which means it has nonempty intersection with each of the $U_i$ and hence $\bar{f}[U\setminus G]=A$. Therefore, $\bar{f}[U]$ is the union of an upset in B with A, and thus is an upset in W.

To see that $\bar{f}$ is dense-continuous, take a nonempty upset $U\subseteq W$, which will be a disjoint union $U=B'\cup A$, with $B'$ being an upset in B. Then $\bar{f}^{-1}[B']=f^{-1}[B']$ is an open set in X and $\bar{f}^{-1}[A]=U_1\cup ...\cup U_n = X\setminus G$. Therefore, $\bar{f}^{-1}[U]$ is the union of an open set and a dense open set and thus a dense open set. This concludes the proof.

1.2 A.2 Proof of Theorem 2.13

Let $(W,\le )$ be a finite preorder with a final cluster. We have the following:

Lemma A.3

$(W,\le )$ is a p-morphic image of a finite disjoint union of finite rooted $\mathsf {S4.2}$ frames, via a dense-open and dense-continuous p-morphism.

Proof

Let $x_1,...,x_n$ be the minimal elements of W. Now, for $1\le i \le n$ take $W'_i={\uparrow }x_i \times \{i \}$. Define an order on $W'=W'_1\cup ...\cup W'_n$ by: $(x,i)\le (y,j)$ iff $i=j$ and $x\le y$. Then $W'_1,...,W'_n$ are pairwise disjoint finite rooted $\mathsf {S4.2}$ frames (with $A\times \{i\}$ as a final cluster) and $(x,i)\mapsto x$ is a p-morphism from $W'$ onto W. It is easy to see that this mapping is dense-open (for every nonempty open set is dense in W) and dense-continuous (for the preimage of a nonempty W-upset is a $W'$-upset which contains all the final clusters, and thus is dense).

We can use Lemma A.3 to construct the map: let $W'_1,...,W'_n$ be the family of pairwise disjoint finite rooted $\mathsf {S4.2}$ frames whose union $W'$ has $(W,\le )$ as a p-morphic image.

Take $z_1,...,z_{n-1}\in \mathbb {R}{\setminus } \mathbb {Q}$ and consider the intervals $A_1=(-\infty ,z_1)$, $A_n=(z_{n-1},\infty )$ and $A_i=(z_{i-1},z_i)$ for $1<i<n$. Now, each $A_i$, as a subspace, is homeomorphic to $\mathbb {Q}$ (and thus a dense-in-itself metrizable space). From each $(A_i,\tau |_{A_i})$ we can find a dense-open, dense-continuous and surjective map $f_i$ onto $W'_i$. Then $f=f_1\cup ...\cup f_n$ is a dense-interior map onto $W'$ which, when composed with the p-morphism in Lemma A.3, gives us the desired map.

1.3 A.3 Proof of Theorem 2.15

We show that $E_0^{\mathbb {Q}}$ is a subbasis for $\mathbb {Q}$. First, given that $X\in E^X_0$ and $f[\mathbb {Q}]=X$, we have that $\mathbb {Q}\in E^\mathbb {Q}_0$, thus $\bigcup E^\mathbb {Q}_0 =\mathbb {Q}$.

Now, suppose $p\in U\in \tau _\mathbb {Q}$. We show that there exist $e^q_1,...,e^q_n\in E^\mathbb {Q}_0$ such that $p\in e^q_1\cap ...\cap e^q_n\subseteq U$. Note that $fp\in f[U]$ which is an open set. Since $E^X_0$ is a subbasis for $(X,\le )$ this means that there exist $e^x_1,...,e^x_n\in E^X_0$ with $fp\in e^x_1\cap ...\cap e^x_n \subseteq f[U]$. Now set

$$\begin{aligned} e^q_i := f^{-1}[e^x_i] {\setminus } \{y\notin U: fy\in f[U] \}. \end{aligned}$$

The fact that $e^q_i\in E^\mathbb {Q}_0$ follows from the fact that $f[e^q_i]=e^x_i$. Indeed, if $y\in f[e^q_i]$ then $y\in ff^{-1}[e^x_i]=e^x_i$ and conversely if $y\in e^x_i$, then either $y\in f[U]$ (in which case $y=fz$ for some $z\in U$ and thus $z\in f^{-1} [e^x_i]$ and therefore $z\notin \{z'\notin U: fz'\in f[U] \}$, which implies $z\in e^q_i$) or $y\notin f[U]$ (in which case $y=fz$ for some z by surjectivity and $z\notin \{z'\notin U: fz'\in f[U] \}$, thus $z\in e^q_i$). In either case, $y\in f[e^q_i]$.

Finally, note that $e^q_1\cap ...\cap e^q_n\subseteq U$. Indeed, for any $x\in e^q_1\cap ...\cap e^q_n$ we have that $fx\in e^x_1\cap ...\cap e^x_n\subseteq f[U]$, and thus by the definition of the $e^q_i$’s it cannot be the case that $x\notin U$.

So for $p\in U\in \tau _\mathbb {Q}$ we have found elements $e^q_1,...e^q_n\in E^\mathbb {Q}_0$ such that $p\in e^q_1\cap ...\cap e^q_n\subseteq U$, and therefore $E_0^\mathbb {Q}$ is a subbasis.

Now set a valuation $V^\mathbb {Q}(p)=\{x\in \mathbb {Q}: fx\in V(p)\}$ and let us show that, for any formula $\phi$ in the language and any $x\in \mathbb {Q}$, we have that $(\mathbb {Q},\tau _\mathbb {Q},E^\mathbb {Q}_0,V^\mathbb {Q}),x\,\models \, \phi$ if and only if $(X,\le ,E^X_0,V),fx\,\models \, \phi$. This is done by an induction on formulas; the only induction step that requires some attention is the one referring to $\square _0$.

Let $x\,\models \,\square _0 \psi$. This means that there exists some $e\in E^\mathbb {Q}_0$ with $x\in e$ and $y\,\models \, \psi$ for all $y\in e$. But then $fx\in f[e]\in E^X_0$ and by the induction hypothesis we have $fy\,\models \, \psi$ for all $fy\in f[e]$ and thus $fx\,\models \,\square _0\psi$. Conversely, if $fx\in e'\subseteq \llbracket \psi \rrbracket ^X$ for some $e'\in E^X_0$, we have that $x\in f^{-1}[e']\in E^\mathbb {Q}_0$ and $fy\,\models \, \psi$ for each $y\in f^{-1}[e']$ and thus, by induction hypothesis, $y\,\models \,\psi$. Therefore $x\,\models \, \square _0\psi$.