Hypersequents constitute a natural generalization of ordinary sequents. They may be thought as finite multisets (or sequences) of usual sequents. Obviously, every standard sequential calculus is also a hypersequential calculus. Hypersequents were first considered by G. Pottinger in 1983 an independently by A. Avron in 1987.

In Gentzen systems, the cut–elimination theorem is the central result which establishes the importance of this kind of systems. Intuitively, the cut–elimination theorem states that any assertion that possesses a proof in the (hyper)sequential calculus that makes use of the cut rule also possesses a cut–free proof, that is a proof that does not make use of the cut rule. A of cut–elimination theorem in a (hyper)sequent calculus for a given logic is desirable because of its important consequences such as the consistency of the logic and interpolation properties. Hypersequent showed to be a very suitable tool for presenting cut-free Gentzen type formulations of logics. The elimination for some systems of other rules such as contraction was already studied in the literature

Session 1. We will present an introduction to hypersequents. Definitions and basic properties will be presented.

Session 2. Some examples of hypersequential calculi will be analyzed. In particular, hypersequents for the four–valued logic T ML (tetravalent modal logic) will be presented as well as a cut–elimination theorem for this calculus.

Session 3. Formal hypersequents will be studied. Departing from a formal presentation of hypersequent in which meta-variables for contexts (i.e., sequents) are introduced in the language, hipersequential calculus will be presented as objects within a suitable category, along with its morphisms. Applications to this formal view of hypersequents will be exhibit.

Prerequisistes This is an introductory course and as such will be highly self-contained. Students will only be assumed to have a basic knowledge of classical propositional logic and some rudiments of category theory.