带双否定算子的直觉主义逻辑扩展的对应数学结构及Heyting代数改造问询

这个关于直觉主义逻辑扩展的问题挺有深度的，先帮你梳理下背景，再聊聊对应的数学结构和Heyting代数的改造思路：

首先回顾哥德尔建立的直觉主义逻辑到经典S4模态逻辑的映射规则：

• 对于正原子公式$A$：$A' = \Box A$
• 直觉主义否定$\sim$的映射：$(\sim A)' = \Box \sim (A')$
• 合取运算：$(A \land B)' = A' \land B'$
• 析取运算：$(A \lor B)' = A' \lor B'$
• 蕴涵运算：$(A \implies B)' = \Box (A' \implies B')$

在此基础上添加新否定算子$\neg$的映射规则：$(\neg A)' = \sim \Box (A')$，就得到了一套能区分两种否定的命题逻辑——其中$\sim$对应“不可能性”，$\neg$对应“不必要性”。需要注意的是，这套逻辑虽是直觉主义逻辑的朴素扩展，但因为新否定算子下排中律可证，所以它是非构造性的。

接下来回答你关心的两个核心问题：

一、对应数学结构/系统 #

从已有的研究来看，这套逻辑并没有像直觉主义对应Heyting代数、简单类型lambda演算那样的“标准”对应结构，但可以从两个方向找到关联：

1. 代数层面：它本质上是带双否定的S4模态Heyting代数——模态Heyting代数（又称拓扑Heyting代数）本身已经包含了$\Box$算子（对应拓扑里的内部算子），而这里的两个否定分别对应：
   • 原直觉主义否定$\sim a = a \implies \bot$（Heyting代数中的伪补）；
   • 新否定$\neg a = \sim \Box a$（对元素先取内部算子再取伪补）。
2. lambda演算层面：目前没有成熟的标准对应系统，但可以通过扩展简单类型lambda演算来构造——需要添加模态类型构造器$\Box$，再为两个否定分别设计对应的项引入/消去规则，不过这类扩展更多是研究性的，尚未成为通用标准。

二、改造Heyting代数的思路 #

要把Heyting代数适配这套逻辑，需要分三步进行：

1. 引入模态算子$\Box$：先将Heyting代数扩展为模态Heyting代数，要求$\Box$满足S4模态的核心公理：
   • $\Box \top = \top$（顶元素的模态闭包还是自身）
   • $\Box(a \land b) = \Box a \land \Box b$（模态算子对合取分配）
   • $\Box a \leq a$（模态闭包是原元素的下界）
   • $\Box a \leq \Box \Box a$（模态闭包的闭包等于自身）
2. 定义双否定算子：
   • 保留原Heyting代数的直觉主义否定：$\sim a = a \implies \bot$（即元素关于$\bot$的伪补）；
   • 基于$\Box$定义新否定：$\neg a = \sim \Box a$。
3. 验证核心性质：需要确保改造后的代数满足逻辑中的关键规则，比如新否定下的排中律$\neg a \lor \neg \neg a = \top$——这一点在S4模态框架下是成立的，对应到代数中也能得到验证。

备注：内容来源于stack exchange，提问作者PW_246