Correspondence Theory for Modal Fairtlough-Mendler Semantics of Intuitionistic Modal Logic

TL;DR

This paper develops a correspondence theory for intuitionistic modal logic within modal Fairtlough-Mendler semantics, extending the ALBA algorithm to this setting and analyzing the interpretation of nominals without using diamonds or conominals.

Contribution

It introduces a novel semantic framework for intuitionistic modal logic and adapts the ALBA algorithm, highlighting the interpretation of nominals as refined regular open closures.

Findings

ALBA is sound for modal FM frames.

ALBA succeeds on inductive formulas in this setting.

Nominals are interpreted as refined regular open closures.

Abstract

We study the correspondence theory of intuitionistic modal logic in modal Fairtlough-Mendler semantics (modal FM semantics) \cite{FaMe97}, which is the intuitionistic modal version of possibility semantics \cite{Ho16}. We identify the fragment of inductive formulas \cite{GorankoV06} in this language and give the algorithm $\mathsf{ALBA}$ \cite{CoPa12} in this semantic setting. There are two major features in the paper: one is that in the expanded modal language, the nominal variables, which are interpreted as atoms in perfect Boolean algebras, complete join-prime elements in perfect distributive lattices and complete join-irreducible elements in perfect lattices, are interpreted as the refined regular open closures of singletons in the present setting, similar to the possibility semantics for classical normal modal logic \cite{Zh21d}; the other feature is that we do not use conominals or diamond, which restricts the fragment of inductive formulas significantly. We prove the soundness of the $\mathsf{ALBA}$ with respect to modal FM frames and show that the $\mathsf{ALBA}$ succeeds on inductive formulas, similar to existing settings like \cite{CoPa12,Zh21d,Zh22a}.