Sahlqvist via Translation

In recent years, unified correspondence has been developed as a generalizedSahlqvist theory which applies uniformly to all signatures of normal andregular (distributive) lattice expansions. This includes a general definitionof the Sahlqvist and inductive formulas and inequalities in every suchsignature, based on order theory. This definition covers in particular all(bi-)intuitionistic modal logics. The theory of these logics has beenintensively studied over the past seventy years in connection with classicalpolyadic modal logics, using suitable versions of Goedel-McKinsey-Tarskitranslations as main tools. It is therefore natural to ask (1) whether ageneral perspective on Goedel-McKinsey-Tarski translations can be attained,also based on order-theoretic principles like those underlying the generaldefinition of Sahlqvist and inductive formulas and inequalities, which accountsfor the known Goedel-McKinsey-Tarski translations and applies uniformly to allsignatures of normal (distributive) lattice expansions; (2) whether thisgeneral perspective can be used to transfer correspondence and canonicitytheorems for Sahlqvist and inductive formulas and inequalities in allsignatures described above under Goedel-McKinsey-Tarski translations. In the present paper, we set out to answer these questions. We answer (1) inthe affirmative; as to (2), we prove the transfer of the correspondence theoremfor inductive inequalities of arbitrary signatures of normal distributivelattice expansions. We also prove the transfer of canonicity for inductiveinequalities, but only restricted to arbitrary normal modal expansions ofbi-intuitionistic logic. We also analyze the difficulties involved in obtainingthe transfer of canonicity outside this setting, and indicate a route to extendthe transfer of canonicity to all signatures of normal distributive latticeexpansions