Hypersequents and Systems of Rules: Embeddings and Applications

TL;DR

This paper establishes a bi-directional embedding between hypersequent calculi and 2-systems, demonstrating their equivalent expressive power and enabling benefits like locality, analyticity, and rule translation.

Contribution

It introduces a novel embedding that links hypersequent calculi with 2-systems, enhancing understanding and application of both proof frameworks.

Findings

Equivalent expressive power of hypersequent calculi and 2-systems

Recovery of locality and analyticity properties for 2-systems

Rewriting hypersequent rules as natural deduction rules

Abstract

We define a bi-directional embedding between hypersequent calculi and a subclass of systems of rules (2-systems). In addition to showing that the two proof frameworks have the same expressive power, the embedding allows for the recovery of the benefits of locality for 2-systems, analyticity results for a large class of such systems, and a rewriting of hypersequent rules as natural deduction rules.