Substructural Logic of Proofs

Abstract

In this paper, we introduce substructural variants of Artemov’s logic of proofs. We show a few things here. First, we introduce a bimodal logic that has both the exponential operator in linear logic and an S4 modal operator which does not bring in any structural feature. Both Girard’s embedding and Gödel’s modal embedding (not the double negation translation) are used to directly connect intuitionistic substructural logics and substructural logics with the involutive negation. Second, we formulate substructural logic of proofs, which is an explicit counterpart of the foregoing bimodal substructural logics, and show that the substructural logic of proofs can realize the bimodal substructural logic, following the idea of [1]. Third, adopting the idea of Yu [10], we also show that the contraction-free, multiplicative S4-fragment of the bimodal substructural logic is realizable without appealing to a so-called “self-referential constant specification.”