## Abstract

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).

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).

Original language | English |
---|---|

Title of host publication | Advances in Modal Logic |

Subtitle of host publication | Volume 14 |

Editors | David Fernández-Duque, Alessandra Palmigiano, Sophie Pinchinat |

Publisher | College Publications |

Pages | 329-348 |

Number of pages | 20 |

ISBN (Electronic) | 9781848904132 |

Publication status | Published - 25 Aug 2022 |

Event | Advances in Modal Logic 2022 - IRISA, Rennes, France Duration: 22 Aug 2022 → 25 Aug 2022 |

### Publication series

Name | Advances in Modal Logic |
---|---|

Publisher | College Publications |

Volume | 14 |

### Conference

Conference | Advances in Modal Logic 2022 |
---|---|

Abbreviated title | AiML 2022 |

Country/Territory | France |

City | Rennes |

Period | 22/08/22 → 25/08/22 |

### Bibliographical note

Acknowledgments:Supported by a UKRI Future Leaders Fellowship, Structure vs. Invariants in Proofs.

## Keywords

- Modal Logic
- Polynomial Hierarchy
- Quantified Boolean Formulas
- Proof Search
- Sequent Calculus