Neighbourhood Structures: Bisimilarity and Basic Model Theory

Neighbourhood structures are the standard semantic tool used to reason aboutnon-normal modal logics. The logic of all neighbourhood models is called classical modallogic. In coalgebraic terms, a neighbourhood frame is a coalgebra for the contravariantpowerset functor composed with itself, denoted by22. We use this coalgebraic modellingto derive notions of equivalence between neighbourhood structures.22-bisimilarity andbehavioural equivalence are well known coalgebraic concepts, and they are distinct, since22does not preserve weak pullbacks. We introduce a third, intermediate notion whose wit-nessing relations we call precocongruences (based on pushouts). We give back-and-forthstyle characterisations for22-bisimulations and precocongruences, we show that on a singlecoalgebra, precocongruences capture behavioural equivalence, and that between neighbour-hood structures, precocongruences are a better approximation of behavioural equivalencethan22-bisimulations. We also introduce a notion of modal saturation for neighbourhoodmodels, and investigate its relationship with definability and image-finiteness. We prove aHennessy-Milner theorem for modally saturated and for image-finite neighbourhood mod-els. Our main results are an analogue of Van Benthem’s characterisation theorem and amodel-theoretic proof of Craig interpolation for classical modal logic