Proving Gabbay rule for Modal Logic

Question

I'm currently working on exercises of the book "Modal Logic" by A.Chagrov and M.Zakharyaschev (for pleasure, not homework).

One exercise asks to prove this version of Gabbay rule (exercise $3.10$): A frame $F$ validates the rule $(\Box p \rightarrow p) \vee \psi$ $/$ $\psi$, with $p$ not appearing in $\psi$, if and only if $F$ is irreflexive.

(Note that: "$p$ not appearing in $\psi$").

I have the $\leftarrow$ part, but I'm having a hard time proving the other implication. I would really like to understand this excercise, and I know that the excercises in this book are sometimes hard. But I think this has to be fairly easy.

Until now I tried proving it by reductio ad absurdum: I have one reflexive node $x$, and I try to find a formula $\phi$ that $x$ doesn't validate, but that every other node does validate. If I can prove such formula exists then I'm done, because I plug it in the rule.

I hope I was clear, thanks in advance!

Answer 1

I don't have the book, but it looks like a formula $ ConditionQ \to ( (B \lor A)) \to A) $ you are trying to find what $ConditionQ$ is

$ConditionQ$ is just that $ ( (B \lor A)) \to A) $ is a theorem, this means that $B $ has to be false, in this case B is the T axiom (valid in all reflexive frames) so the condition Q is that all frames are irreflexive.

Answer 2

The formula you're looking for is $(\Box p \wedge p)$.

Given formulas $\Box p$, $p$, and $A$, there are 8 ways to construct a world, but only 6 of these worlds are reflexive ($R?$).

[]p   p      A      R?
---   ---    ---    ---
F     F      F      T
F     F      T      T
F     T      F      T
F     T      T      T
T     F      F      F
T     F      T      F   <- world x
T     T      F      T
T     T      T      T

The only way for $(\Box p \rightarrow p) \vee \psi / \psi$ to be a valid inference rule is for $A$ to be true and $(\Box p \rightarrow p)$ to be false. You can see from this table that this is only true for the row indicated world x.

For a world to be reflexive, it must be accessible from itself. Accessibility is determined primarily by the definition of $\Box$. The formula $\Box p(w_0)$ indicates that $p$ is necessarily true in all possible worlds that are accessible from world $w_0$, but it is not necessary for $p$ to be true in $w_0$ itself.

If we want to ensure that every world is accessible from itself, we need to impose the restriction that if $\Box p(w)$ is true, then $p(w)$ must also be true.

That is precisely what the logical connective $p \rightarrow q$ ("p implies q") means. The truth table looks like this:

p     q      p -> q
---   ---    ------
F     F      T
F     T      T
T     F      F
T     T      T

Therefore, to ensure reflexivity, we add the axiom $\forall w.\Box p(w) \rightarrow p(w)$, or simply $\Box p \rightarrow p$, and that is why this is called the reflexive axiom.