Modal logic - box rules 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 :).
 A: 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)$.
A: 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.
A: [](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.
