Modal collapse upon addition of the law of the excluded middle to an Intuitionistic modal logic Consider Propositional Lax Logic ($PLL$)


*

*https://www.uni-bamberg.de/fileadmin/uni/fakultaeten/wiai_professuren/grundlagen_informatik/papersMM/pll.pdf
The Hilbert system of $PLL$ takes as axiom schemata all theorems of (or a complete set of axioms for) the Intuitionistic propositional calculus plus the modal axiom schemata $\bigcirc R, \bigcirc M, \bigcirc S$ below. The inference rules are 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)$$
The authors of the above article write that the modal $\bigcirc$ becomes trivial if we add the law of the excluded middle and $\neg \bigcirc false$ to the logic:

"...if we add the axiom of the Excluded Middle (EM) and $\neg \bigcirc false$ which is valid for both $\Diamond$ and $\Box$ to the modal system $\bigcirc R, \bigcirc M, \bigcirc S$ 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$." (p.4, para 1 of above article)

I do not understand how we are able to derive both $\bigcirc M \supset M$ and $M \supset \bigcirc M$ if we add the law of the excluded middle and $\neg \bigcirc false$ to the logic. 
Can anyone help me with this matter?
 A: I'll write $\to$ instead of $\supset$, and $\bot$ instead of false, below.
Since Law of Excluded Middle is given, I'll argue using classical propositional logic.
Since $M\to\bigcirc M$ is already given as Axiom $\bigcirc$R, let's prove $$\bigcirc M\to M.$$
We are given
$$\neg\bigcirc\bot.\tag{*}$$
First, by Axiom $\bigcirc R$,
$$\neg M\wedge\bigcirc M\to\bigcirc \neg M\wedge\bigcirc M.$$
Therefore by $\bigcirc S$, 
$$\neg M\wedge\bigcirc M\to\bigcirc (\neg M\wedge M)$$
Therefore by definition of $\bot$,
$$\neg M\wedge\bigcirc M\to\bigcirc\bot$$
By (*),
$$\neg(\neg M\wedge\bigcirc M)$$
By de Morgan and law of excluded middle,
$$M\vee \neg\bigcirc M$$
So,
$$\bigcirc M\to M$$

Note that Axiom $\bigcirc M$ was not needed.

A: Bjørn Kjos-Hanssen’s answer gives a good concise symbolic proof; but it seems also worth giving the argument in prose as well, to explain the idea more readably.  I will write “$\bigcirc$” as “usually”.
Consider a proposition $A$; we want to show “usually $A$” is equivalent to $A$.  One direction is precisely the axiom $(\bigcirc M)$; it just remains to show that “usually $A$” implies $A$.  In classical logic, it suffices to show that if A usually holds, then $A$ cannot fail.
So: assume $A$ usually holds, but $A$ fails.  Axiom $(\bigcirc M)$ tells us then that $A$ usually fails (i.e. $\bigcirc \lnot A$).  So $A$ usually holds, and $A$ usually fails; so by axiom $(\bigcirc S)$, $A$ usually both holds and fails.  By monotonicity of “usually” (the rule you mention after modus ponens), this tells us we usually have a contradiction — but the assumption of $\lnot {\bigcirc} \bot$ says precisely that this can’t be the case.
This concludes the proof.  A few notes:

*

*As Bjørn notes, the axiom $(\bigcirc C)$ was never needed.

*The key culprit is axiom $(\bigcirc S)$, that if A and B each usually hold, then both together usually hold. This is the only axiom that tells us to read $\bigcirc$ as something like “usually”, rather than as “possibly”.

*The only use of classical logic was the assumption that “if $A$ does not fail, then $A$ holds”.  So we can see this proof in the purely intuitionistic system as a proof that if $A$ satisfies that property (i.e. if $A$ is stable) — or, a fortiori, if either $A$ or $\lnot A$ holds (i.e. $A$ is decidable) — then “usually $A$” is equivalent to $A$.

