Hi guys,
In modal logic i.e. propositional logic with box and diamond, are then any laws to get a box or a diamond from outside a bracket to inside?
I.e. $\Box (x \rightarrow \Box x)$
I want the box inside the brackets :).
$\begingroup$
$\endgroup$
3
-
$\begingroup$ I don't understand the question. Are you asking whether the formula after "I.e." is an axiom in modal logic? Because a rule takes formulas and produces other formulas, and therefore your formula could only be an axiom, but not a rule. Or are you asking for a rule that produces a formula from your formula that does not have a box outside the brackets? In general, there are various different modal logics. Some of them might have what you are looking for, whatever that is exactly. $\endgroup$– Stefan GeschkeCommented Nov 16, 2010 at 11:21
-
$\begingroup$ Hi Stefan, my question was your second point. The semantics I am working with is Kripke semantics. Yes, all I want is to use a rule that makes the formula not have a box outside the brackets. Is that enough information? $\endgroup$– aleCommented Nov 16, 2010 at 11:41
-
$\begingroup$ Also, the same thing for $\Box (\Box x \rightarrow x)$. I would just like to know how to get this outer box inside somehow :S $\endgroup$– aleCommented Nov 16, 2010 at 12:33
Add a comment
|
3 Answers
$\begingroup$
$\endgroup$
3
Thanks for your clarification. If you think about Kripke frames, the logics under consideration are normal modal logics and hence you have the Distribution Axiom $\Box(p\rightarrow q)\rightarrow(\Box p\rightarrow\Box q)$. Since every normal modal logic is also closed under substitution and Modus Ponens, you can derive the rule that from $\Box(A\rightarrow B)$ you can conclude $(\Box A\rightarrow\Box B)$, so in your case from $\Box(x\rightarrow\Box x)$ you can derive $(\Box x\rightarrow\Box\Box x)$.
answered Nov 16, 2010 at 12:56
-
2$\begingroup$ My sense is that the OP asking for an equivalence of expressions. Your deduced implication is far weaker than the original statement, since it holds as long as $A$ isn't necessary, even if the implication $A\to B$ isn't necessary. It seems what the OP wants is a normal form theorem, but basically the situation with modal logic isn't as good as with the quantifiers $\exists$ and $\forall$. $\endgroup$ Commented Nov 16, 2010 at 13:57
-
$\begingroup$ There is no normal form theorem for normal modal logics in general. There is of course a normal form theorem for propositional S5. The given modal formula is of modal degree 2, while in S5 everything is reducible to first degree. Maybe the answer is, if one wants the box inside the brackets, one wants S5. $\endgroup$– MikeCCommented Nov 22, 2010 at 0:04
-
$\begingroup$ Specifically, in S5, the formula is equivalent to $\Box\neg x\lor\Box x$. $\endgroup$ Commented Sep 15, 2011 at 17:03
$\begingroup$
$\endgroup$
Some further cases.
Since tautologies are provable, we have $\vdash p\wedge q\rightarrow q$ and hence by the T axiom $\vdash\square (p\wedge q\rightarrow q)$. So in the context Stefan Geschke describes, $$\vdash\square (p\wedge q)\quad\Longrightarrow\quad \vdash\square p\wedge \square q\tag{1}$$ is a valid inference.
On the other hand, $$\vdash\square (p\vee q)\quad\Longrightarrow\quad \vdash\square p\vee \square q\tag{2}$$ is not a valid inference; consider for example $$\vdash\square (p\vee \neg p),\quad\text{but}\quad \not\vdash\square p\vee \square \neg p$$
So $\square$ works essentially like a $\forall$ quantifier.
answered Nov 16, 2010 at 13:39
$\begingroup$
$\endgroup$
[](p -> []p) <-> (<>p -> []p).
[]([]p -> p) <-> ([]p -> []p).
<>(p -> []p) <-> ([]p -> []p).
<>([]p -> p) <-> ([]p -> <>p).
[](<>p -> p) <-> (<>p -> []p).
[](p -> <>p) <-> (<>p -> <>p).
<>(<>p -> p) <-> (<>p -> <>p).
<>(p -> <>p) <-> ([]p -> <>p).
[](<>p -> []p) <-> <>(<>p -> []p) <-> (<>p -> []p).
<>(p v q) <-> (<>p v <>q).
[](p & q) <-> ([]p & []q).
The above are theorems of S5.
