Expressive power of basic modal intuitionistic logic as a fragment of classical FOL

TL;DR

This paper explores the expressive capabilities of various fragments of modal intuitionistic logic within classical first-order logic, using modified asimulation techniques for semantic characterization.

Contribution

It introduces a modified notion of asimulation to characterize the expressive power of modal intuitionistic logic fragments and extends this to first-order definable subclasses.

Findings

Semantic characterization via asimulation for each fragment.

Extension of characterization to subclasses of classical models.

Framework applicable to various first-order definable classes.

Abstract

The paper treats 4 different fragments of first-order logic induced by their respective versions of Kripke style semantics for modal intuitionistic logic. In order to capture these fragments, the notion of asimulation is modified and extended to yield Van Benthem type of semantic characterization of their respective expressive powers. It is shown, further, that this characterization can be easily carried over to arbitrary first-order definable subclasses of classical first-order models.