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 …

This talk, based on [8], discusses the canonicity of inductive inequalities in a constructive
meta-theory, for classes of logics algebraically captured by varieties of normal and regular
lattice expansions. These results are obtained using the tools of uni ed correspondence
theory [6, 10, 7, 9, 3, 2, 13], and contribute to develop a theoretical environment in which
different proof techniques for canonicity and correspondence can be systematically
compared and connected to each other (cf.[12, 16, 11, 17]). These canonicity results …