Duality for instantial neighbourhood logic via coalgebra

Instantial Neighbourhood Logic (INL) has been introduced recently as a language for neighbourhood frames where existential information can be given about what kind of worlds occur in a neighbourhood of a current world. Apart from its semantics, its proof theory and bisimulation games have also been studied. However, conspicuously absent from the treatment of INL is the notion of descriptive frames.

This is the gap that we are closing in this paper. We introduce descriptive frames for INL and we prove that these are dual to boolean algebras with instantial operators (BAIOs), which give the algebraic semantics of INL. Our methods for establishing this duality make essential use of coalgebra: we observe that BAIOs are algebras for a functor on the category of boolean algebras and show that this functor is dual to the double Vietoris functor (i.e. the composition of the Vietoris functor with itself), thus obtaining a dual equivalence between double Vietoris coalgebras and BAIOs. The proof of our main result is then completed by showing that double Vietoris coalgebras correspond precisely to descriptive frames. As a corollary we obtain that every extension of INL is sound and complete with respect to descriptive frames, that descriptive frames enjoy the Hennessy-Milner property, and as a result, that finite neighbourhood frames enjoy the Hennessy-Milner property.