Willem Conradie ; Alessandra Palmigiano - Constructive Canonicity of Inductive Inequalities

lmcs:4531 - Logical Methods in Computer Science, August 5, 2020, Volume 16, Issue 3 - https://doi.org/10.23638/LMCS-16(3:8)2020
Constructive Canonicity of Inductive InequalitiesArticle

Authors: Willem Conradie ORCID; Alessandra Palmigiano ORCID

    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.


    Volume: Volume 16, Issue 3
    Published on: August 5, 2020
    Accepted on: March 26, 2020
    Submitted on: May 23, 2018
    Keywords: Mathematics - Logic,03B45
    Funding:
      Source : OpenAIRE Graph
    • Aspasia 2011; Funder: Netherlands Organisation for Scientific Research (NWO); Code: 015.008.054

    Consultation statistics

    This page has been seen 1019 times.
    This article's PDF has been downloaded 225 times.