Consider Propositional Lax Logic ($PLL$)

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?


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.

  • $\begingroup$ Does the law of the excluded middle enter into this proof implicitly anywhere? Also, I don't understand why you write "so by (*) it suffices to obtain"? Couldn't the reduction work with the formula presented immediately before this remark? Also, does this proof go through in the Linear version of the logic above, discussed here: math.stackexchange.com/questions/2395602/… ? I suspect it might not, since I think (!) you don't have the converse of Axiom S, which was used in your proof. $\endgroup$ – user65526 Mar 28 '18 at 20:00
  • $\begingroup$ If you could add proof steps it would be much appreciated! :) $\endgroup$ – user65526 Mar 28 '18 at 20:01
  • $\begingroup$ Fantastic. So the proof wouldn't go through with Intuitionistic linear logic, I think, as in the link above, since I think Axiom S doesn't hold in it.math.stackexchange.com/questions/2395602/… $\endgroup$ – user65526 Mar 28 '18 at 20:40
  • $\begingroup$ Are any structural laws (weakening, etc) utilised in the above proof? $\endgroup$ – user65526 Mar 28 '18 at 20:41
  • $\begingroup$ @user65526 I don't know much about structural laws... does it even matter whether you use them, given that you're using Law of Excluded Middle (and hence are not intuitionistic anymore)? $\endgroup$ – Bjørn Kjos-Hanssen Mar 28 '18 at 21:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.