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 which 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 intermediate logic LC (below left) or the modal splitting rule for modal logic S5 (below right):[1]

${\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}}}$ ${\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.

Formal definitions and propositional rules

Formally, a hypersequent is usually taken to be a finite multiset of ordinary sequents, written

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

The sequents making up a hypersequent consist of tuples of multisets of formulae, and are called the components of the hypersequent. Variants defining hypersequents and sequents in terms of sets or lists instead of multisets are also considered, and depending on the considered logic the sequents can be classical or intuitionistic. The rules for the propositional connectives usually are adaptions of the corresponding standard sequent rules with an additional side hypersequent, also called hypersequent context. E.g., a common set of rules for the functionally complete set of connectives ${\displaystyle \{\bot ,\to \}}$ for classical propositional logic is given by the following four rules:

${\displaystyle {\frac {}{{\mathcal {G}}\mid \Gamma ,p\Rightarrow p,\Delta }}}$

${\displaystyle {\frac {}{{\mathcal {G}}\mid \Gamma ,\bot \Rightarrow \Delta }}}$

${\displaystyle {\frac {{\mathcal {G}}\mid \Gamma ,B\Rightarrow \Delta \qquad {\mathcal {G}}\mid \Gamma \Rightarrow A,\Delta }{{\mathcal {G}}\mid \Gamma ,A\to B\Rightarrow \Delta }}}$

${\displaystyle {\frac {{\mathcal {G}}\mid \Gamma ,A\Rightarrow B,\Delta }{{\mathcal {G}}\mid \Gamma \Rightarrow A\to B,\Delta }}}$

Due to the additional structure in the hypersequent setting the structural rules are considered in their internal and external variants. The internal weakening and internal contraction rules are the adaptions of the corresponding sequent rules with an added hypersequent context:

${\displaystyle {\frac {{\mathcal {G}}\mid \Gamma \Rightarrow \Delta }{{\mathcal {G}}\mid \Gamma ,\Sigma \Rightarrow \Delta ,\Pi }}}$

${\displaystyle {\frac {{\mathcal {G}}\mid \Gamma ,A,A\Rightarrow \Delta }{{\mathcal {G}}\mid \Gamma ,A\Rightarrow \Delta }}}$

${\displaystyle {\frac {{\mathcal {G}}\mid \Gamma \Rightarrow A,A,\Delta }{{\mathcal {G}}\mid \Gamma \Rightarrow A,\Delta }}}$

The external weakening and external contraction rules are the corresponding rules on the level of hypersequent components instead of formulae:

${\displaystyle {\frac {\mathcal {G}}{{\mathcal {G}}\mid \Gamma \Rightarrow \Delta }}}$

${\displaystyle {\frac {{\mathcal {G}}\mid \Gamma \Rightarrow \Delta \mid \Gamma \Rightarrow \Delta }{{\mathcal {G}}\mid \Gamma \Rightarrow \Delta }}}$

Soundness of these rules is closely connected to the formula interpretation of the hypersequent structure, nearly always as some form of disjunction. The precise formula interpretation depends on the considered logic, see below for some examples.

Main examples

Modal logics

Hypersequents have been used to obtain analytic calculi for modal logics, for which analytic sequent calculi proved elusive. In the context of modal logics the standard formula interpretation of a hypersequent

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

is the formula

${\displaystyle \Box (\bigwedge \Gamma _{1}\to \bigvee \Delta _{1})\lor \dots \lor \Box (\bigwedge \Gamma _{n}\to \bigvee \Delta _{n})}$

Here if ${\displaystyle \Gamma }$ is the multiset ${\displaystyle A_{1},\dots ,A_{n}}$ we write ${\displaystyle \Box \Gamma }$ for the result of prefixing every formula in ${\displaystyle \Gamma }$ with ${\displaystyle \Box }$, i.e., the multiset ${\displaystyle \Box A_{1},\dots ,\Box A_{n}}$. Note that the single components are interpreted using the standard formula interpretation for sequents, and the hypersequent bar ${\displaystyle \mid }$ is interpreted as a disjunction of boxes. The prime example of a modal logic for which hypersequents provide an analytic calculus is the logic S5. In a standard hypersequent calculus for this logic[1] the formula interpretation is as above, and the propositional and structural rules are the ones from the previous section. Additionally, the calculus contains the modal rules

${\displaystyle {\frac {{\mathcal {G}}\mid \Box \Gamma \Rightarrow A}{{\mathcal {G}}\mid \Box \Gamma \Rightarrow \Box A}}}$

${\displaystyle {\frac {{\mathcal {G}}\mid \Gamma ,A\Rightarrow \Delta }{{\mathcal {G}}\mid \Gamma ,\Box A\Rightarrow \Delta }}}$

${\displaystyle {\frac {{\mathcal {G}}\mid \Box \Gamma ,\Sigma \Rightarrow \Box \Delta ,\Pi }{{\mathcal {G}}\mid \Box \Gamma \Rightarrow \Box \Delta \mid \Sigma \Rightarrow \Pi }}}$

Admissibility of a suitably formulated version of the cut rule can be shown by a syntactic argument on the structure of derivations or by showing completeness of the calculus without the cut rule directly using the semantics of S5. In line with the importance of modal logic S5, a number of alternative calculi have been formulated.[2][3][1][4][5][6][7] Hypersequent calculi have also been proposed for many other modal logics.[6][7][8][9]

Intermediate logics

Hypersequent calculi based on intuitionistic or single-succedent sequents have been used successfully to capture a large class of intermediate logics, i.e., extensions of intuitionistic propositional logic. Since the hypersequents in this setting are based on single-succedent sequents, they have the following form:

${\displaystyle \Gamma _{1}\Rightarrow A_{1}\mid \dots \mid \Gamma _{n}\Rightarrow A_{n}}$

The standard formula interpretation for such an hypersequent is

${\displaystyle (\bigwedge \Gamma _{1}\to A_{1})\lor \dots \lor (\bigwedge \Gamma _{n}\to A_{n})}$

Most hypersequent calculi for intermediate logics include the single-succedent versions of the propositional rules given above, a selection of the structural rules. The characteristics of a particular intermediate logic are mostly captured using a number of additional structural rules. E.g., the standard calculus for intermediate logic LC, sometimes also called Gödel–Dummett logic, contains additionally the so-called communication rule:[1]

${\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}}}$

Hypersequent calculi for many other intermediate logics have been introduced,[1][10][11][12] and there are very general results about cut elimination in such calculi.[13]

Substructural logics

As for intermediate logics, hypersequents have been used to obtain analytic calculi for many substructural logics and fuzzy logics.[1][13][14]

History

The hypersequent structure seem to have appeared first in[2] under the name of cortege to obtain a calculus for modal logic S5. It seems to have been developed independently in,[3] also for treating modal logics, and in the influential,[1] where calculi for modal, intermediate and substructural logics are considered, and the term hypersequent is introduced.

References

1. Avron, Arnon (1996). The method of hypersequents in the proof theory of propositional non-classical logics. Logic: From Foundations to Applications. pp. 1–32. ISBN 978-0-19-853862-2.
2. Mints, Grigori (1971). "On some calculi of modal logic". Proc. Steklov Inst. Of Mathematics. 98: 97–122.
3. Pottinger, Garrell (1983). "Uniform, cut-free formulations of T, S4 and S5 (abstract)". J. Symb. Log. 48 (3): 900.
4. Poggiolesi, Francesca (2008). "A cut-free simple sequent calculus for modal logic S5". Rev. Symb. Log. 1: 3–15. doi:10.1017/S1755020308080040.
5. Restall, Greg (2007). "Proofnets for S5: Sequents and circuits for modal logic". Logic Colloquium 2005. Lecture Notes in Logic. 28: 151–172.
6. Kurokawa, Hidenori (2014). "Hypersequent Calculi for Modal Logics Extending S4". New Frontiers in Artificial Intelligence. Lecture Notes in Computer Science. 8417. pp. 51–68. doi:10.1007/978-3-319-10061-6_4. ISBN 978-3-319-10060-9.
7. Lahav, Ori (2013). "From Frame Properties to Hypersequent Rules in Modal Logics". 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science. pp. 408–417. doi:10.1109/LICS.2013.47. ISBN 978-1-4799-0413-6.
8. Indrzejczak, Andrzej (2015). "Eliminability of cut in hypersequent calculi for some modal logics of linear frames". Information Processing Letters. 115 (2): 75–81. doi:10.1016/j.ipl.2014.07.002.
9. Lellmann, Björn (2016). "Hypersequent rules with restricted contexts for propositional modal logics". Theor. Comput. Sci. 656: 76–105. doi:10.1016/j.tcs.2016.10.004.
10. Ciabattoni, Agata; Ferrari, Mauro (2001). "Hypersequent calculi for some intermediate logics with bounded Kripke models". J. Log. Comput. 11 (2): 283–294. doi:10.1093/logcom/11.2.283.
11. Ciabattoni, Agata; Maffezioli, Paolo; Spendier, Lara (2013). Galmiche, Didier; Larchey-Wendling, Dominique (eds.). "Hypersequent and Labelled Calculi for Intermediate Logics". Tableaux 2013: 81–96.
12. Baaz, Matthias; Ciabattoni, Agata; Fermüller, Christian G. (2003). "Hypersequent Calculi for Gödel Logics – A Survey". J. Log. Comput. 13 (6): 835–861. doi:10.1093/logcom/13.6.835.
13. Ciabattoni, Agata; Galatos, Nikolaos; Terui, Kazushige (2008). "From Axioms to Analytic Rules in Nonclassical Logics". 2008 23rd Annual IEEE Symposium on Logic in Computer Science. pp. 229–240. CiteSeerX 10.1.1.405.8176. doi:10.1109/LICS.2008.39. ISBN 978-0-7695-3183-0.
14. Metcalfe, George; Olivetti, Nicola; Gabbay, Dov (2008). Proof theory for fuzzy logics. Springer, Berlin.