The Topological Mu-Calculus: completeness and decidability

TL;DR

This paper establishes the completeness and decidability of the topological $$-calculus, based on derivative and closure modalities, over various topological and relational spaces, using a novel model-theoretic approach.

Contribution

It provides the first model-theoretic completeness proofs for the topological $$-calculus and its fragments over multiple classes of spaces, introducing a simple, general method.

Findings

Proves completeness and decidability of the topological $$-calculus.

Develops a model-theoretic proof technique using the 'final' submodel.

Extends results to relational $$-calculus over various frames.

Abstract

We study the topological $\mu$-calculus, based on both Cantor derivative and closure modalities, proving completeness, decidability and FMP over general topological spaces, as well as over $T_0$ and $T_D$ spaces. We also investigate relational $\mu$-calculus, providing general completeness results for all natural fragments of $\mu$-calculus over many different classes of relational frames. Unlike most other such proofs for $\mu$-calculus, ours is model-theoretic, making an innovative use of a known Modal Logic method (--the 'final' submodel of the canonical model), that has the twin advantages of great generality and essential simplicity.