Return to Question

This is an intuitionistic modal logic consisting of the usual axioms for intuitionistic logic to which is adjoined a modal operator $\bigcirc$, obeying the following axioms (plus proof rule Modus Ponens and the rule "from $M \rightarrow N$ infer $\bigcirc M \rightarrow \bigcirc N$"):

The bimodal (S4, S4) logic into which we can translate lax logic has the usual propositional connectives together with two dual pairs of modalities $\Box_i, \Diamond_m, \Box_ m, \Diamond_ m$. A bimodal model is a Kripke structure $M=(W, R_m , R_i , V)$ where $W$ is a nonempty set, $R_i , R_m$ are binary relations on $W$, and $V$ is a map that assigns to every propositional constant $A$ a subset $V(A) \in W$. The modal axioms obeyed by the logic are the usual K,T and 4 axioms of S4, except that we have K, T and 4 axioms for both modals $\Box_i$ and $\Box_m$ (for example the K axioms splits into $Ki : \Box_i(M \rightarrow N) \rightarrow \Box_i M \rightarrow \Box_i N$ and $K_m : \Box_m(M \rightarrow N) \rightarrow \Box_m M \rightarrow \Box_m N)$

$$(M \rightarrow N)^g =\Box_i(M^g \rightarrow N^g ) $$

This is an intuitionistic modal logic consisting of the usual axioms for intuitionistic logic to which is adjoined a modal operator $\bigcirc$, obeying the following axioms (plus proof rule Modus Ponens and the rule "from $M \supset N$ infer $\bigcirc M \supset \bigcirc N$"):

The bimodal (S4, S4) logic into which we can translate lax logic has the usual propositional connectives together with two dual pairs of modalities $\Box_i, \Diamond_m, \Box_ m, \Diamond_ m$. A bimodal model is a Kripke structure $M=(W, R_m , R_i , V)$ where $W$ is a nonempty set, $R_i , R_m$ are binary relations on $W$, and $V$ is a map that assigns to every propositional constant $A$ a subset $V(A) \in W$. The modal axioms obeyed by the logic are the usual K,T and 4 axioms of S4, except that we have K, T and 4 axioms for both modals $\Box_i$ and $\Box_m$ (for example the K axioms splits into $Ki : \Box_i(M \supset N) \supset \Box_i M \supset \Box_i N$ and $K_m : \Box_m(M \supset N) \supset \Box_m M \supset \Box_m N)$

$$(M \supset N)^g =\Box_i(M^g \supset N^g ) $$

So as to make this question easier to answer for those unfamiliar with Lax Logic, below I give at the bottom of my question the bimodal translation of lax logic into bimodal (S4, S4)

So as to make this question easier to answer for those unfamiliar with Lax Logic, below I give at the bottom of my question the translation of lax logic into bimodal (S4, S4)

$QLL$ corresponds via the Curry Howard isomorphism to a the computational lambda calculus of Moggi (we write $t : A$, to denote that the lambda term $t$ that corresponds via the Curry Howard Isomorphism to the formula of lax logic $A$): that is, the computational lambda calculus contains a unary type-constructor $T$ such that the denotation of a program computing values of type $A$ is itself of type $TA$ and the formal properties of $\bigcirc$, viewed as an unary type constructor give precisely the data of a strong monad familiar from category theory. In fact, the propositions-as-types principle which yields an equivalence between the Intuitionistic Propositional Calculus (IPC) and bi-Cartesian closed categories can be extended to an equivalence between IPC extended by $\bigcirc$ and bi-Cartesian closed categories with a strong monad. This categorical structure is also known as the computational lambda calculus (Moggi, 1991) Moggi showed that computational lambda calculus was sound and complete with respect to models consisting of a cartesian closed category with finite coproducts and a strong monad.

$QLL$ corresponds via the Curry Howard isomorphism to the computational lambda calculus of Moggi (we write $t : A$, to denote that the lambda term $t$ that corresponds via the Curry Howard Isomorphism to the formula of lax logic $A$): that is, the computational lambda calculus contains a unary type-constructor $T$ such that the denotation of a program computing values of type $A$ is itself of type $TA$ and the formal properties of $\bigcirc$, viewed as an unary type constructor give precisely the data of a strong monad familiar from category theory. In fact, the propositions-as-types principle which yields an equivalence between the Intuitionistic Propositional Calculus (IPC) and bi-Cartesian closed categories can be extended to an equivalence between IPC extended by $\bigcirc$ and bi-Cartesian closed categories with a strong monad. This categorical structure is also known as the computational lambda calculus (Moggi, 1991) Moggi showed that computational lambda calculus was sound and complete with respect to models consisting of a cartesian closed category with finite coproducts and a strong monad.