Abstract

Subintuitionistic logics are the weakenings of intuitionistic propositional calculus. While intuitionistic logic receives a lot of attention, the logics that are obtained from structural weakening, dropping the intuitionistic restrictions, which are persistence, reflexivity, and transitivity on the Kripke frames, are not widely studied. For the first time, we aim to enrich the language of subintuitionistic logic with modal operators. We take an approach to modeltheoretic semantics by equipping the models with two relations <∗ and R, where <∗ acts like the accessibility relations in intuitionistic logics, and substructural logics, and R acts like the accessibility relations in modal logic. This way we can strengthen and weaken the logic both at the intuitionistic level, and the modal level by changing the conditions on the accessibility relation. We give a natural deduction system for these logics. Soundness and Completeness results are proven for the logics that are generated, and we prove that the logics that are generated are distinct. We observe that there does not seem to be good introduction, and elimination rules for the intuitionistic if-then connective in our logic that corresponds to Kripke frames without reflexivity, transitivity, and persistence using standard techniques of formalizing natural deduction. We propose a different deductive calculus for this logic by marking our formulas with ”step-markers”, either 0 or 1, where 0 indicates the formula is actually true, and 1 indicates the formula is true in every accessible world.