Spatial logic of tangled closure operators and modal mu-calculus

There has been renewed interest in recent years in McKinsey and Tarski's interpretation of modal logic in topological spaces and their proof that S4 is the logic of any separable dense-in-itself metric space. Here we extend this work to the modal mu-calculus and to a logic of tangled closure operators that was developed by Fernandez-Duque after these two languages had been shown by Dawar and Otto to have the same expressive power over finite transitive Kripke models. We prove that this equivalence remains true over topological spaces. We extend the McKinsey Tarski topological 'dissection lemma'. We also take advantage of the fact (proved by us elsewhere) that various tangled closure logics with and without the universal modality for all have the finite model property in Kripke semantics. These results are used to construct a representation map (also called a d-p-morphism) from any dense-in-itself metric space X onto any finite connected locally connected serial transitive Kripke frame. This yields completeness theorems over X for a number of languages: (i) the modal mu-calculus with the closure operator lozenge; (ii) lozenge and the tangled closure operators (t) (in fact (t) can express lozenge); (iii) lozenge, for all; (iv) lozenge, for all, (t); (v) the derivative operator (d); (vi) (d) and the associated tangled closure operators (dt); (vii) (d), for all; (viii) ( d), for all, (dt). Soundness also holds, if: (a) for languages with for all, X is connected; (b) for languages with (d), X validates the well-known axiom G(1). For countable languages without for all, we prove strong completeness. We also show that in the presence of for all, strong completeness fails if X is compact and locally connected. (C) 2016 The Author(s). Published by Elsevier B.V.