归纳不等式的构造典范性
Constructive Canonicity of Inductive Inequalities
AI总结：
本文在构造性元理论中，利用统一对应理论工具，通过重新解释ALBA算法中名义变量的语义，证明了归纳不等式的典范性，推广了既有构造性典范性结果。
摘要：
我们在构造性元理论中证明了归纳不等式的典范性，针对由正规和正则格扩张的簇代数刻画的一类逻辑。该结果涵盖了Ghilardi-Meloni和Suzuki关于Sahlqvist公式和不等式的构造性典范性结果，并基于统一对应理论工具的应用。具体而言，我们为格扩张的算法ALBA的语言提供了一种替代解释：名义变量和共名义变量分别被解释为正规/正则格扩张的典范扩张中的闭元素和开元素，而非完全正规/正则格扩张中的完全并不可约和交不可约元素。我们证明了ALBA相对于此解释的正确性。由此事实，通过标准论证的改编，ALBA成功处理的那些不等式的构造性典范性得以推出。所声称的结果随后作为ALBA对归纳不等式成功处理的结果而得出。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
