一句话:在更广的半度量空间上建立 wK4 及相关逻辑的度量完备性,并提出混合缠结以刻画 µ-演算的表达力。
µ-演算可在度量空间上解释,并具有 McKinsey-Tarski 完备性定理和 Dawar-Otto 模态刻画定理的变体;但在不满足基本分离公理的空间中,基模态逻辑不是 K4 而是较弱的 wK4,相关结果失效。本文把语义推广到更广的半度量空间,证明 wK4 及相关逻辑的度量完备性。作者指出 Dawar-Otto 定理仍然失效源于缠结导数在任意拓扑空间中定义不当,因而引入混合缠结:它在度量空间上与缠结导数一致,但在一般情况下表现更好。最后证明只有混合缠结足以定义有限结构的可模拟性,这是 µ-演算表达完备片段的关键测试用例。
The µ-calculus can be interpreted over metric spaces and is known to enjoy, among other celebrated properties, variants of the McKinsey-Tarski completeness theorem and of Dawar and Otto’s modal characterization theorem. In its topological form, this theorem states that every topological fixed point may be defined in terms of the tangled derivative, a polyadic generalization of Cantor’s perfect core. However, these results fail when spaces not satisfying basic separation axioms are considered, in which case the base modal logic is not the well-known K4, but the weaker wK4.In this paper we show how these shortcomings may be overcome. First, we consider semantics over the wider class of hemimetric spaces, and obtain metric completeness results for wK4 and related logics. In this setting, the Dawar-Otto theorem still fails, but we argue that this is due to the tangled derivative not being suitably defined for general application in arbitrary topological spaces. We thus introduce the hybrid tangle, which coincides with the tangled derivative over metric spaces but is better behaved in general. We show that only the hybrid tangle suffices to define simulability of finite structures, a key ‘test case’ for an expressively complete fragment of the µ-calculus.