独立友好逻辑（三）

例如，可以考虑域的戴德金无穷性。当存在从 S 到其真子集的单射函数时，集合 S 正是戴德金无穷的。设 ϕinf 为 IFL 的以下句子：[37]

(∃t)(∀x)(∃z)(∀y)(∃v/∀x)((x=y↔z=v)∧z≠t)。

ϕinf 的 Skolem 范式为

(∃f)(∃g)(∃t)(∀x)(∀y)((x=y↔f(x)=g(y))∧f(x)≠t)。

相对于模型 M，这个 ESO 语句断言存在函数 f 和 g 以及元素 t，使得 f=g（从左到右蕴涵），该函数是单射（从右到左蕴涵），其定义域是 M 的整个定义域，但元素 t 不出现在其值域中。因此，值域是 M 定义域的真子集。换句话说，语句 ϕinf 在模型 M 中为真，当且仅当 M 的定义域是无限的。

值得注意的是，当注意力局限于有限模型时，Ronald Fagin 的著名定理 (1974) 将 ESO 与复杂性类 NP 联系起来：计算问题可以通过在非确定性多项式时间内运行的算法来解决，当且仅当它在 ESO 中相对于所有有限结构类是可定义的。以下是 NP 完全性质，因此可以在所有有限模型类中用 IFL 表示：论域的均匀性、论域的奇性、图的 3-着色性以及图上哈密顿路径的存在性。[38]

与 FO 共有的属性。IF 一阶逻辑与一阶逻辑有许多元逻辑属性。[39]

紧凑性。一组 IFL 句子有一个模型当且仅当它的所有有限子集都有一个模型。

Löwenheim-Skolem 属性。假设 ϕ 是一个具有无限模型或任意大有限模型的 IFL 句子。那么 ϕ 具有所有无限基数的模型。

分离定理在 IFL 中以强化形式成立；“分离句子”θ 特别是 FO 的一个句子。

分离定理。假设 ϕ 是词汇 τ 的 IFL 句子，ψ 是词汇 τ′ 的 IFL 句子。进一步假设 ϕ 和 ψ 没有共同的模型。然后存在一个词汇表 τ∩τ′ 的一阶句子 θ，使得 ϕ 的每个模型都是 θ 的模型，但 θ 和 ψ 没有共同的模型。

众所周知，对于 FO，有一个可靠且完整的证明程序。因为一阶句子 ϕ 是不一致的（不可满足的）当且仅当它的否定 ∼ϕ 有​​效（在所有模型中为真），所以 FO 显然也有一个可靠且完整的反证程序。[40] 后一个属性扩展到 IFL（而前者不扩展，参见第 4.3 节）：

存在完整的反证程序。（Hintikka 1996：68–70, 82）不一致的 IFL 句子集是递归可枚举的。

4.2。否定的复杂性

在第 3.4 小节中，矛盾否定 ¬ 与强否定 ∼ 区分开来。在 FO 中，两者是一致的：对于任何一阶句子 ϕ，当且仅当 M⊨¬ϕ 时，我们有 M⊨∼ϕ。

强否定作为语义操作失败。让我们将句子 ϕ 的模型集写为 [ϕ]。在 FO 的特殊情况下，强否定 ∼ 清楚地定义了一个语义操作：每当 χ 和 θ 是满足 [χ]=[θ] 的句子时，我们就有 [∼χ]=[∼θ]。Burgess (2003) 观察到，在 IF 逻辑的上下文中，这种属性在非常强烈的意义上消失了。事实上，存在 IF 句子 χ 和 θ，使得当 [χ]=[θ] 时，集合 [∼χ] 和 [∼θ] 不仅不同，甚至不相交。

矛盾否定的不可表达性。在 IFL 中，强否定 ∼ 和矛盾否定 ¬ 并不重合：我们可能有 M⊨¬ϕ 而没有 M⊨∼ϕ。这一事实本身仍然保留了这样的可能性，即 IFL 的每个句子 ϕ 的矛盾否定都可以在 IFL 中定义，即存在一个 IFL 句子 neg(ϕ)，当且仅当 M⊭ϕ 时，对于所有模型 M，M⊨ neg(ϕ) 都是成立的。根据排中律的失效，我们只知道，并非在所有情况下都可以将 neg(ϕ) 选为 ∼ϕ。然而，事实上矛盾否定在 IFL 中是无法表达的。存在 IFL 句子 ϕ，使得 ¬ϕ（EIFL 的一个句子）不等同于任何 IFL 句子的真值。这是因为众所周知，ESO 在否定下不封闭，而 IFL 具有与 ESO 相同的表达能力。[41]

矛盾否定的强不可表达性。作为分离定理的推论，结果以更强的形式成立。如果 ϕ 和 ψ 是 IFL 的句子，并且 M⊨ϕ 当且仅当 M⊭ψ 时，则 ϕ 和 ψ 中的每一个都等同于 FO 的句子的真值。因此，矛盾否定 ¬ϕ 仅对那些等同于 FO 句子的 IFL 句子 ϕ 才可以在 IFL 中表达。[42]

确定片段。假设一个 IFL 句子 ϕ 满足：对于所有模型 M，M⊨(ϕ∨∼ϕ)，则它是确定的。IFL 的确定片段是确定 IFL 句子的集合。在确定片段中，矛盾否定在句法上可以通过强否定来表达。由于矛盾否定的强不可表达性，IFL 的确定片段具有与 FO 相同的表达能力。确定片段中的成员资格是 IFL 句子的矛盾否定可以在 IFL 中表达的充分但非必要条件。句子 (∀y)(∃x/∀y)x=y 未确定；[43] 但其矛盾否定 (∀x)(∃y)x≠y 可以在 IFL 中表达。

矛盾否定和 GTS。GTS 产生的真值条件的形式为“存在策略函数 f1,…,fn 使得 —”，即它产生了可以在 ESO 中表达的真值条件。由于矛盾否定具有很强的不可表达性，因此没有一个 IFL 句子不能翻译成 FO，其矛盾否定具有该形式的真值条件。这一事实使人们可以理解为什么矛盾否定不应被期望以与其他逻辑运算符相同的方式接受博弈论解释。然而，可以开发出为矛盾否定分配博弈论解释的不同方法。为此，在完全扩展的 IF 一阶逻辑（FEIFL，参见第 3.4 节）的背景下，Hintikka 建议使用带有子博弈的语义博弈。 （参见 Hintikka 2002c、2006b；有关子博弈，参见 Carlson 和 Hintikka 1979、Hintikka 和 Kulas 1983。）这种方法导致游戏层面与策略层面相混淆：子博弈中个人的选择可能取决于早期子博弈中选择的策略函数。在 Tulenheimo (2014) 中，为由前缀形式公式组成的 FEIFL 片段制定了博弈论语义。相关博弈的游戏不涉及选择任何二阶对象，例如策略函数。矛盾否定 (¬) 通过在游戏位置中引入额外成分来解释：模式。在游戏层面，否定 ¬ 不仅会触发角色转换（如双重否定 ∼），还涉及将模式从正面更改为负面或反之亦然。模式的语义效应在策略层面上变得可见：模式调节句子的真值条件涉及策略函数的存在性或普遍量化的方式。与独立性指示一样，¬ 的出现也根据作用于策略层面的条件进行解释。有关相关研究，请参阅 Figueira 等人（2011 年、2014 年）。

矛盾否定和有限模型。逻辑和理论计算机科学中的某些主要开放问题可以用 IFL 来表述。在复杂性理论中，NP=coNP 是否是一个开放问题，即 NP 可解问题类是否与其补集在 NP 中可解的问题类相同。根据 Fagin 定理（1974 年），这个开放问题可以等效地表述如下：IFL 在有限模型的否定下是否封闭？也就是说，对于每个 IF 语句 ϕ，是否存在另一个 IF 语句 neg(ϕ)，使得对于任何有限模型 M，neg(ϕ) 在 M 中为真，当且仅当 ϕ 在 M 中不为真？证明答案是否定的，将解决臭名昭著的 P=NP 问题，即确定存在一些计算问题，虽然无法有效地找到解决方案，但可以有效地验证所提出的解决方案是否正确。[44]

4.3 公理化失败

众所周知，FO 承认一个合理而完整的证明程序：有一种机械方法可以精确生成那些有效（在所有模型中为真）的一阶句子。这个事实也可以通过说 FO 是可公理化的，或者 FO 的有效句子集是可递归枚举的来表达。[45] 由于其表达能力更强，IFL 的公理化失败。换句话说，IFL 在语义上是不完整的。[46]

证明这一点的一种方式如下。为了反驳，假设有效 IFL 句子集是可递归枚举的。回想一下第 4.1 节中讨论的句子 ϕinf 在所有且仅在无限模型中为真。然后请注意，FO 句子 χ 在所有有限模型中为真当且仅当 IFL 句子 (ϕinf∨χ) 有效。给定一个有效的 IFL 句子，可以有效地检查该句子的句法形式是否为 (ϕinf∨χ)，其中 χ 是一阶句子。因此，所有有效 IFL 句子的递归枚举产生了在所有有限模型中为真的一阶句子 χ 的递归枚举。但这与 Trakhtenbrot 定理相矛盾，根据该定理，在所有有限模型中为真的 FO 句子集不是可递归枚举的。[47]

IFL 无法公理化，这有什么意义呢？在讨论有限偏序量词时，奎因 (1970: 89–91) 建议，我们不应该将逻辑地位赋予任何没有完善的有效性和不一致性证明程序的 FO 泛化。对奎因来说，任何这样的泛化都属于数学，而不是逻辑。由于 FPO 不可公理化，因此它不属于逻辑的范畴。[48]

Hintikka 认为这种指控毫无根据。首先，IFL 与 FO 有许多重要的元逻辑结果（参见第 4.1 节）。其次，与 IFL 一样，FO 也可以翻译成二阶逻辑。唯一的区别在于，前者需要用 Skolem 函数编码的量词（不）依赖性种类比后者更多。为什么前者翻译会让 IFL 成为数学的一部分，而后者却让 FO 保持逻辑性（Hintikka 1991：26-27）？第三，必须区分理解 IFL 句子所需的内容和机械处理 IFL 有效性（逻辑真理）所需的内容。由于 IFL 不可公理化，因此没有机械规则来生成 IFL 所有有效性的集合。然而，理解一个句子就是要知道当句子为真时事情是什么样的，而不是当句子在逻辑上为真时事情是什么样的（Hintikka 1995：13-14）。第四，由于非公理化，IFL 中的有效推理模式不能通过任何递归枚举来穷尽。只要重要的数学问题可以归结为关于 IFL 公式有效性的问题（第 5.3 节），数学的进步就可以看出来（不是发现更强的集合论公理，而是）由建立 IFL 有效性的更强大的规则组成（Hintikka 1996：100；2000：135-136）。

4.4 组合性和塔斯基式语义的失败

组合性原理（又称弗雷格原理）指出，复杂表达式 E 的语义属性由其组成表达式的语义属性和 E 的结构决定。特别是，感兴趣的语义属性（例如真值）可以根据一个或多个辅助语义属性（例如满足度）来确定。[49] Hintikka 认为组合性相当于语义上下文独立性：复杂表达式的语义属性仅取决于其组成表达式的语义属性及其结构 - 它们不依赖于表达式所嵌入的句子上下文。语义上下文独立性使得从内到外进行语义分析成为可能 - 从更简单的表达式到更复杂的表达式。[50] 这正是语义属性的递归定义（例如塔斯基式的真值和可满足性定义）成为可能所需要的。[51]相比之下，GTS 对句子的分析是一个由外而内的过程：语义游戏从整个句子开始，逐步将句子分析成越来越简单的组件，最终达到原子公式（连同适当的变量分配）。因此，GTS 允许解释违反组合性原则的语义上下文依赖性。[52]

在 IFL 中，存在量词可能仅依赖于它所在的某些通用量词。因此，它的解释取决于它与自身范围之外的量词的关系。这样的存在量词是上下文相关的。[53] 从表面上看，IFL 不能不违反组合性原则，并且不承认塔斯基式的真值定义。

然而，霍奇斯（1997a，b）表明，IFL 可以被赋予组合语义。[54]语义是通过递归定义满足关系“M⊨Xϕ”（读作：ϕ 在 M 中由 X 满足）给出的，其中 X 是一组变量分配。FO 的塔斯基语义是关于单个变量分配的，而霍奇斯的语义则采用变量分配集。IFL 的博弈论语义由这种组合语义捕获：对于 IFL 的每个公式 ϕ，当且仅当条件 M⊨{g}ϕ 成立，玩家 2 在 G(ϕ,M,g) 中都有一个获胜策略。由于霍奇斯的存在量词和涉及独立指示的析取的语义子句，相对于单例集 {g} 评估 ϕ 通常会导致评估 ϕ 的句法成分相对于（可能无限）多个变量分配集。 Hintikka 指出 (2006a: 65)，如果一个人足够冷酷无情，他总是可以通过将不同表达式的语义交互定律构建到这些表达式的各自含义中来挽救组合性。[55]

从方法论上来说，值得指出的是，组合性对于定义 IFL 来说并不是必需的。IFL 的存在本身就证明了拒绝组合性并不妨碍制定强大的逻辑 (Hintikka 1995)。还应该注意的是，使 Hodges 的结果奏效的是其类型理论的上升。我们假设 Tarski 类型的组合语义是一种将 n 个自由变量的每个公式 ϕ(x1,…,xn) 解释为域元素的 n 元组的组合语义。因此，FO 的标准语义是塔斯基型的，但霍奇斯采用满足关系“M⊨Xϕ”的语义不是，因为后者相对于整个 n 元组元素集来评估 n 个自由变量的公式 ϕ(x1,…,xn)。Cameron & Hodges (2001) 证明，IFL 实际上没有塔斯基型组合语义。

可以通过对辅助语义属性施加约束来细化组合性的概念。Sandu 和 Hintikka (2001: 60) 类比 FO 提出，“通过单个变量赋值满足”将是与 IFL 相关的自然辅助属性。根据 Cameron 和 Hodges 的结果，IFL 不存在在这种受限意义上是组合性的语义。

4.5 定义真理

真理的可定义性只能与能够自我表达的语言联系起来讨论。让我们考虑一个算术词汇表 τ，并将注意力限制在皮亚诺公理的标准模型 N 上。词汇表 τ 中的每个句子 ϕ 都可以用自然数 ⌜ϕ⌝（其哥德尔数）表示。假设 τ 包含每个数字 ⌜ϕ⌝ 的数字 ⌜ϕ⌝。如果 L 和 L′ 是词汇 τ 的抽象逻辑，例如 FO 或 IFL，并且 TRUE(x) 是 L′ 的一个公式，使得 L 的每个句子 ϕ 都满足：

N⊨ϕ 当且仅当 N⊨TRUE(⌜ϕ⌝)，

则 TRUE(x) 被称为逻辑 L′ 中逻辑 L 的真值谓词（明确的真值定义），适用于模型 N。根据阿尔弗雷德·塔斯基著名的真值不可定义定理（Tarski 1933），对于模型 N，FO 本身中没有 FO 的真值谓词。更一般地，塔斯基表明，在某些假设下，逻辑 L 的真值定义只能在本质上比 L 更强的元语言中给出。其中一个假设是所使用的否定表现得像矛盾否定。另一方面，塔斯基还指出，FO 本身中隐含的真值定义是可能的。令 τ 为算术词汇表，让我们采用皮亚诺公理的标准模型 N。令“TRUE”为未出现在 τ 中的一元谓词。如果对于每个 FO[τ] 句子 ϕ，以下成立，则词汇表 τ∪{TRUE} 的 FO 公式 ψ(x) 是 N 的 FO[τ∪{TRUE}] 中 FO[τ] 的隐含真值定义：

N⊨ϕ 当且仅当存在一元谓词 TRUE 的解释 TRUEN，使得 (N,TRUEN)⊨ψ(⌜ϕ⌝)。[56]

直观地讲，TRUEN 是词汇表 τ 的真算术句子的哥德尔数的自然数的集合； ψ(x) 表示 x 是谓词 TRUE 扩展中的哥德尔数。公式 ψ(x) 是一个合取式，其中包含在对象语言层面上模仿塔斯基型 FO 真值定义的元逻辑递归子句的子句。例如，其中一个合取式是

(∀y)(∀z)(y=⌜χ⌝ ∧z=⌜θ⌝∧x=⌜(χ∧θ)⌝→

[TRUE(x)↔(TRUE(y)∧TRUE(z))])。

真值定义的隐含性质可以从这些子句中谓词 TRUE 出现在等价符号的两侧这一事实中看出。[57]上述 FO 对 N 的隐式真值定义的形式为“存在一个集合 S，它将谓词 TRUE 解释为 ψ(x)。因此，FO 中 FO 的隐式真值定义产生了 ESO[τ] 中 FO[τ] 对 N 的显式真值定义 ∃TRUEψ(x)。由于 ESO 和 IFL 具有相同的表达能力，因此可以在 IFL 中表述 FO 对 N 的真值谓词。

同样的推理可以应用于 ESO 本身，从而应用于 IFL（Hintikka 1991、1996；Hyttinen & Sandu 2000；Sandu 1996、1998）。也就是说，可以制定词汇 τ∪{TRUE} 的 ESO 公式 χ(x)，它是 N 的 ESO[τ] 的隐式真值定义。因此，ESO[τ] 公式 ∃TRUEχ(x) 是 N 的 ESO[τ] 的显式真值定义。这里，真值谓词用定义真值概念的同一语言来制定：ESO。因此，ESO 以及 IFL 能够明确定义相对于 N 的真值谓词。[58] 这个结果并不与塔斯基的不可定义性结果相矛盾，因为这里可能存在不确定的句子；使用的否定不是矛盾否定。[59]

塔斯基 (1983) 采取了一种观点，即自然语言的真值无法定义。 Hintikka & Sandu (1999) 认为，这是由于塔斯基认为自然语言中不存在组合性。[60] IFL 没有塔斯基式的组合语义，但它允许制定一个自我应用的真值谓词。塔斯基认为不可能在自然语言中讨论真值概念的理由，从 IFL 的角度来看是无法接受的。因为，IFL 的案例表明，一种语言的塔斯基式组合性的失败并不意味着该语言无法定义自己的真值谓词。[61]