Collapsing Constructive and Intuitionistic Modal Logics

TL;DR

This paper proves that the constructive and intuitionistic variants of the modal logic KB are equivalent, contrasting with previous results on the non-equivalence of variants of K, highlighting differences in modal logic variants.

Contribution

It establishes the equivalence of constructive and intuitionistic KB, providing new insights into the relationship between these modal logic variants.

Findings

Constructive and intuitionistic KB are equivalent.

Contrasts with previous results on K variants.

Highlights differences in modal logic variants.

Abstract

We prove that the constructive and intuitionistic variants of the modal logic $\mathsf{KB}$ coincide. This result contrasts with a recent result by Das and Marin, who showed that the constructive and intuitionistic variants of $\mathsf{K}$ do not prove the same diamond-free formulas.