Grafting Hypersequents onto Nested Sequents

TL;DR

This paper introduces grafted hypersequents, a new proof framework combining nested sequents and hypersequents, with novel calculi for specific modal logics that support cut elimination and efficient proof search.

Contribution

It presents a new Gentzen-style framework of grafted hypersequents and develops novel calculi for modal logics like K5, KD5, and their extensions, enabling optimal proof procedures.

Findings

Calculi enjoy syntactic cut elimination.

Calculi support backwards proof search of optimal complexity.

Tableaufication yields simplified tableau calculi for K5 and KD5.

Abstract

We introduce a new Gentzen-style framework of grafted hypersequents that combines the formalism of nested sequents with that of hypersequents. To illustrate the potential of the framework, we present novel calculi for the modal logics $\mathsf{K5}$ and $\mathsf{KD5}$, as well as for extensions of the modal logics $\mathsf{K}$ and $\mathsf{KD}$ with the axiom for shift reflexivity. The latter of these extensions is also known as $\mathsf{SDL}^+$ in the context of deontic logic. All our calculi enjoy syntactic cut elimination and can be used in backwards proof search procedures of optimal complexity. The tableaufication of the calculi for $\mathsf{K5}$ and $\mathsf{KD5}$ yields simplified prefixed tableau calculi for these logic reminiscent of the simplified tableau system for $\mathsf{S5}$, which might be of independent interest.