Frame-validity games and lower bounds on the complexity of modal axioms

We introduce frame-equivalence games tailored for reasoning about the size, modal depth, number of occurrences of symbols and number of different propositional variables of modal formulae defining a given frame-property. Using these games, we prove lower bounds on the above measures for a number of well-known modal axioms; what is more, for some of the axioms, we show that they are optimal among the formulae defining the respective class of frames.