# Hypersequent

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Hypersequent
> Markdown URL: https://mediated.wiki/source/Hypersequent.md
> Source: https://en.wikipedia.org/wiki/Hypersequent
> Source revision: 1241073361
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

In [mathematical logic](/source/mathematical_logic), the '''hypersequent''' framework is an extension of the [proof-theoretical](/source/proof_theory) framework of [sequent calculi](/source/Sequent_calculus) used in [structural proof theory](/source/structural_proof_theory) to provide [analytic calculi](/source/Analytic_proof) for logics that are not captured in the sequent framework. A hypersequent is usually taken to be a finite [multiset](/source/multiset) of ordinary [sequent](/source/sequent)s, written

: <math>\Gamma_1 \Rightarrow \Delta_1 \mid \cdots \mid \Gamma_n \Rightarrow \Delta_n</math>  
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](/source/intermediate_logic) LC ([Gödel–Dummett logic](/source/G%C3%B6del%E2%80%93Dummett_logic)) 
: <math>\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}</math>
or the modal splitting rule for the [modal logic](/source/modal_logic) [S5](/source/S5_(modal_logic)):<ref name=":0">{{Cite book|last=Avron|first=Arnon|author-link=Arnon Avron|date=1996|chapter=The method of hypersequents in the proof theory of propositional non-classical logics|title=Logic: From Foundations to Applications|pages=1–32|isbn=978-0-19-853862-2}}</ref>
:  <math>\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}</math>

Hypersequent calculi have been used to treat [modal logic](/source/modal_logic)s, [intermediate logics](/source/intermediate_logics), and [substructural logics](/source/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](/source/multiset) of ordinary [sequent](/source/sequent)s, written

: <math>\Gamma_1 \Rightarrow \Delta_1 \mid \dots \mid \Gamma_n \Rightarrow \Delta_n</math>

The sequents making up a hypersequent consist of pairs 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](/source/intuitionistic_logic). 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](/source/functionally_complete) set of connectives <math>\{\bot,\to\}</math> for [classical propositional logic](/source/classical_propositional_logic) is given by the following four rules:

: <math>\frac{}{\mathcal{G} \mid \Gamma, p \Rightarrow p,\Delta} </math>

: <math>\frac{}{\mathcal{G} \mid \Gamma, \bot \Rightarrow \Delta}</math>

: <math>\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
}</math>

<math>\frac{\mathcal{G} \mid \Gamma,A \Rightarrow B, \Delta
}
{\mathcal{G} \mid \Gamma \Rightarrow A \to B, \Delta
}</math>

Due to the additional structure in the hypersequent setting, the [structural rule](/source/structural_rule)s 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:

: <math>\frac{\mathcal{G} \mid \Gamma \Rightarrow \Delta
}
{\mathcal{G}\mid \Gamma, \Sigma \Rightarrow \Delta, \Pi
}</math>

<math>\frac{\mathcal{G} \mid \Gamma, A, A \Rightarrow \Delta
}
{\mathcal{G} \mid \Gamma, A \Rightarrow \Delta
}</math>

<math>\frac{\mathcal{G} \mid \Gamma \Rightarrow A, A, \Delta
}
{\mathcal{G} \mid \Gamma \Rightarrow A, \Delta
}</math>

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

<math>\frac{\mathcal{G}}{\mathcal{G} \mid \Gamma \Rightarrow\Delta}</math>

<math>\frac{\mathcal{G} \mid \Gamma \Rightarrow\Delta \mid \Gamma\Rightarrow\Delta
}
{\mathcal{G} \mid \Gamma\Rightarrow\Delta
}</math>

[Soundness](/source/Soundness) of these rules is closely connected to the formula interpretation of the hypersequent structure, nearly always as some form of [disjunction](/source/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 logic](/source/modal_logic)s, for which analytic [sequent calculi](/source/Sequent_calculus) proved elusive.  In the context of modal logics the standard formula interpretation of a hypersequent

: <math>\Gamma_1 \Rightarrow \Delta_1 \mid \dots \mid \Gamma_n \Rightarrow \Delta_n</math>

is the formula

: <math>\Box (\bigwedge \Gamma_1 \to \bigvee \Delta_1) \lor \dots \lor \Box( \bigwedge\Gamma_n \to \bigvee\Delta_n)</math>

Here if <math>\Gamma</math> is the multiset <math>A_1, \dots, A_n</math> we write <math>\Box \Gamma</math> for the result of prefixing every formula in <math>\Gamma</math> with <math>\Box</math>, i.e., the multiset <math>\Box A_1, \dots, \Box A_n</math>. Note that the single components are interpreted using the standard formula interpretation for sequents, and the hypersequent bar <math>\mid</math> 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](/source/S5_(modal_logic)). In a standard hypersequent calculus for this logic<ref name=":0" /> 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

: <math>\frac{\mathcal{G} \mid \Box \Gamma \Rightarrow A
}
{\mathcal{G} \mid \Box \Gamma \Rightarrow \Box A
}</math>

<math>\frac{\mathcal{G} \mid \Gamma, A \Rightarrow \Delta
}
{\mathcal{G} \mid \Gamma, \Box A \Rightarrow \Delta
}</math>

<math>\frac{\mathcal{G} \mid \Box \Gamma, \Sigma \Rightarrow \Box \Delta, \Pi
}
{\mathcal{G} \mid \Box \Gamma \Rightarrow \Box\Delta \mid \Sigma \Rightarrow \Pi
}</math>

[Admissibility](/source/Admissible_set) of a suitably formulated version of the [cut rule](/source/cut_rule) can be shown by a syntactic argument on the structure of derivations or by showing [completeness](/source/completeness_(logic)) 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.<ref name=":4">{{Cite journal|last=Mints|first=Grigori|authorlink = Grigori Mints|date=1971|title=On some calculi of modal logic|journal=Proc. Steklov Inst. Of Mathematics|volume=98|pages=97–122}}</ref><ref name=":5">{{Cite journal|last=Pottinger|first=Garrell|date=1983|title=Uniform, cut-free formulations of T, S4 and S5 (abstract)|journal=[J. Symb. Log.](/source/J._Symb._Log.)|volume=48|issue=3|pages=900}}</ref><ref name=":0" /><ref>{{Cite journal|last=Poggiolesi|first=Francesca|date=2008|title=A cut-free simple sequent calculus for modal logic S5|url=https://halshs.archives-ouvertes.fr/halshs-00775809/file/articolos55.pdf|journal=[Rev. Symb. Log.](/source/Rev._Symb._Log.)|volume=1|pages=3–15|doi=10.1017/S1755020308080040|s2cid=37437016}}</ref><ref>{{Cite journal|last=Restall|first=Greg|editor4-first=John R|editor4-last=Steel|editor3-first=Dag|editor3-last=Normann|editor2-first=Ludomir|editor2-last=Newelski|editor1-first=Costas|editor1-last=Dimitracopoulos|date=2007|title=Proofnets for S5: Sequents and circuits for modal logic|journal=Logic Colloquium 2005|series=Lecture Notes in Logic|volume=28|pages=151–172|doi=10.1017/CBO9780511546464.012|hdl=11343/31712|isbn=9780511546464|hdl-access=free}}</ref><ref name=":1">{{Cite book|last=Kurokawa|first=Hidenori|date=2014|title=New Frontiers in Artificial Intelligence|volume=8417|pages=51–68|doi=10.1007/978-3-319-10061-6_4|isbn=978-3-319-10060-9|chapter=Hypersequent Calculi for Modal Logics Extending S4|series=Lecture Notes in Computer Science}}</ref><ref name=":2">{{Cite book |doi = 10.1109/LICS.2013.47|chapter = From Frame Properties to Hypersequent Rules in Modal Logics|title = 2013 28th Annual ACM–IEEE [Symposium on Logic in Computer Science](/source/Symposium_on_Logic_in_Computer_Science)|pages = 408–417|year = 2013|last1 = Lahav|first1 = Ori|isbn = 978-1-4799-0413-6|s2cid = 221813}}</ref> Hypersequent calculi have also been proposed for many other modal logics.<ref name=":1" /><ref name=":2" /><ref>{{Cite journal|last=Indrzejczak|first=Andrzej|date=2015|title=Eliminability of cut in hypersequent calculi for some modal logics of linear frames|journal=[Information Processing Letters](/source/Information_Processing_Letters)|volume=115|issue=2|pages=75–81|doi=10.1016/j.ipl.2014.07.002}}</ref><ref>{{Cite journal|last=Lellmann|first=Björn|date=2016|title=Hypersequent rules with restricted contexts for propositional modal logics|journal=[Theor. Comput. Sci.](/source/Theor._Comput._Sci.)|volume=656|pages=76–105|doi=10.1016/j.tcs.2016.10.004|doi-access=free}}</ref>

=== Intermediate logics ===
Hypersequent calculi based on intuitionistic or [single-succedent sequents](/source/single-succedent_sequents) have been used successfully to capture a large class of [intermediate logics](/source/intermediate_logics), i.e., extensions of [intuitionistic propositional logic](/source/Intuitionistic_logic). Since the hypersequents in this setting are based on single-succedent sequents, they have the following form:

: <math>\Gamma_1 \Rightarrow A_1 \mid \dots \mid \Gamma_n \Rightarrow A_n</math>

The standard formula interpretation for such an hypersequent is

: <math>(\bigwedge\Gamma_1 \to A_1) \lor \dots \lor (\bigwedge\Gamma_n \to A_n)</math>

Most hypersequent calculi for intermediate logics include the single-succedent versions of the propositional rules given above and a selection of the structural rules. The characteristics of a particular intermediate logic are mostly captured using a number of additional [structural rule](/source/structural_rule)s. E.g., the standard calculus for intermediate logic [LC](/source/G%C3%B6del%E2%80%93Dummett_logic), sometimes also called Gödel–Dummett logic, contains additionally the so-called communication rule:<ref name=":0" />

: <math>\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}</math>

Hypersequent calculi for many other intermediate logics have been introduced,<ref name=":0" /><ref>{{Cite journal|last1=Ciabattoni|first1=Agata|author1-link= Agata Ciabattoni |last2=Ferrari|first2=Mauro|date=2001|title=Hypersequent calculi for some intermediate logics with bounded Kripke models|journal=[J. Log. Comput.](/source/J._Log._Comput.)|volume=11|issue=2|pages=283–294|doi=10.1093/logcom/11.2.283}}</ref><ref>{{Cite journal|last1=Ciabattoni|first1=Agata|author1-link= Agata Ciabattoni |last2=Maffezioli|first2=Paolo|last3=Spendier|first3=Lara|date=2013|editor-last=Galmiche|editor-first=Didier|editor2-last=Larchey-Wendling|editor2-first=Dominique|title=Hypersequent and Labelled Calculi for Intermediate Logics|journal=[Tableaux](/source/International_Conference_on_Automated_Reasoning_with_Analytic_Tableaux_and_Related_Methods) 2013|pages=81–96}}</ref><ref>{{Cite journal|last1=Baaz|first1=Matthias|last2=Ciabattoni|first2=Agata|author2-link= Agata Ciabattoni |last3=Fermüller|first3=Christian G.|date=2003|title=Hypersequent Calculi for Gödel Logics – A Survey|journal=J. Log. Comput.|volume=13|issue=6|pages=835–861|doi=10.1093/logcom/13.6.835|citeseerx=10.1.1.8.5319}}</ref> and there are very general results about [cut elimination](/source/cut_elimination) in such calculi.<ref name=":3">{{Cite book |doi = 10.1109/LICS.2008.39|chapter = From Axioms to Analytic Rules in Nonclassical Logics|title = 2008 23rd Annual IEEE Symposium on Logic in Computer Science|pages = 229–240|year = 2008|last1 = Ciabattoni|first1 = Agata|author1-link= Agata Ciabattoni |last2 = Galatos|first2 = Nikolaos|last3 = Terui|first3 = Kazushige|isbn = 978-0-7695-3183-0|citeseerx = 10.1.1.405.8176|s2cid = 7456109}}</ref>

=== Substructural logics ===
As for intermediate logics, hypersequents have been used to obtain analytic calculi for many [substructural logics](/source/substructural_logics) and [fuzzy logics](/source/fuzzy_logics).<ref name=":0" /><ref name=":3" /><ref>{{Cite book|title=Proof theory for fuzzy logics|last1=Metcalfe|first1=George|last2=Olivetti|first2=Nicola|last3=Gabbay|first3=Dov|author3link = Dov Gabbay|publisher=Springer, Berlin|year=2008}}</ref>

== History ==
The hypersequent structure seem to have appeared first in <ref name=":4" /> under the name of ''cortege'', to obtain a calculus for the modal logic [S5](/source/S5_(modal_logic)). It seems to have been developed independently in,<ref name=":5" /> also for treating modal logics, and in the influential,<ref name=":0" /> where calculi for modal, intermediate and substructural logics are considered, and the term hypersequent is introduced.

== References ==
<references />

Category:Proof theory

---
Adapted from the Wikipedia article [Hypersequent](https://en.wikipedia.org/wiki/Hypersequent) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Hypersequent?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.