Labelled Sequent Calculi for Propositional Team Logics

想象一下你正在尝试解决一个逻辑谜题。用传统的方法（称为“塔尔斯基语义学”，Tarskian semantics）来做这件事时，你只是从一个特定的角度来看待这个谜题。你会问：“这个陈述在此地、在这个特定位置是否为真？”

但本文的作者们正在研究一种不同类型的逻辑，称为团队语义学（Team Semantics）。与其只看一个点，不如想象你正在观察一整支团队的人站在一起。你不是在询问一个陈述对某一个人是否成立，而是在询问它对于整个群体作为一个整体行动是否成立。

这种“团队”方法被用于现实世界的场景中，例如弄清楚变量之间是如何相互依赖的（例如：“价格是否取决于颜色？”），或者理解语言中的问题含义（例如：“是‘正在下雨’是真的，还是‘正在下雪’是真的？”）。

问题：如何证明关于团队的命题

作者们想要创建一套规则（一个“计算器”），用来证明关于这些团队的陈述是真是假。他们称之为标记序列演算（Labelled Sequent Calculi）。

把“序列”（sequent）想象成一个天平。天平的一侧是你已知的各种事实（团队当前的状态）；另一侧是你想要证明的结论。目标是展示：如果左侧的事实为真，那么右侧的结论也必然为真。

论文介绍了四种特定的“计算器”（证明系统），对应四种不同类型的团队逻辑：

1. 基础探询逻辑（Basic Inquisitive Logic）：用于处理问题的标准团队逻辑。
2. 命题直觉主义依赖逻辑（Propositional Intuitionistic Dependence Logic）：处理“依赖关系”（如“A 依赖于 B”）的团队逻辑。
3. 两个扩展版本：它们增加了特殊的“张量析取”（Tensor Disjunction，一种表示“将团队拆分为两个独立小组以检查不同事物”的高级方式）。

工具：标签即团队成员

为了让这些演算能够运作，作者使用了标签（labels）。

• 想象每个团队成员都有一个名牌。
• 有些名牌属于个体（单个人）。
• 有些名牌属于群体（整个团队）。
• 这些规则允许你说类似这样的话：“集合 x 与集合 y 是相同的”或者“集合 x 是集合 y 的子集”。

论文提出了两种主要的演算类型：

1. “详细型”计算器 (G(L))

这个版本非常精确。它使用复杂的标签，这些标签可以代表团队、它们的并集（合并两个团队）以及它们的交集（寻找重叠部分）。

• 类比： 这就像是一个高端 GPS，它追踪交通拥堵中的每一辆车、它们的精确位置，以及它们如何汇合或分道。它在数学上是严谨的，并且完美镜像了团队在现实世界中的行为。
• 代价： 由于它追踪了如此多的细节，很难判断这个 GPS 是否会停止计算（它可能会陷入死循环）。

2. “终止型”计算器 (G*(L))

为了解决“陷入死循环”的问题，作者创建了一个简化版本。

• 类比： 这个 GPS 不再追踪每辆车的精确移动，而是说：“我们有一份包含 5 辆车的名单。让我们检查这 5 辆车的所有可能组合。”
• 诀窍： 他们假设存在有限数量的可能“状态”（例如有限数量的可能天气状况）。因为可能性是有限的，所以计算器保证会在一段时间后停止。它要么找到一个证明（成功！），要么撞到一堵墙，此时不再适用任何规则（失败/反例）。
• 意义所在： 这保证了你总是可以编写一个计算机程序，来判定这些逻辑中的陈述是真是假。

游戏的核心规则

论文证明了他们的演算具有可靠性（Sound）和完备性（Complete）：

• 可靠性（Sound）： 如果计算器说“真”，那么它实际上就是真的。（计算器不会撒谎）。
• 完备性（Complete）： 如果某件事实际上是真的，那么计算器最终一定能找到证明。（计算器不会遗漏任何真相）。

他们还证明了这些演算具有容许规则（admissible rules）。

• 弱化（Weakening）： 你可以在你的清单中添加额外的、无用的事实，而不会破坏逻辑。
• 收缩（Contraction）： 如果你在清单中列出了两次相同的结论，你可以将其视为只列出了一次。
• 剪切（Cut）： 如果 A 能推导出 B，且 B 能推导出 C，那么你可以直接跳过中间步骤，得出“A 能推导出 C”。

“张量”挑战

这篇论文中最难的部分之一是处理张量析取（即“拆分”规则）。

• 类比： 想象你有一支侦探团队。
  • 标准逻辑说：“如果全队对答案达成一致，则整个团队破获了案件。”
  • 张量逻辑说：“如果我们可以将团队拆分为两组，其中 A 组解决了案件的一部分，B 组解决了剩余的部分，那么团队就破获了案件。”
• 作者必须发明一种特殊的规则（称为 fin 规则）来处理这一点。因为他们假设“世界”（赋值）的数量是有限的，所以他们可以说明：“每一个团队都只是这些特定的、有限的世界的某种组合。”这使得他们能够通过数学手段模拟这种拆分行为。

总结

简而言之，作者构建了两套用于解决涉及人群（团队）逻辑谜题的规则书：

1. 一套详细的、数学上完美的规则书，它能处理复杂的群体交互，但难以实现自动化。
2. 一套简化的、保证能结束的规则书，它假设存在有限的可能性，从而允许计算机自动检查一个陈述是否为真。

他们证明了这两套规则书对于他们所研究的特定逻辑而言，既是可靠的（涵盖所有真实情况），也是完备的（涵盖所有可能的真理）。