Constructive S4 modal logics with the finite birelational frame property

TL;DR

This paper proves the finite frame property for several intuitionistic modal logics related to S4, establishing their decidability and providing new birelational semantics, which resolves longstanding open problems.

Contribution

It demonstrates the finite frame property for multiple intuitionistic S4 variants and introduces new birelational semantics, advancing understanding of their decidability.

Findings

Proved finite frame property for CS4 and S4I.

Established strong completeness for Gs4 and Gs4c with birelational semantics.

Showed decidability and NEXPTIME bounds for the logics.

Abstract

The logics $\mathsf{CS4}$ and $\mathsf{IS4}$ are the two leading intuitionistic variants of the modal logic $\mathsf{S4}$. Whether the finite model property holds for each of these logics have been long-standing open problems. It was recently shown that $\mathsf{IS4}$ has the finite frame property and thus the finite model property. In this paper, we prove that $\mathsf{CS4}$ also enjoys the finite frame property. Additionally, we investigate the following three logics closely related to $\mathsf{IS4}$. The logic $\mathsf{GS4}$ is obtained by adding the G\"odel--Dummett axiom to $\mathsf{IS4}$; it is both a superintuitionistic and a fuzzy logic and has previously been given a real-valued semantics. We provide an alternative birelational semantics and prove strong completeness with respect to this semantics. The extension $\mathsf{GS4^c}$ of $\mathsf{GS4}$ corresponds to requiring a crisp accessibility relation on the real-valued semantics. We give a birelational semantics corresponding to an extra confluence condition on the $\mathsf{GS4}$ birelational semantics and prove strong completeness. Neither of these two logics have the finite model property with respect to their real-valued semantics, but we prove that they have the finite frame property for their birelational semantics. Establishing the finite birelational frame property immediately establishes decidability, which was previously open for these two logics. Our proofs yield NEXPTIME upper bounds. The logic $\mathsf{S4I}$ is obtained from $\mathsf{IS4}$ by reversing the roles of the modal and intuitionistic relations in the birelational semantics. We also prove the finite frame property, and thereby decidability, for $\mathsf{S4I}$