# Axiomatically prove □(A ∨ ¬B), ¬□A, ⊢ ◇¬B in modal system K

This time I have a more "complex" problem at first glance. I need to create a direct proof using the axioms of system K and rules of inference, but I have been unable to do so.

□(A ∨ ¬B), ¬□A, ⊢ ◇¬B

`````` □(A ∨ ¬B),      premise 1
¬□A,            premise 2
□(¬A → ¬B),     introduction of implication
□¬A → □¬B       axiom K
¬¬□¬A → ¬¬□¬B,  double negation of the previous step
¬◇A → ¬◇B
¬¬◇¬A,          from premise 2
◇¬A             elimination of double negation
``````

No matter what I do, I can't find a way to use modus ponens between premise 2 and premise 1 so I only get □¬B from it.

Can anyone help?

• So to paraphrase, if it's necessary that either A or not B, and it's not necessary that A, then not B is possible. Semantically, this should make sense - If all accessible worlds are (Av¬B) worlds, but not all accessible worlds are A worlds, then presumably they include a ¬B world! So it's about finding the right logical tools in K to do this - you'll probably find Distribution and Necessitation can help you set things up! Commented Jun 22, 2023 at 21:49

Please show that these derived rules hold.

(i): ☐(A -> B) -> (◇A -> ◇B)

(ii): ~☐A -> ◇~A.

Now recall that A or B is classically equivalent to ~A -> B.

I'm not the best at modal logics, but I can try my hand at it, at the very least, perhaps it will set you down the right path, here we go:

□(A ∨ ¬B), premise 1

¬□A, premise 2

□(¬¬B → A), the introduction of implication from (1)

□(B → A), simplification

□B → □A, axiom K

¬□B ∨ □A, Demorgan's law [(p→q)≡(¬p∨q)]

¬¬◇¬B ∨ □A, the definition of □

◇¬B ∨ □A, simplification

`````` ◇¬B         (From 2 & the previous step)
``````

I’m not sure that this is satisfactory, but let me know. Thanks

• hey this sounds good. Can you please explain the last two steps (i.e. getting ◇¬B from ◇¬B ∨ □A? Commented Jun 22, 2023 at 21:23
• @ l0ner9 I did that through a disjunctive syllogism. If we have ◇¬B ∨ □A and we also have ¬□A then we can simply follow the format of the simple syllogistic argument: P v Q, ~Q, Therefore P. The same can be done in the last step: ◇¬B ∨ □A; ¬□A; Therefore ◇¬B. Let me know if you have anymore questions. Commented Jun 22, 2023 at 22:16
• could I have added an additional step where I transformed ◇¬B ∨ □A into ¬ □A --> ◇¬B, and used modus ponens with premise two? Commented Jun 22, 2023 at 22:47
• Yes, you could transform it using Demorgan’s law as you have done above and use modus ponens to derive your answer, but that would be a superfluous step. Your professor might subtract points depending on his grading system, but yes, you could most definitely add that extra step. Commented Jun 22, 2023 at 22:51