Modal logic and the polynomial hierarchy: from QBFs to K and back

In this work we classify formulas of the basic normal modal logic K into fragments complete for each level of the polynomial time hierarchy, with respect to validity. In particular, we identify a pair of encodings, from true Quantified Boolean Formulas (QBFs) to modal logic and vice-versa, whose composition preserves the number of quantifier alternations. This yields a formal analogue of ‘quantifier complexity’ within modal logic.

Our translation from QBFs to modal formulas is an optimised version of common translations employed in modal logic solving. In the other direction, we encode proof search itself, for a cut-free sequent calculus, as an alternating time predicate. The aforementioned tight bounds are obtained by carefully calibrating both the optimisation (QBFs to modal logic) and the measurement of proof search complexity (modal logic to QBFs). This approach is inspired by recent work achieving a similar result for the exponential-free fragment of Linear Logic (MALL).