Intuitionistic modal logic based on neighborhood semantics without superset axiom

TL;DR

This paper develops a neighborhood semantics framework for propositional intuitionistic modal logic without relying on the superset axiom, introducing new modalities and establishing foundational properties.

Contribution

It introduces a novel neighborhood semantics approach for intuitionistic modal logic without the superset axiom, including new modalities and bi-relational models.

Findings

Soundness and completeness of the axiomatization proved.

Finite model property established.

Properties of bisimulation and behavioral equivalence analyzed.

Abstract

In this paper we investigate certain systems of propositional intuitionistic modal logic defined semantically in terms of neighborhood structures. We discuss various restrictions imposed on those frames but our constant approach is to discard superset axiom. Such assumption allows us to think about specific modalities $\Delta, \nabla$ and new functor $\rightsquigarrow$ depending on the notion of maximal neighborhood. We show how it is possible to treat our models as bi-relational ones. We prove soundness and completeness of proposed axiomatization by means of canonical model. Moreover, we show that finite model property holds. Then we describe properties of bounded morphism, behavioral equivalence, bisimulation and n-bisimulation. Finally, we discuss further researches (like some interesting classical cases and particular topological issues).