paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Sahlqvist via Translation

经由翻译的 Sahlqvist 理论
LMCS vol.Volume 15, Issue 12019匹配度 1/10 · 该论文属于纯数理逻辑中的 Sahlqvist 对应理论与 Gödel–McKinsey–Tarski 翻译,核心是模态/直觉主义逻辑的序理论统一视角,与用户关注的 PL→AI(静态分析/Agentic 程序)、AI→PL(LLM 改进静态分析与形式化验证)、浮点程序分析及贝叶斯程序分析几乎没有交集;它不涉及 LLM、程序分析、工业落地或 benchmark。引用 22 inbox
Willem Conradie, Alessandra Palmigiano, Zhiguang Zhao
crossref: 2026-09-10

AI 速览

一句话:提出基于序理论的 Gödel–McKinsey–Tarski 翻译统一视角,并证明归纳不等式对应性与部分可典范性的迁移。

本文研究统一对应理论中 Sahlqvist/归纳公式与不等式的 Gödel–McKinsey–Tarski 翻译。问题在于:能否基于与 Sahlqvist 定义相同的序理论原则,给出适用于所有正规(分配)格扩张的翻译统一视角,并用它迁移对应性与可典范性定理。作者给出了肯定回答,建立了此类翻译的一般框架;随后证明任意正规分配格扩张中归纳不等式的对应性定理可经翻译迁移。对于可典范性,则在双直觉主义逻辑的正规模态扩张中证明了归纳不等式的迁移,并分析了超出该设定时的困难,指出推广到所有正规分配格扩张的可能路径。

问题
如何为 Gödel–McKinsey–Tarski 翻译建立基于序理论的统一视角,并据此迁移 Sahlqvist/归纳公式与不等式的对应性和可典范性。
方法
在统一对应框架下,以序理论定义翻译,处理正规(分配)格扩张以及双直觉主义模态逻辑等签名。
评估
通过元理论证明进行评估:证明归纳不等式对应性可迁移到任意正规分配格扩张;可典范性迁移限于双直觉主义逻辑的正规模态扩张,并讨论扩展困难。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot824,
  title = {Sahlqvist via Translation},
  author = {Willem Conradie and Alessandra Palmigiano and Zhiguang Zhao},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 15, Issue 1},
  year = {2019},
  doi = {10.23638/lmcs-15(1:15)2019}
}