This talk is devoted to modal logics by Grigore Moisil, one of pioniers of computer science and of algebraic logic. In 1942, G. Moisil developed a series of modal logics motivated by—at the time—quite novel considerations. As it turns out these logics are closely connected to some now well-known non-classical logics. The aim of our work is to shed some light on Moisil's work, outline these connections and to supplement formal proofs to some facts Moisil seems to have envisioned. The novelty of Moisil's approach was to associate a logic not with a single matrix but with a class of algebraic systems, namely, the class of bi-residuated lattices, which contain residual operations with respect to both the join (represented by the implication connective) and the meet (represented by the difference connective) operations. This system, which we denote here BiM, turns out to be equivalent to C. Rauszer's logic HB, which, in turn, is a conservative extension of intuitionistic propositional logic with the difference connective. In this way Moisil has anticipated by more than thirty years the development of bi-intuitionistic logic. This logic is also related to Dummett's linear logic and to Gödel-Smetanich (here-and-there) logic via its special and three-valued extensions, respectively. Finally, Moisil has shown that three-valued Łukasewicz logic can be defined within the three-valued BiM-extension.
The modal aspect of Moisil's paper comes in the form of the general modal logic GML, which conservatively extends BiM with operators of impossibility, contingency, possibility, and necessity definable via implication and difference connectives. This logic makes clear how different Moisil's view of modalities was compared to the modern one. Motivated by this fact we compare Mosil's approach to modal logic with the one by J. Łukasiewicz and K. Došen.
The final logic from Moisil's paper we are interested in is the general symmetric modal logic GSML, which is obtained by adding to GML an involutive and contrapositive negation motivated by the properties of Łukasiewicz's negation. As Moisil himself pointed out, the difference connective becomes definable via negation and implication in GSML, illuminating the connection of GSML to both Heyting-Ockham logic N* and the logic HYPE suggested recently by Leitgeb as a basic logic of hyperintensional contexts. These connections were already discussed in the 2021 paper by Odintsov and Wansing and we elaborate on them here.