Some constructive variants of S4 with the finite model property

2021/04/30 by Philippe Balbiani, Balbiani, Philippe, Martín Diéguez +3 · 1 citation
Computer Science · #Advanced Algebra and Logic #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems

paper · doi:10.48550/arxiv.2104.15053

openalex publication_date 2021/04/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Cited by

• Intuitionistic modal logic LIK4 is decidable

Related

• Constructive S4 modal logics with the finite birelational frame property
• Modular Models for Intuitionistic Justification Logic
• A Linear-logical Reconstruction of Intuitionistic Modal Logic S4
• Collapsing Constructive and Intuitionistic Modal Logics
• Intuitionistic modal logic LIK4 is decidable