Modal collapse upon addition of the law of the excluded middle to an Intuitionistic modal logic

Question

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?

Answer 1

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.

Answer 2

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$.