0

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?

Improve this question
1
  • 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!
    – Paul Ross
    Jun 22 at 21:49

2 Answers 2

Reset to default
2

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.

Improve this answer
0

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

Improve this answer
4
  • 1
    hey this sounds good. Can you please explain the last two steps (i.e. getting ◇¬B from ◇¬B ∨ □A?
    – l0ner9
    Jun 22 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.
    – Max Maxman
    Jun 22 at 22:16
  • 1
    could I have added an additional step where I transformed ◇¬B ∨ □A into ¬ □A --> ◇¬B, and used modus ponens with premise two?
    – l0ner9
    Jun 22 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.
    – Max Maxman
    Jun 22 at 22:51

You must log in to answer this question.

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