Recovery operators in quasi-Nelson logic: the prelinear case

会议: ECCV 2026
arXiv: 2606.31277
领域: others
关键词: 准Nelson逻辑, 复原算子, 一致性算子, 未定性算子, 预线性条件, 形式不一致逻辑, 形式未定逻辑

一句话总结

本文将经典的一致性和未定性复原算子推广到准Nelson逻辑的预线性情形，证明在非对合条件下（预线性弱幂零极小代数）所有已有关于对合剩余格上的LFIs/LFUs的代数与逻辑结论均可重新建立。

研究背景与动机

形式不一致逻辑（LFIs）是一类重要的容悖逻辑系统，其核心思想是通过引入一致性算子◦来恢复爆炸原则的有控使用：当一个公式 φ 同时被断言和否定时，只要 φ 是一致的（即 ◦φ 成立），才允许推出矛盾。对偶地，形式未定逻辑（LFUs）则处理排中律不成立的情形，通过未定性算子•来恢复排中律：每个公式 φ 要么为真、要么为假、要么未定。这两类算子统称为复原算子（recovery operators），在哲学逻辑、知识表示和人工智能中的不确定性推理中有深远意义。

经典LFI/LFU理论主要建立在对合剩余格（IMTL-代数）上，即双重否定律 ¬¬x = x 成立的结构。然而现实中的许多非经典逻辑（如直觉主义逻辑、Gödel逻辑、以及更一般的次结构逻辑）并不满足对合性。这就提出了一个自然问题：能否把复原算子理论推广到非对合的场景？准Nelson代数（Quasi-Nelson algebras, QN）恰好提供了一个理想的框架——它同时推广了Nelson代数（对合）和Heyting代数（幂等），形成一个三次幂、可分配、但不必对合的剩余格族，而以弱幂零极小代数（WNM-代数）为特例的预线性准Nelson代数（PQN-代数）更具有良好的代数和逻辑性质（半线性、局部有限性、链生成等）。

然而，非对合情形下一致性和未定性算子不再互为对偶（在IMTL中可通过 ◦φ = ¬•φ 互定义），这一断裂带来了全新的技术挑战。本文的核心贡献正是填补这一空白：系统考察PQN-代数上两类复原算子的代数理论，证明在添加适当的拟等式约束（使否定"几乎对合"）后，半线性和生成性质将被恢复，并给出相应的逻辑系统（LFIs和LFUs）及其语义完全性定理。

核心 idea：在预线性准Nelson代数中，通过引入"几乎对合"的拟等式条件 E(A) = B(A)，使得否定在1的左邻域表现出对合行为，从而在非对合框架下重建一致性算子和未定性算子的全部代数与逻辑理论，并证明相应的半线性和DAT定理。

方法详解

整体框架

本文的方法结构是一条清晰的代数→逻辑的双线路径。代数侧从PQN-代数出发，分别膨胀以未定性算子•和一致性算子◦，考察膨胀后的代数的半线性（是否由全序链生成）与生成性质；逻辑侧则基于代数语义，分别构造对应的LFU和LFI逻辑系统，证明它们的强完全性、保守可扩张性以及传播性与DAT定理。两条线相互支撑：代数结果（如半线性判定）直接决定逻辑系统的链完全性；逻辑结果（如DAT）又反向验证算子定义的恰当。

以下框架图捕捉了论文的整体逻辑结构，每类算子再按"Boolean性"（◦•是否落在Boolean元中）细分为 max/Bmax/min/Bmin 等变种：

%%{init: {'flowchart': {'rankSpacing': 24, 'nodeSpacing': 28, 'padding': 6, 'wrappingWidth': 400}}}%%
flowchart TD
    A["基框架<br/>PQN-代数<br/>(预线性·三次幂·分布·非对合)"] --> B1["未定性算子 •"]
    A --> B2["一致性算子 ◦"]

    B1 --> C1["PQN•ₘ<br/>min-未定性"]
    B1 --> C2["PQN•_Bₘ<br/>Bmin-未定性"]
    B1 --> C3["PQN•_ₘB<br/>minB-未定性"]
    B2 --> C4["PQN◦ₘ<br/>max-一致性"]
    B2 --> C5["PQN◦_Bₘ<br/>Bmax-一致性"]
    B2 --> C6["PQN◦_ₘB<br/>maxB-一致性"]

    C1 --> D1{"是否半线性？"}
    C2 --> D1
    C3 --> D1
    C4 --> D2{"是否半线性？"}
    C5 --> D2
    C6 --> D2

    D1 -->|PQN•_Bₘ 是| E1["由全序链生成<br/>→ 单一标准链生成"]
    D1 -->|其余 否| E2["非半线性<br/>→ 需加 ∨-闭包恢复"]

    D2 -->|PQN◦_Bₘ 否| E3["非半线性<br/>→ 反例 A₆ 链"]
    D2 -->|加'几乎对合'条件| E4["aiPQN◦ 半线性<br/>→ E(A)=B(A)"]

    E1 --> F["逻辑侧"]
    E4 --> F
    E2 --> F

    F --> G1["LFU 逻辑<br/>PQN•_Bₘ<br/>•δ 传播性+完全性"]
    F --> G2["LFI 逻辑<br/>(PQN◦∨ₘ)≤ 度保持<br/>及 nf-PQN◦∨ₘ 非假值保持"]
    F --> G3["DAT 定理<br/>PQN•_Bₘ 与 nf-PQN◦∨ₘ<br/>满足DAT"]

    E1 -.->|链上 •唯一: ˆ•a=0 当a∈{0,1}, 否则1| D1
    E4 -.->|链上 ◦唯一: ˆ◦a=1 当a∈E(A), 否则0| D2

关键设计

1. 膨胀链的算子唯一性：两类复原算子在PQN链上的确定形式

在PQN-代数中，代数结构本身并不唯一确定复原算子的定义——可以有多种方式在代数上添加◦和•。但在全序的PQN-代数（即PQN链）上，情况大大简化：两类算子都唯一确定。

对于未定性算子•，给定一个PQN链 A，其唯一的最小未定性算子 ˆ• 为：ˆ•a = 0 当 a=0 或 a=1，否则 ˆ•a = 1。这个算子同时也是Bmin和minB算子。直观上讲：只有两极值元素是"确定的"（determined），中间元素都是"未定的"——它们既不真也不假。为什么恰由Boolean元素刻画？因为对于链中的非 {0,1} 元素 a，满足 a ∨ ¬a ∨ b = 1 的最小 b 必然就是 1。

对于一致性算子◦，唯一性需要借助爆裂元集合 E(A) = {x ∈ A | x ∧ ¬x = 0}：ˆ◦a = 1 当 a ∈ {0} ∪ E(A)，否则 ˆ◦a = 0。这里的关键洞见是：在预线性情形下，爆裂元并不一定等于Boolean元（后者还要求 x ∨ ¬x = 1），因此在非对合代数上两者是严格包含关系 E(A) ⊇ B(A)。一致性算子选择的就是爆裂元这个更弱的条件——一个元素"可爆炸"是它被认可为一致的前提。

2. 半线性判别条件：Boolean元、爆裂元与"几乎对合"拟等式

在非对合代数上膨胀了复原算子后，得到的（拟）族是否仍由全序链生成（即是否保持半线性），是本文的核心技术问题。

对于未定性算子•，类型Bmin（满足 •x ∨ ¬•x = 1）的膨胀族 PQN•_Bₘ 保持半线性。关键引理（Lemma 3.4）揭示：在PQN•_Bₘ代数中，B(A) = {0,1} 当且仅当 A 是全序的。由此可直接推论出所有次直不可约代数都是链，因此半线性成立。反观min和minB类型，[14]中的反例（有限NM-代数上的非全序次直不可约代数）表明它们并非半线性。

对于一致性算子◦，情况更复杂。类型Bmax的膨胀族 PQN◦_Bₘ 不是半线性的——论文显式构造了一个6元素反例 ⟨A₆, ◦⟩（图2），它不是全序的但却是次直不可约的。要恢复半线性，需要施加一个拟等式 ¬x = 0 ⇒ x = 1，其等价形式为 x ∨ ¬x ∨ ¬◦x = 1。这个条件在代数上的效果是迫使 E(A) = B(A)，即爆裂元集合等于Boolean元集合。它使得标准PQN代数 Sn 的否定在1的左邻域表现出几乎对合的行为（图4），因此得名"几乎对合"。在这个条件下，aiPQN◦_Bₘ 重新获得半线性（Corollary 4.9），且所有三种一致性算子类型（max/Bmax/maxB）在链上等价，从而膨胀链族重合。

3. 逻辑建模与DAT定理：两类逻辑系统的完全性与经典逻辑恢复

论文基于代数结果构建了对应的逻辑系统，并证明了三个层次的结论。

首先是语义完全性。通过将推理规则替换为其 ∨-闭包形式（使规则对析取封闭），可以保证逻辑的链完全性（Theorem 6.3, 7.2）。对于未定性算子，PQN•_Bₘ 本身就是半线性的，故无需 ∨-闭包；对于一致性算子，pqn◦∨指的就是 ∨-闭包后的版本。

其次是传播性（propagation property）：复原算子对逻辑连接词的保持性质。在 PQN•_Bₘ 中，对偶未定性算子 •δ = ¬• 满足完全传播：如果 •δφ₁ 和 •δφ₂ 都成立，则 •δ(φ₁#φ₂) 对任意 #∈{∧,∨,∗,→} 也成立（Proposition 7.13）。在 LFI逻辑 (PQN◦∨ₘ)≤ 和 nf-PQN◦∨ₘ 中，一致性算子◦也满足同样的传播性（Proposition 7.14, 7.16）。

最后是关键的派生性调整定理（Derivability Adjustment Theorem, DAT）：在复原算子保护下可以恢复经典逻辑推理。对于 LFU 逻辑 PQN•Bₘ，由于 •δ 起到双重复原作用（同时恢复爆炸原则和排中律），DAT 成立：Γ ⊢_CPL φ 当且仅当 Γ ∪ {•δp₁, ..., •δpₙ} ⊢ φ（Proposition 7.15）。而对 LFI 逻辑 (PQN◦∨ₘ)≤，DAT不成立（因为◦φ φ ∨ ¬φ 不为定理），但其非假值保持变体 nf-PQN◦∨ₘ 则满足更精细的DAT：利用"守护MP规则" ◦ψ, ◦χ, ψ, ψ→χ ⊢ χ 实现了经典推理的重构（Proposition 7.18）。

损失函数 / 训练策略

本文为纯代数/逻辑理论论文，不涉及数值损失函数或实验训练。

实验关键数据

关键定理与结果

类别	结果	意义
未定性算子·半线性	PQN•_Bₘ 半线性（Thm 3.5），PQN•_ₘ 和 PQN•_ₘB 非半线性	Bmin型保持链生成，其余需∨-闭包
一致性算子·半线性	PQN◦_Bₘ 非半线性（反例 A₆）	与未定性情形形成对比
几乎对合恢复	aiPQN◦_Bₘ 半线性（Cor 4.9），条件 E(A)=B(A)	非对合框架的精确定位
LFU完全性	PQN•∨全链完全，单一链生成（Thm 6.3, Cor 6.5）	与经典LFI理论平行
LFI完全性	(PQN◦∨ₘ)≤ 链完全，构成LFI（Thm 7.6, Cor 7.7）	度保持逻辑的首次完整处理
DAT·LFU	PQN•_Bₘ 满足DAT（Prop 7.15）	双复原效应
DAT·LFI	nf-PQN◦∨ₘ 满足DAT，度保持版本不满足（Prop 7.18）	非假值保持是DAT的关键

关键发现

• 非对合下的一致性与未定性算子不再对偶，这是本文区别于所有已有工作的核心差异。在IMTL中只需定义其一即可通过·→¬·得到另一个；在PQN中两者需要分别研究，且代数性质高度不对称（Bmin半线性但Bmax非半线性）。
• "几乎对合"并非强加而是理论内在需求：要使一致性算子膨胀族保持半线性，不是随便加个条件，而是自然得出 E(A)=B(A) 这个拟等式，它在逻辑上等价于 ¬φ = 0 ⇒ φ = 1，恰好刻画了"否定仅在1处消失"的温和非对合行为。
• Twist结构构造为未来研究提供了通往范畴论和Esakia对偶化的桥梁（Section 8），说明本文的代数模型不是终点而是进一步拓扑/范畴推广的起点。

亮点与洞察

• 爆裂元集合取代Boolean元集合：在非对合设定下，Boolean元不足以刻画一致性——论文使用爆裂元集合 E(A) = {x: x ∧ ¬x = 0} 替代，这是对经典LFI理论的本质扩展。爆裂元更弱但更精确：在Gödel链上每个元素都是爆裂元，但只有 {0, 1} 是Boolean元（Example 4.5），这解释了为什么Heyting代数不适合做LFI语义。
• 单链生成结果的技术优雅性：Theorem 3.8 和 4.11 分别证明 PQN•_Bₘ 和 aiPQN◦_Bₘ 可由单个标准PQN链 Sn 的膨胀生成，这意味着这些逻辑本质上由一个模型就能决定全部语义——一种非常强的有限可公理化形式。
• 双逻辑路径的一致性：度保持伴侣 (PQN◦∨ₘ)≤ 构成LFI但失去DAT，非假值保持伴侣 nf-PQN◦∨ₘ 则恢复DAT。这个发现揭示了"保真"与"保非假"在经典逻辑恢复中不可兼得的微妙权衡，并且不可直接迁移至对合情形。

局限与展望

• 论文框架依赖三次幂性质（x³ = x²），该性质来自Nelson方程。作者明确指出，将结果推广到一般的非对合分配剩余格（摆脱三次幂限制）仍需未来研究（Section 8）。
• 两种算子同时存在时的相互作用仅在Section 5中简要讨论，尚未建立完整的互定义关系在逻辑层面的刻画——特别是在非几乎对合情形下，◦和•的交叉约束是怎样的。
• 白色算子 ◦E 和 ◦B 在非预线性设定下的等价性问题（Remark 4.3）仍未完全解决；超出预线性范围后两者的行为尚需澄清。
• twist构造（准Nelson代数的Heyting+滤子表示）虽然已在代数侧延伸到复原算子扩张，但相应的Esakia对偶理论（拓扑层面）仍有待建立——这将是连接范畴论与逻辑语义的有力工具。

相关工作与启发

• vs [Esteva et al. 2021 (LFI on IMTL)]: 该工作是本文的直接前驱，建立了对合分配剩余格上LFIs/LFUs的完整理论。本文的核心推进是去掉了对合假设，在准Nelson代数上重建了所有结论。本文多处引[14]的反例和技术路径作为起点，然后在PQN环境中进行非对合推广。
• vs [Carnielli et al. 2020 (Recovery operators)]: 该工作从哲学逻辑角度系统分类了复原算子的可能性质。本文则为这种分类提供了在准Nelson代数框架下的具体代数实现，特别是证明了某些算子性质（如Boolean性）在非对合设定下会导致半线性的丧失。
• vs [Rivieccio & Figallo 2024 (Inconsistency operators on QN)]: 该姊妹篇[35]在一般（非预线性）准Nelson代数上引入了一致性和未定性算子。本文的独特贡献在于聚焦预线性子族（PQN），从而可以研究半线性、链生成和逻辑完全性这些在一般QN中无意义的问题。

评分

• 新颖性: ⭐⭐⭐⭐ [将LFI/LFU理论从对合推进到非对合准Nelson代数，填补了次结构逻辑与容错逻辑间的结构性缺口，且发现了非对合下两类算子不对称半线性的精细现象]
• 实验充分度: ⭐⭐⭐⭐ [作为理论数学论文，29页内完成了代数→逻辑→DAT的完整双线论证，包含显式反例构造（A₆）、多条等价链的定理证明、以及标准链生成这一类通常需要高技巧的结果]
• 写作质量: ⭐⭐⭐⭐⭐ [引言清晰阐述了四类复原算子的逻辑动机与代数背景，全文组织结构层次分明（代数侧分•/◦两条线独立展开再在第5节汇合，逻辑侧分度保持/非假值保持两条路径），且每节开头都有明确的前情回顾与承上启下]
• 价值: ⭐⭐⭐⭐ [对非经典逻辑学界（容错逻辑、模糊逻辑、次结构逻辑）有重要意义，为在人工智能中的不确定性推理系统（如基于模糊逻辑的专家系统、需要容错能力的知识库）中嵌入复原算子提供了理论基础]

相关论文

• [ECCV 2026] Belief Contraction in Dynamic Epistemic Logic
• [AAAI 2026] Model Change for Description Logic Concepts
• [ICLR 2026] Improving Set Function Approximation with Quasi-Arithmetic Neural Networks
• [CVPR 2026] NeuroRule: Bridging Vision and Logic with Differentiable Rule Induction
• [AAAI 2026] From Decision Trees to Boolean Logic: A Fast and Unified SHAP Algorithm