Cyclic Hypersequent Calculi for Some Modal Logics with the Master Modality

At LICS 2013, O. Lahav introduced a technique to uniformly construct cut-free hypersequent calculi for basic modal logics characterised by frames satisfying so-called ‘simple’ first-order conditions. We investigate the generalisation of this technique to modal logics with the master modality (a.k.a. reflexive-transitive closure modality). The (co)inductive nature of this modality is accounted for through the use of non-well-founded proofs, which are made cyclic using focus-style annotations. We show that the peculiarities of hypersequents hinder the usual method of completeness via infinitary proof-search. Instead, we construct countermodels from maximally unprovable hypersequents. We show that this yields completeness for a small (yet infinite) subset of simple frame conditions.