Instantial neighbourhood logic

This paper explores a new language of neighbourhood structures where existential information can be given about what kind of worlds occur in a neighbourhood of a current world. The resulting system of ‘instantial neighbourhood logic’ INL has a nontrivial mix of features from relational semantics and from neighbourhood semantics. We explore some basic model-theoretic behavior, including a matching notion of bisimulation, and give a complete axiom system for which we prove completeness by a new normal form technique. In addition, we relate INL to other modal logics by means of translations, and determine its precise SAT complexity. Finally, we discuss proof-theoretic fine-structure of INL in terms of semantic tableaux and some expressive fine-structure in terms of fragments, while discussing concrete illustrations of the instantial neighborhood language in topological spaces, in games with powers for players construed in a new way, as well as in dynamic logics of acquiring or deleting evidence. We conclude with some coalgebraic perspectives on what is achieved in this paper. Many of these final themes suggest follow-up work of independent interest.