Hypersequent calculi for non-normal modal and deontic logics: Countermodels and optimal complexity

TL;DR

This paper develops hypersequent calculi for classical cube modal and deontic logics, providing cut elimination, optimal proof search, and methods for extracting countermodels, thus advancing proof theory and semantics for these logics.

Contribution

It introduces internal hypersequent calculi for all classical cube systems and their extensions, with completeness, cut elimination, and optimal proof search strategies.

Findings

Calculi are complete with respect to axiomatisations.

A terminating, optimal proof search strategy is developed.

Countermodels can be extracted from failed proof leaves.

Abstract

We present some hypersequent calculi for all systems of the classical cube and their extensions with axioms $T$, $P$, $D$, and, for every $n\geq 1$, rule $RD^+_n$. The calculi are internal as they only employ the language of the logic, plus additional structural connectives. We show that the calculi are complete with respect to the corresponding axiomatisation by a syntactic proof of cut elimination. Then we define a terminating root-first proof search strategy based on the hypersequent calculi and show that it is optimal for coNP-complete logics. Moreover, we obtain that from every saturated leaf of a failed proof it is possible to define a countermodel of the root hypersequent in the bi-neighbourhood semantics, and for regular logics also in the relational semantics. We finish the paper by giving a translation between hypersequent rule applications and derivations in a labelled system for the classical cube.