NEIGHBOURHOOD STRUCTURES: BISIMILARITY AND BASIC MODEL THEORY
NEIGHBOURHOOD STRUCTURES: BISIMILARITY AND BASIC MODEL THEORY
复制标题
DOI：
10.2168/lmcs-5(2:2)2009
复制
发表时间：
2009-01-01
影响因子：
0.6
通讯作者：
Pacuit, Eric
中科院分区：
文献类型：
--
作者：
Hansen, Helle Hvid;Kupke, Clemens;Pacuit, Eric
邻域结构是用于推理非正态模态逻辑的标准语义工具。所有邻域模型的逻辑称为经典模态逻辑。在余代数术语中，邻域框架是逆变幂集函子与其自身组成的余代数，用 2(2) 表示。我们使用这种联合代数模型来导出邻域结构之间的等价概念。 2(2)-相似性和行为等价是众所周知的余代数概念，并且它们是不同的，因为 2(2) 不保留弱回调。我们引入第三个中间概念，我们将其见证关系称为先同余（基于推出）。我们给出了 2(2)-互模拟和预同余的来回风格特征，我们表明，在单个代数上，预同余捕获了行为等价性，并且在邻域结构之间，预同余比 2(2)-互模拟更好地近似行为等价性。我们还引入了邻域模型模态饱和的概念，并研究了它与可定义性和图像有限性的关系。我们证明了模态饱和模型和图像有限邻域模型的 Hennessy-Milner 定理。我们的主要结果是 Van Benthem 表征定理的类比以及经典模态 Craig 插值的模型理论证明
Neighbourhood structures are the standard semantic tool used to reason about non-normal modal logics. The logic of all neighbourhood models is called classical modal logic. In coalgebraic terms, a neighbourhood frame is a coalgebra for the contravariant powerset functor composed with itself, denoted by 2(2). We use this coalgebraic modelling to derive notions of equivalence between neighbourhood structures. 2(2)-bisimilarity and behavioural equivalence are well known coalgebraic concepts, and they are distinct, since 2(2) does not preserve weak pullbacks. We introduce a third, intermediate notion whose witnessing relations we call precocongruences (based on pushouts). We give back-and-forth style characterisations for 2(2)-bisimulations and precocongruences, we show that on a single coalgebra, precocongruences capture behavioural equivalence, and that between neighbourhood structures, precocongruences are a better approximation of behavioural equivalence than 2(2)-bisimulations. We also introduce a notion of modal saturation for neighbourhood models, and investigate its relationship with definability and image-finiteness. We prove a Hennessy-Milner theorem for modally saturated and for image-finite neighbourhood models. Our main results are an analogue of Van Benthem's characterisation theorem and a model-theoretic proof of Craig interpolation for classical modal