26.2k views
1 vote
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.

User Tarun
by
8.2k points

1 Answer

4 votes

Final answer:

To solve the modal logic problem, the student needs to apply the modal logic rules correctly, particularly axioms specific to system K and the modus ponens rule. After correctly manipulating the premises, it's possible to affirm that ◇¬B follows from the given premises using a series of justified steps.

Step-by-step explanation:

The student is trying to prove ◇¬B (that it is possible that B is not true) given the premises □(A ∨ ¬B) (it is necessary that A is true or B is not true) and ¬□A (it is not necessary that A is true) using the axioms of modal logic system K and rules of inference. The confusion seems to be in applying modus ponens and trying to manipulate the modal operators. We can resolve this problem by first understanding the axioms and rules of inference, such as modus ponens, and then carefully applying them to the modal logic scenario.

To do a direct proof, we need to reach ◇¬B from our premises. First, let's recall that □(A ∨ ¬B) implies that ¬A → □¬B. Since we are given ¬□A, by modal logic, this is equivalent to ◇¬A. Then, from our implication and the axiom K (□(p→q) → (□p→□q)), we can infer that if ◇¬A is true, then ◇¬B must also be true. The key step is realizing you can distribute □ over the implication inside the parentheses.

The appropriate use of modus ponens here relies on getting to the necessary form for a direct application. That involves a bit of manipulation within the system's framework to present one of the premises as the antecedent of an implication and the other as affirming that antecedent, which then allows the consequent to be affirmed.

User Prathmesh Dali
by
7.5k points