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.

Automated summary

We study and prove the completeness, decidability, and finite model property of both the topological mu-calculus and the relational mu-calculus. We use a model-theoretic approach and make innovative use of a known method from modal logic, resulting in proofs that are both highly general and simple.