一种关于替代的模态方法

《Annals of Pure and Applied Logic》：A modal approach towards substitutions

　　余新图|苏贾塔·戈什|刘芬荣|李大柱美国普林斯顿大学计算机科学系摘要替换在众多领域中起着至关重要的作用，从分析社会舆论的动态、进行数学计算到开展博弈论分析。在许多情况下，考虑一步替换往往就足够了。然而，对于更复杂的情形，迭代替换则变得不可或缺。本文的主要目标是研究能够模拟单步替换和迭代替换的逻辑框架。我们探讨了这些逻辑的诸多特性，包括它们的表达能力、希尔伯特风格的证明系统以及可满足性问题。此外，我们还建立了所提出的框架与现有相关文献中的框架之间的联系。例如，我们明确了单步替换与许多经典逻辑中常见的标准句法替换之间的关系。同时，我们也特别关注迭代替换。在此背景下，我们将所提出的框架与现有的迭代推理框架进行了比较，从而凸显了我们提案的优势。章节节选替换作为一种普遍存在的机制许多现象都以替换作为核心机制。从日常的社会互动到理论计算，包括数学运算、博弈论分析以及逻辑运算，各个领域都有大量例子。在本文中，我们并非研究特定领域中替换的具体表现形式，而是旨在探索用于推理替换本身的逻辑框架。这不仅有助于我们更好地理解这一基本概念。单步替换的基本逻辑：公理化与可判定性现在，让我们提出一个正式的方案来探究替换的本质。本节重点介绍一种相对简单的框架——模态替换逻辑（MSL），它仅包含用于单步更新的替换运算符。针对该逻辑，我们构建了一个完整的希尔伯特风格证明系统，并证明了其可判定性。首先，让我们定义MSL的语言，它是通过以下方式对标准模态逻辑ML的语言LML进行扩展的：定义2.1 语言LMSLL设P为一个可数集合替换运算符与普通替换在第一节中，我们已经阐明了我们所理解的替换与普通替换φ[ψ/p]之间的概念差异。另一方面，承认这两种方法之间的密切关系也同样重要。MSL证明系统中的递归公理就是这种关联的一个例证：替换也具有类似的有效模式[9]。为了更好地理解替换运算符，在这部分中，我们探讨了两者之间的精确关系。迭代替换的模态逻辑这部分探讨了带有迭代替换运算符的增强型模态迭代替换逻辑（MISL）。该逻辑的语言在[5]中有介绍，我们将进一步探讨其形式特性。正如我们将要看到的，迭代计算使得该逻辑比MSL复杂得多。本节将展示各种有效性，以说明迭代运算符的工作原理，并正式证明第一节场景2中引入的向后归纳可以通过某种关系来表征。MISL与其他相关逻辑之间的关系在4.2节中，我们已经展示了MISL可以用来推理玩家的获胜位置，特别是对于有限的棋盘，公式◇?〈p:=□⊥;(p:=p∨□◇p)?〉p能够表示玩家1的获胜位置Win1。然而，如前所述，这也可以用μML来定义。那么，为何还要提出另一种逻辑，即MISL呢？这个问题促使我们探索MISL与其它涉及迭代计算的逻辑系统之间的联系，包括μML。MISL的表达能力与不可判定性在本节中，我们进一步探讨了MISL的其它特性，包括它的表达能力以及其可满足性问题的可判定性。我们将证明，尽管MISL比ML强大得多，但MISL公式的真实性仍然保持不变，符合ML的标准双模拟概念（第6.1节）；同时，该逻辑将被证明是高度不可判定的：其可满足性问题是Σ11完全的（第6.2节）。此外，当我们把注意力限制在非常简单的类别上时……结论鉴于替换在各个领域的广泛应用，我们开发了包含单步替换和迭代替换作为模态运算符的逻辑框架，这些运算符用于更新命题变量的赋值。我们的起点是一种仅有单步替换运算符的简单框架MSL。对于该逻辑，我们提供了完整的证明系统并证明了其可判定性。同时，我们也明确了这些运算符与普通句法替换之间的区别。然后，对于致谢我们感谢Johan van Benthem提出的有见地的讨论和宝贵意见，这些对完成本文至关重要。我们还要感谢Alexandru Baltag和丁一峰提供的有益意见，以及王艳静让我们注意到关于命题赋值的动态逻辑的研究。此外，我们也要感谢两位匿名审稿人提出的非常有用的意见，这些意见帮助提升了本文的质量。刘芬荣得到了清华大学“先进计划”的支持。