Unified correspondence as a proof-theoretic tool

Alessandra Palmigiano - Vrije Universiteit Amsterdam
Unified correspondence as a proof-theoretic tool
Nell'ambito del progetto "Teoria della dimostrazione e informazione extra-logica"

Abstract
In this talk we discuss a systematic connection between correspondence phenomena, well known from classical modal logic, and structural proof theory. This connection has been seminally observed and exploited by Marcus Kracht, in the context of his investigation on the expressive power of display calculi, in which he identified a class of modal axioms (which he calls primitive formulas) which can effectively be 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 beyond its original classical modal logic settings. This extension has given rise to a theory called unified correspondence, the most important technical tools of which are the syntactic characterization of (generalized) Sahlqvist axioms across normal LE-logics (logics the algebraic semantics of which is based on bounded lattices), and the algorithm ALBA, for effectively computing the first-order correspondent of any (generalized) Sahlqvist axiom in any arbitrary LE-language. It turns out that the same algorithm ALBA can also be used to generate the analytic structural rules corresponding to each axiom in a certain subclass of generalized Sahlqvist axioms, which completely characterizes the space of properly displayable LE-logics.