Constructive Modal Logics: Bi-nested Calculi and Bi-relational Countermodels
摘要
The logics CK and WK are two fundamental systems of constructive modal logics, which aim to provide an interpretation of modalities with an intuitionistic base. Semantics of these logics can be specified in terms of bi-relational models. We define bi-nested sequent calculi for these two systems. Our calculi are cut-free and only consist of invertible rules. Moreover, they support terminating proof-search under a suitable strategy. The main feature of the calculi is that they allow to directly construct countermodels in the bi-relational semantics from any failed proof.