依赖逻辑（三）

4.5 团队语义中的广义依赖和连接词

以上提到的依赖逻辑的变体和扩展都是通过引入新的原子或连接词从一阶逻辑（带有团队语义）中生成的。可以考虑广义依赖原子(Kuusisto 2015)，其方式与经典一阶逻辑中引入广义量词的方式大致相同。并提出如下问题：

对于哪些原子或连接词集合 D，FO(D)（即由 D 中的原子和连接词增强的一阶逻辑）在表达上等价于一阶逻辑？这样的集合 D 被称为强一阶的。

给定一个原子和连接词集合 D，对于哪些其他原子和连接词集合 E，FO(D,E) 在表达上等价于 FO(D)？这样的 E 被称为对 D 安全的。

目前尚无这些问题的完整答案。然而，目前已知的部分结果是：

如果 D 是向上封闭依赖关系的集合（也就是说，如果依赖关系在某个模型 M 中对某个团队 X 成立，那么对同一模型中的任何超团队 Y⊇X 也成立），再加上可能的恒定原子（即依赖原子中前面提到的特殊情况，即某个变量在团队中是常数），则 D 是强一阶依赖关系 (Galliani 2015)；

并非所有强一阶依赖关系对所有依赖关系都是安全的：特别是，恒定原子对于一元包含依赖关系 x⊆y 不安全，其中 x 和 y 是单变量；可能性算子 ⋄ϕ 对所有依赖关系集合都是安全的，当且仅当模型 M 中的 X 存在一个非空子集满足 ϕ 时，该算子才被模型 M 中的依赖关系集合 X 所满足。此外，所有依赖关系集合都是安全的，完全性原子（表示某个变量或变量元组取所有可能的值）和非恒定性原子（表示某个变量在一个依赖关系集合中至少取两个不同的值）也是如此（Galliani 即将出版）；

如果 D 是强一阶依赖关系集合，而 E 是向下封闭依赖关系集合（即，依赖关系，只要对某个团队成立，对每个子团队也成立），则 D 对 E 而言是安全的 (Galliani 2019)；

如果 D 是向下封闭且可相对化的依赖关系集合（也就是说，将 D 中依赖关系的相对化添加到一元谓词 P 中，其表达能力并不比添加依赖关系本身更强），则 D 是强一阶的，当且仅当其中的每个依赖关系都可以用恒定原子来定义 (Galliani 2019)。

然而，这些都是部分结果，团队语义学中依赖关系和连接词的一般理论仍处于起步阶段。

一个相关主题是通过广义量词扩展依赖逻辑的研究 (Engström 2012)。沿着这一思路，一个有趣的结果是，通过量词 Q“存在无数个……”对依存逻辑进行扩展，实现了公理化，这对于理论的 FO(Q) 后果而言是健全且完备的 (Engström, Kontinen & Väänänen 2017)。

同样值得一提的是 (Kontinen & Yang 2019) 的工作，他们发现了一种基于团队语义的逻辑（与依存逻辑的“标准”连接词选择不同），其公式精确地捕捉了团队的一阶可定义属性。

4.6 命题依存逻辑

到目前为止，我们考虑的依存原子和独立原子表达了一组赋值中变量可能值之间的关系。然而，依赖性和独立性的概念同样可以自然地应用于命题本身，就像在自然语言表达中发生的那样，例如“他是否通过这门课程只取决于他的期末考试的内容”。命题依赖逻辑在命题逻辑的语境中考虑此类原子。命题依赖逻辑团队是从命题原子 p1…pn 到 {T,F} 的赋值 v 的集合。其语义规则及其论证与一阶团队语义的规则非常相似，依赖原子的规则为：

PTS-dep：

X⊨=(p1…pn,q) 当且仅当任意两个赋值 v1,v2∈X，它们在 p1…pn 的值上一致，在 q 的值上也一致。

一阶依赖逻辑的许多变体和推广都可以毫不费力地降低到命题级别：例如，可以研究命题包含逻辑、命题团队逻辑、命题直觉依赖逻辑等的性质。

尽管（一阶）依赖逻辑严格来说比一阶逻辑更具表达力，但命题依赖逻辑并不比命题逻辑更具表达力，因为这直接源于所有命题函数都可以在命题逻辑中表达。然而，命题依赖逻辑的各组与探究逻辑（Groenendijk 2009；Ciardelli & Roelofsen 2011）的信息状态之间存在着密切的联系，探究逻辑是研究意义和信息交换概念的语义框架：具体而言，探究逻辑的含义与命题直觉依赖逻辑的含义完全相同。

命题依赖逻辑及其许多扩展的公理化可以在（Yang & Väänänen 2016）中找到；该形式主义（以及基于团队语义的相关命题逻辑）的计算复杂性分析可参见 (Virtema 2017; Hannula et al. 2018)。

4.7 模态依赖逻辑

模态依赖逻辑 (Väänänen 2008) 及其变体通过添加命题依赖逻辑中已经考虑过的依赖原子 =(p1…pn,q) 来扩展模态逻辑。

其满足条件可以通过团队语义的一种变体来定义，其中团队被可能世界集合所取代。

大量研究已经探讨了该逻辑、其片段及其扩展的复杂性理论特性 (Ebbing, Lohmann, & Yang 2011; Ebbing & Lohmann 2012; Lohmann & Vollmer 2013)。

模态独立逻辑也已在 (Kontinen et al, 2017) 中得到研究。

4.8 具有团队语义的线性时序逻辑

线性时序逻辑也可以被赋予某种“团队语义”，其中公式的求值是基于迹集（即状态序列集）的，这些迹集表示系统可能的计算。这样的逻辑框架可用于超属性的规范和验证（Krebs 等人，2017，其他互联网资源；Lück，2020），即诸如“系统在有限时间内终止”之类的属性，其真实性无法通过单独检查系统的每个可能迹来确定，而只能通过查看所有可能迹的集合来确定。

4.9 团队语义和依赖逻辑的量化变体

由于团队对应于多组任务分配，因此很自然地会考虑扩展团队语义的可能性，其中满意度的定义不再局限于多团队（即多组任务分配）或任务分配的概率分布。

第一种可能性已在 Durand et al. 2018a 中进行了研究，而第二种可能性已在 Durand et al. 2018b 中进行了研究。特别是第二种研究，导致了与实数描述复杂性问题和元有限模型理论的有趣联系 (Hannula 等人 2019, Hannula 等人 2020)。

5. 依赖逻辑的应用

5.1 依赖逻辑与数据库理论

团队语义的团队与关系数据库理论中研究的关系之间存在直接的联系：给定一个团队 X 及其赋值中出现的变量元组

→

v

=v1…vk，可以定义关系 X(

→

v

)={⟨s(v1),…,s(vn)⟩:s∈X}。此外，依赖逻辑及其变体中研究的依赖原子与数据库理论中考虑的依赖关系类似，并且在许多情况下源自这些依赖关系，例如函数依赖关系（Väänänen 2007a）、多值依赖关系（Engström 2012）以及包含和排除依赖关系（Galliani 2012）。依赖逻辑与数据库理论之间的关系不仅促进了依赖逻辑的进一步发展，也​​促进了数据库理论的发展：例如，Hannula & Kontinen 2016 通过在团队语义学背景下研究类似问题，发现了包含、函数和嵌入多值数据库理论依赖关系的非限制蕴涵问题的有限公理化。

5.2 依赖逻辑与信念表示

如 (Yang 2014) 和 (Yang & Väänänen 2016) 所述，(命题)直觉依赖逻辑与探究逻辑 (Ciardelli & Roelofsen, 2011) 之间存在着密切的联系，探究逻辑是一个用于研究代理之间意义和信息交换的框架。更一般地说，团队语义学中研究的依赖原子和连接词，在信念状态和信念更新方面可以进行自然解释。如 (Galliani 2015) 所述。目前，此类逻辑与动态认知逻辑及其变体 (Van Ditmarsch, van Der Hoek, & Kooi 2007) 之间关系的确切性质在很大程度上尚未得到探索，但有充分的理由怀疑这两个数学和哲学逻辑领域之间存在进一步的联系。

5.3 依赖逻辑与阿罗定理

阿罗定理 (Arrow 1950) 是社会选择理论的一个影响深远的成果，简而言之，它表明不存在任何投票系统（即，不存在任何将个体对不同选项的偏好排序转化为全局的、社会层面的偏好排序的系统）能够满足三个看似合理的条件，即：

如果每个投票者都更喜欢 A 而不是 B，那么整个群体也更喜欢 A 和 B；

群体整体上是偏好 A 而非 B，还是偏好 B 而非 A，完全取决于每个投票者对 A 和 B 的偏好，而非他们对其他可能替代方案的偏好；

没有任何单个投票者是独裁者，也就是说，群体的偏好并非由任何单个投票者的偏好决定。

正如措辞本身所示，第二和第三个条件可以用依赖性和独立性来自然解读：事实上，正如 Pacuit & Yang 2016 所表明的那样，阿罗定理可以用独立性逻辑形式化，并在合适的自然演绎系统中得到证明。

5.4 量子团队逻辑与贝尔不等式

在 (Hyttinen, Paolini, & Väänänen 2015) 中，引入了一种命题团队逻辑的变体，称为量子团队逻辑。在这种形式体系中，团队被量子团队取代。它与普通的命题群逻辑群不同，因为它们允许某些变量的值相对于某些赋值不确定，并且允许同一赋值存在多个实例（从而为群语义添加了量化方面）。然后，在量子群上定义一种语义，用于描述与事件概率相关的不等式，并为其开发一个健全完备的证明系统；最后，证明了贝尔不等式在该系统中存在反例，正如量子力学的预言和实验证据（Einstein, Podolsky, & Rosen 1935; Bell 1964; Aspect, Grangier, & Roger 1981）所证实的那样，而在该框架的经典版本中则不然。