TY - JOUR

T1 - Constructive canonicity of inductive inequalities

AU - Conradie, Willem

AU - Palmigiano, Alessandra

PY - 2020/8/5

Y1 - 2020/8/5

N2 - 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 ex-pansions. 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.

AB - 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 ex-pansions. 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.

KW - Algorithmic correspondence theory

KW - Constructive canonicity

KW - Lattice theory

KW - Modal logic

KW - Sahlqvist theory

UR - http://www.scopus.com/inward/record.url?scp=85090779479&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85090779479&partnerID=8YFLogxK

U2 - 10.23638/LMCS-16(3:8)2020

DO - 10.23638/LMCS-16(3:8)2020

M3 - Article

AN - SCOPUS:85090779479

SN - 1860-5974

VL - 16

SP - 8:1-8:39

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

IS - 3

M1 - 8

ER -