Hypersequent

In mathematical logic, the hypersequent framework is an extension of the proof-theoretical framework of sequent calculi used in structural proof theory to provide analytic calculi for logics that are not captured in the sequent framework. A hypersequent is usually taken to be a finite multiset of ordinary sequents, written

${\displaystyle \Gamma _{1}\Rightarrow \Delta _{1}\mid \cdots \mid \Gamma _{n}\Rightarrow \Delta _{n}}$

The sequents making up a hypersequent are called components. The added expressivity of the hypersequent framework is provided by rules manipulating different components, such as the communication rule for the intermediate logic LC (Gödel–Dummett logic)

${\displaystyle {\frac {\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}\mid \Sigma \Rightarrow A\qquad \Omega _{1}\Rightarrow \Theta _{1}\mid \dots \mid \Omega _{m}\Rightarrow \Theta _{m}\mid \Pi \Rightarrow B}{\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}\mid \Omega _{1}\Rightarrow \Theta _{1}\mid \dots \mid \Omega _{m}\Rightarrow \Theta _{m}\mid \Sigma \Rightarrow B\mid \Pi \Rightarrow A}}}$

or the modal splitting rule for the modal logic S5:^[1]

${\displaystyle {\frac {\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}\mid \Box \Sigma ,\Theta \Rightarrow \Box \Pi ,\Omega }{\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}\mid \Box \Sigma \Rightarrow \Box \Pi \mid \Theta \Rightarrow \Omega }}}$

Hypersequent calculi have been used to treat modal logics, intermediate logics, and substructural logics. Hypersequents usually have a formula interpretation, i.e., are interpreted by a formula in the object language, nearly always as some kind of disjunction. The precise formula interpretation depends on the considered logic.