Sahlqvist Via Translation

Willem Conradie, Alessandra Palmigiano, Zhiguang Zhao

Research output: Contribution to JournalArticleAcademicpeer-review


In recent years, unified correspondence has been developed as a generalized Sahlqvist theory which applies uniformly to all signatures of normal and regular (distributive) lattice expansions. A fundamental tool for attaining this level of generality and uniformity is a principled way, based on order theory, to define the Sahlqvist and inductive formulas and inequalities in every such signature. This definition covers in particular all (bi-)intuitionistic modal logics. The theory of these logics has been intensively studied over the past seventy years in connection with classical polyadic modal logics, using versions of Gödel-McKinsey- Tarski translations, suitably defined in each signature, as main tools. In view of this state-of-the-art, it is natural to ask (1) whether a general perspective on Gödel-McKinsey- Tarski translations can be attained, also based on order-theoretic principles like those underlying the general definition of Sahlqvist and inductive formulas and inequalities, which accounts for the known Gödel-McKinsey-Tarski translations and applies uniformly to all signatures of normal (distributive) lattice expansions; (2) whether this general perspective can be used to transfer correspondence and canonicity theorems for Sahlqvist and inductive formulas and inequalities in all signatures described above under Gödel-McKinsey-Tarski translations. In the present paper, we set out to answer these questions. We answer (1) in the armative; as to (2), we prove the transfer of the correspondence theorem for inductive inequalities of arbitrary signatures of normal distributive lattice expansions. We also prove the transfer of canonicity for inductive inequalities, but only restricted to arbitrary normal modal expansions of bi-intuitionistic logic. We also analyze the difficulties involved in obtaining the transfer of canonicity outside this setting, and indicate a route to extend the transfer of canonicity to all signatures of normal distributive lattice expansions.

Original languageEnglish
Pages (from-to)15:1-15:35
JournalLogical Methods in Computer Science
Issue number1
Publication statusPublished - 1 Jan 2019


The research of the first author was partially supported by the National Research Foundation of South Africa, Grant number 81309. The research of the second and third authors has been made possible by the NWO Vidi grant 016.138.314, by the NWO Aspasia grant 015.008.054, and by a Delft Technology Fellowship awarded in 2013.

FundersFunder number
National Research Foundation of South Africa81309
Nederlandse Organisatie voor Wetenschappelijk Onderzoek015.008.054, 016.138.314


    • algorithmic correspondence
    • bi-Heyting algebras
    • canonicity
    • co-Heyting algebras
    • Gödel-McKinsey-Tarski translation
    • Heyting algebras
    • normal distributive lattice expansions
    • Sahlqvist theory


    Dive into the research topics of 'Sahlqvist Via Translation'. Together they form a unique fingerprint.

    Cite this