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 :).
[Math] Modal logic – box rules
lo.logicmodal-logic
Related Solutions
The relationship between modal logic and graph theory has, indeed, been studied before. Peter mentioned sheaf models in the comments; I want to mention a more classical-logic-y perspective.
(First, let me note that when we say that $\phi$ characterizes a class of frames $V$, we mean that for every frame in $V$, and every valuation on that frame, $\phi$ is true, i.e., $\phi$ is a validity on every frame in $V$. There are frames together with valuations which satisfy, e.g., $\square p\implies \square \square p$ without the frame being transitive.)
It's a natural question to ask which properties of frames can be defined by propositional modal formulas. For example, as you mentioned in the question, we can characterize transitivity by a single modal formula. It turns out that the class of properties of frames which can be captured by modal formulas is substantially larger than the class of first-order-definable properties. Blackburn, de Rijke, and Venema's book ("Modal logic") gives the example of the Lob formula: $$ \square (\square p\implies p)\implies \square p$$ They show that this formula is a validity in precisely those frames in which the relation $R$ is transitive and well-founded (although they use the term "converse well-founded"). By a compactness argument, this class of frames is not first-order axiomatizable. A result of Goldblatt and Thomason in 1974 showed that "a first-order frame property is modally definable iff it is preserved under taking generated subframes, p-morphic frame images, disjoint unions, and inverse ultrafilter extensions." I don't really understand what all that means, but at the very least we can take away that not every first-order property of frames is characterized by a (propositional) modal formula.
In the other direction, since the definition of "valid modal formula" is second-order, it's clear that any class of frames which can be captured by a modal formula is definable in second-order logic. I recall a paper on the strength of modal logic that showed that a sort of converse to this held, despite the converse itself failing (since, as mentioned above, not even every first-order property of frames is modally definable) but I can't track it down at the moment. EDIT: Emil found it - it's "Reduction of second-order logic to modal logic" by S. K. Thomason, and a (very poor) copy can be found here: http://onlinelibrary.wiley.com/doi/10.1002/malq.19750210114/abstract.
In general, the book "Modal logics" by Chagrov and Zakharyaschev is probably the book to look at. I don't know how up-to-date it is anymore, but it seems to include every perspective on modal logics that I've heard of, short of the category-theoretic aspects.
EDIT: Another aspect, which I didn't think of at first, is given by alternate interpretations of modalities. For example, suppose we interpret $\square p$ as meaning "more than half of visible nodes satisfy $p$," instead of "all visible nodes satisfy $p$;" or some other interpretation. Under each interpretation, the classes of graphs we can charaterize by modal formulas changes; and while any specific alternate interpretation is probably not too interesting, general tools for studying that would probably be very deep and valuable. I don't know of any work on this, but I suspect it's been done before; the closest related source I can find at present is the extended abstract of "The Modal Logic of Probability" (Heifetz, Mongin) which seems vaguely along these lines.
Best Answer
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)$.