Logical duality and harmony Hypersequents The hypersequent framework extends the ordinary 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, intermediate and substructural logics A hypersequent is a structure where each 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 sequents. 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 for intermediate logics, or as a disjunction of boxes 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 and the external contraction rule 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 for modal logic S5, where means that every formula in is of the form . Another example is given by the communication rule for the intermediate logic LC Note that in the communication rule the components are single-conclusion sequents. Calculus of structures Nested sequent calculus The nested sequent calculus is a formalisation that resembles a 2-sided calculus of structures. Notes References Proof theory