Unified Correspondence as a Proof-Theoretic Tool

TL;DR

This paper explores the connection between correspondence phenomena in modal logic and display calculi, extending Kracht's results to a broad class of nonclassical logics using unified correspondence theory.

Contribution

It generalizes Kracht's characterization of analytic structural rules to DLE-logics through the application of unified correspondence theory.

Findings

Characterizes the space of properly displayable DLE-logics.

Extends Kracht's results to nonclassical logics.

Uses the ALBA algorithm for uniform Sahlqvist-class formula analysis.

Abstract

The present paper aims at establishing formal connections between correspondence phenomena, well known from the area of modal logic, and the theory of display calculi, originated by Belnap. These connections have been seminally observed and exploited by Marcus Kracht, in the context of his characterization of the modal axioms (which he calls primitive formulas) which can be effectively transformed into `analytic' structural rules of display calculi. In this context, a rule is `analytic' if adding it to a display calculus preserves Belnap's cut-elimination theorem. In recent years, the state-of-the-art in correspondence theory has been uniformly extended from classical modal logic to diverse families of nonclassical logics, ranging from (bi-)intuitionistic (modal) logics, linear, relevant and other substructural logics, to hybrid logics and mu-calculi. This generalization has given rise to a theory called unified correspondence, the most important technical tools of which are the algorithm ALBA, and the syntactic characterization of Sahlqvist-type classes of formulas and inequalities which is uniform in the setting of normal DLE-logics (logics the algebraic semantics of which is based on bounded distributive lattices). We apply unified correspondence theory, with its tools and insights, to extend Kracht's results and prove his claims in the setting of DLE-logics. The results of the present paper characterize the space of properly displayable DLE-logics.