Spatial logic of tangled closure operators and modal mu-calculus
Spatial logic of tangled closure operators and modal mu-calculus
复制标题
缠结闭包算子的空间逻辑和模态 mu 演算
DOI：
10.1016/j.apal.2016.11.006
复制
发表时间：
2017
影响因子：
0.8
通讯作者：
Goldblatt R
中科院分区：
文献类型：
--
作者：
Goldblatt R
近年来，McKinsey和Tarski对拓扑空间中的模态逻辑的解释，以及他们证明S4是任何可分自稠密度量空间的逻辑，重新引起了人们的兴趣。在这里，我们将这项工作推广到模u-演算，以及在Dawar和Otto证明这两种语言对有限传递Klipke模型具有相同的表达能力之后由Fernández-Duque发展的纠缠闭包算子逻辑。我们证明了这种等价性在拓扑空间上仍然成立。我们推广了McKinsey-Tarski拓扑“解剖引理”。我们还利用了这样一个事实(我们在其他地方证明了这一点)，即具有和不具有通用情态∀的各种纠缠闭包逻辑在Kriske语义中具有有限模型性质。这些结果被用来构造从任何自稠密度量空间X到任何有限连通的局部连通的序列传递Kriske框架的表示映射(也称为DP-态射)。这产生了许多语言在X上的完备性定理：(I)具有闭包算子◇的模u演算；(Ii)◇和纠缠闭包算子<；t>；(事实上<；t>；可以表示◇)；(Iii)◇，∀；(Iv)◇，∀，<；t>；(V)导算子<；d>；(Vi)<；d>；以及相关的纠缠闭包算子<；d>；；(Vii)<；d>；，∀；(Viii)<；d>；，∀，<；d t>；。如果：(A)对于有∀的语言，X是连通的；(B)对于有∀的语言，X验证了广为人知的公理G1。对于没有Lt；d>；的可数语言，我们证明了强完备性。我们还证明了在∀存在的情况下，如果X是紧的且局部连通的，则强完备性失败。
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 dp-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◇;(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< d t>;(vii)< d>,∀;(viii)< d>,∀,< d t>. Soundness also holds, if:(a) for languages with∀, X is connected;(b) for languages with< d>, X validates the well-known axiom G 1. 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.
登录
查看更多内容
影响因子：
0.4
作者：
Antonio Montalbán
通讯作者：
Antonio Montalbán
DOI：
--
发表时间：
2016
期刊：
Advances in Modal Logic
影响因子：
--
作者：
R. Goldblatt;I. Hodkinson
通讯作者：
I. Hodkinson
论模态命题逻辑和中间命题逻辑的强邻域完备性（上）
DOI：
--
发表时间：
1996
期刊：
Advances in Modal Logic
影响因子：
--
作者：
V. Shehtman
通讯作者：
V. Shehtman
DOI：
--
发表时间：
2002
期刊：
影响因子：
--
作者：
G. Bezhanishvili;M. Gehrke
通讯作者：
M. Gehrke
不等式的拓扑模态逻辑
DOI：
--
发表时间：
2008
期刊：
影响因子：
--
作者：
A V Kudinov
通讯作者：
A V Kudinov