We show that monadic intuitionistic quantifiers admit the following temporal interpretation: “always in the future” (for$\forall $) and “sometime in the past” (for$\exists $). It is well known that Prior’s intuitionistic modal logic${\sf MIPC}$axiomatizes the monadic fragment of the intuitionistic predicate logic, and that${\sf MIPC}$is translated fully and faithfully into the monadic fragment${\sf MS4}$of the predicate${\sf S4}$via the Gödel translation. To realize the temporal interpretation mentioned above, we introduce a new tense extension${\sf TS4}$of${\sf S4}$and provide a full and faithful translation (...) of${\sf MIPC}$into${\sf TS4}$. We compare this new translation of${\sf MIPC}$with the Gödel translation by showing that both${\sf TS4}$and${\sf MS4}$can be translated fully and faithfully into a tense extension of${\sf MS4}$, which we denote by${\sf MS4.t}$. This is done by utilizing the relational semantics for these logics. As a result, we arrive at the diagram of full and faithful translations shown in Figure 1 which is commutative up to logical equivalence. We prove the finite model property (fmp) for${\sf MS4.t}$using algebraic semantics, and show that the fmp for the other logics involved can be derived as a consequence of the fullness and faithfulness of the translations considered. (shrink)

The Gödel translation provides an embedding of the intuitionistic logic$\mathsf {IPC}$into the modal logic$\mathsf {Grz}$, which then embeds into the modal logic$\mathsf {GL}$via the splitting translation. Combined with Solovay’s theorem that$\mathsf {GL}$is the modal logic of the provability predicate of Peano Arithmetic$\mathsf {PA}$, both$\mathsf {IPC}$and$\mathsf {Grz}$admit provability interpretations. When attempting to ‘lift’ these results to the monadic extensions$\mathsf {MIPC}$,$\mathsf {MGrz}$, and$\mathsf {MGL}$of these logics, the same techniques no longer work. Following a conjecture made by Esakia, we add an appropriate version (...) of Casari’s formula to these monadic extensions (denoted by a ‘+’), obtaining that the Gödel translation embeds$\mathsf {M^{+}IPC}$into$\mathsf {M^{+}Grz}$and the splitting translation embeds$\mathsf {M^{+}Grz}$into$\mathsf {MGL}$. As proven by Japaridze, Solovay’s result extends to the monadic system$\mathsf {MGL}$, which leads us to a provability interpretation of both$\mathsf {M^{+}IPC}$and$\mathsf {M^{+}Grz}$. (shrink)

MIPC is a well-known intuitionistic modal logic of Prior and Bull . It is shown that every normal intuitionistic modal logic L over MIPC has the finite model property whenever L is Kripke-complete and universal.

The paper considers the set ML 1 of first-order polymodal formulas the modal operators in which can be applied to subformulas of at most one free variable. Using a mosaic technique, we prove a general satisfiability criterion for formulas in ML 1 , which reduces the modal satisfiability to the classical one. The criterion is then used to single out a number of new, in a sense optimal, decidable fragments of various modal predicate logics.

Conditional logics have traditionally been intended to formalize various intuitively correct modes of reasoning involving conditional expressions in natural language. Although conditional logics have by now been thoroughly studied in a classical context, they have yet to be systematically examined in an intuitionistic context, despite compelling philosophical and technical reasons to do so. This paper addresses this gap by thoroughly examining the basic intuitionistic conditional logic ICK, the intuitionistic counterpart of Chellas’ important classical system CK. I give ICK both worlds (...) semantics and algebraic semantics, and prove that these are equivalent. I give a Gödel-type embedding of ICK into CK and a Glivenko-type embedding of CK into ICK. I axiomatize ICK and prove soundness, completeness, and decidability results. Finally, I discuss extending ICK. (shrink)

Intuitionistic modal logics are extensions of intuitionistic propositional logic with modal axioms. We treat with two modal languages ${\mathscr{L}}_\Diamond $ and $\mathscr{L}_{\Diamond,\Box }$ which extend the intuitionistic propositional language with $\Diamond $ and $\Diamond,\Box $, respectively. Gentzen sequent calculi are established for several intuitionistic modal logics. In particular, we introduce a Gentzen sequent calculus for the well-known intuitionistic modal logic $\textsf{MIPC}$. These sequent calculi admit cut elimination and subformula property. They are decidable.

In this paper we study natural deduction for the intuitionistic and classical (normal) modal logics obtained from the combinations of the axioms T, B, 4 and 5. In this context we introduce a new multi-contextual structure, called T-sequent, that allows to design simple labelfree natural deduction systems for these logics. After proving that they are sound and complete we show that they satisfy the normalization property and consequently the subformula property in the intuitionistic case.