Embedding the hypersequent calculus in the display calculus

摘要

The difficulty in finding analytic Gentzen sequent calculi for non-classical logics has lead to the development of many new proof frameworks (proof systems) that have been used to give analytic calculi for these logics. The multitude and diversity of such frameworks has made it increasingly important to identify their interrelationships and relative expressive power. Hypersequent and Display calculi are two widely-used proof frameworks employed to present analytic calculi for large classes of logics. In this article, we show how any hypersequent calculus can be used to construct a display calculus for the same logic. The display calculus we obtain preserves proof-theoretic properties of the original calculus including cut-elimination and the subformula property. Since the construction applies to any hypersequent calculus, this result shows that in terms of presenting logics the display calculus formalism subsumes the hypersequent calculus formalism.