Filtration and canonical completeness for continuous modal mu-calculi

TL;DR

This paper investigates the continuous modal mu-calculus, demonstrating that key modal logic techniques like filtration and canonical models remain valid, leading to finite model properties and completeness results for extended logics.

Contribution

It proves filtration and canonical model theorems for the continuous modal mu-calculus, extending modal logic techniques to this fragment and generalizing previous results.

Findings

Filtration theorem holds for continuous modal mu-calculus formulas.

Finite model property is established for a wide range of classes.

Adding continuous fixpoint operators preserves soundness and completeness for canonical logics.

Abstract

The continuous modal mu-calculus is a 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. By game-theoretic means, we show that this relatively expressive fragment still allows two important techniques of basic modal logic, which notoriously fail for the full modal mu-calculus: filtration and canonical models. In particular, we show that the Filtration Theorem holds for formulas in the language of the continuous modal mu-calculus. As a consequence we obtain the finite model property over a wide range of model classes. Moreover, we show that if a basic modal logic L is canonical and the class of L-frames admits filtration, then the logic obtained by adding continuous fixpoint operators to L is sound and complete with respect to the class of L-frames. This generalises recent results on a strictly weaker fragment of the modal mu-calculus, viz. PDL.