### Abstract

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

Original language | English |
---|---|

Article number | 1167 |

Pages (from-to) | 1-38 |

Number of pages | 38 |

Journal | Logical Methods in Computer Science |

Volume | 5 |

Issue number | 2 |

DOIs | |

Publication status | Published - 9 Apr 2009 |

## Fingerprint Dive into the research topics of 'Neighbourhood Structures: Bisimilarity and Basic Model Theory'. Together they form a unique fingerprint.

## Cite this

Hansen, H. H., Kupke, C., & Pacuit, E. (2009). Neighbourhood Structures: Bisimilarity and Basic Model Theory.

*Logical Methods in Computer Science*,*5*(2), 1-38. [1167]. https://doi.org/10.2168/LMCS-5(2:2)2009