Symmetries in Modal Logics

We generalize the notion of symmetries of propositional formulas in conjunctive normal form to modal formulas. Our framework uses the coinductive models introduced in [4] and, hence, the results apply to a wide class of modal logics including, for example, hybrid logics. Our main result shows that the symmetries of a modal formula preserve entailment: if sigma is a symmetry of theta then theta proves psi if and only if theta satisfies sigma (s psi).