Editing Structural proof theory (section)

== Hypersequents ==
{{Main|Hypersequent}}

The hypersequent framework extends the ordinary [[Sequent calculus|sequent structure]] to a [[multiset]] of sequents, using an additional structural connective | (called the '''hypersequent bar''') to separate different sequents. It has been used to provide analytic calculi for, e.g., [[Modal logic|modal]], [[Intermediate logic|intermediate]] and [[Substructural logic|substructural]] logics<ref>{{Cite journal|last=Minc|first=G.E.|date=1971|orig-year=Originally published in Russian in 1968|title=On some calculi of modal logic|url=https://books.google.com/books?id=RbsdZY6hHtoC&dq=%22On+some+calculi+of+modal+logic%22+Minc&pg=PA97|journal=The Calculi of Symbolic Logic. Proceedings of the Steklov Institute of Mathematics|publisher=AMS|volume=98|pages=97–124}}</ref><ref name=":0">{{Cite journal|last=Avron|first=Arnon|date=1996|title=The method of hypersequents in the proof theory of propositional non-classical logics|url=https://www.cs.tau.ac.il/~aa/articles/hypersequents.pdf|journal=Logic: From Foundations to Applications: European Logic Colloquium|publisher=Clarendon Press|pages=1–32}}</ref><ref>{{Cite journal|last=Pottinger|first=Garrel|date=1983|title=Uniform, cut-free formulations of T, S4, and S5|journal=[[Journal of Symbolic Logic]]|volume=48|issue=3|pages=900|doi=10.2307/2273495|jstor=2273495|s2cid=250346853 }}</ref> A '''hypersequent''' is a structure

<math>\Gamma_1 \vdash \Delta_1 \mid \dots \mid \Gamma_n \vdash \Delta_n</math>

where each <math>\Gamma_i \vdash\Delta_i</math> is an ordinary sequent, called a '''component''' of the hypersequent. As for sequents, hypersequents can be based on sets, multisets, or sequences, and the components can be single-conclusion or multi-conclusion [[sequent]]s. The '''formula interpretation''' of the hypersequents depends on the logic under consideration, but is nearly always some form of disjunction. The most common interpretations are as a simple disjunction

<math>(\bigwedge\Gamma_1 \rightarrow \bigvee \Delta_1) \lor \dots \lor (\bigwedge\Gamma_n \rightarrow \bigvee \Delta_n)</math>

for intermediate logics, or as a disjunction of boxes

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

for modal logics.

In line with the disjunctive interpretation of the hypersequent bar, essentially all hypersequent calculi include the '''external structural rules''', in particular the '''external weakening rule'''

<math>\frac{\Gamma_1 \vdash \Delta_1 \mid \dots \mid \Gamma_n \vdash \Delta_n}{\Gamma_1 \vdash \Delta_1 \mid \dots \mid \Gamma_n \vdash \Delta_n \mid \Sigma \vdash \Pi}</math>

and the '''external contraction rule'''

<math>\frac{\Gamma_1\vdash \Delta_1 \mid \dots \mid\Gamma_n \vdash \Delta_n \mid \Gamma_n \vdash \Delta_n}{\Gamma_1\vdash \Delta_1 \mid \dots \mid\Gamma_n \vdash \Delta_n}</math>

The additional expressivity of the hypersequent framework is provided by rules manipulating the hypersequent structure. An important example is provided by the '''modalised splitting rule'''<ref name=":0" />

<math>\frac{\Gamma_1 \vdash \Delta_1 \mid \dots \mid \Gamma_n \vdash \Delta_n \mid \Box \Sigma, \Omega \vdash \Box \Pi, \Theta}{\Gamma_1 \vdash \Delta_1 \mid \dots \mid \Gamma_n \vdash \Delta_n \mid \Box \Sigma \vdash \Box \Pi \mid \Omega \vdash \Theta}</math>

for modal logic '''[[S5 (modal logic)|S5]]''', where <math>\Box \Sigma</math> means that every formula in <math>\Box\Sigma</math> is of the form <math>\Box A</math>.

Another example is given by the '''communication rule''' for the intermediate logic [[Intermediate logic|'''LC''']]<ref name=":0" />

<math>\frac{\Gamma_1 \vdash \Delta_1 \mid \dots \mid \Gamma_n \vdash \Delta_n \mid \Omega \vdash A \qquad \Sigma_1 \vdash \Pi_1 \mid \dots \mid \Sigma_m \vdash \Pi_m \mid \Theta \vdash B }{\Gamma_1\vdash \Delta_1 \mid \dots \mid \Gamma_n \vdash \Delta_n \mid \Sigma_1 \vdash \Pi_1 \mid \dots \mid \Sigma_m \vdash \Pi_m \mid \Omega \vdash B \mid \Theta \vdash A}</math>

Note that in the communication rule the components are single-conclusion sequents.