一句话：在构造性元理论中证明归纳不等式对正规/正则格扩张簇的典范性，推广了 Sahlqvist 结果的构造性版本。
本文在构造性元理论下研究归纳不等式的典范性，对象是由正规与正则格扩张簇代数刻画的逻辑类。作者基于统一对应理论，为格扩张上的 ALBA 算法语言给出一种新解释：nominal 与 conominal 变量分别解释为正规/正则格扩张的典范扩张中的闭元素与开元素，而不是完美扩张中的完全交不可约与完全并不可约元素。论文证明 ALBA 在该解释下的正确性，并由此通过标准论证的构造性改造，得到 ALBA 成功处理的不等式具有构造性典范性。由于 ALBA 对归纳不等式成功，所宣称结论随之成立。该结果涵盖并推广了 Ghilardi-Meloni 与 Suzuki 关于 Sahlqvist 公式和不等式的构造性典范性结果。
We prove the canonicity of inductive inequalities in a constructive meta-theory, for classes of logics algebraically captured by varieties of normal and regular lattice expansions. This result encompasses Ghilardi-Meloni's and Suzuki's constructive canonicity results for Sahlqvist formulas and inequalities, and is based on an application of the tools of unified correspondence theory. Specifically, we provide an alternative interpretation of the language of the algorithm ALBA for lattice expansions: nominal and conominal variables are respectively interpreted as closed and open elements of canonical extensions of normal/regular lattice expansions, rather than as completely join-irreducible and meet-irreducible elements of perfect normal/regular lattice expansions. We show the correctness of ALBA with respect to this interpretation. From this fact, the constructive canonicity of the inequalities on which ALBA succeeds follows by an adaptation of the standard argument. The claimed result then follows as a consequence of the success of ALBA on inductive inequalities.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{ConradieP20,
title = {Constructive Canonicity of Inductive Inequalities},
author = {Willem Conradie and Alessandra Palmigiano},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 3},
year = {2020},
doi = {10.23638/lmcs-16(3:8)2020}
}