Filtration and canonical completeness
for continuous modal $\mu$-calculi

This paper concerns two key methods in the theory of modal logic, both of which were introduced in their modern forms by Lemmon & Scott in [12]. First, filtration, which allows one to shrink a Kripke model into a finite one, by identifying states that agree on the truth of some given finite set of formulas. The Filtration Theorem then states that the equivalence classes in the finite model satisfy the same formulas as their members do in the original model. Filtration is the most important tool for proving the finite model property and the decidability of modal logics. For an overview of recent developments in the theory of filtration, see [3].

The other method central to this paper is that of canonical models. This well-known technique for proving the completeness of modal logics is related to Henkin’s method for first-order logic. Given a modal logic $\mathsf{L}$, it allows one to construct the canonical model $\mathbb{S}^{\mathsf{L}}$ of $\mathsf{L}$ with the powerful property that a formula $\varphi$ is consistent in the logic $\mathsf{L}$ if and only if it is satisfiable in $\mathbb{S}^{\mathsf{L}}$. It follows that $\mathsf{L}$ is complete with respect to any class of frames containing the canonical frame, i.e. the frame underlying $\mathbb{S}^{\mathsf{L}}$. Thus, when then the canonical frame is a frame for $\mathsf{L}$ - in this case $\mathsf{L}$ is said to be canonical - the logic $\mathsf{L}$ is complete with respect to the class of frames for $\mathsf{L}$.

Modal fixpoints logics are extensions of basic modal logic by operators capable of expressing certain kinds of recursive statements. They are of particular interest for computer science, where they are used to express important properties of processes. Examples of modal fixpoint logics are common knowledge logic ($\mathsf{CKL}$), provability logic ($\mathsf{GL}$), propositional dynamic logic ($\mathsf{PDL}$) and computation tree logic ($\mathsf{CTL}$). The central modal fixpoint logic, in which each of the aforementioned logics can be interpreted, is the modal $\mu$-calculus ($\mu\mathsf{ML}$), introduced by Kozen in [10]. It extends basic modal logic with explicit least and greatest fixed point operators, resulting in a large gain of expressive power. Although many desirable properties, such as decidability and bisimulation invariance, withstand this gain in expressive power, the methods of filtration and canonical models do not.

In fact, the method of canonical models breaks down already in the case of relatively simple modal fixpoint logics. The reason is that these logics generally lack the compactness property, preventing the use of infinite maximally consistent sets. If, however, the method of filtration does work for such a logic $\mathsf{L}$, then the canonical model method can often be salvaged. This roughly works as follows. One begins by taking the canonical model $\mathbb{S}^{\mathsf{L}}$. Due to the compactness failure, this model is non-standard, meaning that the frame underlying $\mathbb{S}^{\mathsf{L}}$ fails to satisfy some desired properties. However, by applying filtration to $\mathbb{S}^{\mathsf{L}}$ we obtain a finite model (a finitary canonical model), whose underlying frame often does satisfy these desired properties. This procedure for instance underlies the completeness proof for $\mathsf{PDL}$ by Kozen & Parikh in [11]. In the book [7], Goldblatt applies the same procedure to several modal fixpoint logics, including $\mathsf{CTL}$.

In the recent paper [9], Kikot, Shapirovsky & Zolin, prove a result of this kind that is relatively wide in scope. They show that if a basic modal logic $\mathsf{L}$ allows the method of filtration, then so does its expansion with the transitive closure modality. By iterating this procedure they show the same for the expansion of $\mathsf{L}$ by all modalities of $\mathsf{PDL}$. Subsequently, if the original basic modal logic $\mathsf{L}$ moreover is canonical, the completeness of this $\mathsf{PDL}$-expansion of $\mathsf{L}$ can be obtained by applying filtration to its canonical model.

In this paper we consider the methods of filtration and canonical models for a specific fragment of $\mu\mathsf{ML}$, which is called the continuous modal $\mu$-calculus and is denoted $\mu_{\_}c\mathsf{ML}$. In the paper [6], Fontaine shows that there are two equivalent ways to define $\mu_{\_}c\mathsf{ML}$. First semantically, as the fragment of the modal $\mu$-calculus where the application of fixpoint operators is restricted to formulas whose functional interpretation is Scott-continuous, rather than merely monotone. And second syntactically, as the fragment where the modal operator $\footnotesize\square$ and the fixpoint operator $\nu$ are not allowed to occur in the scope of a $\mu$-operator (and dually for the $\nu$-operator). To the best of our knowledge, the logic $\mu_{\_}c\mathsf{ML}$ was mentioned first in van Benthem [2] under the name ‘$\omega\text{-}\mu$-calculus’. It is related, and perhaps equivalent in expressive power, to the logic $\mathsf{CPDL}$ of concurrent propositional dynamic logic, cf. Carreiro [4, section 3.2] for more information.

There are at least two reasons why the continuous $\mu$-calculus is an interesting logic; first, the continuity condition that is imposed on the formation of fixpoint formulas ensures that the construction of a definable fixpoint using its ordinal approximations will always be finished after $\omega$ many steps. And second, in the same manner that the full $\mu$-calculus is the bisimulation-invariant fragment of monadic second-order logic [8], $\mu_{\_}c\mathsf{ML}$ has the same expressive power as weak monadic second-order logic, when it comes to bisimulation-invariant properties [5].

The goal of the present paper is to show that we can add two more desirable properties to this list: (i) the Filtration Theorem holds for $\mu_{\_}c\mathsf{ML}$ and (ii) completeness for sufficiently nice logics in the language of $\mu_{\_}c\mathsf{ML}$ can be proven using finitary canonical models.

Since $\mu_{\_}c\mathsf{ML}$ is strictly more expressive than $\mathsf{PDL}$ [6, 4], this is a proper generalisation of the aforementioned results from the paper [9]. On the other hand, because the failure of filtration for $\mu\mathsf{ML}$ is witnessed by the formula $\mu x.\rotatebox[origin={c}]{0.0}{$\footnotesize\square$}x$, the syntactic restrictions characterising $\mu_{\_}c\mathsf{ML}$ seem to be not only sufficient, but also necessary for filtration. This indicates that $\mu_{\_}c\mathsf{ML}$ might be positioned as a maximal filtration-allowing language between the basic modal language and the full language of the modal $\mu$-calculus. We leave it for future work to make this statement mathematically precise and to investigate its correctness.

In Section 2 we define the syntax of the continuous modal $\mu$-calculus, the game semantics and other basic notions. In Section 3 we treat filtration. After giving the necessary definitions, we will use game-theoretic arguments to prove the Filtration Theorem for the language $\mu_{\_}c\mathsf{ML}$. As a corollary, we obtain the finite model property for this language interpreted over a wide range of model classes. In Section 4 we prove our completeness result, again using game-theoretic methods.

Unlike for $\mathsf{PDL}$, there is no obvious way to construct a non-standard canonical model for $\mu_{\_}c\mathsf{ML}$. Because of this, we define the finitary canonical model used in our completeness proof directly, instead of as some filtration of a non-standard canonical model. This causes Section 3 and Section 4 to contain some rather similar constructions and proofs. We leave it for future work to unify these two.

The continuous modal $\mu$-calculus will be defined using the syntactic characterisation given by Fontaine in [6]. We fix a countably infinite set $\mathsf{P}$ of propositional variables.

If one of the above fragments is subscripted by a singleton $\{x\}$, we will simply write $x$ instead. We will use formula to refer to a $\mu_{\_}c\mathsf{ML}$-formula. We define the subformula relation $\unlhd$ and, for a given formula $\xi$, the sets $\textnormal{Sf}(\xi)$ of subformulas, $\textnormal{FV}(\xi)$ of free variables and $\textnormal{BV}(\xi)$ of bound variables of $\xi$ in the usual way. Given two formulas $\varphi,\psi$ and a propositional variable $x$, we define $\varphi[\psi/x]$ to be the result of replacing each free occurrence of $x$ in $\varphi$ by $\psi$. We will assume an implicit mechanism of $\alpha$-conversion in order to avoid the capture of free variables of $\psi$ by binders in $\varphi$ in the substitution $\varphi[\psi/x]$.

We say that a formula is tidy if the sets of its free and its bound variables are disjoint. A formula $\varphi$ is called clean if, in addition, we can associate with each bound variable $x$, a unique fixpoint binder $\eta_{\_}x$ and a unique formula $\delta_{\_}x$ such that $\eta x.\delta_{\_}x$ is a subformula of $\varphi$. In this case, if $\eta_{\_}x=\mu$ ($\eta_{\_}x=\nu$), the variable $x$ is said to be a $\mu$-variable ($\nu$-variable). We will sometimes denote by $\overline{\eta}$ the dual of $\eta$. Note that every subformula of a clean formula is itself clean. For convenience we will assume that every formula is tidy. Finally, we will use $\mathsf{ML}$ to refer to the basic modal language (over the set $\mathsf{P}$ of propositional variables).

It is a well-known fact that the closure of a finite set of formulas is finite. Note, moreover, that in the FL-closure of a set of tidy formulas, every formula is tidy.

We say of a subformula $\varphi\unlhd\xi$ that it is a free subformula of $\xi$, and write $\varphi\unlhd_{\_}f\xi$, if $\varphi\in Cl(\xi)$. Equivalently, a subformula $\varphi\unlhd\xi$ is a free subformula of $\xi$ whenever every free variable of $\varphi$ is a free variable of $\xi$.

As usual, formulas will be interpreted in Kripke models.

Given some accessibility relation $R$, we often write $sRt$ instead of $(s,t)\in R$. The algebraic semantics of the continuous $\mu$-calculus extends that of the basic modal language. Given a valuation function $V:\mathsf{P}\rightarrow\mathcal{P}(S)$, we write $V[x\mapsto X]$ for the function given by $V[x\mapsto X](x)=X$ and $V[x\mapsto X](y)=V(y)$ for $y\not=x$.

We say that $\xi$ is satisfied at a state $s$ of the model $\mathbb{S}$, and write $\mathbb{S},s\Vdash\xi$ whenever $s\in[\![\xi]\!]^{\mathbb{S}}$. As usual, we say that $\xi$ is valid in $\mathbb{S}$, written $\mathbb{S}\models\xi$, whenever $\xi$ is satisfied at every state $s$ of $\mathbb{S}$, and valid in the frame $(S,R)$, written $(S,R)\models\xi$, whenever $(S,R,V)\models\xi$ for every valuation function $V:\mathsf{P}\rightarrow\mathcal{P}(S)$.

Two formulas are called equivalent whenever they have the same meaning in every Kripke model. It easy to see that every formula has an equivalent alphabetic variant which is clean.

A well-known equivalent characterisation of the meaning of a formula uses the formalism of infinite games. We assume familiarity with this kind of games.

Note that for formulas of the continuous $\mu$-calculus $x<_{\_}\xi y$ implies that $x$ is a $\mu$-variable if and only if $y$ is a $\mu$-variable. In other words, the continuous modal $\mu$-calculus is alternation free.

The following lemma contains some basic facts about the course of play in evaluation games for $\mu_{\_}c\mathsf{ML}$. Items (1) and (2) hold because the continuous $\mu$-calculus is alternation free. Item (3) is specific to the continuous modal $\mu$-calculus, in the sense that it does not hold for the more expressive alternation free $\mu$-calculus (see e.g. [13] for a formal definition of this language).

We say of an enumeration $\{x_{\_}1,\ldots x_{\_}n\}$ of $\text{BV}(\xi$) that it respects the dependency order if $x_{\_}i<_{\_}\xi x_{\_}j$ implies $i<j$. Since any partial order can be extended to a linear order, every formula $\xi$ admits an enumeration of its bound variables that respects the dependency order. For the rest of this paper we fix such an enumeration of $\text{BV}(\xi)$ for every clean formula $\xi$.

Note that when $\varphi\unlhd_{\_}f\xi$, it holds that $\exp_{\_}\xi(\varphi)=\varphi$. The following well-known theorem provides the central link between the algebraic and the game semantics.

In particular, for any clean formula $\xi$ and $\varphi\unlhd_{\_}f\xi$ we have $\mathbb{S},s\Vdash\varphi$ if and only if $\exists$ has a winning strategy in the game $\mathcal{E}(\xi,\mathbb{S})$ initialised at the position $(\varphi,s)$.

Another useful fact, originally provided by Dexter Kozen in [10], is the following.

We give an axiomatisation of the continuous modal $\mu$-calculus based on an axiomatisation introduced by Dexter Kozen for the full modal $\mu$-calculus in [10].

We will consider axiomatic extensions of $\mu_{\_}c\mathsf{K}$ that are closed under the rules above. We will use $\mu_{\_}c$-logic to refer to such an extension. The term logic will be used to refer to any normal modal logic. If $\mathsf{L}$ is a logic in the basic modal language, we use $\mu_{\_}c$-$\mathsf{L}$ to denote the least $\mu_{\_}c$-logic containing $\mathsf{L}$. Moreover, we will use $\mathsf{Mod}(\mathsf{L})$ ($\mathsf{Fr}(\mathsf{L})$) to denote the class of models (frames) on which every formula in $\mathsf{L}$ is valid. If $(S,R,V)$ belongs to $\mathsf{Mod}(\mathsf{L})$ ($(S,R)$ belongs to $\mathsf{Fr}(\mathsf{L})$) we say that $(S,R,V)$ is an $\mathsf{L}$-model ($(S,R)$ is an $\mathsf{L}$-frame) and write $(S,R,V)\models\mathsf{L}$ ($(S,R)\models\mathsf{L}$).

The relation $R^{\mathsf{min}}$ will be called the finest filtration and the relation $R^{\mathsf{max}}$ the coarsest.

If $f$ is a strategy for the player $\exists$ ($\forall$) in a game $\mathcal{G}$, we say of a (possibly infinite) $\mathcal{G}$-match $\gamma$ that it is $f$-guided whenever every choice made by $\exists$ ($\forall$) in the match $\gamma$ is the choice dictated by the strategy $f$.

Note that the above argument would not go through for the alternation free $\mu$-calculus, since we would no longer be able to guarantee that we create at most finitely many shadow matches in the case of infinitely many $\mu$-unfoldings. A well-known counterexample to the Filtration Theorem for the alternation free $\mu$-calculus is the formula $\mu x.\rotatebox[origin={c}]{0.0}{$\footnotesize\square$}x$.

Having established that filtrations preserve satisfaction of $\mu_{\_}c\mathsf{ML}$-formulas, we will now investigate to which classes of models filtration can be applied.

One might expect that admitting filtration with respect to the basic modal language is a weaker property than admitting filtration with respect to a proper extension of the language. However, for the language $\mu_{\_}c\mathsf{ML}$ it turns out that this is not the case, at least for those classes of models that are determined by some logic.

We will show this by making use of the following technical sufficient condition.

The proof of the following lemma resembles that of Theorem 3.8 in [9].

Note that the above proof does not rely on any specific properties of the language $\mu_{\_}c\mathsf{ML}$. In fact, it could also have been carried out for the full language $\mu\mathsf{ML}$ of the modal $\mu$-calculus. As a corollary, we obtain the finite model property.

For instance, since the class of symmetric models is the class of $\mathsf{KB}$-models, the continuous modal $\mu$-calculus has the finite model property over this class.

For the entirety of this paragraph we fix an arbitrary $\mu_{\_}c$-logic $\mathsf{L}$. We define the negation operator $\sim:\mu_{\_}c\mathsf{ML}\rightarrow\mu_{\_}c\mathsf{ML}$ in the usual way. In particular, that means that we define ${\sim}\eta x.\varphi:=\overline{\eta}x.{\sim}\varphi[\neg x/x]$. We leave it to the reader to verify that $\mathsf{L}\vdash({\sim}\varphi\land\varphi)\leftrightarrow\bot$ and $\mathsf{L}\vdash({\sim}\varphi\lor\varphi)\leftrightarrow\top$.

We say that $\Sigma$ is ${\sim}$FL-closed if it is both FL-closed and ${\sim}$-closed. Note that for every finite set of $\mu_{\_}c\mathsf{ML}$-formulas, the $\sim$-closure of its FL-closure is a finite ${\sim}$FL-closed extension.

A set $\Gamma$ of formulas is said to be $\mathsf{L}$-inconsistent if $\mathsf{L}\vdash(\gamma_{\_}1\land\ldots\land\gamma_{\_}n)\rightarrow\bot$ for some $\gamma_{\_}1,\ldots,\gamma_{\_}n\in\Gamma$. We say of a formula $\varphi$ that it is $\mathsf{L}$-inconsistent whenever $\{\varphi\}$ is.

By a standard argument it can be shown that every $\mathsf{L}$-consistent set of formulas has a maximally $\mathsf{L}$-consistent extension. The proof of the following lemma is also standard and left to the reader.