Abstract Justification logic is an explication of modal logic: boxes are replaced with proof terms formally through realisation theorems. This can be achieved syntactically using a cut-free proof system for a modal logic, e.g., using sequent, hypersequent, or nested sequent calculi. In constructive modal logic, boxes and diamonds are decoupled and not De Morgan dual. Previous work provides a justification counterpart to constructive modal logic $$\textsf{CK}$$ CK (and some extensions) by making diamonds explicit and introducing new terms called satisfiers. We continue this line of work and provide a justification counterpart to intuitionistic modal logic $$\textsf{IK}$$ IK and its extensions with the $$\textsf{t}$$ t and $$\textsf{4}$$ 4 axioms. We extend the syntax of proof terms to accommodate the additional axioms of intuitionistic modal logic and provide an axiomatisation of these justification logics with a syntactic realisation procedure using a cut-free nested sequent system for intuitionistic modal logic.

Abstract The quest of smoothly combining logics so that connectives from different logics can co-exist in peace has been a fascinating topic of research. In 2015, Dag Prawitz introduced a natural deduction system for an ecumenical first-order logic, unifying classical and intuitionistic logics within a shared language. Building upon this foundation, we introduced, in a series of works, sequent systems for ecumenical logics and modal extensions. In this work we propose a new pure sequent calculus version for Prawitz’s original system, where each rule features precisely one logical operator. This is achieved by extending sequents with an additional context, called stoup, and establishing the ecumenical concept of polarities. We smoothly extend these ideas for handling modalities, presenting a new pure labelled system for ecumenical modal logics. Finally, we show how this allows for naturally retrieving the ecumenical modal nested system proposed in a previous work.

We derive an intuitionistic version of Gödel-Löb modal logic (GL) in the style of Simpson, via proof theoretic techniques. We recover a labelled system, ℓIGL, by restricting a non-wellfounded labelled system for GL to have only one formula on the right. The latter is obtained using techniques from cyclic proof theory, sidestepping the barrier that GL’s usual frame condition (converse well-foundedness) is not first-order definable. While existing intuitionistic versions of GL are typically defined over only the box (and not the diamond), our presentation includes both modalities. Our main result is that ℓIGL coincides with a corresponding semantic condition in birelational semantics: the composition of the modal relation and the intuitionistic relation is conversely well-founded. We call the resulting logic IGL. While the soundness direction is proved using standard ideas, the completeness direction is more complex and necessitates a detour through several intermediate characterisations of IGL.

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 obtain this result by performing proof search in a labelled deductive system that, instead of using only one binary relation on the labels, employs two: one corresponding to the accessibility relation of modal logic and the other corresponding to the order relation of intuitionistic Kripke frames. Our search algorithm outputs either a proof or a finite counter-model, thus, additionally establishing the finite model property for intuitionistic S4, which has been another long-standing open problem in the area.

Abstract A variety of intuitionistic versions of modal logic $$ K $$ have been proposed in the literature. An apparent misconception is that all these logics coincide on their $$\Box $$ -only (or $$\Diamond $$ -free) fragment, suggesting some robustness of ‘ $$\Box $$ -only intuitionistic modal logic’. However in this work we show that this is not true, by consideration of negative translations from classical modal logic: Fischer Servi’s $$ IK $$ proves strictly more $$\Diamond $$ -free theorems than Fitch’s $$ CK $$ , and indeed $$i K $$ , the minimal $$\Box $$ -normal intuitionistic modal logic. On the other hand we show that the smallest extension of $$i K $$ by a normal $$\Diamond $$ is in fact conservative over $$i K $$ (over $$\Diamond $$ -free formulas). To this end, we develop a novel proof calculus based on nested sequents for intuitionistic propositional logic due to Fitting. Along the way we establish a number of new metalogical results.

Abstract The logic of Bunched Implications (BI) freely combines additive and multiplicative connectives, including implications; however, despite its well-studied proof theory, proof-search in BI has always been a difficult problem. The focusing principle is a restriction of the proof-search space that can capture various goal-directed proof-search procedures. In this paper we show that focused proof-search is complete for BI by first reformulating the traditional bunched sequent calculus using the simpler data-structure of nested sequents, following with a polarised and focused variant that we show is sound and complete via a cut-elimination argument. This establishes an operational semantics for focused proof-search in the logic of Bunched Implications.

Abstract Labelled proof theory has been famously successful for modal logics by mimicking their relational semantics within deductive systems. Simpson in particular designed a framework to study a variety of intuitionistic modal logics integrating a binary relation symbol in the syntax. In this paper, we present a labelled sequent system for intuitionistic modal logics such that there is not only one but two relation symbols appearing in sequents: one for the accessibility relation associated with the Kripke semantics for normal modal logics and one for the pre-order relation associated with the Kripke semantics for intuitionistic logic. This puts our system in close correspondence with the standard birelational Kripke semantics for intuitionistic modal logics. As a consequence, it can be extended with arbitrary intuitionistic Scott–Lemmon axioms. We show soundness and completeness, together with an internal cut elimination proof, encompassing a wider array of intuitionistic modal logics than any existing labelled system.