The Topological Mu-Calculus: Completeness and Decidability

We study the topological mu-calculus, based on both Cantor derivative and closure modalities, proving completeness, decidability, and finite model property over general topological spaces, as well as over T-0 and T-D spaces. We also investigate the relational mu-calculus, providing general completeness results for all natural fragments of the mu-calculus over many different classes of relational frames. Unlike most other such proofs for mu-calculi, ours is model theoretic, making an innovative use of a known method from modal logic (the 'final' submodel of the canonical model), which has the twin advantages of great generality and essential simplicity.