Strong completeness of modal logics over 0-dimensional metric spaces

TL;DR

This paper establishes strong completeness results for certain modal logics with the universal modality over 0-dimensional metric spaces, and demonstrates limitations of standard systems due to compactness failure.

Contribution

It proves strong completeness for modal logics over 0-dimensional dense metric spaces and shows non-strong completeness in some cases due to compactness issues.

Findings

Strong completeness for modal logics over 0-dimensional spaces

Failure of compactness prevents strong completeness in some languages

Identification of conditions for strong completeness in topological semantics

Abstract

We prove strong completeness results for some modal logics with the universal modality, with respect to their topological semantics over 0-dimensional dense-in-themselves metric spaces. We also use failure of compactness to show that, for some languages and spaces, no standard modal deductive system is strongly complete.

Tables

Table 1. Table 1: For which 0-dimensional dense-in-themselves metric spaces do we have strong completeness?

	$\forall$	$[\ne ]$
$\square$	yes for all	yes for Cantor set; open for others
$\left[d\right]$	no for Cantor set; yes for others	no for Cantor set; open for others

Table 2. Table 2: Summary of results for a 0-dimensional dense-in-itself metric space  X 𝑋 X

$X$		$\square \forall$	$\square [\ne ]$	$\square ⟨n⟩$	$\left[d\right]\forall$	$\left[d\right][\ne ]$	$\left[d\right]⟨n⟩$
non-compact	logic:	S4U	S4DT1S	?	KD4U	?$(\ast )$	?
	compact?	yes	?	?	yes	?	?
Cantor set	logic:	S4U	S4DT1S	?	KD4U	DT1	?
	compact?	yes	yes	yes	no	no	no

Equations

$$\begin{array}[]{rcl}\mathop{\rm cl}\nolimits(A\cup B)&=&\mathop{\rm cl}\nolimits A\cup\mathop{\rm cl}\nolimits B,\\ {\langle d\rangle}(A\cup B)&=&{\langle d\rangle}A\cup{\langle d\rangle}B,\\ \mathop{\rm int}(A\cap B)&=&\mathop{\rm int}A\cap\mathop{\rm int}B.\end{array}$$

$$\Sigma =\{\neg ⟨t⟩\{q,\neg q\},p_0,\forall (p_n\to ◊p_{n+1}),\forall (p_{2n}\to q),\forall (p_{2n+1}\to \neg q):n<\omega \}.$$

$$S=\bigcup \{h(p_n):n<\omega \}\subseteq X.$$

$$O_n=\mathbb{G}\cap N_{{\epsilon }_n}(B)\setminus \bigcup _{m<n}{Z}_m.$$

$$\mathbb{G}\cap ⟨d⟩\bigcup _{n<\omega }{Z}_n=\varnothing .$$

$$⟨d⟩\bigcup _{n\in J}{Z}_n=B.$$

$$|O\cap Z|\le 1\text{mbox}foreveryO\in \mathcal{O}.$$

$$K(z)=K^{+}(z)\setminus \bigcup _{t\in Z\setminus \{z\}}{K}^{+}(t)$$

$${\mathbb{G}}_i=\{\begin{array}{ll}K({\mathbb{I}}_i),& \text{mbox}ifi\ne i_0,\\ \mathbb{G}\setminus {\bigcup }_{j\in I\setminus \{i_0\}}{\mathbb{G}}_j=\mathbb{G}\setminus K(Z\setminus {\mathbb{I}}_{i_0}),& \text{mbox}ifi=i_0.\end{array}$$

$$⟨d⟩\mathbb{B}=⟨d⟩\mathbb{I}\cup ⟨d⟩Z=\mathrm{cl}\mathbb{G}\setminus \mathbb{G}.$$

$$\mathrm{cl}\mathbb{G}\setminus \bigcup _{i\in I}{\mathbb{G}}_i=\mathrm{cl}\mathbb{G}\setminus {\mathbb{G}}^{\prime }=\{\begin{array}{l}(\mathrm{cl}\mathbb{G}\setminus \mathbb{G})\cup (\mathbb{G}\setminus {\mathbb{G}}^{\prime })=⟨d⟩\mathbb{B}\cup \mathbb{B}=\mathrm{cl}\mathbb{B},\\ \mathrm{cl}{\mathbb{G}}^{\prime }\setminus {\mathbb{G}}^{\prime }=\mathrm{cl}{\mathbb{G}}_i\setminus {\mathbb{G}}_i\text{mbox}foreachi\in I.\end{array}$$

$$\Gamma_{x}=\big{\{}\varphi\in{\mathcal{L}}^{\forall}_{[d]}:\{\mathbb{G}\in{\mathcal{E}}(x):{\mathcal{M}},\lambda(\mathbb{G})\models\varphi\}\in D_{x}\big{\}}.$$

$$x\in \mathbb{B}(\mathbb{G})\subseteq \mathrm{cl}\mathbb{B}(\mathbb{G})=\mathrm{cl}{\mathbb{G}}_w\setminus {\mathbb{G}}_w\subseteq \mathrm{cl}{\mathbb{G}}_w\setminus \bigcup _{u\in R(w)}({\mathbb{G}}_w{)}_u=\mathrm{cl}\mathbb{B}({\mathbb{G}}_w).$$

$$S=\mathcal{E}(x)\cap \bigcup \{{\mathcal{G}}_n:0<n<\omega ,1/2^n<\epsilon \},$$

$$\Sigma =\{\exists (q\wedge p_i\wedge \underset{j<i}{\bigwedge }\neg p_j):i<\omega \}\cup \{\forall \neg ⟨d⟩q\}.$$

$$P^Q=\bigcup _{n\in \mathbb{Z}}(2n+\pi ,2n+1+\pi ),$$

$$\begin{array}[]{rcll}\check{b}&=&\{x\in X:M\models x\in b\}&\mbox{for }b\in B,\\ \hat{x}&=&\{b\in B:M\models x\in b\}&\mbox{for }x\in X.\end{array}$$

$$\check{b}\subseteq [[\phi ]{]}^X⟺M\models b\subseteq [[\phi ]],\text{mbox}foreachb\in B.$$

$${\Gamma }_{\mu }=\{\phi \in {\mathcal{L}}_{\square }^{⟨n⟩}:[[\phi ]{]}^X\in \overline{\mu }\}.$$

$$(\mathbb{C},g),\mu \models \phi ⟺\phi \in {\Gamma }_{\mu },\text{mbox}forevery\mu \in \mathbb{C}.$$

Full text

1 Introduction

Modal languages can be given semantics in a metric or topological space, by interpreting $\Box$ as the interior operator. This ‘topological semantics’ predates Kripke semantics and has a distinguished history. In a celebrated result, [18, 19] showed that the logic of an arbitrary separable dense-in-itself metric space in this semantics is the modal logic S4, whose chief axioms are $\Box\varphi\to\varphi$ and $\Box\varphi\to\Box\Box\varphi$. The separability assumption was removed by [20].

So we can say two things. Fix any dense-in-itself metric space $X$ and any set $\Sigma\cup\{\varphi\}$ of modal formulas, and write ‘$\vdash$’ for S4-provability. First, $\vdash$ is sound over $X$: if $\Sigma\vdash\varphi$ then $\varphi$ is a semantic consequence of $\Sigma$ over $X$. Second, $\vdash$ is complete over $X$: if $\varphi$ is a semantic consequence of $\Sigma$ over $X$, and $\Sigma$ is finite, then $\Sigma\vdash\varphi$.

We say that a modal deductive system $\vdash$ is strongly complete over $X$ if the second statement above holds for arbitrary — even infinite — sets $\Sigma$ of formulas.

1.1 Some history

Although McKinsey and Tarski’s result has been well known for a long time, the study of strong completeness for modal languages in topological semantics seems to have begun only quite recently. Gerhardt [9, theorem 3.8] proved that S4 is strongly complete over the metric space $\mathbb{Q}$ of the rational numbers. (He proved further results, in stronger languages, that imply our theorem 4.7 below for this particular space.) The field opened out when [15] proved that S4 is strongly complete over every dense-in-itself metric space, thereby strengthening McKinsey and Tarski’s theorem.

In appendix I of [18], the authors suggested studying the more expressive ‘coderivative’ operator $[d]$. In the modal language incorporating this operator, different dense-in-themselves metric spaces have different logics and can need different treatment. For this language and some stronger ones incorporating the modal mu-calculus or the equivalent ‘tangle’ operators, soundness and strong completeness were shown by [12] for some deductive systems over some dense-in-themselves metric spaces, and by [11] for other deductive systems over all 0-dimensional dense-in-themselves metric spaces. More details will be given in §2.8

None of these languages include the universal modality $\forall$. Indeed, in the presence of $\forall$, strong completeness cannot always be achieved. No modal deductive system for the language with $\Box$ and $\forall$ is sound and strongly complete over any compact locally connected dense-in-itself metric space [12, corollary 9.5].

1.2 The work of this paper

Not covered by the last-mentioned result are the many dense-in-themselves metric spaces that are not compact and locally connected. For example, 0-dimensional dense-in-themselves metric spaces are almost never compact (the only exception is the Cantor set) and never locally connected. So in this paper, we study strong completeness for 0-dimensional dense-in-themselves metric spaces in languages able to express $\forall$. Sound and complete deductive systems for these spaces in languages with $\forall$ were given by [11], and for languages with the even more powerful ‘difference operator’ $[\neq]$ by [16]. In this paper, we ask whether the systems are strongly complete.

The answer depends on both the language and the space, making for an interesting variety as well as some novel techniques. Our main conclusions are outlined in table 1.

In more detail, let $X$ be a 0-dimensional dense-in-itself metric space.

In the language comprising $\forall$ and $\Box$, the system S4U is strongly complete over $X$ (corollary 5.15). 2. 2.

If $X$ is the Cantor set, then in the language comprising $[\neq]$ and $\Box$, the system S4DT1S is strongly complete over $X$ (corollary 5.14). 3. 3.

If $X$ is not homeomorphic to the Cantor set, then in the language comprising $\forall$ and $[d]$, the system KD4U is strongly complete over $X$ (corollary 4.8).

We will not need details of these systems, but briefly, S4U comprises the basic modal K axioms for $\Box$ and $\forall$, the S4 axioms $\Box\varphi\to\varphi$ and $\Box\varphi\to\Box\Box\varphi$, and the U axioms $\forall\varphi\to\varphi$, $\varphi\to\forall\exists\varphi$, $\forall\varphi\to\forall\forall\varphi$, and $\forall\varphi\to\Box\varphi$. In KD4U, $\Box\varphi\to\varphi$ is replaced by the D axiom $\Diamond\top$ (and $\Box$ by $[d]$ throughout). The inference rules are modus ponens and universal generalisation. The axioms of S4DT1S boil down to the S4 axioms for $\Box$, the K axioms for $[\neq]$, $p\to[\neq]\langle\neq\rangle p$, $\forall p\to\Box p\wedge[\neq][\neq]p$, and $[\neq]p\to\Diamond p\wedge[\neq]\Box p$, where $\forall\varphi=\varphi\wedge[\neq]\varphi$; the rules are modus ponens, universal generalisation, and substitution. Full definitions can be found in, e.g., [12, §8.1] and [13], and [16, §2] for S4DT1S.

To prove these results, we will use completeness theorems from [11] and [16]. We lift them to strong completeness by methods similar to those of [15] for non-compact spaces, and first-order compactness for the Cantor set.

Limitative results will also be given:

Let $X$ be a dense-in-itself metric space. In any language able to express $\forall$ and the tangle operators (or the mu-calculus), no modal deductive system is sound and strongly complete over $X$ (corollary 3.2). 2. 5.

Let $X$ be an infinite compact T1 topological space. In any language able to express $\forall$ and $[d]$, no modal deductive system is sound and strongly complete over $X$ (theorem 5.1).

One striking consequence is that for the language comprising $\forall$ and $[d]$, KD4U is sound and complete over every 0-dimensional dense-in-itself metric space $X$ (by the discussion following [11, theorem 8.4]), but by (3) and (5), it is strongly complete only when $X$ is not compact. Over the Cantor set, no orthodox modal deductive system for this language is strongly complete.

2 Basic definitions

In this section, we give the main definitions and some notation. We begin with some stock items. We will use boolean algebras sometimes, and ultrafilters many times, and we refer the reader to, e.g., [10] for information. Let ${\mathcal{B}}=(B,+,-,0,1)$ be a boolean algebra. As usual, for elements $a,b\in B$ we write $a\leq b$ iff $a+b=b$, and $a\cdot b=-(-a+-b)$. An atom of ${\mathcal{B}}$ is a $\leq$-minimal nonzero element, and ${\mathcal{B}}$ is said to be atomless if it has no atoms. An ultrafilter of ${\mathcal{B}}$ is a subset $D\subseteq B$ such that for every $a,b\in B$ we have $b\geq a\in D\Rightarrow b\in D$, $a,b\in D\Rightarrow a\cdot b\in D$, and $a\in D\iff-a\notin D$. We say that $D$ is principal if it contains an atom, and non-principal if not.

We denote the first infinite ordinal by $\omega$. It is also a cardinal. For a set $S$, we write $\wp(S)$ for its power set (set of subsets), and $|S|$ for its cardinality. We say that $S$ is countable if $|S|\leq\omega$, and countably infinite if $|S|=\omega$. An ultrafilter on $S$ is an ultrafilter of the boolean algebra  $(\wp(S),\cup,{\sim},\emptyset,S)$, where ${\sim}$ denotes the unary complement operation (we call such algebras, and subalgebras of them, boolean set algebras). The principal ultrafilters on $S$ are those of the form $\{T\subseteq S:s\in T\}$ for $s\in S$.

2.1 Kripke frames

A (Kripke) frame is a pair ${\mathcal{F}}=(W,R)$, where $W$ is a non-empty set of ‘worlds’ and $R$ is a binary relation on $W$. For $w\in W$, we write $R(w)$ for $\{v\in W:R(w,v)\}$. We say that ${\mathcal{F}}$ is countable if $W$ is countable, serial if $R(w)\neq\emptyset$ for every $w\in W$, and transitive if $R$ is transitive.

For frames ${\mathcal{F}}=(W,R)$ and ${\mathcal{F}}^{\prime}=(W^{\prime},R^{\prime})$, a p-morphism from ${\mathcal{F}}$ to ${\mathcal{F}}^{\prime}$ is a map $f:W\to W^{\prime}$ such that $f(R(w))=R^{\prime}(f(w))$ for every $w\in W$. See standard modal logic texts such as [3] and [5] for information about p-morphisms.

2.2 Topological spaces

We will assume some familiarity with topology, but we give a rundown of the main definitions and notation used later. Other topological terms that we use occasionally, and vastly more information, can be found in topology texts such as [6] and [23] (these two will be our main references).

A topological space is a pair $(X,\tau)$, where $X$ is a non-empty set and $\tau\subseteq\wp(X)$ satisfies:

if ${\mathcal{S}}\subseteq\tau$ then $\bigcup{\mathcal{S}}\in\tau$, 2. 2.

if ${\mathcal{S}}\subseteq\tau$ is finite then $\bigcap{\mathcal{S}}\in\tau$, on the understanding that $\bigcap\emptyset=X$.

So $\tau$ is a set of subsets of $X$ closed under unions and finite intersections. Such a set is called a topology on $X$. By taking ${\mathcal{S}}=\emptyset$, it follows that $\emptyset,X\in\tau$. The elements of $\tau$ are called open subsets of $X$, or just open sets. An open neighbourhood of a point $x\in X$ is an open set containing $x$. A subset $C\subseteq X$ is called closed if $X\setminus C$ is open, and clopen if it is both closed and open. The set of closed subsets of $X$ is closed under intersections and finite unions. Writing ${\sf Clop}(X)$ for the set of clopen subsets of $X$, $({\sf Clop}(X),\cup,{\sim},\emptyset,X)$ is a boolean set algebra. If $O$ is open and $C$ closed then $O\setminus C$ is open and $C\setminus O$ is closed.

We use the signs $\mathop{\rm int}$, $\mathop{\rm cl}\nolimits$, ${\langle d\rangle}$ to denote the interior, closure, and derivative operators, respectively. So for $S\subseteq X$,

• •

$\mathop{\rm int}S=\bigcup\{O\in\tau:O\subseteq S\}$ — the largest open set contained in $S$,

• •

$\mathop{\rm cl}\nolimits S=\bigcap\{C\subseteq X:C$ closed, $S\subseteq C\}$ — the smallest closed set containing $S$; we have $\mathop{\rm cl}\nolimits S=\{x\in X:S\cap O\neq\emptyset\mbox{ for every open neighbourhood\ }O\mbox{ of }x\}$,

• •

${\langle d\rangle}S=\{x\in X:S\cap O\setminus\{x\}\neq\emptyset\mbox{ for every open neighbourhood\ }O\mbox{ of }x\}$.

For all subsets $A,B$ of $X$, we have

[TABLE]

That is, closure and ${\langle d\rangle}$ are additive and interior is multiplicative. It follows that they are all monotonic: if $A\subseteq B$ then $\mathop{\rm cl}\nolimits A\subseteq\mathop{\rm cl}\nolimits B$, ${\langle d\rangle}A\subseteq{\langle d\rangle}B$, and $\mathop{\rm int}A\subseteq\mathop{\rm int}B$.

Fix a topological space $(X,\tau)$. A subspace of $(X,\tau)$ is a topological space of the form $(Y,\tau_{Y})$ where $\emptyset\neq Y\subseteq X$ and $\tau_{Y}=\{O\cap Y:O\in\tau\}$.

For a set $\tau_{0}\subseteq\wp(X)$, the closure $\tau$ of $\tau_{0}$ under arbitrary unions and finite intersections is a topology on $X$, called the topology generated by $\tau_{0}$. A base for (the topology $\tau$ on) $(X,\tau)$ is a set $\tau_{0}\subseteq\tau$ such that $\tau=\{\bigcup{\mathcal{S}}:{\mathcal{S}}\subseteq\tau_{0}\}$.

An open cover of $(X,\tau)$ is a subset ${\mathcal{S}}\subseteq\tau$ with $\bigcup{\mathcal{S}}=X$. We say then that ${\mathcal{S}}$ is locally finite if every $x\in X$ has an open neighbourhood disjoint from all but finitely many sets in ${\mathcal{S}}$. An open cover ${\mathcal{S}}^{\prime}$ of $(X,\tau)$ is a subcover of ${\mathcal{S}}$ if ${\mathcal{S}}^{\prime}\subseteq{\mathcal{S}}$, and a refinement of ${\mathcal{S}}$ if for every $S^{\prime}\in{\mathcal{S}}^{\prime}$ there is $S\in{\mathcal{S}}$ with $S^{\prime}\subseteq S$.

The following assorted topological properties are well known and much studied. We say that $(X,\tau)$ is dense in itself if no singleton subset of $X$ is open; T1 if every singleton subset of $X$ is closed; T2 if every two distinct points of $X$ have disjoint open neighbourhoods; 0-dimensional if it is T1 and has a base consisting of clopen sets; separable if $X$ has a countable subset $D$ with $X=\mathop{\rm cl}\nolimits D$; Lindelöf if every open cover of $X$ has a countable subcover; compact if every open cover of $X$ has a finite subcover; and paracompact if it is T2 and every open cover of $(X,\tau)$ refines to a locally finite open cover of $(X,\tau)$. (Not everyone requires that 0-dimensional spaces be T1 or that paracompact spaces be T2, and some writers add extra conditions such as T2 or regularity to the definitions of compact and Lindelöf. The spaces involved in this paper meet all these conditions.) Easily, T2 implies T1.

We follow standard practice and identify (notationally) the space $(X,\tau)$ with $X$.

2.3 Metric spaces

A metric space is a pair $(X,d)$, where $X$ is a non-empty set and $d:X\times X\to\mathbb{R}$ is a ‘distance function’ (having nothing to do with the operator ${\langle d\rangle}$ above) satisfying, for all $x,y,z\in X$,

$d(x,y)=d(y,x)\geq 0$, 2. 2.

$d(x,y)=0$ iff $x=y$, 3. 3.

$d(x,z)\leq d(x,y)+d(y,z)$ (the ‘triangle inequality’).

Examples of metric spaces abound and include the real numbers $\mathbb{R}$ with the standard distance function $d(x,y)=|x-y|$, $\mathbb{R}^{n}$ with Pythagorean distance, etc. As usual, we often identify (notationally) $(X,d)$ with $X$.

Let $(X,d)$ be a metric space. A subspace of $(X,d)$ is a metric space of the form $(Y,d\restriction Y\times Y)$, for non-empty $Y\subseteq X$. For $x\in X$ define $d(x,Y)=\inf\{d(x,y):y\in Y\}.$ We leave $d(x,\emptyset)$ undefined. For a real number $\varepsilon>0$, we let $N_{\varepsilon}(x)$ denote the ‘open ball’ $\{y\in X:d(x,y)<\varepsilon\}$, and for $S\subseteq X$ we put $N_{\varepsilon}(S)=\bigcup\{N_{\varepsilon}(x):x\in S\}$. A metric space $(X,d)$ gives rise to a topological space $(X,\tau_{d})$ in which a subset $O\subseteq X$ is declared to be open (i.e., in $\tau_{d}$) iff for every $x\in O$, there is some $\varepsilon>0$ such that $N_{\varepsilon}(x)\subseteq O$. In other words, the open sets are the unions of open balls. We will say that a metric space has a given topological property (such as being dense in itself) if its associated topological space has the property. For example, it is known that every metric space is T2 (easy), and paracompact ([21]).

2.4 Modal languages

We fix a countably infinite set $\mathsf{Var}$ of propositional variables, or atoms. We will be considering a number of modal languages. The biggest of them is denoted by ${\mathcal{L}}^{\forall[\neq]\langle n\rangle}_{\Box[d]{\langle t\rangle}}$, which is a set of formulas defined as follows:

each $p\in\mathsf{Var}$ is a formula (of ${\mathcal{L}}^{\forall[\neq]\langle n\rangle}_{\Box[d]{\langle t\rangle}}$), 2. 2.

$\top$ is a formula, 3. 3.

if $\varphi,\psi$ are formulas then so are $\neg\varphi$, $(\varphi\wedge\psi)$, $\Box\varphi$, $[d]\varphi$, $\forall\varphi$, $[\neq]\varphi$, and $\langle n\rangle\varphi$ for each $n<\omega$, 4. 4.

if $\Delta$ is a non-empty finite set of formulas then ${\langle t\rangle}\Delta$ is a formula.

We use standard abbreviations: $\bot$ denotes $\neg\top$, $(\varphi\vee\psi)$ denotes $\neg(\neg\varphi\wedge\neg\psi)$, $(\varphi\to\psi)$ denotes $\neg(\varphi\wedge\neg\psi)$, $(\varphi\leftrightarrow\psi)$ denotes $((\varphi\to\psi)\wedge(\psi\to\varphi))$, $\Diamond\varphi$ denotes $\neg\Box\neg\varphi$, ${\langle d\rangle}\varphi$ denotes $\neg[d]\neg\varphi$, $\exists\varphi$ denotes $\neg\forall\neg\varphi$, and $\langle\neq\rangle\varphi$ denotes $\neg[\neq]\neg\varphi$. Parentheses will be omitted where possible, by the usual methods. For a non-empty finite set $\Delta=\{\delta_{1},\ldots{},\delta_{n}\}$ of formulas, we let $\bigwedge\Delta$ denote $\delta_{1}\wedge\ldots\wedge\delta_{n}$ and $\bigvee\Delta$ denote $\delta_{1}\vee\ldots\vee\delta_{n}$ (the order and bracketing of the conjuncts and disjuncts will always be immaterial). We set $\bigwedge\emptyset=\top$ and $\bigvee\emptyset=\bot$.

The connective $[d]$ is called the coderivative operator, and the connective ${\langle t\rangle}$ is called the tangle connective or tangled closure operator. A more powerful tangle connective ${\langle dt\rangle}$ can also be considered (see, e.g., [11, 12]) but we will not need it here. The connectives $\forall$ and $[\neq]$ are called the universal and difference modalities, respectively, and the connectives $\langle n\rangle$ are sometimes called the counting or graded modalities.

We will be using various sublanguages of ${\mathcal{L}}^{\forall[\neq]\langle n\rangle}_{\Box[d]{\langle t\rangle}}$, and they will be denoted in the obvious way by omitting prohibited operators from the notation. So for example, ${\mathcal{L}}^{\forall}_{\Box}$ denotes the set of all ${\mathcal{L}}^{\forall[\neq]\langle n\rangle}_{\Box[d]{\langle t\rangle}}$-formulas that do not involve $[d],$ ${\langle t\rangle}$, $[\neq]$, or any $\langle n\rangle$.

2.5 Kripke semantics

An assignment or valuation into a frame ${\mathcal{F}}=(W,R)$ is a map $h:\mathsf{Var}\to\wp(W)$. A Kripke model is a triple ${\mathcal{M}}=(W,R,h)$, where $(W,R)$ is a frame and $h$ an assignment into it. The frame of ${\mathcal{M}}$ is $(W,R)$.

For every Kripke model ${\mathcal{M}}=(W,R,h)$ and every world $w\in W$, we define the notion ${\mathcal{M}},w\models\varphi$ of a formula $\varphi$ of ${\mathcal{L}}^{\forall[\neq]\langle n\rangle}_{\Box[d]{\langle t\rangle}}$ being true at $w$ in ${\mathcal{M}}$. The definition is by induction on $\varphi$, as follows:

${\mathcal{M}},w\models p$ iff $w\in h(p)$, for $p\in\mathsf{Var}$. 2. 2.

${\mathcal{M}},w\models\top$. 3. 3.

${\mathcal{M}},w\models\neg\varphi$ iff ${\mathcal{M}},w\not\models\varphi$. 4. 4.

${\mathcal{M}},w\models\varphi\wedge\psi$ iff ${\mathcal{M}},w\models\varphi$ and ${\mathcal{M}},w\models\psi$. 5. 5.

${\mathcal{M}},w\models\Box\varphi$ iff ${\mathcal{M}},v\models\varphi$ for every $v\in R(w)$. 6. 6.

The truth condition for $[d]\varphi$ is exactly the same as for $\Box\varphi$. 7. 7.

${\mathcal{M}},w\models{\langle t\rangle}\Delta$ iff there are worlds $w=w_{0},w_{1},\ldots\in W$ with $R(w_{n},w_{n+1})$ for each $n<\omega$ and such that for each $\delta\in\Delta$ there are infinitely many $n<\omega$ with ${\mathcal{M}},w_{n}\models\delta$. 8. 8.

${\mathcal{M}},w\models\forall\varphi$ iff ${\mathcal{M}},v\models\varphi$ for every $v\in W$. 9. 9.

${\mathcal{M}},w\models[\neq]\varphi$ iff ${\mathcal{M}},v\models\varphi$ for every $v\in W\setminus\{w\}$. 10. 10.

${\mathcal{M}},w\models\langle n\rangle\varphi$ iff $|\{v\in W:{\mathcal{M}},v\models\varphi\}|>n$.

For a set $\Gamma$ of formulas, we write ${\mathcal{M}},w\models\Gamma$ if ${\mathcal{M}},w\models\gamma$ for every $\gamma\in\Gamma$.

2.6 Topological semantics

Given a topological space $X$, an assignment (or valuation) into $X$ is a map $h:\mathsf{Var}\to\wp(X)$. A topological model is a pair $(X,h)$, where $X$ is a topological space and $h$ an assignment into $X$. For every topological model $(X,h)$ and every point $x\in X$, we define $(X,h),x\models\varphi$, for a ${\mathcal{L}}^{\forall[\neq]\langle n\rangle}_{\Box[d]{\langle t\rangle}}$-formula $\varphi$, by induction on $\varphi$:

$(X,h),x\models p$ iff $x\in h(p)$, for $p\in\mathsf{Var}$. 2. 2.

$(X,h),x\models\top$. 3. 3.

$(X,h),x\models\neg\varphi$ iff $(X,h),x\not\models\varphi$. 4. 4.

$(X,h),x\models\varphi\wedge\psi$ iff $(X,h),x\models\varphi$ and $(X,h),x\models\psi$. 5. 5.

$(X,h),x\models\Box\varphi$ iff there is an open neighbourhood $O$ of $x$ with $(X,h),y\models\varphi$ for every $y\in O$. 6. 6.

$(X,h),x\models[d]\varphi$ iff there is an open neighbourhood $O$ of $x$ with $(X,h),y\models\varphi$ for every $y\in O\setminus\{x\}$. 7. 7.

For a non-empty finite set $\Delta$ of formulas for which we have inductively defined semantics, write $[\![\delta]\!]=\{x\in X:(X,h),x\models\delta\}$ for each $\delta\in\Delta$. Then:

$(X,h),x\models{\langle t\rangle}\Delta$ iff there is some $S\subseteq X$ such that $x\in S\subseteq\bigcap_{\delta\in\Delta}\mathop{\rm cl}\nolimits([\![\delta]\!]\cap S)$. 8. 8.

$(X,h),x\models\forall\varphi$ iff $(X,h),y\models\varphi$ for every $y\in X$. 9. 9.

$(X,h),x\models[\neq]\varphi$ iff $(X,h),y\models\varphi$ for every $y\in X\setminus\{x\}$. 10. 10.

$(X,h),x\models\langle n\rangle\varphi$ iff $|\{y\in X:(X,h),y\models\varphi\}|>n$.

Writing $[\![\varphi]\!]=\{x\in X:(X,h),x\models\varphi\}$, we have $[\![\Box\varphi]\!]=\mathop{\rm int}([\![\varphi]\!])$, $[\![\Diamond\varphi]\!]=\mathop{\rm cl}\nolimits([\![\varphi]\!])$, and $[\![{\langle d\rangle}\varphi]\!]={\langle d\rangle}([\![\varphi]\!])$ for each $\varphi$.

As with Kripke semantics, for a set $\Gamma$ of formulas we write $(X,h),x\models\Gamma$ if $(X,h),x\models\gamma$ for every $\gamma\in\Gamma$. We say that $\Gamma$ is satisfiable in $(X,h)$ if $(X,h),x\models\Gamma$ for some $x\in X$; and satisfiable in $X$ if it is satisfiable in $(X,h)$ for some assignment $h$ into $X$. We say that $\Gamma$ is finitely satisfiable in $(X,h)$ (respectively, $X$) if every finite subset of $\Gamma$ is satisfiable in $(X,h)$ (respectively, $X$). Of course, we say that a formula $\varphi$ is satisfiable in these ways if $\{\varphi\}$ is so satisfiable. We write $\Gamma\models_{X}\varphi$ if $\Gamma\cup\{\neg\varphi\}$ is not satisfiable in $X$. For a language ${\mathcal{L}}\subseteq{\mathcal{L}}^{\forall[\neq]\langle n\rangle}_{\Box[d]{\langle t\rangle}}$, the ${\mathcal{L}}$-logic of $X$ is the set $\{\varphi\in{\mathcal{L}}:\emptyset\models_{X}\varphi\}$.

2.7 Weaker, stronger, and equivalent languages

We say that formulas $\varphi,\psi$ are (topologically) equivalent if $(X,h),x\models\varphi\leftrightarrow\psi$ for every topological model $(X,h)$ and every $x\in X$. For languages ${\mathcal{L}},{\mathcal{L}}^{\prime}\subseteq{\mathcal{L}}^{\forall[\neq]\langle n\rangle}_{\Box[d]{\langle t\rangle}}$, we say that ${\mathcal{L}}$ is weaker than ${\mathcal{L}}^{\prime}$, and ${\mathcal{L}}^{\prime}$ is stronger than ${\mathcal{L}}$, if every formula of ${\mathcal{L}}$ is equivalent to a formula of ${\mathcal{L}}^{\prime}$. We say that ${\mathcal{L}}$ is equivalent to ${\mathcal{L}}^{\prime}$ if ${\mathcal{L}}$ is both weaker and stronger than ${\mathcal{L}}^{\prime}$, and that ${\mathcal{L}}$ is strictly weaker than ${\mathcal{L}}^{\prime}$, and ${\mathcal{L}}^{\prime}$ is strictly stronger than ${\mathcal{L}}$, if ${\mathcal{L}}$ is weaker but not stronger than ${\mathcal{L}}^{\prime}$.

Some operators of ${\mathcal{L}}^{\forall[\neq]\langle n\rangle}_{\Box[d]{\langle t\rangle}}$ can express others. Clearly, $\Box\varphi$ is (topologically) equivalent to $\varphi\wedge[d]\varphi$ and to $\neg{\langle t\rangle}\{\neg\varphi\}$, and $\forall\varphi$ is equivalent to $\neg\langle 0\rangle\neg\varphi$. It follows for example that ${\mathcal{L}}^{\forall}_{\Box}$, ${\mathcal{L}}^{\forall\langle n\rangle}_{\Box[d]}$ are weaker than ${\mathcal{L}}^{\langle n\rangle}_{[d]}$, and in fact the first strictly so.

In the same vein, $\langle\neq\rangle\varphi$ is equivalent to $(\neg\varphi\to\exists\varphi)\wedge(\varphi\to\langle 1\rangle\varphi)$, $\exists\varphi$ is equivalent to $\varphi\vee\langle\neq\rangle\varphi$, and $\langle 1\rangle\varphi$ is equivalent to $\exists(\varphi\wedge\langle\neq\rangle\varphi)$. So we can exchange $\{\forall,\langle 1\rangle\}$ with $[\neq]$, preserving language equivalence; and the language ${\mathcal{L}}^{[\neq]}_{\zeta}$ is weaker than ${\mathcal{L}}^{\langle n\rangle}_{\zeta}$, for any $\zeta$.

2.8 Strong completeness

This is the topic of the paper. We assume familiarity, e.g., from [11] and [12, §§2.10, 2.12, 8.1], with (modal) deductive systems. They are Hilbert systems containing, at least, all propositional tautologies as axioms and the modus ponens inference rule. For such a system $\vdash$, a theorem of $\vdash$ is a formula $\varphi$ that is provable in $\vdash$, in which case we write $\vdash\varphi$; for a set $\Sigma$ of formulas, we write $\Sigma\vdash\varphi$ if there is some finite $\Sigma_{0}\subseteq\Sigma$ such that $\vdash(\bigwedge\Sigma_{0})\to\varphi$; and $\Sigma$ is said to be ($\vdash$-)consistent if $\Sigma\not\vdash\bot$. All deductive systems mentioned later in the paper are taken to be of this form. For such systems, though not for all deductive systems in the world, consistency reduces to a property of the set of theorems, and $\Sigma$ is consistent iff each of its finite subsets is consistent.

A deductive system $\vdash$ for a language ${\mathcal{L}}\subseteq{\mathcal{L}}^{\forall[\neq]\langle n\rangle}_{\Box[d]{\langle t\rangle}}$ is said to be sound over a topological space $X$ if for every ${\mathcal{L}}$-formula $\varphi$, if $\vdash\varphi$ then $\emptyset\models_{X}\varphi$. Equivalently, every finitely satisfiable (in $X$) set of ${\mathcal{L}}$-formulas is $\vdash$-consistent. We say that $\vdash$ is strongly complete over $X$ if for every set $\Sigma\cup\{\varphi\}$ of ${\mathcal{L}}$-formulas, if $\Sigma\models_{X}\varphi$ then $\Sigma\vdash\varphi$, and complete over $X$ if this holds when $\Sigma$ is finite. It follows that $\vdash$ is (strongly) complete over $X$ iff every finite $\vdash$-consistent set (respectively, every $\vdash$-consistent set) of formulas is satisfiable in $X$. Recall that $\mathsf{Var}$ is countable, so we are dealing always with countable sets of formulas.

For many topological spaces and sublanguages of ${\mathcal{L}}_{\Box[d]{\langle t\rangle}}$, strongly complete deductive systems are known.

• •

[15] showed that for ${\mathcal{L}}_{\Box}$, the system S4 is strongly complete over every dense-in-itself metric space. (It had long been known from the work of [18, 19] that S4 is sound and complete over every such space.)

• •

In the language ${\mathcal{L}}_{\Box{\langle t\rangle}}$, the system S4$t$ is sound and strongly complete over every dense-in-itself metric space [12, theorem 9.3(1)].

• •

In the language ${\mathcal{L}}_{[d]}$, the system KD4G1 is strongly complete over every dense-in-itself metric space, and sound if the space has a property called ‘G1’ [12, theorem 9.2].

• •

The same holds for the system KD4G${}_{1}t$ in a language expanding ${\mathcal{L}}_{[d]}$ by the stronger tangle operator ${\langle dt\rangle}$ already mentioned [12, theorem 9.1].

• •

In this latter language, the system KD4t is sound and strongly complete over every 0-dimensional dense-in-itself metric space [11, theorem 8.5].

2.9 Compactness

For a language ${\mathcal{L}}\subseteq{\mathcal{L}}^{\forall[\neq]\langle n\rangle}_{\Box[d]{\langle t\rangle}}$ and a topological space $X$, we say that ${\mathcal{L}}$ is compact over $X$ if every set of ${\mathcal{L}}$-formulas that is finitely satisfiable in $X$ is satisfiable in $X$. Do not confuse this with compactness of the space $X$.

Obviously, if ${\mathcal{L}}$ is compact over $X$ then so is every sublanguage of ${\mathcal{L}}$, and every weaker language. For example, if ${\mathcal{L}}^{\langle n\rangle}_{[d]}$ is compact over $X$ then so are ${\mathcal{L}}^{\forall}_{\Box}$, ${\mathcal{L}}^{\forall\langle n\rangle}_{\Box[d]}$, etc.

Compactness is tightly connected to strong completeness. The following is well known and easy to prove.

FACT 2.1

Let $\vdash$ be a deductive system for a language ${\mathcal{L}}\subseteq{\mathcal{L}}^{\forall[\neq]\langle n\rangle}_{\Box[d]{\langle t\rangle}}$, and let $X$ be a topological space. If $\vdash$ is complete over $X$ and ${\mathcal{L}}$ is compact over $X$, then $\vdash$ is strongly complete over $X$. The converse holds if $\vdash$ is sound over $X$.

So on the one hand, where a complete deductive system is known for a space, compactness, if available, can be used to show that the system is actually strongly complete. Soundness is not required. This is how the results of [11, 12] mentioned in §2.8 were proved.

On the other hand, failure of compactness kills any hope of finding a sound and strongly complete deductive system. As we mentioned in 1, no deductive system for ${\mathcal{L}}^{\forall}_{\Box}$ is sound and strongly complete over a compact locally connected dense-in-itself metric space [12, corollary 9.5], and this was proved using failure of compactness.

This paper is about strong completeness over 0-dimensional dense-in-themselves metric spaces in languages able to express $\forall$. Relevant sound and complete deductive systems were given by [16] and [11], and we are therefore interested in determining which sublanguages of ${\mathcal{L}}^{\forall[\neq]\langle n\rangle}_{\Box[d]{\langle t\rangle}}$ are compact over which 0-dimensional dense-in-themselves metric spaces. The rest of the paper is devoted to this question, and the answers are varied and interesting.

3 Strong completeness with $\forall$ and tangle fails always

The following is based on an example in [13, §5] using $\Box$. Here we use $\forall$ instead.

THEOREM 3.1

Compactness fails for the language ${\mathcal{L}}^{\forall}_{{\langle t\rangle}}$ over every dense-in-itself metric space $X$.

• *Proof. *

Since ${\mathcal{L}}^{\forall}_{{\langle t\rangle}}$ can express $\Box\varphi$, via $\neg{\langle t\rangle}\{\neg\varphi\}$, we can work in ${\mathcal{L}}^{\forall}_{\Box{\langle t\rangle}}$. Fix pairwise distinct atoms $q,p_{0},p_{1},\ldots\in\mathsf{Var}$, and define

[TABLE]

For each $n<\omega$, the subset $\Sigma_{n}$ of formulas in $\Sigma$ using atoms $p_{0},\ldots{},p_{n},q$ only is true at 0 in the Kripke model $M_{n}=(\{0,\ldots,n\},\leq,h)$, with $h(p_{i})=\{i\}$ for $i\leq n$, and $h(q)=\{2i:i<\omega,\;2i\leq n\}$. The frame of $M_{n}$ validates the axioms of the system S4$t$.UC of [12, §8.1], so $\Sigma_{n}$ is S4$t$.UC-consistent. Now by [12, theorem 8.4(2)], S4$t$.UC is complete over every dense-in-itself metric space, and $\Sigma_{n}$ is finite, so $\Sigma_{n}$ is satisfiable in $X$. It follows that $\Sigma$ is finitely satisfiable in $X$.

Suppose for contradiction that $(X,h),x_{0}\models\Sigma$, for some assignment $h$ and some $x_{0}\in X$. Below, we write $x\models\varphi$ as short for $(X,h),x\models\varphi$. Let

[TABLE]

We show that $S\subseteq\mathop{\rm cl}\nolimits(S\cap h(q))\cap\mathop{\rm cl}\nolimits(S\setminus h(q))$. Let $x\in S$. Pick $n<\omega$ such that $x\models p_{n}$. Suppose that $n$ is even (the case where it is odd is similar). Since $x_{0}\models\forall(p_{n}\to q)$, we have $x\in S\cap h(q)$ already, so certainly $x\in\mathop{\rm cl}\nolimits(S\cap h(q))$. Now let $O$ be any open neighbourhood of $x$. Since $x_{0}\models\forall(p_{n}\to\Diamond p_{n+1})$, and $x\models p_{n}$, there is $y\in O$ with $y\models p_{n+1}$. So $y\in S$, and also $y\models\neg q$ as $x_{0}\models\forall(p_{n+1}\to\neg q)$ because $n+1$ is odd. As $O$ was arbitrary, $x\in\mathop{\rm cl}\nolimits(S\setminus h(q))$. As $x$ was arbitrary, $S\subseteq\mathop{\rm cl}\nolimits(S\cap h(q))\cap\mathop{\rm cl}\nolimits(S\setminus h(q))$ as required.

By semantics of tangle (§2.6), every point in $S$ satisfies $\langle t\rangle\{q,\neg q\}$. Since $x_{0}\in h(p_{0})\subseteq S$, $x_{0}\models\langle t\rangle\{q,\neg q\}$, contradicting that $x_{0}\models\Sigma$.  $\Box$

The proof applies to any language able to express $\forall$, $\Box$, and $\langle t\rangle\{\varphi,\neg\varphi\}$. The following is immediate via fact 2.1.

COROLLARY 3.2

Let $X$ be a dense-in-itself metric space. No deductive system for ${\mathcal{L}}^{\forall}_{{\langle t\rangle}}$ or any stronger language is sound and strongly complete over $X$.

One such stronger language comprises $\Box$, $\forall$  and the modal mu-calculus [12, lemma 4.2].

By corollary 3.2, in the presence of $\forall$ we can forget about tangle.

4 Non-compact 0-dimensional spaces with $\forall$ and $[d]$

We now aim to show that ${\mathcal{L}}^{\forall}_{[d]}$ is compact over every non-compact 0-dimensional dense-in-itself metric space. This will have consequences for strong completeness in the languages ${\mathcal{L}}^{\forall}_{[d]}$ and ${\mathcal{L}}^{\forall}_{\Box}$.

4.1 Topology

We will need some topology. Fix a dense-in-itself metric space $(X,d)$.

FACT 4.1

First we quote some basic results, some of which are true much more generally. They are easy to prove.

[12, lemma 5.3] Every non-empty open subset of $X$ is infinite. 2. 2.

If $S\subseteq X$ then $\mathop{\rm int}S\subseteq S\cap{\langle d\rangle}S$ and $\mathop{\rm cl}\nolimits S=S\cup{\langle d\rangle}S$. 3. 3.

${\langle d\rangle}$ is additive: if $S,T\subseteq X$ then ${\langle d\rangle}(S\cup T)={\langle d\rangle}S\cup{\langle d\rangle}T$ (as already mentioned). 4. 4.

[12, lemma 5.1(2)] If $N\subseteq X$ has empty interior and $O\subseteq X$ is open, then $\mathop{\rm cl}\nolimits(O\setminus N)=\mathop{\rm cl}\nolimits O$.

The following will be useful. For a real number $\varepsilon>0$, we say that a subset $S\subseteq X$ is $\varepsilon$-sparse if $d(x,y)\geq\varepsilon$ for every distinct $x,y\in S$. In that case, ${\langle d\rangle}S=\emptyset$.

LEMMA 4.2

Let $\mathbb{G}\subseteq X$ be open and let $I$ be a countable index set. Then there are pairwise disjoint sets $\mathbb{I}_{i}\subseteq\mathbb{G}$ $(i\in I)$ such that

${\langle d\rangle}\mathbb{I}_{i}=\mathop{\rm cl}\nolimits\mathbb{G}\setminus\mathbb{G}$* for every $i\in I$,* 2. 2.

$\mathbb{G}\cap{\langle d\rangle}\bigcup_{i\in I}\mathbb{I}_{i}=\emptyset$.

Without part 2, this follows from [12, theorem 6.1], and part 2 can be extracted from the proof of that theorem. But the lemma is fairly quick to prove, so we prove it here.

• *Proof. *

Write $B=\mathop{\rm cl}\nolimits\mathbb{G}\setminus\mathbb{G}$. If $B=\emptyset$, we can take $\mathbb{I}_{i}=\emptyset$ for each $i\in I$. We are done.

Assume now that $B\neq\emptyset$. Define $\varepsilon_{n}=1/2^{n}$ for each $n<\omega$. We define pairwise disjoint subsets $Z_{n}\subseteq\mathbb{G}$ ($n<\omega$), with ${\langle d\rangle}Z_{n}=\emptyset$, by induction as follows. Let $n<\omega$ and assume inductively that $Z_{m}$ has been defined for each $m<n$. Let

[TABLE]

Using Zorn’s lemma, choose $Z_{n}$ to be a maximal $\varepsilon_{n}$-sparse subset of $O_{n}$. As we said, ${\langle d\rangle}Z_{n}=\emptyset$, and plainly $Z_{n}\subseteq\mathbb{G}$. This completes the definition of the pairwise disjoint $Z_{n}$.

We first show that

[TABLE]

Let $x\in\mathbb{G}$ be arbitrary, and choose $n<\omega$ so large that $N_{2\varepsilon_{n}}(x)\subseteq\mathbb{G}$. Consequently, $d(x,B)\geq 2\varepsilon_{n}$. Now for each $m\geq n$ we have $Z_{m}\subseteq O_{m}\subseteq N_{\varepsilon_{n}}(B)$. If there is $z\in N_{\varepsilon_{n}}(x)\cap Z_{m}$, then $d(x,B)\leq d(x,z)+d(z,B)<\varepsilon_{n}+\varepsilon_{n}=2\varepsilon_{n}$, a contradiction. So $N_{\varepsilon_{n}}(x)\cap\bigcup_{m\geq n}Z_{m}=\emptyset$, and $x\notin{\langle d\rangle}\bigcup_{m\geq n}Z_{m}$. By fact 4.1, ${\langle d\rangle}\bigcup_{m<n}Z_{m}=\bigcup_{m<n}{\langle d\rangle}Z_{m}=\emptyset$, so $x\notin{\langle d\rangle}\bigcup_{m<n}Z_{m}$ as well. Hence, $x\notin{\langle d\rangle}\bigcup_{m<n}Z_{m}\cup{\langle d\rangle}\bigcup_{m\geq n}Z_{m}={\langle d\rangle}\bigcup_{m<\omega}Z_{m}$, proving (1).

Now let $J\subseteq\omega$ be infinite; we show that

[TABLE]

Write $Z=\bigcup_{n\in J}Z_{n}$. Certainly, since $Z\subseteq\mathbb{G}$ we have ${\langle d\rangle}Z\subseteq\mathop{\rm cl}\nolimits\mathbb{G}$. By (1) and monotonicity of ${\langle d\rangle}$, $\mathbb{G}\cap{\langle d\rangle}Z=\emptyset$, so ${\langle d\rangle}Z\subseteq B$.

For the converse, let $b\in B$ and let $\varepsilon>0$ be given. We will show that $Z\cap N_{\varepsilon}(b)\neq\emptyset$.

Choose $n\in J$ so large that $2\varepsilon_{n}\leq\varepsilon$. By fact 4.1, $\mathop{\rm int}\bigcup_{m<n}Z_{m}\subseteq{\langle d\rangle}\bigcup_{m<n}Z_{m}=\emptyset$. So $\bigcup_{m<n}Z_{m}$ has empty interior. By fact 4.1 again, $\mathop{\rm cl}\nolimits\mathbb{G}=\mathop{\rm cl}\nolimits(\mathbb{G}\setminus\bigcup_{m<n}Z_{m})$.

Now $b\in\mathop{\rm cl}\nolimits\mathbb{G}$. So there is $x\in N_{\varepsilon_{n}}(b)\cap\mathbb{G}\setminus\bigcup_{m<n}Z_{m}\subseteq O_{n}$. If $Z_{n}\cap N_{\varepsilon}(b)=\emptyset$, then for every $z\in Z_{n}$ we have $d(x,z)\geq d(b,z)-d(b,x)>\varepsilon-\varepsilon_{n}\geq\varepsilon_{n}$, so $x$ could be added to $Z_{n}$, contradicting its maximality. Hence, $Z\cap N_{\varepsilon}(b)\neq\emptyset$, as required.

This holds for every $\varepsilon>0$, and hence $b\in\mathop{\rm cl}\nolimits Z=Z\cup{\langle d\rangle}Z$ (fact 4.1). Since $Z\subseteq\mathbb{G}$, we have $b\notin Z$, so $b\in{\langle d\rangle}Z$. As $b\in B$ was arbitrary, we obtain $B\subseteq{\langle d\rangle}Z$, so proving (2).

Now to prove the lemma, simply partition $\omega$ into infinite sets $J_{i}$ $(i\in I)$ and define $\mathbb{I}_{i}=\bigcup_{n\in J_{i}}Z_{n}$.  $\Box$

From now on, assume further that $X$ is 0-dimensional.

LEMMA 4.3

Let $\mathbb{G}\subseteq X$ be open, and suppose that $Z\subseteq\mathbb{G}$ and $\mathbb{G}\cap{\langle d\rangle}Z=\emptyset$. Then there is a family $(K(T):T\subseteq Z)$ of subsets of $\mathbb{G}$ such that for each $T\subseteq Z$:

$T\subseteq K(T)\subseteq\mathbb{G}$, 2. 2.

if ${\mathcal{U}}\subseteq\wp(Z)$ then $K(\bigcup{\mathcal{U}})=\bigcup_{U\in{\mathcal{U}}}K(U)$, and hence $K(\emptyset)=\emptyset$, 3. 3.

if $U\subseteq Z$ and $T\cap U=\emptyset$ then $K(T)\cap K(U)=\emptyset$, 4. 4.

$K(T)$* is open,* 5. 5.

$\mathbb{G}\setminus K(T)$* is open.*

• *Proof. *

If $Z=\emptyset$, define $K(\emptyset)=\emptyset$; we are done. So assume from now on that $Z$, and hence $\mathbb{G}$, are non-empty, so that $\mathbb{G}$ is a subspace of $X$. Since $\mathbb{G}\cap{\langle d\rangle}Z=\emptyset$, it follows that ${\mathcal{O}}^{+}=\{Q\subseteq\mathbb{G}:Q$ open, $|Q\cap Z|\leq 1\}$ is an open cover of the subspace $\mathbb{G}$. This subspace, being a metric space, is paracompact — see [21] or [6, 5.1.3]. So there is a locally finite open cover ${\mathcal{O}}$ of $\mathbb{G}$ that refines ${\mathcal{O}}^{+}$. Evidently,

[TABLE]

For each $z\in Z$, use 0-dimensionality to choose a clopen neighbourhood $K^{+}(z)$ of $z$ contained in some $O\in{\mathcal{O}}$ and disjoint from all but finitely many sets in ${\mathcal{O}}$. Since $z\in K^{+}(z)$, it follows from (3) that each $O\in{\mathcal{O}}$ contains at most one set $K^{+}(z)$. Since $K^{+}(z)$ intersects only finitely many sets in ${\mathcal{O}}$, it therefore intersects only finitely many $K^{+}(t)$ $(t\in Z\setminus\{z\})$. The union of these finitely many sets is clopen, so the set

[TABLE]

is clopen. It also follows from (3) that $K^{+}(z)$ is the only $K^{+}(t)$ that contains $z$; so $z\in K(z)$.

For each $T\subseteq Z$ define $K(T)=\bigcup_{t\in T}K(t)$. We prove the lemma under this definition. Items 1 and 2 are trivial. Item 3 holds because the $K(z)$ $(z\in Z)$ are plainly pairwise disjoint. Item 4 holds because by definition, $K(T)$ is a union of open sets. For item 5, see [23, 20.4–5], or prove it directly as follows. Each $x\in\mathbb{G}\setminus K(T)$ has an open neighbourhood $U$ such that $\{O\in{\mathcal{O}}:U\cap O\neq\emptyset\}$ is finite, and hence also $\{t\in T:U\cap K(t)\neq\emptyset\}$ is finite. Since a finite union of sets $K(t)$ is closed, and $x\notin K(T)$, the set $U\setminus K(T)$ is an open neighbourhood of $x$. It follows that $\mathbb{G}\setminus K(T)$ is open.  $\Box$

The following is the first result needed later, and is where non-compactness comes in.

THEOREM 4.4

$X$* is not compact iff $X$ can be partitioned into infinitely many non-empty open sets.*

• *Proof. *

$\Leftarrow$ is obvious. For $\Rightarrow$, assume that $X$ is not compact. By [6, 3.10.3], there is an infinite subset $Z\subseteq X$ with ${\langle d\rangle}Z=\emptyset$. Taking $\mathbb{G}$ in lemma 4.3 to be $X$, the lemma tells us that $X$ is partitioned into the pairwise disjoint open sets $K(\{z\})$ $(z\in Z)$ and $X\setminus K(Z)$. The non-empty sets among these (all but perhaps $X\setminus K(Z)$) form the required partition.  $\Box$

By grouping sets together, an infinite partition into open sets can be ‘coarsened’ into a partition into any finite number of open sets.

The next corollary is similar. Cf. [11, theorem 7.5].

COROLLARY 4.5

Let $\mathbb{G}\subseteq X$ be open, and $I$ be non-empty and countable. Then $\mathbb{G}$ can be partitioned into open sets $\mathbb{G}_{i}$ $(i\in I)$ such that $\mathop{\rm cl}\nolimits(\mathbb{G})\setminus\mathbb{G}=\mathop{\rm cl}\nolimits(\mathbb{G}_{i})\setminus\mathbb{G}_{i}$ for each $i\in I$.

• *Proof. *

By lemma 4.2, we can select pairwise disjoint sets $\mathbb{I}_{i}\subseteq\mathbb{G}$ for $i\in I$, with ${\langle d\rangle}\mathbb{I}_{i}=\mathop{\rm cl}\nolimits\mathbb{G}\setminus\mathbb{G}$ for every $i\in I$, and $\mathbb{G}\cap{\langle d\rangle}Z=\emptyset$, where $Z=\bigcup_{i\in I}\mathbb{I}_{i}$. Choose sets $K(T)\subseteq\mathbb{G}$ (for $T\subseteq Z$) as in lemma 4.3. Fix any $i_{0}\in I$. For each $i\in I$ let

[TABLE]

By lemma 4.3, the $\mathbb{G}_{i}$ are pairwise disjoint open subsets of $\mathbb{G}$, and they plainly partition $\mathbb{G}$.

Let $i\in I$. We check that $\mathop{\rm cl}\nolimits\mathbb{G}\setminus\mathbb{G}=\mathop{\rm cl}\nolimits\mathbb{G}_{i}\setminus\mathbb{G}_{i}$. Notice that $\mathbb{I}_{i}\subseteq\mathbb{G}_{i}$, even when $i=i_{0}$. So $\mathop{\rm cl}\nolimits\mathbb{G}\setminus\mathbb{G}={\langle d\rangle}\mathbb{I}_{i}\subseteq\mathop{\rm cl}\nolimits\mathbb{G}_{i}$. Since $\mathop{\rm cl}\nolimits\mathbb{G}\setminus\mathbb{G}$ is disjoint from $\mathbb{G}$ and hence also from $\mathbb{G}_{i}$, we obtain $\mathop{\rm cl}\nolimits\mathbb{G}\setminus\mathbb{G}\subseteq\mathop{\rm cl}\nolimits\mathbb{G}_{i}\setminus\mathbb{G}_{i}$.

Conversely, of course $\mathbb{G}_{i}\subseteq\mathbb{G}$, so $\mathop{\rm cl}\nolimits\mathbb{G}_{i}\subseteq\mathop{\rm cl}\nolimits\mathbb{G}$. Now $\bigcup_{j\in I\setminus\{i\}}\mathbb{G}_{j}$ is open and disjoint from $\mathbb{G}_{i}$, so it is also disjoint from $\mathop{\rm cl}\nolimits\mathbb{G}_{i}$. Hence, $\mathop{\rm cl}\nolimits\mathbb{G}_{i}\setminus\mathbb{G}_{i}$ is disjoint from $\mathbb{G}_{i}\cup\bigcup_{j\in I\setminus\{i\}}\mathbb{G}_{j}=\mathbb{G}$. We obtain $\mathop{\rm cl}\nolimits\mathbb{G}_{i}\setminus\mathbb{G}_{i}\subseteq\mathop{\rm cl}\nolimits\mathbb{G}\setminus\mathbb{G}$ as required.  $\Box$

Now we come to the second result needed later. The first part is equivalent to Tarski’s well-known ‘dissection theorem’ ([22], later strengthened in [18]), except that $I$ can be infinite. The second part is distinctively 0-dimensional: for example, the theorem can fail when $X=\mathbb{R}$ and $|I|\geq 3$. The third part harks back to the ‘$\varepsilon$ clause’ in [15, lemma 4.3].

THEOREM 4.6

For any non-empty countable set $I$ and any $\varepsilon>0$, any non-empty open subset $\mathbb{G}\subseteq X$ can be partitioned into a non-empty set $\mathbb{B}$ and (necessarily non-empty) open sets $\mathbb{G}_{i}$ ($i\in I$) such that

$\displaystyle\mathop{\rm cl}\nolimits(\mathbb{G})\setminus\bigcup_{i\in I}\mathbb{G}_{i}=\mathop{\rm cl}\nolimits\mathbb{B}=\mathop{\rm cl}\nolimits\mathbb{G}_{i}\setminus\mathbb{G}_{i}$* for each $i\in I$,* 2. 2.

$\mathbb{G}\cap{\langle d\rangle}\mathbb{B}=\emptyset$, 3. 3.

$d(x,\mathbb{B})<\varepsilon$* for every $x\in\mathbb{G}$.*

• *Proof. *

Using Zorn’s lemma, choose a maximal $\varepsilon$-sparse set $Z\subseteq\mathbb{G}$. Then ${\langle d\rangle}Z=\emptyset$, $Z$ is non-empty (since any singleton subset of $\mathbb{G}$ is $\varepsilon$-sparse), and $d(x,Z)<\varepsilon$ for every $x\in\mathbb{G}$ (else $x$ could be added to $Z$, contradicting its maximality).

Now use lemma 4.2 with $I$ a singleton to choose $\mathbb{I}\subseteq\mathbb{G}$ such that ${\langle d\rangle}\mathbb{I}=\mathop{\rm cl}\nolimits\mathbb{G}\setminus\mathbb{G}$, and define $\mathbb{B}=\mathbb{I}\cup Z\subseteq\mathbb{G}$. Then

[TABLE]

Since $Z\subseteq\mathbb{B}$, we have $\mathbb{B}\neq\emptyset$ and $d(x,\mathbb{B})<\varepsilon$ for every $x\in\mathbb{G}$. So parts 2 and 3 hold.

Let $\mathbb{G}^{\prime}=\mathbb{G}\setminus\mathbb{B}$. Note that ${\langle d\rangle}\mathbb{B}$ is disjoint from $\mathbb{G}$. So by fact 4.1, $\mathbb{G}^{\prime}=\mathbb{G}\setminus(\mathbb{B}\cup{\langle d\rangle}\mathbb{B})=\mathbb{G}\setminus\mathop{\rm cl}\nolimits\mathbb{B}$, which is open; $\mathop{\rm int}\mathbb{B}\subseteq\mathbb{B}\cap{\langle d\rangle}\mathbb{B}=\emptyset$, so $\mathbb{B}$ has empty interior; hence $\mathop{\rm cl}\nolimits\mathbb{G}^{\prime}=\mathop{\rm cl}\nolimits\mathbb{G}$. We now use corollary 4.5 to partition $\mathbb{G}^{\prime}$ into open sets $\mathbb{G}_{i}$ $(i\in I)$ with $\mathop{\rm cl}\nolimits\mathbb{G}_{i}\setminus\mathbb{G}_{i}=\mathop{\rm cl}\nolimits\mathbb{G}^{\prime}\setminus\mathbb{G}^{\prime}$ for each $i\in I$. Then

[TABLE]

Each $\mathbb{G}_{i}$ is non-empty since $\mathbb{B}\subseteq\mathop{\rm cl}\nolimits\mathbb{G}_{i}$. This proves part 1, and we are done.  $\Box$

4.2 Logic

THEOREM 4.7

The language ${\mathcal{L}}^{\forall}_{[d]}$ is compact over every non-compact 0-dimensional dense-in-itself metric space.

• *Proof. *

We adopt a broadly similar approach to [15], and extend it to handle $\forall$ and $[d]$. Fix a non-compact 0-dimensional dense-in-itself metric space $X$ and a set $\Sigma$ of ${\mathcal{L}}^{\forall}_{[d]}$-formulas that is finitely satisfiable in $X$. We show that $\Sigma$ is satisfiable in $X$.

Step 1.

By the argument of [11, theorem 8.4] and the comments after it, in the language ${\mathcal{L}}^{\forall}_{[d]}$ the system KD4U is sound and complete over $X$. Since $\Sigma$ is finitely satisfiable in $X$, it is KD4U-consistent. Hence, using the canonical model and the downward Löwenheim–Skolem theorem, which are standard modal techniques, we can find a countable Kripke model ${\mathcal{M}}=(W,R,h)$ whose frame $(W,R)$ validates KD4 and so is serial and transitive, and $w_{0}\in W$, such that ${\mathcal{M}},w_{0}\models\Sigma$. (The U axioms are used in obtaining ${\mathcal{M}}$.)

Step 2.

We now define by induction on $n<\omega$ a set ${\mathcal{G}}_{n}$ of pairwise disjoint non-empty open subsets of $X$, and a ‘labeling’ map $\lambda_{n}:{\mathcal{G}}_{n}\to W$.

Since $X$ is not compact, we can use theorem 4.4 to partition it into pairwise disjoint non-empty open sets $O_{w}$ $(w\in W)$. We define ${\mathcal{G}}_{0}=\{O_{w}:w\in W\}$ and $\lambda_{0}(O_{w})=w$ for each $w\in W$. Since the $O_{w}$ are pairwise disjoint, $\lambda_{0}$ is well defined.

Let $n<\omega$ and suppose inductively that ${\mathcal{G}}_{n},\lambda_{n}$ have been defined. Let $\mathbb{G}\in{\mathcal{G}}_{n}$, and suppose that $\lambda_{n}(\mathbb{G})=u$, say. Use theorem 4.6 to partition $\mathbb{G}$ into non-empty open sets $\mathbb{G}_{w}$ ($w\in R(u)$) and a non-empty set $\mathbb{B}(\mathbb{G})$ with

• –

$\mathop{\rm cl}\nolimits\mathbb{G}\setminus\bigcup_{w\in R(u)}\mathbb{G}_{w}=\mathop{\rm cl}\nolimits\mathbb{B}(\mathbb{G})=\mathop{\rm cl}\nolimits\mathbb{G}_{w}\setminus\mathbb{G}_{w}$ for each $w\in R(u)$,

• –

$\mathbb{G}\cap{\langle d\rangle}\mathbb{B}(\mathbb{G})=\emptyset$,

• –

$d(x,\mathbb{B}(\mathbb{G}))<1/2^{n+1}$ for every $x\in\mathbb{G}$.

We can apply the theorem here because the frame $(W,R)$ is serial and so $R(u)\neq\emptyset$. Let ${\mathcal{G}}_{n+1}=\{\mathbb{G}_{w}:\mathbb{G}\in{\mathcal{G}}_{n},\;w\in R(\lambda_{n}(\mathbb{G}))\}$. Also define $\lambda_{n+1}:{\mathcal{G}}_{n+1}\to W$ by $\lambda_{n+1}(\mathbb{G}_{w})=w$. This is well defined, because the elements of ${\mathcal{G}}_{n}$ are pairwise disjoint, so each $\mathbb{G}_{w}$ gets into ${\mathcal{G}}_{n+1}$ in only one way.

That completes the definition of the ${\mathcal{G}}_{n},\lambda_{n}$. Let ${\mathcal{G}}=\bigcup_{n<\omega}{\mathcal{G}}_{n}$ and $\lambda=\bigcup_{n<\omega}\lambda_{n}$. Then $({\mathcal{G}},\supset)$ is a forest (that is, a disjoint union of trees) with roots the $O_{w}$ and whose branches all have height $\omega$. Also, since $R$ is transitive, it follows that $\lambda:({\mathcal{G}},\supset)\to(W,R)$ is a surjective p-morphism.

Step 3.

For each $x\in X$, let ${\mathcal{E}}(x)=\{\mathbb{G}\in{\mathcal{G}}:x\in\mathbb{G}\}$. This is either a branch of the forest $({\mathcal{G}},\supset)$, or a finite initial segment of such a branch. It is non-empty, since there is $w\in W$ with $x\in O_{w}$, and then $O_{w}\in{\mathcal{E}}(x)$.

Select an ultrafilter $D_{x}$ on ${\mathcal{E}}(x)$ as follows. If ${\mathcal{E}}(x)$ is finite, its $\subseteq$-minimal element is $\bigcap{\mathcal{E}}(x)$, and we let $D_{x}$ be the principal ultrafilter $\{S\subseteq{\mathcal{E}}(x):\bigcap{\mathcal{E}}(x)\in S\}$. If ${\mathcal{E}}(x)$ is infinite, we let $D_{x}$ be any non-principal ultrafilter on ${\mathcal{E}}(x)$. Now let

[TABLE]

Observe that

• $({\dagger})$

every $\varphi\in\Gamma_{x}$ is true in ${\mathcal{M}}$ at some world of the form $\lambda(\mathbb{G})$ for some $\mathbb{G}\in{\mathcal{E}}(x)$,

• $({\ddagger})$

if $\mathbb{G}\in{\mathcal{G}}$ and $x\in\mathbb{B}(\mathbb{G})$, then $\bigcap{\mathcal{E}}(x)=\mathbb{G}$ and $\Gamma_{x}=\{\varphi\in{\mathcal{L}}^{\forall}_{[d]}:{\mathcal{M}},\lambda(\mathbb{G})\models\varphi\}$.

Step 4.

Define an assignment $g$ into $X$ by $g(p)=\{x\in X:p\in\Gamma_{x}\}$, for each atom $p\in\mathsf{Var}$.

Step 5.

We now prove a ‘truth lemma’: that for every $\varphi\in{\mathcal{L}}^{\forall}_{[d]}$, we have $\varphi\in\Gamma_{x}$ iff $(X,g),x\models\varphi$ for each $x\in X$.

The proof is by induction on $\varphi$. For $\varphi\in\mathsf{Var}$ it holds by definition of $g$, and the boolean cases (including $\top$) follow from the fact that every $D_{x}$ is an ultrafilter.

For the remaining cases, assume the result for $\varphi$ inductively, and let $x\in X$ be given.

For the case $\forall\varphi$, if $\forall\varphi\in\Gamma_{x}$ then by $({\dagger})$, $\forall\varphi$ is true at some world of ${\mathcal{M}}$, so $\varphi$ is true at every world of ${\mathcal{M}}$. It follows from the definition of $\Gamma_{y}$ that $\varphi\in\Gamma_{y}$, and inductively that $(X,g),y\models\varphi$, for every $y\in X$. So $(X,g),x\models\forall\varphi$.

Conversely, suppose that $(X,g),x\models\forall\varphi$. Let $w\in W$ be given. Choose any $y\in\mathbb{B}(O_{w})$. Then $(X,g),y\models\varphi$, so inductively, $\varphi\in\Gamma_{y}$. By $({\ddagger})$ and because $\lambda(O_{w})=w$, we get ${\mathcal{M}},w\models\varphi$. As $w$ was arbitrary, we get ${\mathcal{M}},w\models\forall\varphi$ for every $w\in W$. It is now immediate from the definition of $\Gamma_{x}$ that $\forall\varphi\in\Gamma_{x}$.

Finally we consider the case $[d]\varphi$. Suppose first that $[d]\varphi\in\Gamma_{x}$. By $({\dagger})$, there is $\mathbb{G}\in{\mathcal{E}}(x)$ with ${\mathcal{M}},\lambda(\mathbb{G})\models[d]\varphi$. Then for every $y\in\mathbb{G}\setminus\mathbb{B}(\mathbb{G})$, the set $S=\{\mathbb{G}^{\prime}\in{\mathcal{E}}(y):\mathbb{G}^{\prime}\subsetneq\mathbb{G}\}$ is in $D_{y}$ by choice of $D_{y}$. Also, every $\mathbb{G}^{\prime}\in S$ satisfies $R(\lambda(\mathbb{G}),\lambda(\mathbb{G}^{\prime}))$ as $\lambda$ is a p-morphism (again we need transitivity of $R$ here), and so ${\mathcal{M}},\lambda(\mathbb{G}^{\prime})\models\varphi$ by Kripke semantics. So $\varphi\in\Gamma_{y}$ by definition of $\Gamma_{y}$, and inductively, $(X,g),y\models\varphi$, for every $y\in\mathbb{G}\setminus\mathbb{B}(\mathbb{G})$.

Now $x\in\mathbb{G}$. If $x\notin\mathbb{B}(\mathbb{G})$, then $\mathbb{G}\setminus\mathbb{B}(\mathbb{G})$ is already an open neighbourhood of $x$ all of whose elements satisfy $\varphi$. If $x\in\mathbb{B}(\mathbb{G})$, then recalling that $\mathbb{G}\cap{\langle d\rangle}\mathbb{B}(\mathbb{G})=\emptyset$, we can find an open neighbourhood $O$ of $x$ with $O\subseteq\mathbb{G}$ and $O\cap\mathbb{B}(\mathbb{G})=\{x\}$. By the above, $(X,g),y\models\varphi$ for every $y\in O\setminus\{x\}$. Either way, we have shown that $(X,g),x\models[d]\varphi$.

Conversely, suppose that $(X,g),x\models[d]\varphi$. So there is $\varepsilon>0$ such that $(X,g),y\models\varphi$ for every $y\in N_{\varepsilon}(x)\setminus\{x\}$. We show that $[d]\varphi\in\Gamma_{x}$.

Suppose first that ${\mathcal{E}}(x)$ is finite, with least element $\bigcap{\mathcal{E}}(x)=\mathbb{G}$, say. Then $x\in\mathbb{B}(\mathbb{G})$, so by $({\ddagger})$ it suffices to show ${\mathcal{M}},\lambda(\mathbb{G})\models[d]\varphi$. Accordingly, take any $w\in R(\lambda(\mathbb{G}))$. We show that ${\mathcal{M}},w\models\varphi$. Now

[TABLE]

And $x\notin\mathbb{B}(\mathbb{G}_{w})$ since $\mathbb{B}(\mathbb{G})$ is disjoint from $\mathbb{G}_{w}$. So there is $y\in\mathbb{B}(\mathbb{G}_{w})\cap N_{\varepsilon}(x)\setminus\{x\}$. For such a $y$ we have $(X,g),y\models\varphi$, so inductively, $\varphi\in\Gamma_{y}$, and by $({\ddagger})$ we obtain ${\mathcal{M}},w\models\varphi$ since $\lambda(\mathbb{G}_{w})=w$. We are done.

Now suppose instead that ${\mathcal{E}}(x)$ is infinite. Let

[TABLE]

a cofinite subset of ${\mathcal{E}}(x)$. Pick arbitrary $\mathbb{G}\in S$. We show that ${\mathcal{M}},\lambda(\mathbb{G})\models[d]\varphi$. Suppose $\mathbb{G}\in{\mathcal{G}}_{n}$. By choice of $\mathbb{B}(\mathbb{G})$ we have $d(x,\mathbb{B}(\mathbb{G}))<1/2^{n}<\varepsilon$. Now $x\notin\mathbb{B}(\mathbb{G})$ since ${\mathcal{E}}(x)$ is infinite. So there is $y\in\mathbb{B}(\mathbb{G})\cap N_{\varepsilon}(x)\setminus\{x\}$. Then $N_{\varepsilon}(x)\setminus\{x\}$ is an open neighbourhood of $y$, and every $z\in N_{\varepsilon}(x)\setminus\{x\}$ satisfies $(X,g),z\models\varphi$. So $(X,g),y\models[d]\varphi$. Since $y\in\mathbb{B}(\mathbb{G})$, ${\mathcal{E}}(y)$ is finite, so by the proof above we have ${\mathcal{M}},\lambda(\mathbb{G})\models[d]\varphi$ as required.

We have shown that each $\mathbb{G}\in S$ satisfies ${\mathcal{M}},\lambda(\mathbb{G})\models[d]\varphi$. Since $S$ is cofinite in ${\mathcal{E}}(x)$, it is certainly in $D_{x}$, and it follows by definition of $\Gamma_{x}$ that $[d]\varphi\in\Gamma_{x}$ as required.

Step 6.

Recall that ${\mathcal{M}},w_{0}\models\Sigma$. Take any $x\in\mathbb{B}(O_{w_{0}})$. By $({\ddagger})$, $\Sigma\subseteq\Gamma_{x}$, so by step 5 (the truth lemma) above, $(X,g),x\models\Sigma$. So $\Sigma$ is satisfiable in $X$.  $\Box$

COROLLARY 4.8

Let $X$ be a non-compact 0-dimensional dense-in-itself metric space. In the language ${\mathcal{L}}^{\forall}_{[d]}$, the system KD4U is sound and strongly complete over $X$. In the weaker language ${\mathcal{L}}^{\forall}_{\Box}$, the system S4U is sound and strongly complete over $X$.

• *Proof. *

S4U and KD4U are outlined in §1.2 and defined fully in, e.g., [11] and [12, §8.1]. As shown in the former (in particular by theorem 5.1, the argument of theorem 8.4, and the discussion following it), they are sound and complete over every 0-dimensional dense-in-itself metric space in their respective languages. The corollary now follows by theorem 4.7 and fact 2.1.  $\Box$

5 Cantor set

In the preceding section we proved strong completeness of the system KD4U in the language ${\mathcal{L}}^{\forall}_{[d]}$ over every non-compact 0-dimensional dense-in-itself metric space. Actually, this covers all 0-dimensional dense-in-themselves metric spaces except one — the Cantor set.

The Cantor set is, up to homeomorphism, the unique compact 0-dimensional dense-in-itself metric space (see [4] or [23, 29.5, 30.4]). As a topological space, it is the Stone space of the countable atomless boolean algebra (see [1, theorem 6.6 and text after corollary 7.7] or [14, example 7.24]).

In this section we show that, over the Cantor set, compactness fails for ${\mathcal{L}}_{[d]}^{\forall}$ — in surprising contrast to non-compact spaces — but holds for ${\mathcal{L}}^{\langle n\rangle}_{\Box}$. Compactness for the weaker languages ${\mathcal{L}}^{\forall}_{\Box}$ and ${\mathcal{L}}_{\Box}^{[\neq]}$ follows immediately, and here we also obtain strong completeness results. We have none for ${\mathcal{L}}^{\langle n\rangle}_{\Box}$ itself only because we do not know the logic of the Cantor set in this language.

5.1 Strong completeness fails with $[d],\forall$

We start by observing that the results for non-compact spaces of the preceding section cannot be replicated for the Cantor set.

THEOREM 5.1

Let $X$ be an infinite compact T1 topological space (such as the Cantor set). The language ${\mathcal{L}}_{[d]}^{\forall}$ is not compact over $X$. Hence, in ${\mathcal{L}}_{[d]}^{\forall}$ or any stronger language, no deductive system is sound and strongly complete over $X$.

• *Proof. *

We write down ${\mathcal{L}}_{[d]}^{\forall}$-formulas saying that the valuation of an atom is infinite but has empty derivative. Let $p_{0},p_{1},\ldots,q\in\mathsf{Var}$ be pairwise distinct, and let

[TABLE]

Any finite subset of $\Sigma$ is satisfiable in $X$: if the subset involves only $p_{0},\ldots{},p_{n},q$, choose pairwise distinct points $x_{0},\ldots{},x_{n}\in X$, assign each $p_{i}$ to $\{x_{i}\}$, and $q$ to $\{x_{0},\ldots{},x_{n}\}$. No point satisfies ${\langle d\rangle}q$, since in a T1 space, every finite set has empty derivative (and conversely).

Suppose for contradiction that $\Sigma$ as a whole were satisfiable in $(X,h)$ for some assignment $h$ into $X$. For each $i<\omega$ pick $x_{i}\in X$ with $(X,h),x_{i}\models q\wedge p_{i}\wedge\bigwedge_{j<i}\neg p_{j}$. The $x_{i}$ are plainly pairwise distinct, and hence $h(q)$ is infinite. Since $X$ is compact, by [6, 3.10.3] every infinite subset of $X$ has non-empty derivative. So there is $x\in{\langle d\rangle}h(q)$, and therefore $(X,h),x\models{\langle d\rangle}q$, contradicting the truth of $\forall\neg{\langle d\rangle}q$ in $(X,h)$.

So ${\mathcal{L}}_{[d]}^{\forall}$ is not compact over $X$, proving the first part of the theorem. The second part follows by fact 2.1.  $\Box$

The proof really needs ${\langle d\rangle}$: using $\forall\neg\Diamond q$ in $\Sigma$ instead loses finite satisfiability, since even $\{\exists q,\forall\neg\Diamond q\}$ is not satisfiable. In theorem 5.13 we will show that the result needs ${\langle d\rangle}$ too.

5.2 Compactness holds with $\Box,\langle n\rangle$ for $n<\omega$

Replacing $[d]$ by the weaker connective $\Box$, we have more success. In fact, we will prove compactness for ${\mathcal{L}}^{\langle n\rangle}_{\Box}$ over the Cantor set. Our proof uses a third kind of compactness — in first-order logic. Every consistent set of first-order sentences has a model.

5.2.1 Two-sorted first-order structures

To formulate topological models in first-order logic, we introduce a two-sorted first-order signature $L$. It has a ‘point’ sort and a ‘set’ sort, so $L$-structures have the form $M=(X,B)$, where $X$ is the set of elements of $M$ of point sort, and $B$ is the set of elements of set sort. The symbols of $L$ comprise a binary relation symbol $\in$ relating points to sets, ‘boolean’ function symbols $+$ (binary) and $-$ (unary), and constants $0,1$, all acting on the set sort, and a unary relation symbol $P$ of point sort for each $p\in\mathsf{Var}$. For convenience, we also include in $L$ a point-sorted constant $k$. As usual, we write $s^{M}$ for the interpretation of a symbol $s$ of $L$ in an $L$-structure $M$. We use $x,y,z,\ldots$ for point-sorted variables (and also by abuse for point-sorted elements), and $b,c,o,O,\ldots$ for set-sorted variables (and also by abuse for elements of set sort).

Given an $L$-structure $M=(X,B)$, for each $b\in B$ we let $\check{b}=\{x\in X:M\models x\in b\}\subseteq X$. It may be that $\check{b}=\check{c}$ for distinct $b,c\in B$, but this will not happen in our applications.

We can view a topological model as an $L$-structure as follows. Let $X$ be a 0-dimensional topological space and write ${\sf Clop}(X)$ for the set of all clopen subsets of $X$. This is a base for the topology on $X$, and $({\sf Clop}(X),\cup,{\sim},\emptyset,X)$ is a boolean set algebra. Let $h:\mathsf{Var}\to\wp(X)$ be an assignment. Then the topological model $(X,h)$ can be turned into a two-sorted $L$-structure $(X,h)^{(2)}=M$, say, where $M$ has the form $(X,{\sf Clop}(X))$, $\in$ is interpreted in $M$ as ordinary set membership, the boolean operations are interpreted as $b+c=b\cup c$, $-b=X\setminus b$, $0=\emptyset$, and $1=X$, the constant $k$ has arbitrary interpretation in $X$, and $P^{M}=h(p)$ for each $p\in\mathsf{Var}$. The structure $(X,h)^{(2)}$ is not unique: it depends on the interpretation of $k$. Each $b\in{\sf Clop}(X)$ is both a set-sorted element of $M$ and a set of point-sorted elements of $M$, and by definition of $\in^{M}$ we have $b=\check{b}\subseteq X$. So we often do not need to write $\check{b}$ when dealing with ‘concrete’ structures like this (the proof of lemma 5.4 is an example).

Conversely, given an $L$-structure $M=(X,B)$, we endow $X$ with the topology generated by $\check{B}=\{\check{b}:b\in B\}$. Define an assignment $h:\mathsf{Var}\to\wp(X)$ by $h(p)=P^{M}\subseteq X$ for each $p\in\mathsf{Var}$. We end up with a topological model $M^{(1)}=(X,h)$, where $X$ is the topological space just defined. Plainly, if $X$ is 0-dimensional then $((X,h)^{(2)})^{(1)}=(X,h)$ for any $h$.

5.2.2 Standard translation

Every ${\mathcal{L}}^{\langle n\rangle}_{\Box}$-formula $\varphi$ has a ‘standard translation’ to an $L$-formula $\varphi^{x}$, for any first-order variable $x$ of point sort. The translation $\varphi^{x}$ will have at most the variable $x$ free. We define $\varphi^{x}$ by induction on $\varphi$:

• •

$p^{x}=P(x)$ for $p\in\mathsf{Var}$

• •

$\top^{x}=\top$

• •

$(\neg\varphi)^{x}=\neg\varphi^{x}$, and $(\varphi\wedge\psi)^{x}=\varphi^{x}\wedge\psi^{x}$

• •

$(\Box\varphi)^{x}=\exists O(x\in O\wedge\forall y(y\in O\to\varphi^{y}))$

• •

(\langle n\rangle\varphi)^{x}=\mathop{\mathchoice{\vbox{\hbox{\huge\exists}}}{\vbox{\hbox{\large\exists}}}{\vbox{\hbox{\large\exists}}}{\vbox{\hbox{\scriptstyle\exists}}}}\displaylimits_{0\leq i\leq n}x_{i}(\bigwedge_{i<j\leq n}x_{i}\neq x_{j}\wedge\bigwedge_{i\leq n}\varphi^{x_{i}}), for $n<\omega$.

As one might expect, $\varphi^{x}$ generally ‘means the same’ as $\varphi$, as the following lemma shows. In the lemma and later, $M\models\varphi^{x}(a)$ means that $\varphi^{x}$ is true in $M$ when $x$ is assigned to $a$, and $\varphi^{x}(k/x)$ denotes the $L$-sentence obtained by substituting the constant $k$ for every free occurrence of $x$ in $\varphi^{x}$.

LEMMA 5.2

Let a topological model $(X,h)$ and an $L$-structure $M=(X,B)$ be given, and suppose that $\check{B}=\{\check{b}:b\in B\}$ is a base for the topology on $X$. Then for every $\varphi\in{\mathcal{L}}^{\langle n\rangle}_{\Box}$ and $a\in X$ we have $(X,h),a\models\varphi$ iff $M\models\varphi^{x}(a)$, and hence $(X,h),k^{M}\models\varphi$ iff $M\models\varphi^{x}(k/x)$.

• *Proof. *

[Proof (sketch)] The proof is by induction on $\varphi$. We consider only the case $\Box\varphi$, as the other cases are straightforward. Let $a\in X$. Then $(X,h),a\models\Box\varphi$ iff $a$ has an open neighbourhood $O$ with $(X,h),a^{\prime}\models\varphi$ for every $a^{\prime}\in O$. As $\check{B}$ is a base for the topology on $X$, and by the inductive hypothesis, this is iff there is $b\in B$ with $a\in\check{b}$ and $M\models\varphi^{x}(a^{\prime})$ for every $a^{\prime}\in\check{b}$. This is plainly iff $M\models(\Box\varphi)^{x}(a)$.  $\Box$

We will prove that ${\mathcal{L}}^{\langle n\rangle}_{\Box}$ is compact over the Cantor set using standard translations, which give us access to first-order compactness. Suppose that $\Sigma$ is a set of ${\mathcal{L}}^{\langle n\rangle}_{\Box}$-formulas that is finitely satisfiable over the Cantor set. It will follow that for a certain first-order theory $T$, the theory $T\cup\{\varphi^{x}(k/x):\varphi\in\Sigma\}$ is consistent, so by first-order compactness, it has a model. We will transform a countable model of it into a model of $\Sigma$ over the Cantor set. The ‘side theory’ $T$ allows us to do this. It will in fact be the theory $T_{good}$, defined next.

5.2.3 Good $L$-structures

For set-sorted terms $b,c$, we write $b\leq c$ to abbreviate the $L$-formula $b+c=c$, and for any ${\mathcal{L}}^{\langle n\rangle}_{\Box}$-formula $\varphi$, we write $b\subseteq[\![\varphi]\!]$ to abbreviate the $L$-formula $\forall x(x\in b\to\varphi^{x})$.

DEFINITION 5.3

An $L$-structure $M=(X,B)$ is said to be good if

$(B,+^{M},-^{M},0^{M},1^{M})$ is an atomless boolean algebra 2. 2.

$M\models\forall bcx([x\in b+c\leftrightarrow x\in b\vee x\in c]\wedge[x\in-b\leftrightarrow\neg(x\in b)])$ 3. 3.

$M\models\forall bc(\forall x(x\in b\leftrightarrow x\in c)\to b=c)$ 4. 4.

$M\models\forall xy(\forall b(x\in b\leftrightarrow y\in b)\to x=y)$ 5. 5.

\displaystyle M\models\forall b\Big{(}b\subseteq[\![\bigvee_{\psi\in\Psi}\Box\psi]\!]\to\mathop{\mathchoice{\vbox{\hbox{\huge\exists}}}{\vbox{\hbox{\large\exists}}}{\vbox{\hbox{\large\exists}}}{\vbox{\hbox{\scriptstyle\exists}}}}\displaylimits_{\psi\in\Psi}c_{\psi}\Big{(}(b\leq\sum_{\psi\in\Psi}c_{\psi})\wedge\bigwedge_{\psi\in\Psi}(c_{\psi}\subseteq[\![\Box\psi]\!])\Big{)}\Big{)},

for every non-empty finite set $\Psi$ of ${\mathcal{L}}^{\langle n\rangle}_{\Box}$-formulas.

Let $T_{good}$ be the first-order $L$-theory comprising first-order sentences expressing clause 1 and the $L$-sentences from clauses 2–5 above.

An $L$-structure $M$ is good iff $M\models T_{good}$. Let us give some examples of good and ‘bad’ $L$-structures. Good structures arise from topological models over the Cantor set, and more generally over any separable 0-dimensional dense-in-itself metric space:

LEMMA 5.4

Let $X$ be a separable 0-dimensional dense-in-itself metric space, let $(X,h)$ be any topological model over $X$, and let $M=(X,{\sf Clop}(X))=(X,h)^{(2)}$ be an $L$-structure derived from $(X,h)$ as described in §5.2.1. Then $M$ is good.

• *Proof. *

As $X$ is 0-dimensional and dense in itself, $({\sf Clop}(X),\cup,{\sim},\emptyset,X)$ is an atomless boolean algebra, and clauses 2–4 of definition 5.3 clearly hold for $M$.

We check clause 5. For a ${\mathcal{L}}^{\langle n\rangle}_{\Box}$-formula $\varphi$, write $[\![\varphi]\!]^{X}$ for $\{x\in X:(X,h),x\models\varphi\}$. Let $b\in{\sf Clop}(X)$ and let a non-empty finite set $\Psi$ of ${\mathcal{L}}^{\langle n\rangle}_{\Box}$-formulas be given, with $b\subseteq[\![\bigvee_{\psi\in\Psi}\Box\psi]\!]^{X}$.

Now we use some topology. As $X$ is a separable metric space, it is Lindelöf [6, 4.1.16]. As it is also 0-dimensional, by [6, 6.2.5, 6.2.7] the finite open cover $\{-b\}\cup\{[\![\Box\psi]\!]^{X}:\psi\in\Psi\}$ of $X$ can be refined to a cover consisting of pairwise disjoint open sets. Plainly, any union of these sets is clopen. So we can find clopen sets $c_{\psi}\in{\sf Clop}(X)$ with $c_{\psi}\subseteq[\![\Box\psi]\!]^{X}$ (for each $\psi\in\Psi$) such that $b\subseteq\bigcup_{\psi\in\Psi}c_{\psi}$.

Clause 5 now follows by clauses 1–3 and lemma 5.2, which applies since ${\sf Clop}(X)$ is a base for the topology on $X$. So $M$ is good.  $\Box$

EXAMPLE 5.5

An example of a bad $L$-structure is Q=(\mbox{\mathbb{Q}},B), where $\mathbb{Q}$ is the set of rational numbers, $B$ is the countable atomless boolean algebra consisting of finite unions of intervals of $\mathbb{Q}$ of the form $(x+\pi,y+\pi)$ (where $x<y$ in \mbox{\mathbb{Q}}\cup\{\pm\infty\}), $\in^{Q}$ is ordinary set membership, and for some atom $p\in L$ we have

[TABLE]

where $\mathbb{Z}$ denotes the set of integers. Under the standard metric $d(x,y)=|x-y|$, $\mathbb{Q}$ is a separable 0-dimensional dense-in-itself metric space, and $B$ is a base of clopen sets for its topology. However, $\mathbb{Q}$ has continuum-many clopen sets, and indeed $P^{Q}$ is clopen but is not in $B$. So B\subsetneq{\sf Clop}(\mbox{\mathbb{Q}}).

Now \mbox{\mathbb{Q}}\in B and \mbox{\mathbb{Q}}\subseteq[\![\Box p\vee\Box\neg p]\!]^{X}. But the sets $[\![\Box p]\!]^{X}$ and $[\![\Box\neg p]\!]^{X}$ (which are $P^{Q}$ and \mbox{\mathbb{Q}}\setminus P^{Q}, respectively) are disjoint. So for any $c,c^{\prime}\in B$, if \mbox{\mathbb{Q}}\subseteq c\cup c^{\prime}, $c\subseteq[\![\Box p]\!]^{X}$, and $c^{\prime}\subseteq[\![\Box\neg p]\!]^{X}$, then in fact $c=P^{Q}$, which is impossible since $P^{Q}\notin B$. So there are no such $c,c^{\prime}$, and clause 5 of definition 5.3 fails. (The other clauses are ok.)

5.2.4 Ultrafilter extensions of good structures

We now aim to construct an ‘ultrafilter extension’ of a good structure. In §5.2.5, we will show that for a countable good structure, this extension is homeomorphic to the Cantor set, and ‘truth-preserving’.

So until the end of §5.2.5, fix a good $L$-structure $M=(X,B)$. Then $(B,+^{M},-^{M},0^{M},1^{M})$ is an atomless boolean algebra, which we write henceforth simply as $B$. We write

[TABLE]

Each $\hat{x}$ is a (non-principal) ultrafilter of $B$. By clauses 2–3 of definition 5.3, the map $(b\mapsto\check{b})$ is a boolean embedding of $B$ into the boolean set algebra $(\wp(X),\cup,{\sim},\emptyset,X)$. We form the topological model $M^{(1)}=(X,h)$ as outlined in §5.2.1 above. Then $\check{B}=\{\check{b}:b\in B\}$ contains $X$ and is closed under finite intersections, and hence [23, 5.3] is a base for the topology on $X$. So lemma 5.2 applies to $M$ and $(X,h)$. We have $\check{B}\subseteq{\sf Clop}(X)$, but the inclusion may be proper (see example 5.5).

We will let $\varphi,\psi,$ etc., denote arbitrary ${\mathcal{L}}^{\langle n\rangle}_{\Box}$-formulas. We write $[\![\varphi]\!]^{X}=\{x\in X:(X,h),x\allowbreak\models\varphi\}$.

DEFINITION 5.6

Let $\mu$ be an ultrafilter of $B$. For a ${\mathcal{L}}^{\langle n\rangle}_{\Box}$-formula $\varphi$, we write

1. $\bullet$

$\mu\Vdash\Box\varphi$ if there is $b\in\mu$ such that $\check{b}\subseteq[\![\varphi]\!]^{X}$, 2. $\bullet$

$\mu\Vdash\Diamond\varphi$ if $\mu\not\Vdash\Box\neg\varphi$.

We define $F_{\mu}=\{\check{b}:b\in\mu\}\cup\{[\![\Diamond\psi]\!]^{X}:\mu\Vdash\Diamond\psi\}\cup\{\{x\}:x\in X,\;\mu=\hat{x}\}$. So $F_{\mu}\subseteq\wp(X)$.

LEMMA 5.7

For each ultrafilter $\mu$ of $B$, the set $F_{\mu}$ has the finite intersection property (i.e., $\bigcap S\neq\emptyset$ for every non-empty finite $S\subseteq F_{\mu}$).

• *Proof. *

Suppose first that $\mu=\hat{x}$ for some $x\in X$. Then $x$ is unique (by clause 4 of definition 5.3), $x\in\check{b}$ for every $b\in\mu$, and $x\in[\![\Diamond\psi]\!]^{X}$ for every $\psi$ with $\mu\Vdash\Diamond\psi$. So $x\in\bigcap F_{\mu}$ and we are done.

Now suppose that there is no such $x$, so $F_{\mu}=\{\check{b}:b\in\mu\}\cup\{[\![\Diamond\psi]\!]^{X}:\mu\Vdash\Diamond\psi\}$. As we said, lemma 5.2 applies to $M$ and $(X,h)$, so

[TABLE]

Assume for contradiction that there are $b\in\mu$ and ${\mathcal{L}}^{\langle n\rangle}_{\Box}$-formulas $\psi_{0},\ldots{},\psi_{n-1}$ with $\mu\Vdash\Diamond\psi_{i}$ for each $i<n$, such that $\check{b}\cap\bigcap_{i<n}[\![\Diamond\psi_{i}]\!]^{X}=\emptyset$. Hence, $n>0$ and $\check{b}\subseteq\bigcup_{i<n}[\![\Box\neg\psi_{i}]\!]^{X}$. Then (4) gives $M\models b\subseteq[\![\bigvee_{i<n}\Box\neg\psi_{i}]\!]$. Since $M$ is good, there are $c_{0},\ldots{},c_{n-1}\in B$ with $M\models c_{i}\subseteq[\![\Box\neg\psi_{i}]\!]$ for each $i<n$, and $M\models b\leq\sum_{i<n}c_{i}$. But $\mu$ is an ultrafilter containing $b$, so $c_{i}\in\mu$ for some $i<n$. Using (4) again, $\check{c}_{i}\subseteq[\![\Box\neg\psi_{i}]\!]^{X}\subseteq[\![\neg\psi_{i}]\!]^{X}$, so $\mu\Vdash\Box\neg\psi_{i}$, contradicting $\mu\Vdash\Diamond\psi_{i}$.  $\Box$

DEFINITION 5.8

For each ultrafilter $\mu$ of $B$, we choose an ultrafilter $\overline{\mu}$ on $X$ containing $F_{\mu}$. (By lemma 5.7 and the boolean prime ideal theorem, this is possible.) We then define

[TABLE]

LEMMA 5.9

Let $\mu$ be an ultrafilter of $B$. Then for all ${\mathcal{L}}^{\langle n\rangle}_{\Box}$-formulas $\varphi,\psi$, we have:

$\neg\varphi\in\Gamma_{\mu}$* iff $\varphi\notin\Gamma_{\mu}$.* 2. 2.

$\varphi\wedge\psi\in\Gamma_{\mu}$* iff $\{\varphi,\psi\}\subseteq\Gamma_{\mu}$.* 3. 3.

$\Box\varphi\in\Gamma_{\mu}$* iff $\mu\Vdash\Box\varphi$. Either condition implies $\varphi\in\Gamma_{\mu}$.* 4. 4.

If $\varphi\in\Gamma_{\mu}$ then $\mu\Vdash\Diamond\varphi$. 5. 5.

If $x\in X$ and $\mu=\hat{x}$, then $\varphi\in\Gamma_{\mu}$ iff $(X,h),x\models\varphi$.

• *Proof. *

1. 1, 2.

These hold since $\overline{\mu}$ is an ultrafilter on $X$. 2. 3.

If $\mu\Vdash\Box\varphi$ then there is $b\in\mu$ with $\check{b}\subseteq[\![\varphi]\!]^{X}$. But $\check{b}$ is open, so $\check{b}\subseteq\mathop{\rm int}[\![\varphi]\!]^{X}=[\![\Box\varphi]\!]^{X}$. As $\check{b}\in F_{\mu}\subseteq\overline{\mu}$, we have $[\![\Box\varphi]\!]^{X}\in\overline{\mu}$ as well, and so $\Box\varphi\in\Gamma_{\mu}$.

Conversely, if $\Box\varphi\in\Gamma_{\mu}$, then $[\![\Box\varphi]\!]^{X}\in\overline{\mu}$. Since $\overline{\mu}$ is an ultrafilter, $[\![\Diamond\neg\varphi]\!]^{X}\notin\overline{\mu}\supseteq F_{\mu}$. This means that $\mu\not\Vdash\Diamond\neg\varphi$, and hence clearly $\mu\Vdash\Box\varphi$.

In either case, $[\![\Box\varphi]\!]^{X}\in\overline{\mu}$. But $[\![\Box\varphi]\!]^{X}\subseteq[\![\varphi]\!]^{X}$. So also $[\![\varphi]\!]^{X}\in\overline{\mu}$, and $\varphi\in\Gamma_{\mu}$. 3. 4.

This follows from 3 and 1. 4. 5.

We have $\{x\}\in F_{\mu}\subseteq\overline{\mu}$. In this case, $\overline{\mu}$ is principal. So $\varphi\in\Gamma_{\mu}$ iff $[\![\varphi]\!]^{X}\in\overline{\mu}$, iff $x\in[\![\varphi]\!]^{X}$, iff $(X,h),x\models\varphi$.

$\Box$

5.2.5 Models over Cantor set from

countable good structures

We now further assume that the boolean algebra $B$ is countable. As $B$ is also atomless, its Stone space (of ultrafilters) is homeomorphic to the Cantor set $\mathbb{C}$ (as pointed out at the start of 5), and we will identify the two. So we take $\mathbb{C}$ to be the set of ultrafilters of $B$, and the clopen sets in $\mathbb{C}$ to be the sets of the form $\{\mu\in\mathbb{C}:b\in\mu\}$ for $b\in B$. These sets form a base for the topology on $\mathbb{C}$.

DEFINITION 5.10

Define an assignment $g:\mathsf{Var}\to\wp(\mathbb{C})$ by $g(p)=\{\mu\in\mathbb{C}:p\in\Gamma_{\mu}\}$, for each atom $p\in\mathsf{Var}$. Here, $\Gamma_{\mu}$ is as in definition 5.8.

LEMMA 5.11** (truth lemma)**

For every ${\mathcal{L}}^{\langle n\rangle}_{\Box}$-formula $\varphi$, we have

[TABLE]

• *Proof. *

The proof is by induction on $\varphi$. For $\varphi\in\mathsf{Var}$ it follows from the definition of $g$, and obviously $\top\in\Gamma_{\mu}$. The boolean cases $\neg\varphi$ and $\varphi\wedge\psi$ are easy, using lemma 5.9(1,2). For the remaining cases, assume the result for $\varphi$ inductively, and first consider $\Box\varphi$.

Let $\mu\in\mathbb{C}$ be given. If $\Box\varphi\in\Gamma_{\mu}$, then $\mu\Vdash\Box\varphi$ by lemma 5.9(3), so there is $b\in\mu$ such that $\check{b}\subseteq[\![\varphi]\!]^{X}$. So $\nu\Vdash\Box\varphi$ for every $\nu\in\mathbb{C}$ with $b\in\nu$ — $b$ itself witnesses this. So by lemma 5.9(3) again, $\varphi\in\Gamma_{\nu}$ for all such $\nu$. Inductively, $(\mathbb{C},g),\nu\models\varphi$ for all such $\nu$. The set of these $\nu$ is a clopen subset of $\mathbb{C}$ containing $\mu$, so by semantics, $(\mathbb{C},g),\mu\models\Box\varphi$.

Conversely, if $(\mathbb{C},g),\mu\models\Box\varphi$ then there is $b\in\mu$ with $(\mathbb{C},g),\nu\models\varphi$ for every $\nu\in\mathbb{C}$ containing $b$. Inductively, $\varphi\in\Gamma_{\nu}$ for all such $\nu$. In particular, for every $x\in\check{b}$, since $b\in\hat{x}$, we have $\varphi\in\Gamma_{\hat{x}}$. By lemma 5.9(5), $(X,h),x\models\varphi$ for all such $x$. So $\check{b}\subseteq[\![\varphi]\!]^{X}$, and thus $\mu\Vdash\Box\varphi$. By lemma 5.9(3), $\Box\varphi\in\Gamma_{\mu}$.

Finally, let $n<\omega$ and consider the case $\langle n\rangle\varphi$. Let $\mu\in\mathbb{C}$ be given. If $\langle n\rangle\varphi\in\Gamma_{\mu}$, then $[\![\langle n\rangle\varphi]\!]^{X}\in\overline{\mu}$, so certainly $\langle n\rangle\varphi$ is true at some point of $(X,h)$. So there are more than $n$ points $x\in X$ at which $(X,h),x\models\varphi$. For each such $x$ we have $\varphi\in\Gamma_{\hat{x}}$ by lemma 5.9(5), so $(\mathbb{C},g),\hat{x}\models\varphi$ by the inductive hypothesis. By clause 4 of definition 5.3, the $\hat{x}$ are pairwise distinct, so $(\mathbb{C},g),\mu\models\langle n\rangle\varphi$ by semantics.

Conversely suppose $(\mathbb{C},g),\mu\models\langle n\rangle\varphi$, so there are pairwise distinct $\mu_{0},\ldots{},\mu_{n}\in\mathbb{C}$ with $(\mathbb{C},g),\mu_{i}\models\varphi$, and hence inductively $\varphi\in\Gamma_{\mu_{i}}$, for each $i\leq n$. Using standard properties of ultrafilters, we can find elements $b_{i}\in\mu_{i}$ ($i\leq n$) such that $\check{b}_{0},\ldots{},\check{b}_{n}$ are pairwise disjoint. For each $i\leq n$, since $\varphi\in\Gamma_{\mu_{i}}$, by lemma 5.9(4) we have $\mu_{i}\Vdash\Diamond\varphi$. So since $b_{i}\in\mu_{i}$, there is $x_{i}\in\check{b}_{i}$ with $(X,h),x_{i}\models\varphi$. The $x_{i}$ are plainly pairwise distinct, so $\langle n\rangle\varphi$ is true in $(X,h)$ at every point. Then $[\![\langle n\rangle\varphi]\!]^{X}=X\in\overline{\mu}$, so $\langle n\rangle\varphi\in\Gamma_{\mu}$.  $\Box$

It follows that $(\mathbb{C},g)$ ‘extends’ $(X,h)$ in a truth-preserving way:

COROLLARY 5.12

$(X,h),x\models\varphi$* iff $(\mathbb{C},g),\hat{x}\models\varphi$, for every ${\mathcal{L}}^{\langle n\rangle}_{\Box}$-formula $\varphi$ and $x\in X$.*

• *Proof. *

By lemmas 5.9(5) and 5.11, $(X,h),x\models\varphi$ iff $\varphi\in\Gamma_{\hat{x}}$, iff $(\mathbb{C},g),\hat{x}\models\varphi$.  $\Box$

5.2.6 Compactness and strong completeness

We can now prove that ${\mathcal{L}}^{\langle n\rangle}_{\Box}$ is compact over the Cantor set.

THEOREM 5.13

Every set $\Sigma$ of ${\mathcal{L}}^{\langle n\rangle}_{\Box}$-formulas that is finitely satisfiable in the Cantor set $\mathbb{C}$ is satisfiable in $\mathbb{C}$.

• *Proof. *

Define $U=T_{good}\cup\{\varphi^{x}(k/x):\varphi\in\Sigma\}$.

Claim. $U$ is consistent.

**Proof of claim. **Let $\Sigma_{0}\subseteq\Sigma$ be finite. As $\Sigma$ is finitely satisfiable in $\mathbb{C}$, there are an assignment $h$ into $\mathbb{C}$, and a point $x\in\mathbb{C}$, with $(\mathbb{C},h),x\models\Sigma_{0}$. Let $M=(\mathbb{C},{\sf Clop}(\mathbb{C}))$ be an $L$-structure of the form $(\mathbb{C},h)^{(2)}$ as described in §5.2.1, in which the constant $k$ is interpreted as $x$. Then ${\sf Clop}(\mathbb{C})$ is a base for the topology on $\mathbb{C}$, so by lemma 5.2, $M\models\{\varphi^{x}(k/x):\varphi\in\Sigma_{0}\}$. Now $\mathbb{C}$ is a compact metric space, and hence is separable [6, 4.1.18]. So lemma 5.4 applies, and $M$ is good, giving $M\models T_{good}\cup\{\varphi^{x}(k/x):\varphi\in\Sigma_{0}\}$. Since $\Sigma_{0}$ was an arbitrary finite subset of $\Sigma$, this shows that $U$ is consistent and proves the claim.

So by first-order compactness and the downward Löwenheim–Skolem theorem, we can take a countable model $M=(X,B)\models U$ — that is, both $X$ and $B$ are countable. Then $M$ is good, since $M\models T_{good}$. We apply the preceding work to $M$. Define $(X,h)=M^{(1)}$, and $g:\mathsf{Var}\to\wp(\mathbb{C})$ as in definition 5.10. Since $M\models\varphi^{x}(k/x)$ for every $\varphi\in\Sigma$, and lemma 5.2 applies to $M$ and $(X,h)$, we obtain $(X,h),k^{M}\models\Sigma$. So by corollary 5.12, $(\mathbb{C},g),\widehat{k^{M}}\models\Sigma$ as required.  $\Box$

We can offer no strong completeness result for ${\mathcal{L}}^{\langle n\rangle}_{\Box}$ over the Cantor set $\mathbb{C}$, because as far as we know, the ${\mathcal{L}}^{\langle n\rangle}_{\Box}$-logic of $\mathbb{C}$ has not been determined or axiomatised. But the logic of $\mathbb{C}$ in the weaker language ${\mathcal{L}}_{\Box}^{[\neq]}$ has been axiomatised by [16], and this yields:

COROLLARY 5.14

In the language ${\mathcal{L}}_{\Box}^{[\neq]}$, the system S4DT1S defined in [16, §2] is sound and strongly complete over the Cantor set.

• *Proof. *

We work in the language ${\mathcal{L}}_{\Box}^{[\neq]}$. As we mentioned in §2.7, ${\mathcal{L}}_{\Box}^{[\neq]}$ is weaker than ${\mathcal{L}}^{\langle n\rangle}_{\Box}$, so by theorem 5.13 it is compact over $\mathbb{C}$. By [16, lemmas 6 & 8], S4DT1S is sound, and by [16, theorem 36], complete, over every 0-dimensional dense-in-itself metric space, including of course $\mathbb{C}$. Strong completeness of S4DT1S over $\mathbb{C}$ now follows by fact 2.1.  $\Box$

In the still weaker language ${\mathcal{L}}^{\forall}_{\Box}$, we can present a strong completeness result for all 0-dimensional dense-in-themselves metric spaces:

COROLLARY 5.15

In the language ${\mathcal{L}}^{\forall}_{\Box}$, the system S4U is sound and strongly complete over every 0-dimensional dense-in-itself metric space.

• *Proof. *

By corollary 4.8, S4U is strongly complete over every non-compact 0-dimensional dense-in-itself metric space. As we mentioned in the proof of the corollary, S4U is sound and complete over every 0-dimensional dense-in-itself metric space, including the Cantor set. So by theorem 5.13 and fact 2.1, it is strongly complete over the Cantor set too.  $\Box$

6 Conclusion

We now have some kind of picture of compactness and strong completeness over 0-dimensional dense-in-themselves metric spaces for languages able to express $\forall$. A summary is in table 2. Entries in the two ‘compact’ rows in the table indicate whether the designated language is compact (as defined in §2.9) over the relevant space. The bold entries imply the others in the same row. By fact 2.1, a ‘yes’ entry implies strong completeness, and a ‘no’ entry implies lack of it, for any logic named.

We now justify some of the statements in the table, make explicit the open questions arising from the gaps in the table, and list some further questions.

Most entries in the table follow from corollaries 4.8, 5.14, and 5.15, and theorems 5.1 and 5.13. We briefly discuss the penultimate column of the table. The key fact is:

FACT 6.1** ([17])**

The ${\mathcal{L}}^{[\neq]}_{[d]}$-logic of any separable 0-dimensional dense-in-itself metric space is DT1.

Briefly, DT1 can be axiomatised by the KD4 axioms for each of $[d]$ and $[\neq]$, plus $[\neq]\varphi\to\forall[d]\varphi$. As we saw in the proof of theorem 5.13, the Cantor set is separable, so by fact 6.1, its ${\mathcal{L}}^{[\neq]}_{[d]}$-logic is DT1; but strong completeness fails, by theorem 5.1. If fact 6.1 extends to non-separable spaces, the entry marked $(*)$ in the table, currently open, would also be DT1.

PROBLEM 6.2

Let $X$ be a non-compact 0-dimensional dense-in-itself metric space (not necessarily separable). Are the languages ${\mathcal{L}}^{[\neq]}_{\Box}$, ${\mathcal{L}}^{\langle n\rangle}_{\Box}$, ${\mathcal{L}}^{[\neq]}_{[d]}$, and ${\mathcal{L}}^{\langle n\rangle}_{[d]}$ compact over $X$? Axiomatise the logic of $X$ in these languages. (For ${\mathcal{L}}^{[\neq]}_{\Box}$ it is S4DT1S, as shown by [16]. For ${\mathcal{L}}^{[\neq]}_{[d]}$ and separable $X$ it is DT1, by fact 6.1). Are the logics the same for all $X$?

PROBLEM 6.3

Axiomatise the logic of the Cantor set in the languages ${\mathcal{L}}^{\langle n\rangle}_{\Box}$ and ${\mathcal{L}}^{\langle n\rangle}_{[d]}$.

The language ${\mathcal{L}}^{\langle n\rangle}_{[d]}$ is important. [8] proved that over T3 spaces it is equivalent to the monadic 2-sorted first-order language $L_{t}$ of [7]. This language can be thought of as the fragment of the language $L$ of §5.2.1 without the boolean function symbols that is invariant under change of base (in $L$-structures where the set sort is a base for the topology on the point sort). [8] also gave an axiomatisation of ${\mathcal{L}}^{\langle n\rangle}_{[d]}$ that is sound and complete over every class of T1 spaces that contains all T3 spaces. This may be relevant to problems 6.2 and 6.3.

0-dimensional spaces are often the easiest to handle. Going beyond them, what about arbitrary dense-in-themselves metric spaces? Or arbitrary metric spaces? We can ask about the logic of such spaces, and strong completeness, in each of the languages we have considered. For the language ${\mathcal{L}}_{\Box}$, the logic of every metric space was determined by [2], and it seems reasonable to ask about corresponding strong completeness results. We can even go beyond metric spaces and ask for results on non-metrisable topological spaces. And what about uncountable sets of formulas (when $\mathsf{Var}$ is allowed to be uncountable)? This is not much explored. Finally, where compactness fails, can we find novel strongly complete deductive systems using infinitary inference rules?