# Proving Gabbay rule for Modal Logic

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!

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.

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.

• If I understand you correctly, you are missing the "$p$ not appearing in $\psi$" part. – Luis N Scoccola Feb 24 '14 at 12:18
• Well, it's implied by the first truth table. For example, if $A = p$, then world x contains a contradiction, because $p$ is true and $A$ is false, so that line would have to be removed from the list (along with all the other lines where $A$ and $p$ don't match). The only way you get all 8 possible combinations of 3 boolean variables is to make the variables completely independent. – tangentstorm Feb 24 '14 at 13:23
• I don't get how this solves the problem. You say that the formula I'm looking for is $(\Box p \wedge p)$ but $p$ does appear in that formula. And I can't substitue it for, say, $q$ because then we don't get the desired result. – Luis N Scoccola Feb 24 '14 at 23:17
• Perhaps I was wrong about $(\Box p \wedge p)$: I don't really understand the nature of the proof you're trying to write. I don't know what "the $\leftarrow$ part" means or "the other part". All I know is that the only possible way for the statement $(\Box p\rightarrow p) \vee A / A$ to be valid is if $A$ is a theorem and $(\Box p\rightarrow p)$ is an antitheorem. I then showed (by the first truth table) that this is only possible in one situation (world x), and that a frame containing world x cannot be reflexive because $(\Box p\rightarrow p)$ is a necessary condition for reflexivity. – tangentstorm Feb 25 '14 at 8:55