Multi-type Sequent Calculi

TL;DR

This paper introduces multi-type sequent calculi that extend display calculi by allowing multiple types and relaxing display properties, enabling better handling of complex logics like multi-modal and dynamic logics.

Contribution

It generalizes display calculi to a multi-type framework and weakens display properties, broadening applicability to diverse logical systems.

Findings

Establishes a canonical cut elimination meta-theorem for multi-type calculi.

Shows the framework's usefulness for multi-modal and dynamic logics.

Provides a unified proof-theoretic setting for generalized calculi.

Abstract

Display calculi are generalized sequent calculi which enjoy a `canonical' cut elimination strategy. That is, their cut elimination is uniformly obtained by verifying the assumptions of a meta-theorem, and is preserved by adding or removing structural rules. In the present paper, we discuss a proof-theoretic setting, inspired both to Belnap's Display Logic and to Sambin's Basic Logic, which generalises these calculi in two directions: by explicitly allowing different types, and by weakening the so-called display and visibility properties. The generalisation to a multi-type environment makes it possible to introduce specific tools enhancing expressivity, which have proved useful e.g. for a smooth proof-theoretic treatment of multi-modal and dynamic logics. The generalisation to a setting in which full display property is not required makes it possible to account for logics which admit connectives which are neither adjoints nor residuals, or logics that are not closed under uniform substitution. In the present paper, we give a general overview of the calculi which we refer to as multi-type calculi, and we discuss their canonical cut elimination meta-theorem.