Heyting-Lewis 蕴涵的 Gödel-McKinsey-Tarski 与(不甚)Blok-Esakia 定理
逻辑
2026-03-02 v2 计算机科学中的逻辑
摘要
Heyting-Lewis 逻辑是直觉主义命题逻辑的一种扩展,带有严格蕴涵联结词,满足可在经典模态逻辑中证明的严格蕴涵公理的构造性对应物。该逻辑的变体出奇地广泛:它们作为(扩展了)Haskell 风格箭头的简单类型论的 Curry-Howard 对应物出现,在 Heyting 算术的可保持性逻辑中、在守卫(协)递归的证明论中,以及在直觉主义认知逻辑的一般化中出现。Heyting-Lewis 逻辑可在扩展了二元关系以解释严格蕴涵的直觉主义 Kripke 框架中解释。我们利用该语义定义描述框架(Esakia 空间的一般化),并建立代数解释与框架语义之间的范畴对偶。随后我们改造 Wolter 和 Zakharyaschev 的一种变换,将 Heyting-Lewis 逻辑翻译为带两个一元算子的经典模态逻辑。这使我们能借助经典结果获得一大类 Heyting-Lewis 逻辑的有限模型性质与可判定性。
引用
@article{arxiv.2105.01873,
title = {G\"odel-McKinsey-Tarski and (not quite) Blok-Esakia for Heyting-Lewis Implication},
author = {Jim de Groot and Tadeusz Litak and Dirk Pattinson},
journal= {arXiv preprint arXiv:2105.01873},
year = {2026}
}