2. Background

In this section, we review the syntax and semantics of the topological $\mu$ -calculus. Following Baltag et al. (Reference Baltag, Bezhanishvili and Fernández-Duque2021) and Fernández-Duque and Iliev (Reference Fernández-Duque and Iliev2018), we present our semantics in the general setting of derivative spaces and work in a language with $\nu$ (rather than $\mu$ ) as primitive.

Definition 1. We fix a countable set $\mathsf{Prop}$ of atomic propositions (also called variables). The language $\mathcal L_{\mu}$ of the modal $\mu$ -calculus is defined by the following grammar:

\[\varphi : : = p \mid \neg \varphi \mid \varphi \land \varphi \mid \lozenge \varphi \mid \nu p.\varphi\]

where $p \in \mathsf{Prop}$ and in the construct $\nu p.\varphi$ , the formula $\varphi$ is positive in p, that is, every occurrence of p lies under the scope of an even number of negations. The abbreviations $\varphi \lor \psi$ , $\varphi \rightarrow \psi$ , $\varphi \leftrightarrow \psi$ , $\square \varphi$ , $\bot,$ and $\top$ are defined as usual. We also assume that every formula $\varphi$ is clean, that is, no bound variable is also a free variable, and for every variable p there is at most one subformula of $\varphi$ of the form $\nu p.\psi$ . We denote by $\varphi[{\psi_1,\dots,\psi_n}/p_1,\dots,p_n]$ the formula $\varphi$ where each formula $\psi_i$ is substituted for every free occurrence of the variable $p_i$ . Some implicit renaming may be carried out to ensure that the resulting formula is clean. We then introduce the abbreviation $\mu p.\varphi : = \neg \nu p.\neg \varphi[{\neg p}/p]$ . Finally, the basic modal language $\mathcal L_{\lozenge}$ is the fragment of $\mathcal L_{\mu}$ without occurrences of $\nu$ .

In modal logic, it is customary to study morphisms that preserve validity. In the context of derivative spaces, these are known as d-morphisms – see, e.g., Kudinov and Shehtman (Reference Kudinov and Shehtman2014).

Presenting our semantics in terms of derivative spaces is useful, as both weakly transitive Kripke frames and topological spaces (either with the closure or the d operator) can be viewed as special cases of derivative spaces. While our “intended” semantics is topological, Kripke semantics will be useful in establishing many of our main results.

Useful will be the notion of path. Recall that $\omega$ denotes the smallest infinite ordinal.

Now we turn our attention to the “official” semantics of the topological $\mu$ -calculus.

Given a topological space X, it is easily observed that the pair $(X,\mathrm{d})$ is a derivative space. Conversely, the topology $\tau$ can be recovered from d since for all $A \subseteq X$ , the set A is closed if and only if $\mathrm{d}{(A)}\subseteq A$ . For this reason, we choose, again, to identify $(X,\tau)$ and $(X,\mathrm{d})$ . Then, (pointed) derivative models based on topological spaces will be called (pointed) topological models. Observe that the familiar closure and interior operators can be defined by $\mathrm{Cl}{(A)}: = A \cup \mathrm{d}{(A)}$ and $\mathrm{Int}{(A)}: = A \cap \widehat{\mathrm{d}}{(A)}$ . Writing $\square^+ \varphi : = \varphi \land \square \varphi$ and $\lozenge^+ \varphi : = \varphi \lor \lozenge \varphi$ , we then have $[\![ \square^+ \varphi]\!]_{\mathfrak M} = \mathrm{Int}{([\![ \varphi]\!]_{\mathfrak M})}$ and $[\![ \lozenge^+ \varphi]\!]_{\mathfrak M} = \mathrm{Cl}{([\![ \varphi]\!]_{\mathfrak M})}$ for all topological models $\mathfrak M$ . We recall some important classes of topological spaces that will be useful throughout the text.

Aleksandroff spaces are closely connected to Kripke frames, via the following construction.

It is not hard to check that a space of the form $(W,\tau_R)$ is always Aleksandroff – and, indeed, every Aleksandroff space is of this form, see Aleksandroff (Reference Aleksandroff1937). In fact, we will simply not distinguish a weakly transitive Kripke frame from the topological space induced by it. This is partly motivated by the following proposition.

Proposition 13. Let $\mathfrak M = (W,R,V)$ be an irreflexive and weakly transitive Kripke model, and let $\mathfrak M' : = ((W,\tau_{R}),V)$ be the space induced by it. For all $w \in W$ and $\varphi \in \mathcal L_{\mu,}$ we have

\[\mathfrak M,w \vDash \varphi \iff \mathfrak M',w \vDash \varphi.\]

The modal logic of all topological spaces is known as $\mathbf{wK4}$ and consists of the following inference rules and axioms:

Note that this axiomatization differs from the usual presentation, as it is adapted to a language where $\lozenge$ (instead of $\square$ ) is taken as primitive. The axiomatic system $\mathbf{K4}$ is the extension of $\mathbf{wK4}$ with the axiom $\mathsf 4 : = \lozenge p \rightarrow \lozenge \lozenge p$ . The axiomatic system $\mathbf{\mu wK4}$ is the extension of $\mathbf{wK4}$ with the fixed point axiom $\nu p.\varphi \rightarrow \varphi[{\nu p.\varphi}/p]$ and the induction rule:

\[\text{from } \varphi \rightarrow \psi[\varphi/p] \text{ infer } \varphi \rightarrow \nu p.\psi.\]

In order to compare the expressivity of different languages, we need to introduce the notion of definable classes.

In particular, a $\mathcal L_{\lozenge}$ -definable class will be called modally definable, and a $\mathcal L_{\mu}$ -definable class will be called $\mu$ -definable. As discussed in Footnote 2, this notion of expressivity is also known as reducibility or axiomatic expressivity. The choice to compare expressivity relatively to a class of derivative spaces is convenient as it allows to derive all kinds of auxiliary results. We will consider the following classes of interest:

\begin{align*} \mathcal C_{\mathsf{all}} & : = & \{\mathcal X \mid \mathcal X \text{ is a derivative space}\} \\ \mathcal C_{\mathsf{fin}} & : = & \{(X,\mathrm{d}) \in \mathcal C_{\mathsf{all}} \mid X \text{ is finite}\} \\ \mathcal C_{\mathsf{Kripke}} & : = & \{\mathfrak F \mid \mathfrak F \text{ is a } \mathbf{wK4} \text{ frame}\} \\ \mathcal C_{\mathsf{irrefl}} & : = & \{\mathfrak F \in \mathcal C_{\mathsf{Kripke}} \mid \mathfrak F \text{ is irreflexive}\} \\ \mathcal C_{\mathsf{topo}} & : = & \{X \mid X \text{ is a topological space}\} \\ \mathcal C_{\mathbf{K4}} & : = & \{\mathcal X \in \mathcal C_{\mathsf{all}} \mid \mathcal X \vDash \mathbf{K4}\}\end{align*}

It is well established that $\mathcal C_{\mathsf{Kripke}} \cap \mathcal C_{\mathbf{K4}}$ is the class of transitive Kripke frames – see Blackburn et al. (Reference Blackburn, de Rijke and Venema2001), while $\mathcal C_{\mathsf{topo}} \cap \mathcal C_{\mathbf{K4}}$ is the class of $T_d$ spaces – see van Benthem and Bezhanishvili (Reference van Benthem and Bezhanishvili2007).

3. Classes Defined by Least Fixed Points

Our primary goal is to prove that the $\mu$ -calculus is more axiomatically expressive than basic modal logic; however, as we will see in this section, least (as opposed to greatest) fixed points alone do not yield additional expressive power. Of course, least and greatest fixed points are interdefinable using negation, but this is not the case for formulas expressed in negation normal form (or NNF for short), defined by the following grammar:

\[\varphi : : = p \mid \neg p \mid \varphi \land \varphi \mid \varphi \lor \varphi \mid \square \varphi \mid \lozenge \varphi \mid \nu p.\varphi \mid \mu p.\varphi\]

It is well known that for every formula in $\mathcal L_{\mu}$ , there is an equivalent formula in NNF. Then, when omitting the $\mu$ operator in the above grammar, one obtain the $\mu$ -free language $\mathcal L_\mu^0$ .

We are thus going to show that the full language does not define more classes of spaces than the $\mu$ -free language. In other words, one can recover all the axioms of the $\mu$ -calculus (up to equivalence) by enumerating only the $\mu$ -free formulas. This result is not only interesting in itself: by providing a simpler syntactic form for axioms, it will simplify the process of finding one that is not reducible to a basic modal axiom.

We recall that the extension of $\mu p.\varphi$ in a derivative model $\mathfrak M = (X,\mathrm{d},V)$ is defined as

\[[\![ \mu p.\varphi]\!]_{\mathfrak M} : = \bigcap \{A \subseteq X \mid [\![ \varphi]\!]_{\mathfrak M[p : = A] } \subseteq A\}.\]

So, given $x \in X$ , we have

\[\mathfrak M,x \vDash \mu p.\varphi \text{ iff } \forall A \subseteq X, ([\![ \varphi]\!]_{\mathfrak M[p : = A] } \subseteq A) \implies x \in A.\]

We can then observe that the universal quantification over the subsets of X is, implicitly, nothing more than a quantification over the possible valuations of p – and this is precisely the kind of quantification that validity of formulas is able to capture. As a result, one can rewrite axioms in a way that rids them of their least fixed points. Here, the textbook example would be the formula $\mu p.\square p$ , which defines the same class of spaces as the well-known Löb axiom $\square(\square p \rightarrow p) \rightarrow \square p$ – see van Benthem (Reference van Benthem2006). Drawing inspiration from this result, we arrive at a uniform translation $\mathsf{tr}:\mathcal L_{\mu} \rightarrow \mathcal L_\mu^0$ , defined by induction as follows:

1. • ,

2. • ,

3. • ,

4. • ,

5. • ,

6. • ,

7. • ,

8. • .

Recall that formulas of the $\mu$ -calculus are assumed to be clean, so each formula of the form $\nu p.\varphi$ or $\mu p.\varphi$ comes with its own variable p. Our goal is then to prove that . One direction is obtained by a stronger claim.

Now assume that $\mathfrak M,w \vDash \mu p.\varphi$ and . Since $\mathfrak M$ is rooted in w, this implies . By the induction hypothesis, we also have , and thus $[\![ \varphi]\!]_{\mathfrak M} \subseteq [\![ p]\!]_{\mathfrak M}$ . If we set $A : = [\![ p]\!]_{\mathfrak M}$ , we obtain $[\![ \varphi]\!]_{\mathfrak M[p : = A] } = [\![ \varphi]\!]_{\mathfrak M} \subseteq A$ , and thus $[\![ \mu p.\varphi]\!]_{\mathfrak M} \subseteq A$ . Since $\mathfrak M,w \vDash \mu p.\varphi$ , it follows that $w \in A$ , i.e., $\mathfrak M,w \vDash p$ . Therefore, , as desired.

For the other direction, we will need to transform a model of into a model of $\varphi$ . This is obtained by tweaking a valuation in a way that makes any formula of the form $\mu p.\psi$ coextensive with p.

Note that $\mathfrak M^{\varphi}$ is well-defined precisely because the formula $\varphi$ is clean.

Proof. By induction on $\varphi$ . Again, this is straightforward for Boolean and modal formulas. Suppose that . Then, there exists $A \subseteq W$ such that . By the induction hypothesis, we have

and by construction we also have $\mathfrak M^{\nu p.\varphi}[p : = A] = \mathfrak M[p : = A] ^{\varphi}$ . It follows that $A \subseteq [\![ \varphi]\!]_{\mathfrak M[p : = A] }$ , and therefore $\mathfrak M^{\nu p.\varphi},w \vDash \nu p.\varphi$ .

Now suppose that . We write $A : = [\![ \mu p.\varphi]\!]_{\mathfrak M}$ and then the fixed point equation gives $A = [\![ \varphi]\!]_{\mathfrak M[p : = A] }$ . By the induction hypothesis, we also have , and $\mathfrak M[p : = A] ^{\varphi} = \mathfrak M^{\mu p.\varphi}$ by construction, so

Hence, , and in particular . By assumption, it follows that $\mathfrak M^{\mu p.\varphi},w \vDash p$ . Therefore, $\mathfrak M,w \vDash \mu p.\varphi$ .

We can now conclude with the desired result.

As an immediate consequence, we obtain for all $\varphi \in \mathcal L_{\mu}$ , and this yields the following result.

4. Classes Defined by Greatest Fixed Points

The goal of this section is to exhibit $\mu$ -definable classes that are not modally definable. Thanks to the previous section, we know that we can restrict our attention to formulas without least fixed points. It turns out that a large family of axioms of the form $\theta \lor \nu p.\lozenge p$ will yield the desired result. We easily see that given a pointed Kripke model $(\mathfrak M,w)$ , we have $\mathfrak M,x \vDash \nu p.\lozenge p$ if and only if there exists an infinite path beginning on w. Topologically, $\nu p.\lozenge p$ holds in the perfect core of X, the largest dense-in-itself subset of X. While the existence of an infinite path is not in general modally definable, it is not hard to check that $\mathcal C(\nu p.\lozenge p) = \mathcal C(\lozenge\top)$ , as this is just the class of dense-in-themselves spaces. However, the story becomes more complicated if we only require certain points in the space to satisfy $\nu p.\lozenge p$ . In this case, the following can be applied to exhibit many modally undefinable classes of spaces.

Then, $\mathcal C( \theta \lor \nu p.\lozenge p)$ is not modally definable within $\mathcal C_{\mathsf{irrefl}} \cap \mathcal C_{\mathbf{K4}}$ . If in addition every $\mathfrak F_n$ is finite, then $\mathcal C( \theta \lor \nu p.\lozenge p)$ is not modally definable within $\mathcal C_{\mathsf{irrefl}} \cap \mathcal C_{\mathsf{fin}}$ and $\mathcal C_{\mathsf{Kripke}} \cap \mathcal C_{\mathsf{fin}} \cap \mathcal C_{\mathbf{K4}}$ .

From now on, we fix a formula $\theta$ and a family of frames $(\mathfrak F_n)_{n \in \mathbb N}$ satisfying the assumptions of Theorem 22. For all $n \in \mathbb N$ , we assume that $W_n \cap \omega = \varnothing$ . We start with an elementary observation.

Given a world $w \in W_n$ , we define the $\mathbf{wK4}$ frames $\mathfrak F_{n,w}^{\mathsf{point}} = (W^0,R^0)$ , $\mathfrak F_{n, w}^{\mathsf{cycle}} = (W^1,R^1)$ and $\mathfrak F_{n,w}^{\mathsf{spine}} = (W^2,R^2)$ by:

In words, $\mathfrak F_{n,w}^{\mathsf{point}}$ is the frame $\mathfrak F_n$ endowed with a reflexive point reachable from the root, and which sees all the successors of w (as well as w itself). The frames $\mathfrak F_{n, w}^{\mathsf{cycle}}$ and $\mathfrak F_{n,w}^{\mathsf{spine}}$ are constructed similarly but with respectively a two-element loop and an infinite branch, instead of a reflexive point. The three frames are depicted in Fig. 1.

Figure 1.

The frames $\mathfrak F_{n,w}^{\mathsf{point}}$ , $\mathfrak F_{n, w,}^{\mathsf{cycle}}$ and $\mathfrak F_{n,w}^{\mathsf{spine}}$ .

If some modal formula $\psi$ defines the same class of spaces as $\theta \lor \nu p.\lozenge p$ , then by construction $\psi$ should be refuted at $(\mathfrak F_n,r_n)$ for all n but not at $(\mathfrak F_{n,w}^{\mathsf{spine}},r_n)$ or $(\mathfrak F_{n,w}^{\mathsf{cycle}},r_n)$ or $(\mathfrak F_{n,w}^{\mathsf{point}},r_n)$ , since in all three of them there is an infinite path beginning on the root. Yet we will prove that if n is big enough and $\neg \psi$ is satisfiable on $(\mathfrak F_n,r_n)$ , then it is also satisfiable on $(\mathfrak F_{n,w}^{\mathsf{point}},r_n)$ for some w, leading to a contradiction.^{Footnote 3} The proof is rather technical, but we can sketch the main lines of our strategy. First, it is clear that transferring the satisfiability of a diamond formula (i.e., of the form $\lozenge \varphi)$ or a Boolean formula from $(\mathfrak F_n,r_n)$ to $(\mathfrak F_{n,w}^{\mathsf{point}},r_n)$ is immediate, so the challenge really comes from box formulas (of the form $\square \varphi$ ). The central argument is that since n may be arbitrarily large, we can select some $\mathfrak F_n$ with an arbitrarily long path. By means of a pigeonhole argument, we will then manage to show that on some point w of this path, if $\square \varphi$ is satisfied, then so is $ \square^+ \varphi$ (when $\square \varphi$ is any subformula of $\neg \psi$ ). Then, transferring the truth of $\square \varphi$ to the reflexive point of $\mathfrak F_{n,w}^{\mathsf{point}}$ will be straightforward. First, we will need a notion of type of a possible world.

As explained above, the following result allows to transfer the satisfiability of box formulas, as soon as the parameter n is large enough.

Proof. First, we know that $\mathfrak F_n$ contains a path $(w_i)_{i \in [1, n]}$ of size n. By construction, there are $2^{|\varphi|_{\mathsf{\square}}}$ different box types relative to $\varphi$ . Thus, by the pigeonhole principle, there exists $i,j \in \mathbb N$ such that $1 \leq i < j \leq n$ and $t_{\mathfrak M}^{\varphi}(w_i) = t_{\mathfrak M}^{\varphi}(w_j)$ . We then define a valuation V’ over $\mathfrak F_{n,w_j}^{\mathsf{point}}$ by setting, for all $p \in \mathsf{Prop}$ :

\[V'(p) : = \begin{cases} V(p) \cup \{0\} & \text{if } w_j \in V(p) \\ V(p) & \text{otherwise} \end{cases}.\]

So V and V’ coincide over $\mathfrak F_n$ , and V’ is defined over 0 so that this point satisfies the same atomic propositions as $w_j$ . We then prove by induction on $\psi \trianglelefteq \varphi$ that $\mathfrak F_n,V,w_j \vDash \psi$ implies $\mathfrak F_{n, w_j}^{\mathsf{point}},V', 0 \vDash \psi$ :

1. • If $\psi$ is of the form $\psi = p$ or $\psi = \neg p$ with $p \in \mathsf{Prop}$ this is just true by construction.

2. • If $\psi$ is of the form $\psi = \psi_1 \land \psi_2$ , then $\mathfrak F_n,V,w_j \vDash \psi_1 \land \psi_2$ implies $\mathfrak F_n,V,w_j \vDash \psi_1$ and $\mathfrak F_n,V,w_j \vDash \psi_2$ and it suffices to apply the induction hypothesis. If $\psi$ is of the form $\psi = \psi_1 \lor \psi_2$ , then $\mathfrak F_n,V,w_j \vDash \psi_1 \lor \psi_2$ implies $\mathfrak F_n,V,w_j \vDash \psi_1$ or $\mathfrak F_n,V,w_j \vDash \psi_2$ and the result follows in the same way.

3. • Suppose that $\psi$ is of the form $\psi = \lozenge \psi_0$ and $\mathfrak F_n,V,w_j \vDash \psi$ . Then since V and V’ coincide over $\mathfrak F_n$ , we have $\mathfrak F_{n, w_j}^{\mathsf{point}},V',w_j \vDash \psi$ as well. By transitivity, it follows that $\mathfrak F_{n, w_j}^{\mathsf{point}},V',0 \vDash \psi$ .

4. • Suppose that $\psi$ is of the form $\psi = \square \psi_0$ and that $\mathfrak F_n,V,w_j \vDash \psi$ . Then since $t_{\mathfrak M}^{\varphi}(w_i) = t_{\mathfrak M}^{\varphi}(w_j)$ , we have $\mathfrak F_n,V,w_i \vDash \psi$ as well. Since $w_i R_n w_j$ it follows $\mathfrak F_n, V,w_j \vDash \psi_0$ , and then $\mathfrak F_{n, w_j}^{\mathsf{point}},V',0 \vDash \psi_0$ by the induction hypothesis. Since V and V’ coincide over $\mathfrak F_n,$ we also have $\mathfrak F_{n, w_j}^{\mathsf{point}},V',w_j \vDash \square^+ \psi_0$ . All in all, we obtain $\mathfrak F_{n, w_j}^{\mathsf{point}},V',0 \vDash \square \psi_0$ as desired.

Now observe that since $w_i R_n w_j$ we must have $w_j \neq r_n$ ; otherwise, we would obtain $r_n R_n r_n$ by transitivity, contradicting Claim 25. Thus, $r_n R_n w_j$ , and from $\mathfrak F_n,V,r_n \vDash \square \varphi$ we obtain $\mathfrak F_n,V,w_j \vDash \varphi$ , whence $\mathfrak F_{n, w_j}^{\mathsf{point}},V',0 \vDash \varphi$ . Since V and V’ coincide over $\mathfrak F_n$ , we conclude that $\mathfrak F_{n, w_j}^{\mathsf{point}},V',r_n \vDash \square \varphi$ .

We can then extend the result to any modal formula.

Proof. Applying the theorem of disjunctive normal form for propositional logic, and using the fact that $\square$ and $\land$ commute, we can assume that $\varphi$ is of the form $\varphi = \bigvee_{i=1}^m \sigma_i$ with

\[\sigma_i = \rho_i \land \square \psi_i \land \bigwedge_{j=1}^{m_i} \lozenge \theta_{i,j}\]

for all $i \in [1, m]$ , where $\rho_i$ is a propositional formula. Note that since $\square \top$ is a tautology, we can always assume the presence of $\square \psi_i$ . We also suppose that $\psi_i$ is presented in NNF. We then define

\[n : = 1 + \mathrm{max}\ \{2^{|\psi_i|_{\mathsf{\square}}} \mid 1 \leq i \leq m\}\]

and assume that there exists a valuation V such that $\mathfrak F_n,V,r_n \vDash \varphi$ . Then there exists $i \in [1, m]$ such that $\mathfrak F_n,V,r_n \vDash \sigma_i$ . It follows that $\mathfrak F_n,V,r_n \vDash \square \psi_i$ with $n > 2^{|\psi_i|_{\mathsf{\square}}}$ , so by Claim 27 there exists $w \in W_n$ and a valuation V’ over $\mathfrak F_{n,w}^{\mathsf{point}}$ such that $\mathfrak F_{n,w}^{\mathsf{point}},V',r_n \vDash \square \psi_i$ , and V and V’ coincide over $\mathfrak F_n$ . It is then clear that $\mathfrak F_{n,w}^{\mathsf{point}},V',r_n \vDash \sigma_i$ , and thus $\mathfrak F_{n,w}^{\mathsf{point}},V',r_n \vDash \varphi$ .

This proves that $\varphi$ is satisfiable on $\mathfrak F_{n,w}^{\mathsf{point}}$ . Now consider the function $f:W_1 \rightarrow W_0$ defined by $f(0) : = f(1) : = 0$ and $f(w) : = w$ for all $w \in W_n$ . Likewise, we define a function $g:W_2 \rightarrow W_0$ by $g(n) : = 0$ for all $n \in \omega$ , and $g(w) : = w$ for all $w \in W_n$ . Then, f defines a bounded morphism from $\mathfrak F_{n,w}^{\mathsf{cycle}}$ to $\mathfrak F_{n,w}^{\mathsf{point}}$ , and g defines a bounded morphism from $\mathfrak F_{n,w}^{\mathsf{spine}}$ to $\mathfrak F_{n,w}^{\mathsf{point}}$ . It follows that $\varphi$ is satisfiable on $\mathfrak F_{n,w}^{\mathsf{spine}}$ and $\mathfrak F_{n,w}^{\mathsf{cycle}}$ .

We are now ready to prove Theorem 22:

Thus, $\neg \psi$ is satisfiable on $(\mathfrak F_n,v)$ for some $v \in W_n$ . If $v \neq r_n$ , we denote by $\mathfrak F$ the subframe of $\mathfrak F_n$ generated by v. Then, $\mathfrak F$ does not contain $r_n$ ; otherwise, we would have $v R_n r_n R_n v$ and thus $v R_n v$ , a contradiction. The assumption on $\mathfrak F_n$ yields $\mathfrak F \vDash \theta$ , so $\mathfrak F \vDash \theta \lor \nu p.\lozenge p$ and thus $\mathfrak F \vDash \psi$ . Therefore, $\mathfrak F_n,v \vDash \psi$ , a contradiction. Hence, we have $r_n = v$ . Then, by Claim 28, there exists $w \in W_n$ such that $\neg \psi$ is satisfiable on $\mathfrak F_{n,w}^{\mathsf{spine}}$ . Yet $\mathfrak F_{n,w}^{\mathsf{spine}} \in \mathcal C_{\mathsf{irrefl}} \cap \mathcal C_{\mathbf{K4}}$ and $\mathfrak F_{n,w}^{\mathsf{spine}} \vDash \theta \lor \nu p.\lozenge p$ , so $\mathfrak F_{n,w}^{\mathsf{spine}} \vDash \psi$ , a contradiction.

Now suppose that every $\mathfrak F_n$ is finite. By the same reasoning, we can show that $\mathcal C(\theta \lor \nu p.\lozenge p)$ is not modally definable within $\mathcal C_{\mathsf{irrefl}} \cap \mathcal C_{\mathsf{fin}}$ and $\mathcal C_{\mathsf{Kripke}} \cap \mathcal C_{\mathsf{fin}} \cap \mathcal C_{\mathbf{K4}}$ . To that end, it suffices to replace $\mathfrak F_{n,w}^{\mathsf{spine}}$ by, respectively, $\mathfrak F_{n,w}^{\mathsf{cycle}}$ , which is irreflexive and finite, and $\mathfrak F_{n,w}^{\mathsf{point}}$ , which is transitive and finite.

Theorem 22 remains a very general statement, and it is worth instantiating it with examples. The following result shows the existence of infinitely many non-modally definable classes of spaces.

Consider, for all $n \in \mathbb N$ , the frame $\mathfrak F_n^m : = (W_n^m,R_n^m)$ depicted in Fig. 2. We can see that the $\mathfrak F_n^m$ ’s fulfill all the conditions of Theorem 22, so we are done (see Remark 24 for why the result applies to topological spaces). Finally, if $1 \leq m < k$ we can see that $\mathfrak F_1^{m-1} \vDash \mathsf{IP}\mathsf{.2}_{m}^{+}$ whereas $\mathfrak F_1^{m-1} \nvDash \mathsf{IP}\mathsf{.2}_{k}^+$ , and this proves that $\mathbf{\mu wK4} + \mathsf{IP}\mathsf{.2}_{m}^{+} \neq \mathbf{\mu wK4} + \mathsf{IP}\mathsf{.2}_{k}^+$ .

Figure 2.

The fork-like frame $\mathfrak F_n^m$ .

In Section 6, we will analyze these axioms further to see that they are well-behaved, but we find it appropriate to end this section by presenting an intuitive topological interpretation of the axiom $\mathsf{IP}\mathsf{.2}_{0}^+$ , which reduces to $.\mathsf{2}^+ \lor \nu p.\lozenge p$ . Given a formula $\theta$ and a space X, we say that X is $\theta$ -imperfect if there exist two disjoint subspaces Y and Z of X such that $X = Y \cup Z$ , $Y \vDash \theta$ and Z is dense-in-itself.

From right to left, suppose that such a decomposition $X = Y \cup Z$ exists. Let $x \in X$ and V be a valuation over X. Suppose that $x \in Z$ . Since Z is dense-in-itself, we have $Z \subseteq \mathrm{d}(Z)= [\![ \lozenge p]\!]_{X,V[p: = Z]}$ so $Z \subseteq [\![ \nu p.\lozenge p]\!]_{X,V}$ . Therefore, $X,V,x \vDash \nu p.\lozenge p$ . Otherwise, we have $x \in Y$ . If $x \notin \mathrm{Int}{(Y)}$ , then $x \in \mathrm{Cl}{(Z)}$ and since $x \notin Z$ it follows that $x \in \mathrm{d}(Z)$ . We have seen that $X,V,z \vDash \nu p.\lozenge p$ for all $z \in Z$ , so $X,V,x \vDash \lozenge \nu p.\lozenge p$ , and then the fixed point equation gives $X,V,x \vDash \nu p.\lozenge p$ . Otherwise, we have $x \in \mathrm{Int}{(Y)}$ . Since $Y \vDash \theta$ and $\mathrm{Int}{(Y)}$ is open in Y, we have $\mathrm{Int}{(Y)}\vDash \theta$ . Then, $\mathrm{Int}{(Y)},V,x \vDash \theta$ and since $\mathrm{Int}{(Y)}$ is open, we finally get $X,V,x \vDash \theta$ . In all cases, we obtain $X,V,x \vDash \theta \lor \nu p.\lozenge p$ as desired.

In our example, the axiom $.\mathsf{2}^{+}$ is known to define the class of extremally disconnected spaces – see Definition 11 and also van Benthem and Bezhanishvili (Reference van Benthem and Bezhanishvili2007). We thus obtain the following result:

5. Completeness for Imperfect Spaces

We have shown that there are $\mu$ -definable classes that are not modally definable, including infinitely many classes of imperfect spaces. We can make these examples even stronger by showing that the logics we have exhibited are complete for these classes. To this end, we construct the canonical model and use the technique of the final model applied by Fine and Zakharyashev to modal logic (see Bezhanishvili et al. Reference Bezhanishvili, Ghilardi and Jibladze2011; Chagrov and Zakharyaschev Reference Chagrov and Zakharyaschev1997) and by Baltag et al. (Reference Baltag, Bezhanishvili and Fernández-Duque2021) to the $\mu$ -calculus. Central will be the notion of cofinal subframe logic.

Under the right assumptions, it can be proven that (1) $\mathfrak M_\Sigma$ is a cofinal submodel of $\mathfrak M$ , (2) $\psi$ belongs to some $\Sigma$ -final world, and (3) the Truth Lemma holds in $\mathfrak M_\Sigma$ for the formulas in $\Sigma$ . This yields Kripke completeness of $\mathbf{\mu wK4}$ and, in fact, of any logic of the form $\mathbf{\mu wK4} + \theta$ where $\theta \in \mathcal L_{\lozenge}$ and $\mathbf{wK4} + \theta$ is a canonical and cofinal subframe logic. Note that this result is limited to extensions of $\mathbf{\mu wK4}$ with basic modal axioms. By contrast, the present work is novel in that it offers completeness results for axioms with fixed points. First, we need a technical lemma.

See Fig. 3 for a visual depiction of these frames. We know that $\mathfrak F_\Sigma$ is a cofinal subframe of $\mathfrak F$ . In addition, we have $\mathbf L \subseteq \mathbf L_0$ , so for all maximal consistent sets $\Gamma$ such that $\mathbf L_0 \subseteq \Gamma$ we also have $\mathbf L \subseteq \Gamma$ ; it is also clear that R and $R_0$ coincide over $\Omega_0$ . Thus, $\mathfrak F_0$ is a subframe of $\mathfrak F$ . We then introduce

\[\Omega' : = \{\Gamma \in \Omega_\Sigma \mid \mathfrak M_\Sigma,\Gamma \vDash \neg \nu p.\lozenge p\}\]

which induces a generated subframe $\mathfrak F' = (\Omega',R')$ of $\mathfrak F$ . Indeed, if $\Gamma \in \Omega'$ and $\Gamma R_\Sigma \Delta$ , then since $\mathfrak M_\Sigma,\Gamma \vDash \neg \nu p.\lozenge p$ we have $\mathfrak M_\Sigma,\Delta \vDash \neg \nu p.\lozenge p$ too and thus $\Delta \in \Omega'$ . Further, given $\Gamma \in \Omega'$ we have $\mathfrak M_\Sigma,\Gamma \vDash \neg \nu p.\lozenge p$ , and we obtain $\neg \nu p.\lozenge p \in \Gamma$ by the Truth Lemma. If $\mathbf L_0 \vdash \varphi$ , then $\mathbf L \vdash \varphi \lor \nu p.\lozenge p$ by Lemma 37, and from $\varphi \lor \nu p.\lozenge p \in \Gamma$ and $\neg \nu p.\lozenge p \in \Gamma$ we deduce $\varphi \in \Gamma$ . Therefore, $\mathbf L_0 \subseteq \Gamma$ , and we obtain $\Gamma \in \Omega_0$ . This proves that $\mathfrak F'$ is a subframe of $\mathfrak F_0$ .

Figure 3.

The canonical frame of $\mathbf L$ and its subframes.

Now, suppose that $\Gamma \in \Omega'$ , $\Delta \in \Omega_0,$ and $\Gamma R \Delta$ . Since $\mathfrak F_\Sigma$ is cofinal in $\mathfrak F$ , there exists $\Lambda \in \Omega_\Sigma$ such that $\Delta R^+ \Lambda$ . By weak transitivity, it follows that $\Gamma R^+ \Lambda$ , and since $\mathfrak F'$ is a generated subframe of $\mathfrak F_\Sigma$ it follows that $\Lambda \in \Omega'$ . Therefore, $\mathfrak F'$ is a cofinal subframe of $\mathfrak F_0$ . As observed by Baltag et al. (Reference Baltag, Bezhanishvili and Fernández-Duque2021), that $\mathbf{wK4} + \theta$ is canonical implies that $\mathbf{\mu wK4} + \theta$ is canonical too, so $\mathfrak F_0 \vDash \theta$ . Since $\mathbf L_0$ is cofinal subframe, it follows that $\mathfrak F' \vDash \theta$ as well.

We now show that $\mathfrak F_\Sigma \vDash \theta \lor \nu p.\lozenge p$ . Let $V_{\bullet}$ be a valuation over $\Omega_\Sigma$ and $\Gamma \in \Omega_\Sigma$ . If $\Gamma \in \Omega'$ , let $(\Omega',R',V'_\bullet)$ be the submodel of $(\Omega_\Sigma,R_\Sigma,V_\bullet)$ induced by $\Omega'$ . We know that $(\Omega',R',V_{\bullet}'),\Gamma \vDash \theta$ , and since $\mathfrak F'$ is a generated subframe of $\mathfrak F_\Sigma$ , it follows that $(\Omega_\Sigma,R_\Sigma,V_{\bullet}),\Gamma \vDash \theta$ . Otherwise, we have $\mathfrak M_\Sigma,\Gamma \vDash \nu p.\lozenge p$ , but obviously the truth value of $\nu p.\lozenge p$ does not depend on the valuation $V_{\Sigma}$ , and thus $(\Omega_\Sigma,R_\Sigma,V_{\bullet}),\Gamma \vDash \nu p.\lozenge p$ . This proves our claim. Finally, as mentioned earlier, $\psi$ is satisfiable on $\mathfrak M_\Sigma$ , and this concludes the proof of Kripke completeness.

There remains to prove that $\psi$ is satisfiable on a finite Kripke model. In the work of Baltag et al. (Reference Baltag, Bezhanishvili and Fernández-Duque2021), we find the construction of a finite model $\mathfrak M_\Sigma^\ast = (\Omega_\Sigma^\ast, R_\Sigma^\ast, V_\Sigma^\ast)$ – obtained as a quotient of $\mathfrak M_\Sigma$ by so-called $\Sigma$ -bisimilarity – together with a surjection $\rho:\Omega_\Sigma \rightarrow \Omega_\Sigma^*$ such that for all $\Gamma \in \Omega_\Sigma$ , the pointed models $(\mathfrak M_\Sigma,\Gamma)$ and $(\mathfrak M_\Sigma^\ast,\rho(\Gamma))$ satisfy the same formulas among those of $\Sigma$ . In particular, this entails that $\mathfrak M_\Sigma^* \vDash \mathbf L$ and that $\psi$ is satisfiable on $\mathfrak M_\Sigma^*$ , as desired.

In order to prove topological completeness, we apply the technique used by Baltag et al. (Reference Baltag, Bezhanishvili and Fernández-Duque2021) to turn a $\mathbf{wK4}$ frame into an appropriate topological space. The construction essentially consists of replacing every reflexive point w of a frame by countably many copies of w and to arrange them all into a dense-in-itself subspace, so as to mimic the reflexivity of w in a topological manner.

We then prove that Z is dense-in-itself. Let $(\Gamma,\alpha) \in Z$ and U be an open neighborhood of $(\Gamma,\alpha)$ . From $(\Gamma,\alpha) \in Z,$ we know that $\Gamma \notin \Omega'$ , that is, $\mathfrak M_\Sigma,\Gamma \vDash \nu p.\lozenge p$ . If $\alpha \neq \omega$ , then $\Gamma$ is reflexive. We select some $\beta \geq n^U_{w,\alpha}$ such that $\beta \neq \alpha$ , and by definition of $n^U_{w,\alpha}$ we obtain $(\Gamma,\beta) \in U$ . We also have $(\Gamma,\beta) \in Z$ . Otherwise, we have $\alpha = \omega$ , and then $\Gamma$ is irreflexive. From this and $\mathfrak M_\Sigma,\Gamma \vDash \nu p.\lozenge p,$ we obtain the existence of $\Delta \neq \Gamma$ such that $\Gamma R \Delta$ and $\mathfrak M_\Sigma,\Delta \vDash \nu p.\lozenge p$ . We set $\beta : = n^U_{w,\alpha}$ if $\Delta$ is reflexive, and $\beta : = \omega$ otherwise; we then have $(\Delta,\beta) \in Z$ by definition. Depending on whether $\Delta R \Gamma$ or not, we apply either item 1 or item 2 of Definition 39, and in both cases we obtain $(\Delta,\beta) \in U$ . Both cases bring the existence of some element in $U \cap Z$ different from $(\Gamma,\alpha)$ , and we are done.

It follows that $X \vDash \theta \lor \nu p.\lozenge p$ . We know that $\psi$ is satisfiable on $\mathfrak F_\Sigma$ , and since $\pi$ is a d-morphism it follows by Proposition 6 that $\psi$ is satisfiable on X as well. This concludes the proof.

In the following corollary, we finally apply these results to our examples.

Let $w \in W'$ . First, suppose that $\mathfrak F,w \vDash .\mathsf{2}^{+}$ . Then if $w R^+ u$ and $w R^+ v$ with $u,v \in W'$ , we have by assumption $u R^+ t$ and $v R^+ t$ for some $t \in W$ . Then since $\mathfrak F'$ is cofinal in $\mathfrak F$ we have $t R^+ t'$ for some $t' \in W'$ , and thus $u R^+ t'$ and $v R^+ t'$ . This proves that $\mathfrak F',w \vDash .\mathsf{2}^{+}$ . Otherwise, there exists a valuation V such that $\mathfrak F,V,w \nvDash .\mathsf{2}^{+}$ , and since $\mathfrak F,V,w \vDash .\mathsf{2}^{+}_{m}$ it follows that $\mathfrak F,V,w \vDash \square^m \bot$ . From this, we deduce $\mathfrak F',w \vDash \square^m \bot$ . In both cases, we obtain $\mathfrak F',w \vDash .\mathsf{2}^{+}_{m}$ . Therefore, $\mathfrak F' \vDash \mathbf L_0$ , and this proves the claim.