{"docId":1167,"paperId":1167,"url":"https:\/\/lmcs.episciences.org\/1167","doi":"10.2168\/LMCS-5(2:2)2009","journalName":"Logical Methods in Computer Science","issn":"","eissn":"1860-5974","volume":[{"vid":129,"name":"Volume 5, Issue 2"}],"section":[],"repositoryName":"arXiv","repositoryIdentifier":"0901.4430","repositoryVersion":4,"repositoryLink":"https:\/\/arxiv.org\/abs\/0901.4430v4","dateSubmitted":"2007-12-19 00:00:00","dateAccepted":"2015-06-25 11:52:22","datePublished":"2009-04-09 00:00:00","titles":["Neighbourhood Structures: Bisimilarity and Basic Model Theory"],"authors":["Hansen, Helle Hvid","Kupke, Clemens","Pacuit, Eric"],"abstracts":["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.","Comment: uses LMCS.cls (included), 2 figures (both ps and pdf)"],"keywords":["Computer Science - Logic in Computer Science","F.1.1","F.3.2","F.4.1","I.2.4"]}