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

TL;DR

This paper introduces frame-equivalence games to analyze the complexity of modal formulas defining frame-properties, establishing lower bounds and optimality results for well-known modal axioms.

Contribution

It develops a novel game-theoretic approach to measure and prove lower bounds on the complexity of modal axioms defining frame-properties.

Findings

Lower bounds on size, depth, and symbol occurrences for modal axioms.

Optimality of certain axioms within their class of frame-defining formulas.

Applicability of the method to well-known modal axioms.

Abstract

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.