I have two questions. Suppose we have a Hilbert style axiomatic intuitionistic propositional calculus which we supplement with a modal operator $\bigcirc$ (see the bottom of the question for the relation to Category theory), one of the axioms of the operator being $\bigcirc R$ (for formulas $M$):
$$ \bigcirc R: \hspace{0.5cm}M \supset \bigcirc M$$
Suppose have the deduction theorem in our calculus (and the logic is sound and complete) and also that $(MOD)$ holds:
$$(MOD): \hspace{0.8cm} \vdash \bigcirc M \hspace{0.5cm} \textit{implies} \hspace{0.5cm} \vdash M$$
$\textbf{QUESTION 1}$: Do we then, necessarily, have $\bigcirc R^{'}$ also?
$$\bigcirc R^{'} \hspace{0.8cm} \bigcirc M \supset M$$
Fairtlough and Michael Mendler seem to suggest this is not true of a logic they discuss in
- Matt Fairtlough and Michael Mendler, Propositional Lax Logic (1997).
They present PLL (Propositional Lax Logic), a logic (sound and complete relative to a class of Kripke frames) for which $\bigcirc R$, $(MOD)$ and the deduction theorem hold, but write
If we add the axiom of the Excluded Middle and false $\neg \bigcirc false$ (which is valid for both $\diamond$ and $\Box$) to the modal system, $\bigcirc R$$\hspace{0.2cm}[\text{see above}$], $\bigcirc M, \bigcirc S$ [$\text{see below for these principles}$] then $\bigcirc$ becomes trivial. We can derive both $\bigcirc M \supset M$ and $M \supset \bigcirc M$. In other words there is no classical Kripke semantics for $\bigcirc$. In an intuitionistic setting, however, the situation is different. There, modal operators like $\bigcirc$ arise very naturally.
$$\bigcirc M: \hspace{0.8cm} (\thinspace \bigcirc \bigcirc M\thinspace) \supset \bigcirc M$$
$$\bigcirc S: \hspace{0.8cm}(\bigcirc M \land \bigcirc N) \supset \bigcirc(M \land N)$$
$\textbf{QUESTION 2}$: Do we have $M \equiv \bigcirc M$ in their logic? (I take it they are suggesting that we do not have that $M \equiv \bigcirc M$ in their logic)
Maybe those knowledgeable of Category theory or the Lambda calculus could also answer my question, since Fairtlough and Mendler point out a connection between their logic and these two fields:
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 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 $\lambda_c$ (Moggi, 1991)