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?


2 Answers 2


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, 2018 at 20:00
  • $\begingroup$ If you could add proof steps it would be much appreciated! :) $\endgroup$
    – user65526
    Mar 28, 2018 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, 2018 at 20:40
  • $\begingroup$ Are any structural laws (weakening, etc) utilised in the above proof? $\endgroup$
    – user65526
    Mar 28, 2018 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$ Mar 28, 2018 at 21:27

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$.
  • $\begingroup$ Great but I don't think "usually" is a good reading of $\bigcirc$, for the would mean that "If I win the lottery then it is is usual that I win the lottery" by the injection axiom. $\endgroup$
    – user65526
    Apr 20, 2022 at 20:27
  • $\begingroup$ @user65526: Yes, I agree it’s not a terribly good reading. Unfortunately I’ve never found a satisfactory intuitive reading for modalities satisfying this combination of axioms (even though they’re very important in several topics I’m interested in, e.g. topos theory). Alternative suggestions are very welcome indeed… $\endgroup$ Apr 21, 2022 at 10:20
  • $\begingroup$ Perhaps an ability modal where propositional letters are restricted the actions performed by some fixed agent, so that the injection reads "If I perform an action then I am able to perform that action", and the other axioms read "If I am able to make it the case that I am able to make it the case that I perform an action, then I am able to perform the action. The third axiom is more tricky on this reading perhaps, for their may be mutually exclusive actions. But it seems reasonable for many actions that if I am able to perform an action in a fixed context and am able to perform another action $\endgroup$
    – user65526
    Apr 22, 2022 at 11:07
  • $\begingroup$ ...in that same context, then I am able to perform an action consisting of both the actions. Incidentally, we know from natural language theory that ability modals don't necessarily distributive over disjunction (see the paper by Rick Nouwen in Semantics and Pragmatics). $\endgroup$
    – user65526
    Apr 22, 2022 at 11:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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