Imperial College London
Portrait Picture

Emeritus ProfessorIanHodkinson

Faculty of Engineering, Department of Computing

Emeritus Professor of Logic and Computation
 
 
 
//

Contact

 

i.hodkinson Website

 
 
//

Location

 

noneHuxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@article{Goldblatt:2017:10.1016/j.apal.2016.11.006,
author = {Goldblatt, R and Hodkinson, I},
doi = {10.1016/j.apal.2016.11.006},
journal = {Annals of Pure and Applied Logic},
pages = {1032--1090},
title = {Spatial logic of tangled closure operators and modal mu-calculus},
url = {http://dx.doi.org/10.1016/j.apal.2016.11.006},
volume = {168},
year = {2017}
}
Download

RIS format (EndNote, RefMan)

TY  - JOUR
AB  - There has been renewed interest in recent years in McKinsey and Tarski’s interpretation of modallogic in topological spaces and their proof that S4 is the logic of any separable dense-in-itselfmetric space. Here we extend this work to the modal mu-calculus and to a logic of tangledclosure operators that was developed by Fernández-Duque after these two languages had beenshown 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 advantageof the fact (proved by us elsewhere) that various tangled closure logics with and without theuniversal modality ∀ have the finite model property in Kripke semantics. These results are usedto construct a representation map (also called a d-p-morphism) from any dense-in-itself metricspace 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 mucalculuswith the closure operator <>; (ii) <> and the tangled closure operators <t> (in fact <t> canexpress <>); (iii) <>, ∀; (iv) <>, ∀, <t>; (v) the derivative operator <d>; (vi) <d> and the associatedtangled closure operators <dt>; (vii) <d>, ∀; (viii) <d>, ∀,<dt>. Soundness also holds, if: (a) forlanguages with ∀, X is connected; (b) for languages with <d>, X validates the well-known axiomG1. For countable languages without ∀, we prove strong completeness. We also show thatin the presence of ∀, strong completeness fails if X is compact and locally connected
AU  - Goldblatt,R
AU  - Hodkinson,I
DO  - 10.1016/j.apal.2016.11.006
EP  - 1090
PY  - 2017///
SN  - 1873-2461
SP  - 1032
TI  - Spatial logic of tangled closure operators and modal mu-calculus
T2  - Annals of Pure and Applied Logic
UR  - http://dx.doi.org/10.1016/j.apal.2016.11.006
UR  - http://hdl.handle.net/10044/1/42574
VL  - 168
ER  -
Download