Let \(M^\mathsf{L}\) be the canonical Kripke model for the modal logic \(\mathsf{L}\). Given a modal formula \(\varphi\) and a world \(\Gamma\) of \(M^\mathsf{L}\), \[ \varphi\in\Gamma \text{ iff } \varphi\text{ holds at }\Gamma. \] This is the Truth Lemma for \(\mathsf{L}\). We show that, in general, the Truth Lemma for the modal \(\mu\)-calculus is false.
The Truth Lemma is a convenient tool to prove the completeness and finite model property of modal logics. Completeness and the finite model property do hold for the \(\mu\)-calculus, but their proofs require other techniques. See Bradfield and Stirling's survey for more pointers.
Variations of the Truth Lemma for the \(\mu\)-calculus can be used in some settings. \(\mathsf{wK4}\) is the modal logic of weakly-transitive frames and of derivative topological semantics. Baltag, Bezhanishvili, and Fernández-Duque used a Truth Lemma for the final canonical model of \(\mathsf{wK4}\) to show its completeness, decidability, and the finite model property.
The failure of the Truth Lemma on the modal \(\mu\)-calculus is a folklore result, but I couldn't find the proof written anywhere. I wrote this post so a there is a findable proof on the internet. It has been asked in the FOL mailing list, without an answer. A related question about \(\mathsf{PDL}\) is on Mathematics Stack Exchange.
We begin with a very short introduction to the \(\mu\)-calculus. The \(\mu\)-calculus is obtained by adding least and greatest fixed-point operators to modal logic. We write them as \(\mu\) and \(\nu\), respectively. The logic \(\mu\mathsf{K}\) is the least set of formulas containing
and closed under
The model \(M^\mathsf{L}\) is a triple consisting of a set of worlds, an accessibility relation between worlds, and a valuation function assigning propositions to the set of worlds where they hold. The worlds of the canonical model \(M^{\mu\mathsf{K}}\) are the complete extensions of the logic \(\mu\mathsf{K}\). A complete extension \(\Gamma\) of \(\mu\mathsf{K}\) is a set of formulas such that \(\mu\mathsf{K}\subseteq \Gamma\); no contradiction is provable from \(\Gamma\); and, for all \(\varphi\) either \(\varphi\in\Gamma\) or \(\neg\varphi\in \Gamma\). The canonical model's accessibility relation and valuation function will not be relevant in the proof below.
Before our proof, we review the meaning of some formulas. Fix a Kripke model \(M\). \(\mu X.P\lor \Diamond X\) holds at a world \(w\) iff there is a path starting from \(w\) which ends in a world where \(P\) holds. Abbreviate a sequence of \(n\) many \(\Diamond\)s by \(\Diamond^n\). Then \(\Diamond^n P\) holds at a world \(w\) iff there is a path starting from \(w\) which has length \(n\) and ends in a world where \(P\) holds. (I plan to eventually write a post with the basic semantics of the \(\mu\)-calculus.)
Consider the set of formulas \[\Gamma_0 = \{\mu X.P\lor \Diamond X\} \cup \{\neg \Diamond^n P \mid n\in\mathbb{N} \}.\] Now, \(\Gamma_0\) is not satisfiable: if \(\mu X.P\lor \Diamond X\) holds at a world \(w\) then \(\Diamond^n P\) holds at \(w\) for some \(n\in\mathbb{N}\). But \(\Gamma_0\) is consistent, since any of its finite subsets is satisfiable. To see that, let \(M_n = (W,R,V)\) be a Kripke model such that:
In a picture:
On one hand, there is a path of length \(n\) starting at \(w_0\) and ending in a world (\(w_n\)) where \(P\) holds. On the other hand, there is no shorter path with this property. So \(w_0\) satisfies \(\{\mu X.P\lor \Diamond X\} \cup \{\neg P, \neg \Diamond P,\dots, \neg \Diamond^{n-1} P \}\).
Suppose the Truth Lemma holds in the \(\mu\)-calculus. Let \(\Gamma\) be a complete extension of \(\Gamma_0\). Then \(\Gamma\) is a world in the canonical model \(M^{\mu\mathsf{K}}\). By the Truth Lemma, \(\Gamma\) satisfies each formula in \(\Gamma_0\). As \(\Gamma_0\) is not satisfiable, we have a contradiction. Therefore the Truth Lemma fails in the \(\mu\)-calculus.