My question regards the Curry Howard Isomorphism and how it constrains models in the case of a particular logic.
Consider quantified Lax Logic $QLL$.
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$"):
$$\text{Axiom} \bigcirc R: \hspace{0.5cm}M \supset \bigcirc M$$ $$\text{Axiom} \bigcirc M: \hspace{0.8cm} (\thinspace \bigcirc \bigcirc M\thinspace) \supset \bigcirc M$$ $$\text{Axiom} \bigcirc S: \hspace{0.8cm}(\bigcirc M \land \bigcirc N) \supset \bigcirc(M \land N)$$
$\bigcirc$ behaves in some ways like a necessity modal, and in some ways like a possibility modal (Axioms $\bigcirc R$ and $\bigcirc M$ are typical of a modality of possibility $\Diamond$, while $\bigcirc S$ is typical for necessity $\Box$); in fact, there exists a translation of the logic into bimodal (S4, S4) which is based on the Godel translation of intuitionistic logic into the classical modal logic S4, and the translation of the modal operator $\bigcirc$ of $PLL$ into classical bimodal (S4 S4) (given at the bottom of the question) brings out the fact that it behaves in some respects like a necessity operator and in others like a possibility operator. (In addition,there also exists a translation of Lax logic into the underlying Intuitionistic logic, given here:https://link.springer.com/content/pdf/10.1007%2F3-540-45620-1.pdf: p.78)
$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.
Recently, Lax logic has been used by computational linguists (including myself and colleagues) in order to give a semantic theory for natural language. It is usual practice in natural language semantic theory to treat the simply typed lambda calculus as part of a classical higher order logic or type theory, as for example in the work of Montague and his student Gallin (see https://www.elsevier.com/books/intensional-and-higher-order-modal-logic/gallin/978-0-7204-0360-2 [1975]) The logic is higher order in that quantification and lambda abstraction is permitted over entities of all types (i.e, if ϕ is a formula and x is a variable of any type, then ∀x ϕ is a formula and if A is a term of type β and x is a variable of type α, then λx (A) is a term of type αβ;)
The standard semantics given for higher-order logics of this kind is a possible world semantics, which we briefly review for the case of Gallin's TY2.
Gallin’s TY2 has two ground types:
• $s$, which stands for world-time pairs
• $e$, which is the type of (possible) individuals or entities (individuals which exist in some possible world at some point in time)
Complex types are built up as follows:
(1) (TY2 types) The set of TY2 types is the smallest set of strings such that:
i. $e, s$ and $t$ are TY2 types;
ii. if α and β are TY2 types, then (αβ) is a TY2 type
Models for the logic are based on hierarchies of typed domains, as defined below:
(2) (TY2 frames) A TY2 frame is a set {$D_α$ | α is a TY2 type} such that:
• $D_e \neq ∅$
• $D_s \neq ∅$
• $D_t = {0, 1}$
• $D_{αβ} ⊆ \{F | F : D_α → D_β\}$ for each type $αβ$
(3) A TY2 frame is standard if $D_{αβ} = \{ F | F : D_α → D_β \}$ for each type $αβ$
A standard model for TY2 is is a tuple (F, I) where F is a standard frame and I is an interpretation function for F.
I have the following questions. Consider the lambda side corresponding to the lax logic via the Curry Howard Isomorphism. Is it possible to supply a model theory with a possible world semantics of Gallin variety (i.e a possible world semantics for higher order logic) for the lambda calculus augmented with a monad which corresponds to Lax Logic? Could we use the same classical bimodal (S4, S4) models into which Lax Logic can be translated as models for the computational lambda calculus of Moggi? Could we provide an intuitionistic version of Gallin's theory for the lambda side? More generally, what constraints on models does the Curry Howard impose on the lambda side of the terms $t:A$? Does it require that the lambda side be given an intuitionistic semantics?
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)
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)$
We now translate every formula $M$ of $PLL$ into a bimodal formula $M^g$. Let $f$ be a distinguished propositional constant and A range over propositional constants (The trick of using a distinguished propositional constant $f$ is borrowed from Johansson 1936 (http://www.numdam.org/article/CM_1937__4__119_0.pdf) who used it to embed intuitionistic logic into minimal logic):
$$false^g = \Box_i f$$
$$A^g = \Box_i(A \lor f ) $$
$$(M \land N)^g =M^g \land N^g $$
$$(M \lor N)^g =M^g \lor N^g $$
$$(M \supset N)^g =\Box_i(M^g \supset N^g ) $$
$$(\bigcirc M)^g = \Box_i \Diamond_m M^g$$
