Modeling Deontic Modal Logic in ASP

想象一下你是一名裁判，正在电脑大脑内部进行一场巨大的、隐形的“如果……会怎样？”游戏。在逻辑的世界里，讨论规则有两种主要方式。第一种就像一个严格的数学方程：“如果 A 为真，那么 B 必须 为真。”这是经典逻辑，它非常擅长处理事实。但第二种方式则更具人性化：“你 应当 做 B”，“或者 禁止 做 A”，“或者你被 允许 做 B”。这就是义务逻辑（deontic logic，源自希腊语中的“责任”一词）。它是关于规则、法律和道德义务的逻辑。棘手之处在于，现实生活是混乱的。有时你负有某种义务，但你却无法做到；有时你被禁止做某事，但你还是做了。几十年来，计算机科学家和哲学家一直致力于教计算机如何处理这些“应当”和“禁止”，而不至于让它们感到困惑或陷入被称为“悖论”的逻辑矛盾中。

这篇题为《在 ASP 中建模义务模态逻辑》（Modeling Deontic Modal Logic in ASP）的论文，正是在解决这个问题的。作者们是一组来自美国和西班牙的研究人员，他们提出了一种巧妙的新方法，来教计算机如何理解规则。他们使用了一种名为答案集编程（Answer Set Programming, ASP）的编程语言，这种语言本身就以处理“如果……会怎样”的情景和不完整信息的能力而闻名。论文指出，通过将规则视为全局约束（就像裁判在规则被违反时吹响的哨声，而不是强制事实发生的硬性命令），计算机终于可以解决困扰逻辑学家数十年的旧谜题。他们展示了这种方法如何优雅地修复著名的逻辑陷阱，比如“违背义务”（Contrary-to-Duty）悖论——即当一个人未能遵守之前的规则时，规则看起来似乎会产生自我矛盾。

“应当”与“必须”的魔力

要理解作者所做的工作，我们首先需要认识故事中的两个主角：义务（Obligation）与许可（Permission）。在日常生活中，我们知道“太阳升起是必然的”（自然事实）与“你应该归还图书馆的书”（可能会被打破的规则）之间的区别。在逻辑世界中，前者被称为真理模态（alethic，关于真理与必然性），后者被称为义务模态（deontic，关于责任与规范）。

作者注意到，计算机已经拥有两种处理这些不同思维类型的特殊工具，但它们一直被误用了：

1. 强否定（Strong Negation）： 这就像是一个硬性的“不”。如果计算机说“不是 在下雨”（强否定），这意味着它有证据证明确实没在下雨。这是一个事实。
2. 缺省否定（Default Negation，也称否定即失败）： 这就像是一个“可能不是”。如果计算机说“不是 在下雨”（缺省否定），它仅仅意味着它没有找到任何证据表明“正在下雨”。这是一种基于信息缺失的猜测。

论文的核心思想是将这两种计算机工具直接映射到这两种逻辑上。他们建议，当我们谈论“P 是必然的”（一个事实）时，我们使用强否定。但当我们谈论“并非必然 P”（意味着 P 可能为假，或者我们只是不知道）时，我们使用缺省否定。这个简单的切换让计算机能够区分硬性事实与可以被打破的规则。

“裁判”方法

这篇论文最具有创意性的部分在于他们如何处理义务。在许多旧系统中，像“你必须还车”这样的义务被视为一种强制计算机让“还车”这一事实发生的命令。但如果车被偷了呢？计算机就会崩溃，因为它无法强制让车被归还。

作者提出了另一种方法：将义务视为全局约束（或称为“否定”）。想象一下足球场上的裁判。裁判并不会强迫球员进球；裁判只是在发生犯规时吹哨。在作者的系统中，义务不是一个让某事变为真的命令，而是一个规则，它说：“如果你处于一个违反了该规则的世界中，那么这个世界就是无效的。”

例如，如果规则是“你必须系安全带”，计算机并不会强迫你系上。相反，它设置了一个约束：“任何你在驾驶时没有系安全带的世界都是无效的。”如果你在开车且没有系安全带，计算机只会简单地说：“在这些规则下，该场景是不可能的”，然后寻找另一个你确实系了安全带的场景。但至关重要的一点是，如果你有正当理由不系安全带（比如医疗紧急情况），计算机可以“预先拦截”这条规则。它会撤销针对特定情况的约束，允许该场景存在而不至于崩溃。

解决“奇肖姆”谜题

当论文解决违背义务悖论（也称为奇肖姆悖论，Chisholm's Paradox）时，其表现最为出色。这是一个著名的逻辑难题，过程如下：

1. 你应当去参加派对。
2. 如果你去，你应当告诉你的母亲。
3. 如果你不去，你应当不告诉你的母亲。
4. 你没去。

在旧的逻辑系统中，这会产生一团乱麻。计算机试图弄清楚你是否应该告诉你的母亲，结果导致了矛盾：你既应该告诉她，又不应该告诉她。这就像机器人得了头痛一样。

作者展示了他们的“裁判”方法是如何瞬间解决这个问题的。他们将规则设定为约束：

• 约束 1：如果你不去，你就不能告诉你的母亲。
• 约束 2：如果你去，你必须告诉你的母亲。

当计算机看到你没去（事实 4）时，它会检查约束。它看到约束 2（“如果你去”的规则）并不适用，因为前提条件未满足。接着它查看约束 1。由于你没去，规则说“不要告诉”。计算机可以轻松找到一个你既没去也没告诉母亲的有效世界。没有矛盾，没有头痛。这个“悖论”消失了，因为规则被视为只在满足其条件时才生效的灵活约束，而不是互相冲突的硬性命令。

为什么这很重要

作者不仅解决了一个谜题，还展示了这种方法如何适用于一整类逻辑问题，包括“福雷斯特悖论”（Forrester's paradox）和“萨特困境”（Sartre's dilemma）。他们证明了通过使用具备处理“如果……会怎样”和“例外情况”能力的答案集编程，我们可以比以前更自然地模拟复杂的伦理和法律系统。

他们还展示了这如何处理“次级义务”。想象一下你借了朋友的车。你有一个主规则：“还车”。但还有次级规则：“中午前还车”以及“还车时电量充满”。如果你撞坏了车（违反了主规则），次级规则可能会改变或消失。作者展示了他们的系统如何自动“预先拦截”这些规则。如果车毁坏了，约束“中午前还车”就会被撤销，因为前提条件（拥有一辆可以归还的车）已经不存在了。计算机不会感到困惑，它只是更新了有效世界的列表。

总结

这篇论文并不声称已经解决了伦理学或法律中的所有问题。相反，它提供了一个简洁、优雅的工具包，用于构建理解规则的系统。它证明了通过将“应当”视为对可能世界的约束而非改变现实的命令，我们可以构建出像人类一样进行推理的计算机：灵活、接受例外，并且不会陷入逻辑循环。作者指出，这种方法比以往的方法更简单、更直接，因为以往的方法通常需要复杂的数学模型或“制裁”（惩罚）才能使逻辑生效。通过利用答案集编程中已有的工具，他们表明，通往理解人类式规则之路可能比我们想象的要更短、更直。