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?