Knowing-Value Logic with Successor Arithmetic

技术摘要：带有后继算术的知值逻辑

问题陈述
本文旨在解决现有“知值”（knowing-value）逻辑的局限性，特别是 Wang 和 Fan 提出的条件知值逻辑 ($ELKvr$) 及其公开公告扩展 ($PALKvr$)。虽然这些系统形式化了诸如“代理$i$在给定$\phi$的条件下知道$c$ 的值”之类的陈述，但它们缺乏处理算术运算和等式的句法机制。因此，它们无法捕捉涉及数字的命题的内部结构，例如连续整数之间的关系。在自然语言场景和逻辑谜题（如“连续数字”谜题）中，推理通常依赖于认识算子、等式与算术函数（特别是后继函数）之间的相互作用。现有的框架将数值条件视为不透明的命题字母，未能推导出在自然语言中显而易见的蕴含关系（例如，知道一个数是 4 位数，且知道“如果是 4 位数则为 1111”这一蕴含式，应当意味着知道其值为 1111）。此外，这些逻辑基于非结构化对象集的标准语义，不足以对具有后继函数的自然数等特定数学结构进行建模。

方法论
作者引入了一种新的逻辑 $ELKvSAr$**（**$PALKvSAr$ 的无公告版本），它通过以下方式扩展了条件知值逻辑：

1. 项（Terms）： 包括一个刚性常量 $0$、非刚性常量$C$以及后继函数$S$。
2. 原子公式（Atomic Formulas）： 项之间的等式 ($t_1 \approx t_2$)。
3. 语义（Semantics）： 本文定义了两类不同的模型：
   • 标准模型（Standard Models）： 基于标准自然数 $(\mathbb{N}, S)$。
   • 非标准模型（Non-Standard Models）： 基于特定的后继算术非标准模型 $(\mathbb{N}^\star, S^\star)$，其中 $\mathbb{N}^\star$ 包含标准自然数以及无限多个“Z-链”（整数的副本）。这种扩展是必要的，因为该逻辑在标准模型类上不具备紧致性。

技术方法包括：

• 公理化（Axiomatization）： 提出了系统 $ELKVSAr$**，它包含了等式公理、后继算术公理（例如$\neg Sx \approx 0$、$S$的单射性）以及连接知值与算术的特定公理/规则（例如$KvrS$、$KVE1$、$KVE2$）。一个关键特征是 **$Kvr\text{-}Elim$ 规则，其功能类似于一阶逻辑中的存在消去，允许在推导过程中移除相对化的知值算子。
• 完备性证明（Completeness Proof）： 证明了其对非标准模型的强完备性。该证明利用了一种新颖的**树状规范框架（tree-like canonical frame）**构建方法，而非标准的规范模型。这涉及构建极大一致集的历史（histories），并定义一个赋值函数，将常量映射到 $\mathbb{N}^\star$ 中的元素，同时尊重由知值算子和算术结构诱导的等价关系。
• 有限模型性质与可判定性（Finite Model Property and Decidability）： 证明了任何可满足的公式都具有一个有限的非标准模型，该模型随后可以通过一个保持算术距离并分离组件的单射映射到有限的标准模型。这确立了该逻辑的有限模型性质和可判定性。
• 应用（Application）： 使用公开公告算子（$PALKvSAr$）将“连续数字”谜题形式化，以展示代理的知识如何通过算术推导而演进。

主要贡献与结果

1. 逻辑扩展： 引入了 $ELKvSAr$和$PALKvSAr$，将等式和后继函数整合进条件知值逻辑。
2. 公理系统： 定义了 $ELKVSAr$，并证明其：
   • 对非标准模型是强完备的。
   • 对标准模型是弱完备的。
3. 元逻辑属性：
   • 有限模型性质 (FMP)： 该逻辑对于标准模型和非标准模型都具有 FMP。
   • 可判定性： $ELKvSAr$ 的可满足性问题是可判定的。
4. 非紧致性： 本文证明了 $ELKvSAr$ 对于标准模型不是紧致的，从而说明了引入非标准模型进行完备性证明的必要性。
5. 谜题求解： “连续数字”谜题被成功地在系统中形式化并求解，证明了该逻辑能够捕捉基于算术约束和认识更新的逐步可能性消除过程。

意义
本文声称提供了一个将认识逻辑与算术相结合的新颖框架。通过用后继函数丰富知值逻辑，该系统克服了以往方法粒度过粗的问题，使得形式化依赖于数值命题内部结构的推理成为可能。这项工作在表达能力（处理算术与认识交互）与计算复杂度（保持可判定性）之间取得了平衡。作者指出，该框架为未来涉及更复杂算术结构（加法和乘法）的扩展奠定了基础，而这些扩展对于解决如“和与积”之类的谜题是必要的，尽管此类扩展在完备性和可判定性方面面临着重大挑战。