A proof of the modal collapse (We can derive both $\bigcirc M \supset M$ and $M \supset \bigcirc M$) in a certain Intuitionistic modal logic was given here: Modal collapse upon addition of the law of the excluded middle to an Intuitionistic modal logic. This modal collapse was also discussed here: Can we avoid the modal collapse in a certain Intuitionistic modal logic by abandoning ¬◯⊥ but retaining the law of the excluded middle?

The modal collapse was claimed in https://www.uni-bamberg.de/fileadmin/uni/fakultaeten/wiai_professuren/grundlagen_informatik/papersMM/pll.pdf:

"...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 the above article)

However, I was wondering:

(1) Does the proof of the modal collapse go through if we add the law of the excluded middle and $\neg \bigcirc \bot$ to a classical multiplicative linear logic? (i.e, if we abandon the structural rules of contraction and weakening) and adopt the following rules)

$$ \frac{\qquad }{A \vdash A} \,{Id} $$

$$ \frac{\Gamma\vdash B, \Delta \qquad B, \Gamma'\vdash \Delta'}{\Gamma, \Gamma' \vdash \Delta', \Delta} \,{Cut} $$

$$ \frac{\Gamma\vdash A, \Delta \qquad \Gamma', B\vdash \Delta'}{\Gamma, \Gamma', A \rightarrow B \vdash \Delta, \Delta'} \,{\rightarrow L} $$

$$ \frac{\Gamma, A \vdash B, \Delta}{\Gamma \vdash A \rightarrow B, \Delta} \,{\rightarrow R} $$

$$ \frac{\Gamma \vdash A, \Delta'}{\Gamma \vdash \bigcirc A, \Delta'} \,{\bigcirc R} $$

$$ \frac{\Gamma, A \vdash \bigcirc B, \Delta' \qquad }{\Gamma, \bigcirc A \vdash \bigcirc B, \Delta'} \,{\bigcirc L} $$

(2) Does the proof of the modal collapse go through if we add the law of the excluded middle and $\neg \bigcirc \bot$ to the following sequent calculus but treat $\rightarrow$ as primitive, and not as definable via other connectives, as it usually is in linear logic (in linear logic $\rightarrow$ is usually defined as $\neg A \thinspace \Box \thinspace B$, where we use $\Box$ to denote the multiplicative 'or')

$$ \frac{\qquad }{A \vdash A} \,{Id} $$

$$ \frac{\Gamma\vdash B \qquad B, \Delta\vdash C}{\Gamma, \Delta \vdash C} \,{Cut} $$

$$ \frac{\Delta\vdash A \qquad \Gamma, B\vdash C}{\Gamma, \Delta, A \rightarrow B \vdash C} \,{\rightarrow L} $$

$$ \frac{\Gamma, A \vdash B}{\Gamma \vdash A \rightarrow B} \,{\rightarrow R} $$

$$ \frac{\Gamma \vdash A}{\Gamma \vdash \bigcirc A} \,{\bigcirc R} $$

$$ \frac{\Gamma, A \vdash \bigcirc B \qquad }{\Gamma, \bigcirc A \vdash \bigcirc B} \,{\bigcirc L} $$

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

A proof of the modal collapse (We can derive both $\bigcirc M \supset M$ and $M \supset \bigcirc M$) of $PLL$ obtained by adding the Excluded Middle (EM) and $\neg \bigcirc false$ was given in this answer: Modal collapse upon addition of the law of the excluded middle to an Intuitionistic modal logic.

However, I was wondering:

(1) Does the proof of the modal collapse go through if we add the law of the excluded middle and $\neg \bigcirc \bot$ to a classical multiplicative linear logic? (i.e, if we abandon the structural rules of contraction and weakening) and adopt the following rules)

$$ \frac{\qquad }{A \vdash A} \,{Id} $$

$$ \frac{\Gamma\vdash B, \Delta \qquad B, \Gamma'\vdash \Delta'}{\Gamma, \Gamma' \vdash \Delta', \Delta} \,{Cut} $$

$$ \frac{\Gamma\vdash A, \Delta \qquad \Gamma', B\vdash \Delta'}{\Gamma, \Gamma', A \rightarrow B \vdash \Delta, \Delta'} \,{\rightarrow L} $$

$$ \frac{\Gamma, A \vdash B, \Delta}{\Gamma \vdash A \rightarrow B, \Delta} \,{\rightarrow R} $$

$$ \frac{\Gamma \vdash A, \Delta'}{\Gamma \vdash \bigcirc A, \Delta'} \,{\bigcirc R} $$

$$ \frac{\Gamma, A \vdash \bigcirc B, \Delta' \qquad }{\Gamma, \bigcirc A \vdash \bigcirc B, \Delta'} \,{\bigcirc L} $$

(2) Does the proof of the modal collapse go through if we add the law of the excluded middle and $\neg \bigcirc \bot$ to the following sequent calculus but treat $\rightarrow$ as primitive, and not as definable via other connectives, as it usually is in linear logic (in linear logic $\rightarrow$ is usually defined as $\neg A \thinspace \Box \thinspace B$, where we use $\Box$ to denote the multiplicative 'or')

$$ \frac{\qquad }{A \vdash A} \,{Id} $$

$$ \frac{\Gamma\vdash B \qquad B, \Delta\vdash C}{\Gamma, \Delta \vdash C} \,{Cut} $$

$$ \frac{\Delta\vdash A \qquad \Gamma, B\vdash C}{\Gamma, \Delta, A \rightarrow B \vdash C} \,{\rightarrow L} $$

$$ \frac{\Gamma, A \vdash B}{\Gamma \vdash A \rightarrow B} \,{\rightarrow R} $$

$$ \frac{\Gamma \vdash A}{\Gamma \vdash \bigcirc A} \,{\bigcirc R} $$

$$ \frac{\Gamma, A \vdash \bigcirc B \qquad }{\Gamma, \bigcirc A \vdash \bigcirc B} \,{\bigcirc L} $$