独立友好逻辑（二）

[我们] 将我的符号逻辑和一般游戏语义称为斜线逻辑。近年来，该领域的许多作家（但欣蒂卡本人从未这样做过）将“IF 逻辑”的名称改为斜线逻辑，通常没有意识到其中的区别。在术语稳定下来之前，我们必须警惕那些没有明确说明其意图的示例和证明。

霍奇斯对斜线逻辑和 IF 逻辑的区分有助于理清文献中混杂的 IF 一阶逻辑的不同表述。[16]

3.1. 语法

IF 一阶逻辑是一阶逻辑的扩展。现在，任何一阶公式都等同于一个一阶公式，其中没有变量既是自由的又是有界的，并且没有两个嵌套量词带有相同的变量。满足这两个句法条件的公式将被称为常规公式。从今以后，我们将系统地将注意力限制在常规一阶公式上。[17] 词汇表（签名，非逻辑术语）是关系符号（每个符号都带有固定的元数）、函数符号（每个符号也带有固定的元数）和常量符号的任何可数集 τ。词汇表 τ 的一阶逻辑将被称为 FO[τ]。这里假设在一阶逻辑的逻辑符号中有恒等符号 (=)。身份符号在句法上是一个二元关系符号，但其语义解释是固定的，而非逻辑术语中的项的解释则不是。

如果所有否定符号 ∼ 的出现都紧接着一个原子公式，则 FO[τ] 的公式为否定范式。IF 一阶逻辑词汇 τ（或 IFL[τ]）的公式集可以定义为最小集合，使得：

如果 ϕ 是 FO[τ] 的否定范式公式，则 ϕ 为公式。

如果 ϕ 为公式，且在 ϕ 中 (∃x) 的标记出现在包括 (∀y1),…,(∀yn) 在内的多个全称量词的句法范围内，则在 ϕ 中用 (∃x/∀y1,…,∀yn) 替换 (∃x) 的标记的结果为公式。

如果 φ 是一个公式，且在 φ 中，∨ 的标记出现在包括 (∀y1),…,(∀yn) 在内的多个全称量词的句法范围内，则在 φ 中用 (∨/∀y1,…,∀yn) 替换 ∨ 的标记的结果是一个公式。

如果 φ 是一个公式，且在 φ 中，(∀x) 的标记出现在包括 (∃y1),…,(∃yn) 在内的多个存在量词的句法范围内，则在 φ 中用 (∀x/∃y1,…,∃yn) 替换 (∀x) 的标记的结果是一个公式。

如果 ϕ 是一个公式，且在 ϕ 中，∧ 的标记出现在包括 (∃y1),…,(∃yn) 在内的多个存在量词的句法范围内，则在 ϕ 中用 (∧/∃y1,…,∃yn) 替换 ∧ 的标记的结果是一个公式。

子句 (2) 和 (3) 允许全称量词列表为空 (n=0) 的退化情况。结果表达式 (∃x/) 和 (∨/) 分别与通常的存在量词 (∃x) 和通常的析取 ∨ 相一致。对子句 (4) 和 (5) 也做出了类似的规定。

在合适的词汇表中，以下每个都是一个公式：

(∀x)(∀y)(∃z/∀x)R(x,y,z,v),

(∀x)(∀y)(x=y(∨/∀x)Q(x,y)),

(∃x)(S(x)(∧/∃x)T(x)),

(∀x)(∃y)(∀z/∃y)(∃v/∀x)R(x,y,z,v)。

相比之下，以下符号序列都不是公式：

(∃y/∀x)P(x,y),

(∃x)(∃y/∃x)P(x,y),

(∀x)(∀y/∀x)P(x,y),

(∀x)(S(x)(∨/∃y)T(x))。

如果 ϕ 是一个 IFL 公式，由上述子句从某个 FO 公式 ϕ∗ 生成，则 ϕ 的自由变量只是 ϕ∗ 的自由变量。没有自由变量的 IFL 公式是 IFL 句子。[18]

3.2. 语义

使用 GTS 定义逻辑的语义是一个两步过程。第一步是定义相关的语义游戏。第二步是根据语义游戏定义“真”和“假”的概念；这通过参考获胜策略的概念来实现。语义游戏可以通过递归指定与给定公式 ϕ 相关的游戏的替代开始方式来定义。[19]

对于每个词汇 τ、IFL[τ] 公式 ϕ、模型（τ 结构）M 和变量赋值 g，玩家 1 和玩家 2 之间都有一个双人零和游戏 G(ϕ,M,g)。[20] 如果 g 是变量赋值，则 g[x/a] 是变量赋值，它与 g 类似，但将变量 x 映射到对象 a。

如果 ϕ=R(t1,…,tn) 且 M,g⊨R(t1,…,tn)，则​​玩家 2 获胜（玩家 1 失败）；否则玩家 1 获胜（玩家 2 失败）。

如果 ϕ=t1=t2 且 M,g⊨t1=t2，则玩家 2 获胜（玩家 1 失败）；否则玩家 1 获胜（玩家 2 失败）。

如果 ϕ=∼R(t1,…,tn) 且 M,g⊭R(t1,…,tn)，则​​玩家 2 获胜（玩家 1 输）；否则玩家 1 获胜（玩家 2 输）。

如果 ϕ=∼t1=t2 且 M,g⊭t1=t2，则玩家 2 获胜（玩家 1 输）；否则玩家 1 获胜（玩家 2 输）。

如果 ϕ=(ψ(∧/∃y1,…,∃yn)χ)，则玩家 1 选择 θ∈{ψ,χ}，其余游戏与 G(θ,M,g) 相同。

如果 ϕ=(ψ(∨/∀y1,…,∀yn)χ)，则玩家 2 选择 θ∈{ψ,χ}，其余游戏与 G(θ,M,g) 相同。

如果 ϕ=(∀x/∃y1,…,∃yn)ψ，玩家 1 从 M 中选择一个元素 a，游戏的其余部分与 G(ψ,M,g[x/a]) 相同。

如果 ϕ=(∃x/∀y1,…,∀yn)ψ，玩家 2 从 M 中选择一个元素 a，游戏的其余部分与 G(ψ,M,g[x/a]) 相同。

请注意，独立指示在游戏规则中不起作用。事实上，量词独立性将在策略层面上实现。

如果 (∨/∀y1,…,∀yn) 或 (∃x/∀y1,…,∀yn) 的标记出现在公式 ϕ 中，且在全称量词 ∀y1,…,∀yn,∀z1,…,∀zm（且仅这些全称量词）的范围内，则玩家 2 在游戏 G(ϕ,M,g) 中针对此标记的策略函数是满足以下条件的任何函数 f：

f 的参数是玩家 1 选择的元素 a1,…,am，以便解释量词 ∀z1,…,∀zm。当标记是析取时，值 f(a1,…,am) 是左或右析取；当标记是存在量词时，是域的元素。

玩家 1 对于 (∧/∃y1,…,∃yn) 和 (∀x/∃y1,…,∃yn) 标记的策略函数概念可以对偶定义。策略函数被解释为 Skolem 函数 - 这里不考虑在斜线逻辑中起作用的更一般的策略函数概念（参见第 3 节开头和第 6.1 节）。量词独立性将直接根据策略函数的参数实现。

玩家 2 在游戏 G(ϕ,M,g) 中的策略是她的策略函数集 F，对于出现在 ϕ 中的每个 (∨/∀y1,…,∀yn) 和 (∃x/∀y1,…,∀yn) 标记，都有一个函数。如果在游戏 G(ϕ,M,g) 进行时，对于 (∨/∀y1,…,∀yn) 和 (∃x/∀y1,…,∀yn) 中的每个标记，她必须移动一步，则称玩家 2 遵循策略 F。玩家 2 在 G(ϕ,M,g) 中的获胜策略是策略 F，这样，对于玩家 1 的任何移动序列，遵循策略 F 都会让玩家 2 获胜。对于玩家 1，策略和获胜策略的概念可以类似地定义。[21]

在分配 g 下，模型 M 中 IFL 公式 ϕ 的满足和不满足定义如下：[22]

（满足）ϕ 在 g 下的 M 中得到满足，当且仅当在游戏 G(ϕ,M,g) 中玩家 2 存在获胜策略。

（不满足）当且仅当游戏 G(ϕ,M,g) 中玩家 1 有获胜策略时，ϕ 在 M 中不满足条件。

与 FO 一样，变量分配不会影响句子（即不包含自由变量的公式）的（不）满足。事实上，我们可以定义：[23]

（真）当且仅当游戏 G(ϕ,M) 中玩家 2 有获胜策略时，ϕ 在 M 中为真。

（假）当且仅当游戏 G(ϕ,M) 中玩家 1 有获胜策略时，ϕ 在 M 中为假。

φ在M中为真这一事实将用“M⊨φ”表示。写M⊭φ表示φ在M中不为真。这并不意味着φ在上述定义的意义上在M中为假。如第2节末尾所述，存在语义游戏中双方都没有获胜策略。

可以通过删除否定符号只能作为原子公式前缀出现的限制来概括IFL的语法。[24]。为了解释GTS中的否定，在游戏规范中添加了两个角色作为新成分：“验证者”和“证伪者”。最初，玩家1扮演“证伪者”的角色，玩家2扮演“验证者”的角色。角色可能会互换，但只有一个原因：当遇到否定符号时。所有定义语义游戏的子句都必须根据角色而不是玩家来重新表述。扮演“验证者”角色的玩家会为析取和存在量词采取行动，同样，扮演“证伪者”角色的玩家会为合取和全称量词采取行动。当遇到公式 ∼ψ 时，玩家会交换角色，游戏继续进行 ψ。最后，如果遇到的原子公式为真，则“验证者”获胜，“证伪者”失败，否则收益将逆转。否定 ∼ 被称为强否定、双重否定或博弈论否定。[25] 它的工作方式与预期一致：φ 在 M 中为假，当且仅当它的否定 ∼φ 在 M 中为真（参见 Sandu 1993）。

3.3. 基本属性和概念

二价性失败。在 IFL 和模型 M 中存在句子 ϕ，使得 ϕ 在 M 中既非真亦非假。考虑在一个定义域恰好有两个元素 a 和 b 的模型上评估句子 (∀x)(∃y/∀x)x=y。玩家 1 没有获胜策略。如果他选择 a 来解释 ∀x，他将输掉玩家 2 选择 a 来解释 (∃y/∀x) 的玩法。同样，如果玩家 1 选择 b，他将输掉玩家 2 同样选择 b 的玩法。玩家 2 也没有获胜策略。她对于 (∃y/∀x) 的策略函数是常数（零位函数）。有两个这样的常数可用：a 和 b。无论玩家 2 采用哪一个策略函数，玩家 1 都有一步棋可以击败它。如果玩家 2 选择 a，玩家 1 赢得他选择 b 的玩法；如果玩家 2 选择 b，则玩家 1 赢得他选择 a 的比赛。游戏 G(ϕ,M) 是不确定的：两个玩家都没有获胜策略。[26] 不确定性的概念也可以扩展到公式中：

（非确定性）当且仅当在游戏 G(ϕ,M,g) 中，玩家 1 和玩家 2 都没有获胜策略时，ϕ 在 g 下的 M 中是不确定的。

在 IFL 中，非真不会产生虚假。也就是说，二值性在 IFL 中不成立。但是，应该注意的是，它不会因为第三个真值或真值间隙的假设而失败（参见 Hintikka 1991：20、55）。[27] 相反，失败是整个语义理论 (GTS) 基本假设的结果。非确定性对应于一种结构属性：某些类型的函数在所考虑的模型中不存在。

由于二值性的失败，排中律对对偶否定 ∼ 不成立。实际上，当且仅当 M⊭(ϕ∨∼ϕ) 时，ϕ 在 M 中是不确定的。

逻辑等价。如果 IFL 中的句子 ψ 和 χ 在完全相同的模型中为真，则它们为真等价；如果在完全相同的模型中为假，则它们为假等价。如果句子 ψ 和 χ 既是真等价又是假等价，则它们在逻辑上是等价的。[28] 由于二价性失效，在 IFL 中，真等价并不保证逻辑等价。

真、假和独立指示。IFL 的语法允许公式中全称量词和存在量词都以斜线出现，例如，

ϕ:(∀x)(∃y/∀x)(∀z/∃y)R(x,y,z)。

另一方面，量词独立性是在策略层面实现的。因此，当考虑公式的满足（句子的真值）时，全称量词后面的独立指示是空洞的。类似地，当公式的不满足（句子的假性）受到威胁时，存在量词后面的独立性指示也是空洞的。当且仅当玩家 2 在游戏 G(ϕ,M) 中有一个获胜策略 F={c} 时，句子 ϕ 在模型 M 中为真。这又意味着，无论玩家 1 选择哪个元素 a 和 b 分别解释 (∀x) 和 (∀z/∃y)，由 (零位) 策略函数 c 给出的 (∃y/∀x) 的常数解释 c 在 M 中都满足 R(a,c,b)。但这相当于要求无论玩家 1 选择哪个元素 a 和 b 分别解释 (∀x) 和 (∀z)，(∃y/∀x) 的常数解释 c 在 M 中都满足 R(a,c,b)。事实上，φ 是与不包含斜线全称量词的句子等价的真值：

φ 在模型 M 中为真当且仅当句子 (∀x)(∃y/∀x)(∀z)R(x,y,z) 在 M 中为真。

类似地，φ 是与不包含斜线存在性量词的句子等价的假值量词：φ在模型M中为假当且仅当句子(∀x)(∃y)(∀z/∃y)R(x,y,z)在其中为假。

3.4. 扩展IF一阶逻辑

如果φ是FO的一个句子，φ在模型M中为假当且仅当∼φ在M中为真当且仅当φ在M中不为真。相反，在IFL中，假和非真并不重合。可以引入IFL的扩展，其中可以谈论句子的非真。为此，让我们引入一个新的否定符号¬，称为弱否定、矛盾否定或经典否定。[29]扩展 IF 一阶逻辑的公式集（记为 EIFL）是通过在 ¬、∧ 和 ∨ 运算下将其封闭而从 IFL 公式集获得的：[30]

IFL 的所有公式都是 EIFL 的公式。

如果 ϕ 和 ψ 是 EIFL 的公式，则 ¬ϕ、(ϕ∧ψ) 和 (ϕ∨ψ) 也是 EIFL 的公式。

因此，如果 ϕ 和 ψ 是 IFL 公式，例如 ¬ϕ 和 (¬ϕ∨ψ) 是 EIFL 公式；相反，(∀x)¬ϕ 不是。有关 ¬ 不能出现在量词范围内的关键限制，请参阅 Hintikka (1991: 49; 1996: 148)。但是，有关此限制的反例，请参见 Hintikka (1996: 148; 2002c) 和特别是 Hintikka (2006b)，其中考虑了所谓的完全扩展 IF 一阶逻辑 (FEIFL)。在 FEIFL 中，任何 ¬ 的出现都是允许的，但要符合以下句法条件：如果 (Qx/W) 是 ¬ 出现的句法范围内的量词，则 W 中列出的所有量词同样在 ¬ 出现的句法范围内。

由矛盾否定形成的 EIFL 公式的语义很简单：

M,g⊨¬ϕ 当且仅当 M,g⊭ϕ。

从 GTS 的角度来看，连接词 ¬ 的行为方式不同寻常。对于 IFL 的所有连接词，都有一个游戏规则（可以看作是指定连接词的含义）。对于矛盾否定，没有游戏规则，其语义不能用语义游戏的玩法来解释。公式 ¬ϕ 可以全局地表示整个游戏 G(ϕ,M,g) 的某些内容。如果 ϕ 是一个句子，那么说 ¬ϕ 在 M 中为真就是说玩家 2 在游戏 G(ϕ,M) 中没有获胜策略。如果玩家 2 在 G(ϕ,M) 中确实有获胜策略，则根据规定 ¬ϕ 在 M 中为假。[31]

¬ϕ 本身不仅不是 IFL 公式，而且通常甚至不能用 IFL 表达（参见第 4.2 节）。排中律适用于矛盾否定：对于所有句子 ϕ 和所有模型 M，确实 M⊨(ϕ∨¬ϕ)。在第 5 节中，我们将看到 Hintikka 提议在讨论数学哲学问题时如何使用 EIFL。

4. IF 一阶逻辑的元逻辑性质

IFL 的元逻辑性质已在 Hintikka 和 Sandu 的几篇出版物中进行了讨论。[32] 在介绍它们时，将参考存在性二阶逻辑 (ESO)；[33] 进一步的重要概念是 IFL 公式的 Skolem 化和 Skolem 范式。有关这些概念的精确定义，可以查阅补充文件。简而言之，ESO 是通过允许对一阶公式中的关系和函数符号进行存在性量化从 FO 获得的。IFL 公式 ϕ 的 skolem 化 sk[ϕ] 是词汇量更大的一阶公式。它以函数符号的形式阐明了 ϕ 的存在量词和析取符号如何依赖于前面的全称量词。例如，词汇表 {R} 的 IFL 句子 ϕ=(∀x)(∃y)(∀z)(∃v/∀x)R(x,y,z,v) 的 Skolem 化是词汇表 {R,f,h} 的 FO 句子 sk[ϕ]=(∀x)(∀z)R(x,f(x),z,h(z))。其 Skolem 范式同样是 ESO 句子 SK[ϕ]=(∃f)(∃h)(∀x)(∀z)R(x,f(x),z,h(z))。一阶句子 sk[ϕ] 一定不能与二阶句子 SK[ϕ] 混淆。

4.1. 一阶逻辑和存在二阶逻辑

FO 的博弈论语义与 Tarskian 语义。 FO 的公式集是 IFL 公式集的真子集。FO 的标准语义不是 GTS 提供的语义，而是塔斯基语义，它递归地指定满足关系 M,g⊨ϕ。如果假设选择公理，[34]FO 的两个语义是一致的：

定理（假设 AC）。（Hodges 1983：94，Hintikka & Kulas 1985：6-7）让 τ 为任何词汇，M 为任何 τ 结构，g 为任何变量赋值，ϕ 为任何 FO[τ] 公式。然后 M,g⊨ϕ 在标准意义上成立，当且仅当在游戏 G(ϕ,M,g) 中玩家 2 有一个获胜策略。[35]

与 ESO 的关系。IFL 和 ESO 是可互译的：[36]

定理（假设 AC）ESO 和 IFL 具有相同的表达能力。

也就是说，(1) 对于每个 IFL[τ] 公式 ϕ，都有一个 ESO[τ] 公式 ϕ′，使得对于所有 τ 结构 M 和变量分配 g，我们有：M,g⊨ϕ当且仅当 M,g⊨ϕ′。实际上，SK[ϕ] 是一个合适的 ESO 公式。(2) 对于每个 ESO[τ] 公式 ψ，都有一个 IFL[τ] 公式 ψ′，使得对于所有 τ 结构 M 和变量分配 g，M,g⊨ψ当且仅当 M,g⊨ψ′。这是因为 ESO 可以转化为 FPO（Enderton 1970，Walkoe 1970），而 FPO 又可以转化为 IFL。

Hintikka 认为，IFL 本质上是一种一阶逻辑：其量化变量所涵盖的实体是个体，语义游戏的参与者与之互动的所有实体也是如此。 （有关这一想法的讨论，请参阅第 5.1 节。）互译性定理的部分兴趣在于，如果欣蒂卡的争议性主张被接受，这将意味着 ESO 的表达能力实际上可以在一阶水平上实现。

IFL 比 FO 更具表现力。以下是可以在 ESO（因此也可以在 IFL）中表达但不能在 FO 中表达的属性示例：域的 Dedekind 无穷性、线性顺序的非完备性、二元关系的无根据性、图的不连续性、两个一阶公式 ϕ(x) 和 ψ(x) 扩展的等基数性、一阶公式 ϕ(x) 扩展的无穷性以及开集的拓扑概念（例如，参见 Hintikka 1996、Väänänen 2007）。