Discussing "The Method of Hypersequents in the Proof Theory of Propositional Non-Classical Logics"

 (Link)

Author: Arnon Avron (Tel Aviv University)

Reference: Arnon Avron. The method of hypersequents in the proof theory of propositional non-classical logics. In Wilfrid Hodges, Martin Hyland, Charles Steinhorn, and John Truss, editors, Logic: From Foundations to Applications: European Logic Colloquium, page 1–32. Clarendon Press, USA, 1996.

Why this paper? Cited by Nested Sequents for First-Order Modal Logics via Reachability Rules and Falsification-Aware Calculi and Semantics for Normal Modal Logics Including S4 and S5

This paper returns us to the world of structural proof theory, and in particular the sequent calculus, a formalism for organising and (often) generating proofs in various logics. The `various logics’ part of that phrase is very important here – there are a huge number of different logics out there, capturing different notions of truth and ways of combining propositions. Unfortunately many of these logics do not, in any obvious way, lend themselves to a well behaved sequent calculus. This paper reviews some work on a more flexible generalisation of sequent calculus based on hypersequents.

A sequent is simply a list of assumptions (or premises) and a list of conclusions. Working with a list of all current assumptions is very natural, but a list of conclusions may seem more unusual. The intuition is to view that list as disjunctive, i.e. proving any one of the conclusions will do. Working with a list of conclusions rather than a single one is not necessary for every logic, but turns out to be important for some. Similarly, hypersequents are simply a list of sequents, typically viewed as a disjunction. As for standard sequents, this is pointless for some logics but does allow other logics to be handled that would otherwise resist a nice structural treatment. The magic of this is that we can create new proof rules that allow sequents to communicate with each other within the hypersequent, for example by exchanging conclusions between them, in ways that allow the proof of new theorems.

Hypersequent calculi are shown to exist for a variety of interesting logics. We see Gödel–Dummett logic, also known as Dummett’s LC, a logic in which propositions can be assigned a position on an infinitely long truth spectrum, with one proposition implying another if the second proposition is ‘more true’ than the first; the relevance logic RM, which can be understood via the Sugihara matrix - truth values range across the integers, with the non-negative integers designated as ‘true’, and logical negation exactly matching the negation of integers; S5, a long established member of the family of modal logics that resisted the toolkit of standard proof theory; and a couple of three-valued logics which allow for a single intermediate position between absolute truth and falsity.