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}$

翻译：逻辑 $\mathsf{CS4}$ 和 $\mathsf{IS4}$ 是模态逻辑 $\mathsf{S4}$ 的两种主要直觉主义变体。这些逻辑是否具有有限模型性质一直是长期未决的开放问题。最近研究表明 $\mathsf{IS4}$ 具有有限框架性质，从而具备有限模型性质。本文证明 $\mathsf{CS4}$ 也享有有限框架性质。此外，我们研究了与 $\mathsf{IS4}$ 密切相关的以下三种逻辑：逻辑 $\mathsf{GS4}$ 是通过在 $\mathsf{IS4}$ 中添加歌德尔-达米特公理得到的；它既是超直觉主义逻辑又是模糊逻辑，此前已具有实数值语义。我们为其提供了一种替代的双关系语义，并证明了与该语义相关的强完备性。逻辑 $\mathsf{GS4}$ 的扩展 $\mathsf{GS4^c}$ 对应在实数值语义上要求清晰的可达关系。我们在 $\mathsf{GS4}$ 双关系语义基础上给出了额外汇合条件对应的双关系语义，并证明了强完备性。这两种逻辑在其实数值语义下都不具有有限模型性质，但我们证明它们在其双关系语义下具有有限框架性质。建立有限双关系框架性质立即确立了可判定性，这此前对这两种逻辑是开放问题。我们的证明给出了NEXPTIME上界。逻辑 $\mathsf{S4I}$ 是通过在双关系语义中交换模态关系和直觉主义关系的角色从 $\mathsf{IS4}$ 得到的。我们还证明了 $\mathsf{S4I}$ 的有限框架性质，从而其可判定性。