一句话:提出基于序理论的 Gödel–McKinsey–Tarski 翻译统一视角,并证明归纳不等式对应性与部分可典范性的迁移。
本文研究统一对应理论中 Sahlqvist/归纳公式与不等式的 Gödel–McKinsey–Tarski 翻译。问题在于:能否基于与 Sahlqvist 定义相同的序理论原则,给出适用于所有正规(分配)格扩张的翻译统一视角,并用它迁移对应性与可典范性定理。作者给出了肯定回答,建立了此类翻译的一般框架;随后证明任意正规分配格扩张中归纳不等式的对应性定理可经翻译迁移。对于可典范性,则在双直觉主义逻辑的正规模态扩张中证明了归纳不等式的迁移,并分析了超出该设定时的困难,指出推广到所有正规分配格扩张的可能路径。
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. This includes a general definition of the Sahlqvist and inductive formulas and inequalities in every such signature, based on order theory. 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 suitable versions of Goedel-McKinsey-Tarski translations as main tools. It is therefore natural to ask (1) whether a general perspective on Goedel-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 Goedel-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 Goedel-McKinsey-Tarski translations. In the present paper, we set out to answer these questions. We answer (1) in the affirmative; 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.