依赖逻辑（一）_数学联邦政治世界观

依赖逻辑是一阶逻辑的扩展，它添加了依赖原子，即形式为 =(x1…xn,y) 的表达式，它断言 y 的值在函数上依赖于 x1…xn 的值（换句话说，由 x1…xn 的值决定）。这些原子允许指定变量之间的非线性有序依赖模式，这与 IF 逻辑中的斜线量词非常相似；但与 IF 逻辑不同的是，依赖逻辑将量化与此类依赖/独立条件的指定分开。

依赖逻辑的主要语义称为团队语义，它通过让表达式根据变量赋值集而不是单个赋值满足或不满足来推广塔斯基语义。这种语义早于依赖逻辑本身的发展，最初由 Wilfrid Hodges 在 IF 逻辑的背景下开发 (Hodges 1997)。依赖逻辑也存在一种基于不完全信息博弈的博弈论语义，大致类似于独立友好逻辑的博弈论语义 (Väänänen 2007a)。严格地说，“依赖逻辑”一词专指将上述函数依赖原子添加到一阶逻辑语言中获得的语言；但该术语也用于更广义的意义上，指研究通过在一阶逻辑中添加各种依赖性和独立性概念而获得的逻辑属性的研究领域，例如独立性逻辑（Grädel & Väänänen 2013），直觉主义依赖逻辑（Yang 2013）或包含逻辑（Galliani 2012，Galliani & Hella 2013），甚至通过类似原子扩展其他逻辑框架的逻辑，例如模态依赖逻辑（Väänänen 2008）。

本文中，“依赖逻辑”一词将用于指代真正的依赖逻辑，而“依赖和独立逻辑”一词将用于指代其变体和推广。

1. 一阶逻辑及其扩展中的依赖模式

2. 团队语义

2.1 博弈论语义

3. 性质

3.1 表达力

3.2 依赖逻辑中的层次结构

3.3 依赖逻辑中的否定

3.4 依赖逻辑中的真值、有效性和证明系统

4. 依赖逻辑的变体

4.1 独立逻辑

4.2 包含逻辑

4.3 团队逻辑

4.4 直觉依赖逻辑

4.5 团队语义中的广义依赖和联结词

4.6 命题依赖逻辑

4.7 模态依赖逻辑

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

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

5. 依赖逻辑的应用

5.1 依赖逻辑与数据库理论

5.2 依赖逻辑与信念表示

5.3 依赖逻辑与阿罗定理

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

参考文献

学术工具

其他网络资源

1. 一阶逻辑及其扩展中的依赖模式

一阶逻辑的一个特性在很大程度上解释了其表达能力和适用性，即它允许量词嵌套，因此，它允许在量化变量之间指定依赖模式。例如，考虑以下语句（希望是错误的）： “每个男孩都会爱上一个爱着另一个男孩的女孩”。它可以直接转化为一阶逻辑：

∀x(BOY(x)→∃y(GIRL(y)∧LOVES(x,y)∧

∃z(BOY(z)∧x≠z∧LOVES(y,z))))

根据塔斯基的惯常语义，其真值条件恰如其分：上述表达式为真，当且仅当对于每个男孩 b，都有可能找到一个女孩 g 和一个男孩 b′，使得 b 爱 g，g 爱 b′，且 b 和 b′ 不相同。女孩 g 的身份当然可能取决于第一个男孩 b 的身份——毕竟，要使这个表达式为真，我们并不要求所有男孩都爱上所有女孩——此外，第二个男孩 b′ 的身份可能既取决于第一个男孩 b 的身份（因为 b′ 必须不同于 b），也取决于 b 爱的女孩 g 的身份。因此，我们量化变量之间的依赖模式如下：y 依赖于 x，而 z 同时依赖于 x 和 y。从句法角度来看，这体现在 ∃y 位于 ∀x 的范围内，而 ∃z 同时位于 ∀x 和 ∃y 的范围内。

算子之间依赖模式的差异可以用来形式化重要的区别，例如函数 f 的连续性之间的区别

∀x∀ϵ∃δ∀x′(|x−x′|<δ→|f(x)−f(x′)|<ϵ)

与其一致连续性之间的区别

∀ϵ∃δ∀x∀x′(|x−x′|<δ→|f(x)−f(x′)|<ϵ)

或者，在一阶逻辑的内涵扩展中，用来表达 De Dicto 和 De Re 解读之间的区别（例如，“每个人都有可能疯掉”可以理解为：对于每个人 p，p 都可能疯掉，∀x(PERSON(x)→⬦CRAZY(x))，或者理解为：每个人都有可能一起疯掉， ⬦∀x(PERSON(x)→CRAZY(x)))。

一阶逻辑中，量化变量之间的依赖模式必然是传递的。从它们与相应子表达式作用域的联系可以看出：如果∃y 在∀x 的范围内，且∃z 在∃y 的范围内，则∃z 必然在∀x 的范围内（因此依赖于∀x）。此外，某个子公式α 所处范围内的所有量词的集合是线性有序的：如果α 在Q1x1 和Q2x2 的范围内，则要么Q1x1 在Q2x2 的范围内，要么反之亦然。

这限制了一阶逻辑的表达可能性。例如，假设我们希望修改之前关于男孩和女孩的断言如下：每个男孩都爱着某个女孩，而这个女孩又爱着另一个男孩，并且这个第二个男孩的选择独立于第一个男孩。直观地说，这意味着足够简单：对于每个男孩 b，我们都能找到一个女孩 g，使得 b 爱 g；对于每个这样的女孩，我们都能找到一个男孩 b′，使得 g 爱 b′ 且 b≠b′；此外，我们只需根据女孩 g 的身份，无需知道 b 的身份就能确定第二个男孩 b′ 的身份。在某些情况下，这仍然成立，例如，两个男孩 b1 和 b2 分别爱着两个女孩 g1 和 g2，而她们分别只爱 b2 和 b1。然而，很容易看出，它并不等同于我们之前的陈述：例如，如果我们的宇宙（如上文 (b) 所示）由两个男孩 b、b′ 和一个女孩 g 组成，并且 b 和 b′ 都爱着 g，而 g 也爱着他们两个，那么我们之前的断言是正确的，而当前的断言是错误的。

[两个相似的图形，两个图形的顶部都有“男孩”和“女孩”两个词，中间用水平空格隔开。图 (a) 中，左上角为 b1，右上角为 g1，左下角为 b2，右下角为 g2。箭头从 g1 指向 b1，从 b1 指向 g2，从 g2 指向 b2，以及 b2 到 g1。图 (b) 中 b1 位于左上角，b2 位于左下角，g1 位于中间右侧。一个箭头指向 b1 和 g1，同样，也指向 b2 和 g1。]

(1) 为真的两种情况。在 (a) 中，z 可以独立于 x 选择；在 (b) 中，则不能。

然而，目前尚不清楚如何在一阶逻辑中形式化这一条件。本质上，我们需要修改 (1)，使 z 不在 x 的范围内，因此它不依赖于 x；然而，我们仍然希望 z 依赖于 y，y 依赖于 x。然而，正如刚才所讨论的，这种依赖模式在一阶逻辑中是无法实现的。我们可以通过诉诸高阶量化来回避这个问题：事实上，我们可以看到表达式

∃F∀x(BOY(x)→∃y(GIRL(y)∧LOVES(x,y)∧BOY(F(y))∧

x≠F(y)∧LOVES(y,F(y))))

捕捉到了我们想要的解释，但这是以对函数进行显式存在量化为代价的。

一个可能的替代方案是扩展一阶逻辑的语法，以解除量化变量之间依赖模式的限制。这是分支量词逻辑 (Henkin 1961) 所采用的路径，其中 (2) 的真值条件对应于

(

∀x ∃y

∀z ∃w

)(BOY(x)→(GIRL(y)∧LOVES(x,y)∧

(y=z→(BOY(w)∧x≠w∧LOVES(z,w)))))) 的真值条件，

也对应于独立性友好逻辑，其中 (2) 等价于

∀x∃y(BOY(x)→(GIRL(y)∧LOVES(x,y)∧(∃z/x)(BOY(z)∧

x≠z∧LOVES(y,z))))。

我们在此不对这两个形式主义的语义进行详细解释；可以说，在 (3) 中，w 的值不依赖于 x 和 y 的值（尽管它可能依赖于 z 的值），因为它们属于复数量词 ( ∀x ∃y

∀z ∃w

) 的不同“行”，而在 (4) 中，z 的值不依赖于 x 的值。因为这种依赖关系被量词 (∃z/x) 明确地“削去”。

我们可以看出，分支量词逻辑和独立性友好逻辑的一个共同特点是，它们没有将变量的量化与非标准依赖模式的指定分开：就像一阶逻辑的情况一样，量化变量 v1 是否依赖于另一个量化变量 v2 将由它们各自的量词的位置和形式决定。

依赖逻辑采用了不同的方法来扩展一阶逻辑以表示 (2)。与 (1) 相比，唯一新颖的条件是 z 的值由 y 的值决定（即函数依赖于）；这对应于一个新的原子条件 =(y,z)，称为依赖原子，其预期含义是 z 的值是 y 值的函数。与分支量词逻辑或独立性友好逻辑的情况不同，这是一个关于 y 和 z 可取值的条件，而不是关于量词 ∃z 行为的条件：事实上，通常根本没有理由要求 z 是一个量化变量——它很可能是一个自由变量，或者是一个包含多个变量的复数项。

在依赖逻辑中，(2) 可以形式化为

∀x∃y∃z(=(y,z)∧(BOY(x)→(GIRL(y)∧LOVES(x,y)→

(BOY(z)∧x≠z∧LOVES(y,z)))))

(2)、(3)、(4) 和 (5) 的真值条件完全相同：任何满足这些表达式之一（在相应的语言中）的模型都满足所有四个表达式。更一般地说，正如我们将看到的，存在二阶逻辑的表达能力，独立友好逻辑和依赖逻辑在模型类的可定义性方面完全相同。然而，对于包含自由变量的公式而言，情况并非如此；此外，这些逻辑可以沿着截然不同的思路进行扩展和修改。

2. 团队语义

团队语义最初由 Wilfrid Hodges 在独立友好逻辑（Hodges 1997）的背景下提出，它是塔斯基一阶逻辑语义的推广，适用于元素对变量进行多重赋值的情况。此类赋值的集合（由于历史原因被称为团队）构成了团队语义的基本语义概念，公式的满足或不满足取决于这些赋值，而不是取决于单个赋值。团队语义与塔斯基语义之间的联系由以下结果展示，该结果在依赖逻辑及其所有一阶变体中均成立：

保守性：

团队 X 满足一个一阶公式（在团队语义学意义上），当且仅当所有赋值 s∈X 都满足该公式（在塔斯基语义学意义上）。

更一般地，团队可以理解为信念集，表示某个代理认为可能存在的所有世界状态（=赋值）的集合。然后，团队 X 满足某个公式 ϕ，当且仅当当 X 是所有可能状态的集合时 ϕ 成立；在这种情况下，我们将其记为 X⊨ϕ（或者，如果模型 M 的选择不明确，则记为 M,X⊨ϕ）。在本节中，我们将根据该原则研究团队语义的规则及其解释；然后在下一节中，我们将讨论该原则如何从依赖逻辑的不完美信息博弈论语义中衍生出来。

新依赖原子的条件 =(x1…xn,y)，这对应于“y 的值是关于 x1…xn 的值的函数”这一陈述，很容易理解：

TS-dep：

X⊨ =(x1…xn,y) 当且仅当任意两个在 x1…xn 的值上一致的分配关系 s1,s2∈X，在 y 的值上也一致。

例如，假设 X 是关于三个变量 x1、x2 和 y 的分配关系集合，其中 x1 表示某个职位候选人的国籍，x2 表示他们的分数（根据合适的评估方法），y 表示他们是否被录用或拒绝。那么，原子 =(x2,y) 对应于“录用通知仅由分数决定”这一陈述：如果两个候选人的分数相同，他们将获得完全相同的录用通知，而不受其他因素的影响。依赖原子的一个特例是常量原子 =(y)，根据上述语义，当且仅当一个团队的所有赋值都对 y 的值一致时，该常量原子才满足依赖原子的条件。

赋值 x1 x2 y

s0 0 0 0

s1 0 1 1

s2 1 0 1

s3 1 1 2

表 1：一个团队 X，其中 y=x1+x2。这里 y 是 x1 和 x2 的函数，因此 =(x1x2,y) 成立；然而，y 不是 x1 单独的函数，因此 =(x1,y) 不成立。

在同样的解释下，一阶文字和合取的规则很容易推导（为简单起见，我们假设表达式符合否定范式；并且，按照惯例，我们假设依赖原子的否定永远不会被满足）：

TS-lit：

对于所有一阶文字 α，X⊨α 当且仅当对于所有赋值 s∈X，s⊨α 满足通常的塔斯基语义学意义；

TS-∧：

X⊨ϕ∧ψ 当且仅当 X⊨ϕ 和 X⊨ψ 满足。

值得指出的是，正如我们已经从这些规则中看到的，排中律在依存逻辑中不成立（就像在独立性友好逻辑中不成立一样）：例如，如果一个团队 X 同时包含赋值 s（s(x)=s(y)）和赋值 s′（s′(x)≠s′(y)），则 X⊭x=y 且 X⊭x≠y。本节中，我们将介绍不带显式否定运算符的依存逻辑语言；之后，我们将讨论将其添加到依存逻辑语言中会产生什么后果。

全称量化又如何呢？在什么情况下，全称量化表达式 ∀vψ 应该在团队中成立？同样，我们必须回顾一下团队代表一组可能状态的直觉。如果我们想要评估 ∀vψ，我们应该根据哪些可能的状态来评估 ψ？自然的答案是，我们应该考虑所有与 X 中的状态仅在 v 的值方面不同的状态。这证明了以下规则：

TS-∀：

X⊨∀vψ 当且仅当 X[M/v]⊨ϕ，其中 X[M/v] 是集合 {s′:∃s∈X s.t. s′∼vx}

其中 s′∼vs 表示两个赋值 s 和 s′ 之间的最大差异在于变量 v 的值。

赋值 x

s0 0

s1 1

⇒X[M/y]=

赋值 x y

′

0 0

′

0 1

′

1 0

′

1 1

表 2：包含两个元素 0 和 1 的模型中的 X 和 X[M/y]。

现在我们来考虑析取。ϕ∨ψ 何时成立？为了回答这个问题，我们再次回顾一下：团队可以理解为事物可能状态的集合，因此，两个团队 Y 和 Z 的并集表示当 Y 或 Z 成立时可能发生的所有状态。因此，如果团队集合 {Y1…Yn,…} 和 {Z1…Zn,…} 分别满足这两个公式 ϕ 和 ψ，则团队集合 {Yi∪Zj:i,j∈1,…} 应该满足它们的析取公式 ϕ∨ψ，或者，等价地，

TS-∨：

X⊨ϕ∨ψ 当且仅当 X=Y∪Z，其中 Y 和 Z 有两个分支，且 Y⊨ϕ 和 Z⊨ψ。

这里值得指出的是，我们通常不要求 Y 和 Z 不相交。由于向下闭包性质（我们稍后会讨论），这个附加条件对依赖逻辑本身的语义没有影响；但在某些扩展和依赖逻辑的变体中，这个附加要求会与局部性原理相冲突，根据该原理，表达式的满足条件仅取决于其中自由出现的变量的值（Galliani 2012）。

同样需要注意的是，在依存逻辑中，析取不是幂等的：例如，=(x,y)∨=(x,y) 不等价于 =(x,y)，并且团队 X 满足析取条件当且仅当 X 中每三个在 x 上一致的赋值中至少有两个在 y 上一致。这看起来可能有些违反直觉；但这直接源于以下事实：在我们的解释下，=(x,y)∨=(x,y) 应理解为“所有可能的事物状态都来自两组事物状态中的一组，并且在这两组中 y 都是 x 的函数”。由于函数的并集通常不是函数，因此依存逻辑中的析取不是幂等的也就不足为奇了。

最后，我们考虑存在量化的情况。表达式 ∃vψ 何时会被团队满足？为了回答这个问题，我们可以先考虑一下限制算子的解释：给定任意一个团队 X，都会得到一个团队 X∖v，即从所有赋值 s∈X 中移除变量 v（如果存在）（然后，由于 X 是一个集合，因此会折叠相同的赋值）。这可以理解为一个遗忘操作，通过这种方式，我们可以删除所有关于 v 值的信息——例如，因为我们对这个值的认知不可靠，或者因为这个值已被改变。现在假设 X∖v=Y∖v：那么，按照我们的解释，这意味着 X 和 Y 所表示的事物可能状态集最多在 v 值方面存在差异。因此，如果 Y 满足条件 ϕ，我们可以说，如果不是因为 y 的值，X 也会满足 ϕ，或者，等价地，X 满足 ∃vψ。这证明了以下规则：

TS-∃：

X⊨∃vψ 当且仅当存在某个 Y，其包含 X 和 v 的变量，使得 X∖v=Y∖v 且 Y⊨ψ。

很容易验证，当且仅当 Y 的形式为 X[F/y]={s[a/y]:s∈X,a∈F(s)}，其中某个函数 F 源于 X 中对我们模型中元素非空集的赋值。

这里值得指出的是，上述定义通常并不要求 X 和 Y 包含相同数量的赋值：X 中的一个赋值很可能对应于 Y 中的多个赋值；并且——如果 v 已经是 X 赋值中的一个变量——Y 中的一个赋值也可能对应于 X 中的多个赋值。

赋值 x

s0 0

s1 1

⇒X[F/y]=

赋值 x y

′

0 0

′