标题： 统一对应作为证明论工具 显示英文标题

标题： Unified Correspondence as a Proof-Theoretic Tool

摘要： 本文旨在建立对应现象之间的形式联系，这些现象在模态逻辑领域是众所周知的，并且与Belnap提出的显示演算理论相关。 这些联系由Marcus Kracht首次观察并加以利用，在他对于可以有效转化为显示演算的“分析性”结构规则的模态公理（他称之为原始公式）的特征描述背景下。 在此背景下，如果将一个规则添加到显示演算中，并保持Belnap的消去定理，则该规则是“分析性”的。 近年来，对应理论的最新进展已从经典模态逻辑统一扩展到各种非经典逻辑家族，范围从（双）直觉主义（模态）逻辑、线性逻辑、相关逻辑和其他子结构性逻辑，到混合逻辑和mu演算。 这种推广产生了一种称为统一对应的理论，其中最重要的技术工具是算法ALBA，以及在正常DLE逻辑（其代数语义基于有界分配格的逻辑）设置下对Sahlqvist类型公式和不等式的语法特征描述。 我们应用统一对应理论及其工具和见解，以扩展Kracht的结果，并在DLE逻辑的背景下证明他的主张。 本文的结果描述了适当可显示DLE逻辑的空间。 显示英文摘要

摘要： 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.