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 :).
MathOverflow is a question and answer site for professional mathematicians. It only takes a minute to sign up.
Sign up to join this communityHi 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 :).
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)$.
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.
[](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.