# Prove or disprove ~◇◻p → ◇◇~p in system K

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. – Jishin Noben Feb 16 '19 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 Feb 17 '19 at 10:10
• Then you should ask "In what modal systems is this formula valid?", not for a proof. – Jishin Noben Feb 17 '19 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 Feb 17 '19 at 11:16

~◇◻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.

https://en.wikipedia.org/wiki/Modal_logic#Axiomatic_systems

Note

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.

• 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 Feb 16 '19 at 14:59
• Thank you very much, I understood this! @SmootQ – saraherceg Feb 16 '19 at 15:34
• You are welcome ^^ – SmootQ Feb 16 '19 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 Feb 17 '19 at 10:14
• 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 Feb 17 '19 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. – Jishin Noben Feb 17 '19 at 23:37
• @JishinNoben: Good point. Added a bit about D, which also suffices here. – Kevin Feb 18 '19 at 6:24