Spatial logic of tangled closure operators and modal mu-calculus
File(s)
Published version
Author(s)
Goldblatt, R
Hodkinson, I
Type
Journal Article
Abstract
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 Fernández-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 ∀ 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 mucalculus
with the closure operator <>; (ii) <> and the tangled closure operators <t> (in fact <t> can
express <>); (iii) <>, ∀; (iv) <>, ∀, <t>; (v) the derivative operator <d>; (vi) <d> and the associated
tangled closure operators <dt>; (vii) <d>, ∀; (viii) <d>, ∀,<dt>. Soundness also holds, if: (a) for
languages with ∀, X is connected; (b) for languages with <d>, X validates the well-known axiom
G1. For countable languages without ∀, we prove strong completeness. We also show that
in the presence of ∀, strong completeness fails if X is compact and locally connected
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 Fernández-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 ∀ 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 mucalculus
with the closure operator <>; (ii) <> and the tangled closure operators <t> (in fact <t> can
express <>); (iii) <>, ∀; (iv) <>, ∀, <t>; (v) the derivative operator <d>; (vi) <d> and the associated
tangled closure operators <dt>; (vii) <d>, ∀; (viii) <d>, ∀,<dt>. Soundness also holds, if: (a) for
languages with ∀, X is connected; (b) for languages with <d>, X validates the well-known axiom
G1. For countable languages without ∀, we prove strong completeness. We also show that
in the presence of ∀, strong completeness fails if X is compact and locally connected
Date Issued
2017-11-21
Date Acceptance
2016-10-24
Citation
Annals of Pure and Applied Logic, 2017, 168, pp.1032-1090
ISSN
1873-2461
Publisher
Elsevier Masson
Start Page
1032
End Page
1090
Journal / Book Title
Annals of Pure and Applied Logic
Volume
168
Copyright Statement
© 2016 The Author(s). Published by Elsevier B.V. This is an open access article
under the CC BY license (http://creativecommons.org/licenses/by/4.0/).
under the CC BY license (http://creativecommons.org/licenses/by/4.0/).
Sponsor
Engineering & Physical Science Research Council (EPSRC)
Grant Number
EP/L020750/1
Subjects
Science & Technology
Physical Sciences
Mathematics, Applied
Mathematics
Logic
Science & Technology - Other Topics
Derivative operator
Dense-in-itself metric space
Modal logic
Finite model property
Strong completeness
DYNAMIC TOPOLOGICAL LOGIC
COMPLETENESS
General Mathematics
0101 Pure Mathematics
Publication Status
Published