模态μ演算与纠缠闭包算子的空间逻辑

近年来，McKinsey和Tarski在拓扑空间中对模态逻辑的解释以及他们关于S4是任意可分、自身稠密度量空间的逻辑的证明，重新引起了兴趣。在此我们将此工作扩展到模态μ演算和纠缠闭包算子逻辑，后者由Fernández-Duque在Dawar和Otto证明这两种语言在有限传递Kripke模型上具有相同表达力之后发展起来。我们证明这种等价性在拓扑空间上依然成立。我们建立了带或不带全称模态 $\forall$ 的各种纠缠闭包逻辑在Kripke语义中的有限模型性质。我们还扩展了McKinsey--Tarski拓扑“剖分引理”。这些结果被用于构造从任意自身稠密度量空间 $X$ 到任意有限连通局部连通串行传递Kripke框架的表示映射(也称为d-p-态射)。这给出了在 $X$ 上针对若干语言的完备性定理：(i) 带闭包算子 $\Diamond$ 的模态μ演算；(ii) $\Diamond$ 与纠缠闭包算子 $\langle t \rangle$；(iii) $\Diamond,\forall$；(iv) $\Diamond,\forall,\langle t \rangle$；(v) 导数算子 $\langle d \rangle$；(vi) $\langle d \rangle$ 与关联的纠缠闭包算子 $\langle dt \rangle$；(vii) $\langle d \rangle,\forall$；(viii) $\langle d \rangle,\forall,\langle dt \rangle$。若满足以下条件，可靠性也成立：(a) 对于带 $\forall$ 的语言，$X$ 是连通的；(b) 对于带 $\langle d \rangle$ 的语言，$X$ 验证熟知的公理 $\mathrm{G}_1$。对于不带 $\forall$ 的可数语言，我们证明了强完备性。我们还表明在 $\forall$ 存在时，若 $X$ 是紧且局部连通的，则强完备性失败。