Proof systems: from nestings to sequents and back

TL;DR

This paper investigates the relationships between various proof systems like sequent, nested, and labelled calculi, providing algorithms for transformation and semantic characterizations for multiple logics.

Contribution

It introduces a general algorithm for converting nested proof systems into sequent calculus systems and offers semantic characterizations for several modal logics via translations.

Findings

Transformation algorithm from nested to sequent systems

Semantic characterizations for intuitionistic and modal logics

Case-by-case translation between labelled nested and sequent systems

Abstract

In this work, we explore proof theoretical connections between sequent, nested and labelled calculi. In particular, we show a general algorithm for transforming a class of nested systems into sequent calculus systems, passing through linear nested systems. Moreover, we show a semantical characterisation of intuitionistic, multi-modal and non-normal modal logics for all these systems, via a case-by-case translation between labelled nested to labelled sequent systems.