How to start with the following proof? Any help would be appreciated. I have tried by assuming the left side is true, however, I get confused with the negation.

~◇◻p → ◇◇~p
  • This is impossible to answer unless you specify the proof system you want to construct your proof in. Commented Feb 16, 2019 at 23:02
  • The question is more regarding if it holds in all the cases. Is there a counter-example where this formula fails, where left is true and right side false? @JishinNoben
    – saraherceg
    Commented Feb 17, 2019 at 10:10
  • Then you should ask "In what modal systems is this formula valid?", not for a proof. Commented Feb 17, 2019 at 11:08
  • @JishinNoben Sorry, that is my bad then. The exercises just stated to prove it or disprove it. It is actually considering the system K. Thanks for the note
    – saraherceg
    Commented Feb 17, 2019 at 11:16

2 Answers 2


~◇◻P → ◇◇~P

Following is the proof.

 - ~◇◻P
 - ∴ ◻~◻P
 - ∴ ◻◇~P

From ◻◇~P we can apply an axiom from Modal System D, stating that everything that is necessary is also possible, that is if P is necessarily the case then P cannot be impossible.

D: ◻A → ◇A

Then from ◻◇~P using Axiom D, it follows that : ◇◇~P

You can find an application of System D to modal Deontic logic here : https://plato.stanford.edu/entries/logic-modal/#DeoLog , but the same applies to alethic logic too.

I suggest reading about System D on wikipedia :



You should have specified the system in which you want to prove it, although I proved it using System D, it is up to you to see if this is what you want.

  • 1
    Of course you should have specified the system in which you want to prove it ... If you happen to solve it in System S4, then you will be able to drop one diamond : ◇ , and conclude that ◇~P
    – SmootQ
    Commented Feb 16, 2019 at 14:59
  • 1
    Thank you very much, I understood this! @SmootQ
    – saraherceg
    Commented Feb 16, 2019 at 15:34
  • You are welcome ^^
    – SmootQ
    Commented Feb 16, 2019 at 15:49
  • Regarding your note, this question was asked as in, if you can find one counterexample, where the left side is true and right side false then it is enough to disprove it. However, this formula should always be true, right? Thanks! @SmootQ
    – saraherceg
    Commented Feb 17, 2019 at 10:14
  • 1
    Sorry, my bad that I did not specify it before.. the exercises just stated to prove or disprove but I see that it is considering the system K! So, in system K, it is not possible to prove this? Will it be ok to consider a world only having a 'p' as a counterexample? Thank you so much for your explanations! @SmootQ
    – saraherceg
    Commented Feb 17, 2019 at 11:15

You surely cannot do this in System K.

Instead of focusing on symbol manipulation, it's important to understand the semantics of these sentences. System K is a normal modal logic, so we may dispense with axioms and focus on the frame conditions instead:

  1. ~◇◻P is saying that there is no accessible world W, such that every world that W can access satisfies P.
  2. ◇◇~P is saying that there is an accessible world W', such that W' can access some world that does not satisfy P.

What does it mean for #1 to imply #2? Well, for a start, it means that there are accessible worlds, since #1 does not assert that any world is accessible while #2 does. Secondly, those worlds are not "dead ends"; they themselves can access worlds.

Both of those properties are trivially satisfied by System T, in which accessibility is reflexive (so each world can, at a minimum, access itself), and by System D, in which accessibility is not necessarily reflexive but nevertheless cannot have dead ends (i.e. it is a serial relation). But System K does not guarantee "no dead ends" in the accessibility relation, because System K makes no guarantees about the accessibility relation at all. So you will not be able to prove this from within System K.

  • +1 for the semantical view. D is weaker than T, and already enough to prove the formula. Commented Feb 17, 2019 at 23:37
  • 1
    @JishinNoben: Good point. Added a bit about D, which also suffices here.
    – Kevin
    Commented Feb 18, 2019 at 6:24

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .