Some constructive variants of S4 with the finite model property

TL;DR

This paper proves that several intuitionistic variants of the modal logic S4, including CS4, GS4, and S4I, possess the finite model property, resolving long-standing open problems.

Contribution

The paper introduces two new logics, GS4 and S4I, related to IS4, and proves that CS4, GS4, and S4I all have the finite model property.

Findings

CS4, GS4, and S4I all enjoy the finite model property.

Introduces GS4 by adding the Godel-Dummett axiom to IS4.

Introduces S4I by reversing modal and intuitionistic relations.

Abstract

The logics CS4 and IS4 are intuitionistic variants of the modal logic S4. Whether the finite model property holds for each of these logics has been a long-standing open problem. In this paper we introduce two logics closely related to IS4: GS4, obtained by adding the Godel-Dummett axiom to IS4, and S4I, obtained by reversing the roles of the modal and intuitionistic relations. We then prove that CS4, GS4, and S4I all enjoy the finite model property.