Neighbourhood Structures: Bisimilarity and Basic Model Theory

TL;DR

This paper explores the coalgebraic semantics of neighbourhood structures in non-normal modal logics, introducing new notions of equivalence and proving key theorems like Hennessy-Milner and Craig interpolation.

Contribution

It introduces precocongruences as an intermediate notion of equivalence, providing better approximations of behavioural equivalence in neighbourhood models.

Findings

Precocongruences better approximate behavioural equivalence than bisimulations.

Established a Hennessy-Milner theorem for modally saturated and image-finite models.

Proved an analogue of Van Benthem's theorem and Craig interpolation for classical modal logic.

Abstract

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 logic.