依赖逻辑（二）

最后，我们需要定义依存逻辑句子相对于模型的真值。由于句子没有自由变量，根据局部性原则，我们立即得到：要么所有非空组都满足它，要么没有非空组满足它。这类似于塔斯基语义学的情况，其中一个句子要么由所有变量赋值满足，要么由任何赋值都不满足。因此，我们可以用通常的方式定义真值：

团队语义中的真值：

句子 ϕ 在模型 M 中为真，当且仅当 M,{∅}⊨ϕ，其中 {∅} 表示仅包含空赋值的团队。在这种情况下，我们记作 M⊨ϕ。

2.1 博弈论语义

如上所述，依赖逻辑的博弈论语义是独立友好逻辑的不完美信息语义的一种变体，而独立友好逻辑本身是对一阶逻辑博弈论语义的改编。我们请读者参阅 (Väänänen 2007a) 以获得该语义的正式、详细定义。

在博弈论语义学中，句子 ϕ 和模型 M 被设计成对应于一个（通常是双人）博弈 GM(ϕ)。然后，真理被定义为其中一名玩家（在本文中，简称为“玩家 0”）的获胜策略的存在：换句话说，如果 σ0 是玩家 0 的策略（可能为非确定性策略），且 Π(GM(ϕ),σ0) 是所有与 σ0 兼容的策略集合，则 ϕ 为真当且仅当 Π(GM(ϕ),σ0) 中的每个策略对玩家 0 来说都是赢家。我们可以将博弈 GM(ϕ) 视为两个玩家之间的辩论，其中一人（玩家 0）希望证明 ϕ 成立，而另一人（玩家 1）希望证明 ϕ 不成立。

与一阶逻辑和独立友好逻辑的情况一样，在依赖逻辑的不完美信息博弈中，博弈的立场是 (θ,s) 对，其中 θ 是 ϕ 子公式的一个实例（即，同一表达式作为 ϕ 子公式的多次出现应单独考虑），s 是模型 M 上的变量赋值。[1]初始位置为 (ϕ,∅)，其中 ∅ 为空赋值；对于玩家 0 来说，非确定性策略 σ0 会根据以下规则，针对每个析取和存在量化操作，选择当前位置的一个或多个后继：

如果当前位置的形式为 (ψ∨θ,s)，则其后继为 (ψ,s) 和 (θ,s)；

如果当前位置的形式为 (∃vψ,s)，则其后继为所有 s′∼vs 的 (ψ,s′) 位置。

类似地，(ψ∧θ,s) 的后继为 (ψ,s) 和 (θ,s)，而 (∀vψ,s) 的后继为所有 s′∼vs 的 (ψ,s′) 形式的位置；但玩家 0 的策略无法为这些位置指定后继，因为系统假设玩家 1 会选择它们之后的位置。

位置序列

¯

ρ

=ρ0ρ1…ρn 是 GM(ϕ) 的演绎，当且仅当

ρ0=(ϕ,∅)；

对于所有 i=1…n，ρi 是 ρi−1 的后继。

此外，如果每当 ρi 对应于析取或存在量词时，ρi+1∈σ0(ρi)，我们称

¯

ρ

服从策略 σ0；如上所述，我们将 GM(ϕ) 上所有服从 σ0 的策略集合记为 Π(GM(ϕ),σ0)。

如果所有以 (α,s) 结束的策略

¯

ρ

使得赋值 s 满足塔斯基语义学中通常意义的 α，则称策略 σ0 获胜。依赖原子——以及以依赖原子结束的策略——对于判断给定策略是否获胜无关。然而，它们用于指定给定策略是否一致：

一致条件

如果任意两个策略

¯

ρ

,

¯

γ

∈Π(GM(ϕ),σ0) 的策略为一致，且对于依赖原子 =(x1…xn,y) 的同一个实例，它们的最终结果为两个位置 (=(x1…xn,y),s)，(=(x1…xn,y),s′)，则

如果 s(x1)…s(xn)=s′(x1)…s′(xn)，则 s(y)=s′(y)。

那么，我们可以将博弈论语义中的真值定义如下：

博弈论语义中的真值：

句子 ϕ 在模型 M 中为真（就博弈论语义而言），当且仅当玩家 0 在 GM(ϕ) 中具有一致制胜策略。

可以证明，这个概念等同于团队语义学中的真值概念。事实上，我们还可以证明更多。如果对于任何团队 X 和公式 ϕ，博弈 GM,X(ϕ) 按照 GM(ϕ) 进行，但每次博弈的初始位置都从 {(ϕ,s):s∈X} 中随机选择，则以下成立：

GTS 与团队语义的等价性：

当且仅当玩家 0 在 GM,X(ϕ) 中具有一致的制胜策略时，团队 X（关于模型 M）才满足公式 ϕ。

顺便说一句，这个结果清楚地解释了为什么依赖逻辑的团队语义满足空集性质和向下闭包性质。事实上，如果 X=∅，那么 GM 中玩家 0 的每个策略，X(ϕ) 是均匀获胜的；如果 X⊆Y，则 GM,X(ϕ) 中玩家 0 的任何均匀获胜策略，也是 GM,Y(ϕ) 中玩家 0 的均匀获胜策略。

3. 性质

3.1 表达能力

依存逻辑在句子层面上等价于二阶逻辑的存在性片段 Σ

1

1

。更准确地说，可以证明 (Väänänen 2007a)：

依存逻辑与 Σ

1

1

的句子层面等价性：

对于每个依存逻辑句子 ϕ，都存在一个 Σ

1

1

句子 ϕ∗，使得

对于所有模型 M，M⊨ϕ⇔M⊨ϕ∗。

类似地，对于每个 Σ

1

1

句子 ϕ∗，都存在一个依存逻辑句子 ϕ，使得 (6) 成立。

Fagin 定理 (Fagin 1974) 表明，有限模型的某个性质可在 Σ

1

1

中定义，当且仅当它可被非确定性图灵机在多项式时间内识别（即，当且仅当它属于 NPTIME 范畴），由此可知：

依存逻辑与 NPTIME：

对于任何依存逻辑语句 ϕ，所有满足它的有限模型的类均属于 NPTIME 范畴。此外，对于任何 NPTIME 范畴的有限模型 K，存在一个依存逻辑语句 ϕ，使得 M⊨ϕ 当且仅当 M∈K。

依存逻辑与 Σ

1

1

在句子层面上的等价性的另一个直接推论是，紧致性定理和勒文海姆-斯科伦定理也对依存逻辑成立 (Väänänen 2007a)：

紧致性：

如果有限依存逻辑句子的集合 Φ 在任何模型中都不可满足，则它的某个有限子集 Φ0⊆fΦ 已经不可满足。

勒文海姆-斯科伦定理：

如果一个依存逻辑句子具有无限模型，则它具有所有无限基数的模型。

然而，当涉及到包含自由变量的公式时，问题就变得更加微妙了。然后，可以证明（Kontinen & Väänänen 2009），依赖逻辑对应于存在性二阶逻辑的向下闭合部分：

依赖逻辑中的团队可定义性

模型 M 上的团队集合 X 和变量集合 V 的形式为 {X:M,X⊨ϕ}，其中依赖逻辑公式 ϕ 在 V 中具有自由变量，当且仅当

X 非空；

X 向下闭合，即 Y⊆X∈X⇒Y∈X；

X 在 M 中可 Σ

1

1

定义，即存在一个 Σ

1

1

句子 Ψ(R)，其范围涵盖 M 的词汇表以及新的 |V| 元关系符号 R，且

X∈X 当且仅当 M,Rel(X)⊨Ψ(R)

其中 Rel(X) 是与团队 X 对应的 |V| 元关系 {s(V):s∈X}。

3.2 依赖逻辑中的层次结构

在 (Durand & Kontinen 2012) 中，研究了限制依赖原子的因变量数量或全称量词数量的影响。已证明，这两种定义依赖逻辑片段的方式都会产生层次结构：

对于所有 k，令 D(k−∀) 为限制为最多 k 个全称量词的依赖逻辑，令 D(k−dep) 为限制为依赖原子的依赖逻辑，其形式为 =(

→

x

,y)，其中 |

→

x

|≤k。则

D(k−∀) ＜ D(k+1−dep)，

D(k−∀) ≤ D(k−dep)≤ D(k+1−dep)

且

D(k−∀) ＜ D(2k+2−∀)

关于句子的表达能力。

3.3 依赖逻辑中的否定

到目前为止，我们假设所有依赖逻辑表达式都符合否定范式，并且依赖原子永远不会被否定。另一方面，在依赖逻辑语言中添加显式的否定运算符则有些问题，因为存在性二阶逻辑在否定下不封闭。事实上，“显而易见的”否定规则

X⊨∼ϕ 当且仅当 X⊭ϕ

极大地提升了依赖逻辑的表达能力，并将其扩展至团队逻辑 (Väänänen 2007a,b)，这在非常强的意义上等同于完整的二阶逻辑 (Kontinen & Nurmi 2009)。

一个强度较低的“双重”否定 ¬ 可以根据德·摩根规则定义：¬(ϕ∨[∧]ψ)≡(¬ϕ)∧[∨](¬ψ) 和 ¬(∃v[∀v]ϕ)≡∀v[∃v](¬ϕ)，再加上双重否定律 ¬¬ϕ≡ψ 以及依赖原子否定的规则

X⊨¬=(

→

x

,y) 当且仅当 X=∅

(Väänänen 2007a,b)。由此产生的语言在表达上等价于无否定的依赖逻辑，事实上，(Väänänen 2007a) 的依赖逻辑描述将此否定视为其语言的一部分；然而，如 (Kontinen & Väänänen 2011) 所示，依存逻辑公式的满足条件与其否定的满足条件之间几乎没有联系。更准确地说：

对偶否定与依存逻辑：

对于任何两个依存逻辑公式 ϕ 和 ψ，且 ϕ∧ψ 不可满足，存在一个依存逻辑公式 θ，使得

M,X⊨θ 当且仅当 M,X⊨ϕ

且

M,X⊨¬θ 当且仅当 M,X⊨ψ

对所有模型 M 和团队 X 成立。

因此，关于 ϕ 的对偶否定，除了它等同于某个依存逻辑表达式，而任何满足 ϕ 的团队都不满足该表达式之外，我们一般无法给出任何结论。由于如前所述，排中律在依存逻辑中失效，因此这不是一个非常有用的性质；具体来说，在依赖逻辑（具有对偶否定）中，可以找到具有非等价否定的等价表达式，例如 x≠x∧y≠y 和 ¬=(x,y)。

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

与独立友好逻辑类似，依存逻辑可以定义自己的真值算子 (Väänänen 2007a)，也就是说，如果对于所有公式 ϕ，⌈ϕ⌉ 是 ϕ 的哥德尔数，那么我们就可以找到一个公式 τ(x)，其中 x 是其唯一自由变量，并且

M⊨ϕ 当且仅当 M⊨τ(⌈ϕ⌉)

对于所有满足皮亚诺自然数公理的模型 M。这与塔斯基的不可定义性定理并不矛盾，因为依存逻辑在矛盾否定下并不封闭。

判断一个依存逻辑句子是否有效（即在所有模型中为真）是非算术问题，并且实际上对于莱维层次的 Π2 类是完备的。尽管如此，依存逻辑的证明理论已经得到了研究。特别是在 (Kontinen & Väänänen 2013) 中，针对寻找依存逻辑理论的一阶后果问题，已经开发出一套完善的证明系统。

4. 依存逻辑的变体

在本节中，我们将简要总结研究最多的依存逻辑变体的性质。此类变体有很多，并且已经对它们的分类和比较进行了大量研究。在本文中，我们将仅提及那些由于与依存逻辑本身的关系而具有特殊意义的变体。

4.1 独立性逻辑

独立性逻辑 (Grädel & Väänänen 2013) 不是用依赖原子 =(

→

x

,y) 来扩展一阶逻辑，而是用独立原子

→

x

⊥

→

z

→

y

来扩展一阶逻辑。其预期解释是“对于

→

z

的任何可能选择，

→

x

和

→

y

的可能值都是独立的”——换句话说，给定

→

z

的任何固定选择，知道

→

x

所取的值并不能传达任何关于

→

y

所取值的信息。这是一个具有重要概念意义的概念：例如，我们可能想要表达：如果不知道加密密钥，那么查看消息的加密版本并不包含任何关于相应明文版本的信息。如果 x 表示加密消息，y 表示明文消息，则这对应于条件 x⊥y，其中

→

z

在这种情况下为空。类似地，如果 k 表示密钥，则 x⊥k 表示无法从加密消息推断出密钥的断言；而合取依赖原子 =(k,x,y)（我们很快就会看到，它可以用独立逻辑表示）表示可以根据加密消息和密钥解码明文消息的断言。

形式上，独立原子的满足规则可以表示如下：

TS-indep:

M⊨X

→

x

⊥

→

z

→

y

当且仅当对于所有s,s′∈X，且s(

→

z

)=s′(

→

z

)，存在一个s″∈X，且s″(

→

z

→

x

)=s(

→

x

→

z

)且s″(

→

y

)=s′(

→

y

)。

赋值 x1 x2 x3

s0 0 0 0

s1 0 1 1

s2 1 0 1

s3 1 1 0

独立逻辑严格来说比依赖逻辑更具表达力：事实上，它缺乏向下闭合性，并且依赖原子 =(

→

x

,y) 等价于独立原子 y⊥

→

x

y。此外，还可以证明（Galliani & Väänänen 2014），条件独立原子

→

x

⊥

→

y

→

z

可以用无条件独立原子

→

x

⊥

→

y

来定义。

从句子角度来看，独立逻辑也等价于存在性二阶逻辑 Σ

1

1

;但从公式角度来看，它更具表达力，Galliani 2012 证明它可以捕获所有非空的 Σ

1

1

-可定义团队属性。

4.2 包含逻辑

包含逻辑 (Galliani 2012,Galliani & Hella (2013) 扩展了一阶逻辑，使其具有包含原子

→

x

⊆

→

y

，类似于数据库理论中的包含依赖关系。其语义为：

TS-inc:

M⊨X

→

x

⊆

→

y

当且仅当对于所有 s∈X，存在一个 s′∈X 使得 s(

→

x

)=s′(

→

y

)。

赋值 x1 x2

s0 0 0

s1 0 1

s2 1 2

s3 2 3

与依赖逻辑和独立逻辑不同，包含逻辑（就句子而言）严格弱于存在性二阶逻辑。事实上，可以证明（Galliani & Hella 2013）它等价于最大不动点逻辑的正片断，因此，它能够捕捉有限序模型上的PTIME性质。从公式角度来看，包含逻辑严格弱于独立逻辑，但与依赖逻辑不可比：事实上，其公式的可满足性条件并非向下闭合，而是通过并集闭合，即

M,Xi⊨ϕ∀i∈I⇒M,

⋃

i

Xi⊨ϕ。

4.3 团队逻辑

团队逻辑（Väänänen 2007a,b；Kontinen & Nurmi 2009）通过添加矛盾否定¬扩展了依赖逻辑。它与完整的二阶逻辑具有同等表达能力，无论是在模型类别的可定义性方面 (Väänänen 2007b)，还是在团队逻辑表达式可以针对给定模型定义的团队类别方面 (Kontinen & Nurmi 2009)。在 (Lück 2019) 中，发现了团队逻辑（及其模态和命题等价物）的希尔伯特式公理化，该公理化对于其无依赖片段（即不存在依赖原子的片段）是完备的。

4.4 直觉依赖逻辑

直觉依赖逻辑 (Abramsky & Väänänen 2009; Yang 2013) 通过添加蕴涵联结词 ϕ→ψ 来扩展依赖逻辑。其满足规则在团队语义中由以下公式给出：

TS-→：

X⊨ϕ→ψ 当且仅当对于 X 的所有子集 Y，如果 Y⊨ϕ 则 Y⊨ψ。

该算子被称为“直觉蕴涵”，因为它的语义与克里普克（Kripke）直觉逻辑语义学中的蕴涵算子（Kripke 1965）的语义相似。它在信念方面的解释非常简单：如果 X 中的赋值表示某个代理认为可能的状态，那么 X 的子集 Y 可能表示信念更新的结果，在该信念更新中，代理拒绝了一些先前认为的可能状态，并且ϕ→ψ 状态比任何导致 ϕ 成立的更新也会导致 ψ 成立。从这个角度来看，这是一个非常自然的概念，它使我们能够描述关于此类代理的整体信念状态将如何对信念更新做出反应的预测。

然而，由于其语义中隐含着二阶全称量词，这种连接词足以大大增加逻辑的表达复杂性：具体而言，如(Yang 2013)所示，任何二阶逻辑的句子都等价于直觉依赖逻辑的某个句子。直觉依赖逻辑保留了向下闭合性：如果一个团队满足直觉依赖逻辑公式，则其所有子集也都满足。