Related papers: A Bi-nested Calculus for Intuitionistic K: Proofs …
We introduce FIK, a natural intuitionistic modal logic specified by Kripke models satisfying the condition of forward confluence. We give a complete Hilbert-style axiomatization of this logic and propose a bi-nested calculus for it. The…
We investigate intuitionistic modal logics with locally interpreted $\square$ and $\lozenge$. The basic logic LIK is stronger than constructive modal logic WK and incomparable with intuitionistic modal logic IK. We propose an axiomatization…
This paper studies the relationship between labelled and nested calculi for propositional intuitionistic logic, first-order intuitionistic logic with non-constant domains and first-order intuitionistic logic with constant domains. It is…
We introduce a monotone modal analogue of the intuitionistic (normal) modal logic IK using a translation into a suitable (intuitionistic) first-order logic. We axiomatise the logic and give a semantics by means of intuitionistic…
We study an intuitionistic version of common knowledge logic (CK), called ICK, which was introduced by J\"ager and Marti. ICK extends intuitionistic propositional logic (IPL) by multiple box modalities interpreted as knowledge operators for…
Bi-intuitionistic logic is the conservative extension of intuitionistic logic with a connective dual to implication. It is sometimes presented as a symmetric constructive subsystem of classical logic. In this paper, we compare three sequent…
In this work, we explore proof theoretical connections between sequent, nested and labelled calculi. In particular, we show a general algorithm for transforming a class of nested systems into sequent calculus systems, passing through linear…
We present a labelled and non-wellfounded calculus for the bimodal provability logic CS. The system is obtained by modelling the Kripke-like semantics of this logic. As in arXiv:2309.00532, we enforce the second-order property of converse…
Bi-intuitionistic logic is the extension of intuitionistic logic with a connective dual to implication. Bi-intuitionistic logic was introduced by Rauszer as a Hilbert calculus with algebraic and Kripke semantics. But her subsequent…
We consider an extension of bi-intuitionistic logic with the traditional modalities from tense logic Kt. Proof theoretically, this extension is obtained simply by extending an existing sequent calculus for bi-intuitionistic logic with…
Intuitionistic grammar logics fuse constructive and multi-modal reasoning while permitting the use of converse modalities, serving as a generalization of standard intuitionistic modal logics. In this paper, we provide definitions of these…
This paper shows how to derive nested calculi from labelled calculi for propositional intuitionistic logic and first-order intuitionistic logic with constant domains, thus connecting the general results for labelled calculi with the more…
We introduce an intuitionistic modal logic strictly contained in the intuitionistic modal logic IK and being an appropriate candidate for the title of ``minimal normal intuitionistic modal logic''.
Justification logics are modal-like logics that provide a framework for reasoning about justifications. This paper introduces labeled sequent calculi for justification logics, as well as for hybrid modal-justification logics. Using the…
In this paper we demonstrate decidability for the intuitionistic modal logic S4 first formulated by Fischer Servi. This solves a problem that has been open for almost thirty years since it had been posed in Simpson's PhD thesis in 1994. We…
We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this method for classical tense logic, its extensions with path…
In this note, by integrating ideas concerning terminating tableaux-based procedures in modal logics and finite frame property of intuitionistic modal logic IK, we provide new and simpler decidability proofs for FIK and LIK.
We present a family of paraconsistent counterparts of the constructive modal logic CK. These logics aim to formalise reasoning about contradictory but non-trivial propositional attitudes like beliefs or obligations. We define their…
We introduce a basic intuitionistic conditional logic $\mathsf{IntCK}$ that we show to be complete both relative to a special type of Kripke models and relative to a standard translation into first-order intuitionistic logic. We show that…
We introduce and study single-conclusioned nested sequent calculi for a broad class of intuitionistic multi-modal logics known as "intuitionistic grammar logics (IGLs)." These logics serve as the intuitionistic counterparts of classical…