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
Philosophy Stack Exchange is a question and answer site for those interested in the study of the fundamental nature of knowledge, reality, and existence. It only takes a minute to sign up.Sign up to join this community
~◇◻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.
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:
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.