多分类逻辑（二）

重合引理

与经典一阶逻辑一样，重合引理成立（参见经典逻辑条目）：对于任何公式 φ 和赋值 s1 和 s2：如果 s1 和 s2 在 φ 中的自由变量上一致，则 A,s1⊨φ 当且仅当 A,s2⊨φ。

对于自由变量在 {x1,…,xn} 中的公式 φ(x1,…,xn)，可以写成

A⊨φ[x1,…,xn]

而不是

A,s(x1/x1,…,xn/xn)⊨φ。

通过应用重合引理，我们可以在处理句子时摆脱赋值，因此我们只需写 A⊨φ（而不是 A,s⊨φ）。在这种情况下，我们通常说 A 是 φ 的模型。

对于一组句子 Γ，当 A 是 Γ 中每个句子 γ 的模型时，我们说 A 是 Γ 的模型（简称 A⊨Γ）。结构和语言共享特征。

语义的抽象模式可以这样看：我们有一个语言 L 和一类数学结构，它们共享给定的特征 Σ。在这些数学现实之间，我们刚刚建立了一座桥梁，即结构中的真理概念。在一个方向上，我们从句子循环到这些句子为真的结构；在另一个方向上，我们从结构循环到在这些结构中为真的句子。在第一种情况下，从签名为 Σ 的句子集 Γ 中，我们将 Mod(Γ) 定义为签名为 Σ 的结构类，这些结构是 Γ 的模型。在第二种情况下，从签名为 Σ 的结构 A 中，我们定义 Th(A)（A 的理论），即在结构 A 处为真的无限句子集

Mod(Γ)={Σ 结构 A:A⊨Γ}Th(A)={φ∈Sent(L):A⊨φ}

基本嵌入

在上一节中，结构之间的关系是在没有借助于多种形式语言的情况下定义的。但对于基本嵌入，情况并非如此，它是同一签名的多种结构之间的另一种关系。两个 Σ-结构 A 和 A′ 之间的基本嵌入 π 是满足以下条件的嵌入：

对于结构域中的所有 Σ-公式 φ(x1,…,xn) 和元素 x1,…,xn，变量和元素具有相同的类别，A⊨φ[x1,…,xn] 当且仅当 A′⊨φ[π(x1),…π(xn)]

。

两个结构 A 和 B 基本等价当且仅当它们的理论相同，Th(A)=Th(B)。

可满足性、有效性和后果

可满足性、有效性和后果的概念定义与经典一阶逻辑相同。给定签名为 Σ 的语言 L 和 L 的公式 φ：φ 可满足当且仅当存在 Σ 结构 A 及其上的赋值 s，使得 A,s⊨φ 成立；φ 有效（⊨φ）当且仅当 A,s⊨φ 对签名为 Σ 的所有 A 以及 A 上的任何赋值 s 都成立。

给定签名为给定 Σ 的语言 L，我们定义结果关系如下：Γ⊨φ 当且仅当对于每个结构 A（签名为 Σ）和赋值 s，使得 A,s⊨γ，对于所有 γ∈Γ，我们有 A,s⊨φ。

如果 Γ 和 φ 是句子，则 Γ⊨φ 可以这样表示：Mod(Γ)⊆Mod(φ)。

理论：给定语言 L 的一组句子 Γ，我们说 Γ 是一个理论[6]当且仅当它在结果下是封闭的；也就是说，对于每个 φ∈Sent(L)：如果 Γ⊨φ 则 φ∈Γ。

2. 微积分

2.1 演绎演算

在模型论中，通常将逻辑视为至少包含三个不同的东西：一类结构、描述这些结构的形式语言以及确定语言公式何时对给定结构为真的满足关系。可以添加演绎演算。

事实上，任何一类一阶逻辑的演算都可以很容易地扩展到多类一阶逻辑的演算；唯一需要调整的规则是处理量词和替换的规则，因为它们必须考虑到允许的种类的多样性。在经典逻辑中，需要更改的规则是：引入和消除全称量词（∀I 和 ∀E）、引入和消除存在量词（∃I 和 ∃E）以及处理相等的规则（=I 和 =E）。

Manzano (1996: 240–257) 提出的序贯演算是对 Ebbinghaus、Flum 和 Thomas (1984) 提出的序贯演算的多类扩展。王浩 (1952: 106) 是研究多类逻辑的先驱逻辑学家之一，他已经在他的开创性著作中为这种逻辑引入了公理演算（有关更多信息，请参阅早期历史补充）。

照例，为了表示从一组公式中得出公式的可导性，我们写为Δ⊢φ。在需要时，我们将可导性符号⊢写为带下标的符号；即⊢MSL。在任何这些演算中，证明的概念都是有效的，因为有一种方法，只要给出一个公式序列的有限序列，就总能有效地确定它是否是一个证明。任何这些演算都是不可判定的，因为没有算法可以检查是否⊢φ。事实上，情况不可能不是这样，因为多排序逻辑的可满足性问题（即确定有效性，或等效地，测试给定公式的可满足性）是不可判定的。所以，我们处于与一排序一阶逻辑中遇到的相同的情况。

当然，如果微积分要有用，它就绝不会允许错误的推理：它不会让我们从正确的假设得出错误的结论。它必须是一个合理的微积分。此外，非常希望一组 Γ 假设的所有后果都能从 Γ 中推导出来。也就是说，我们希望有一个强完备的微积分。在我们的第 2.3 节中，您将找到这种完备性证明的草图。

最大一致性和具有见证的性质

句法概念的定义也是标准的；[7] 即一致性、最大一致性和具有见证的性质。在目前的情况下，如果每个存在公式都带有见证（∃xiφ∈Δ 意味着 φ(t/xi)∈Δ，对于 i 类项 t），则公式集包含见证。这三个都是公式和/或公式集的性质，在它们的定义中我们使用可导性；即演绎演算。

一致性可以看作是可满足性的句法对应物，就像 ⊢ 和 ⊨ 相互对应一样。事实上，Henkin 的完备性证明基本上包括为每个一致集构建一个模型。

2.2 完备性概念

证明和真值由独立方法定义，证明它们在外延上是相同的并非易事，但却是必要的。当此属性以健全的演算为前提时，这就是完备性定理的内容。当完备性作为理论的前提时，它还有另一层含义：当对于每个句子，φ 或 ¬φ 都是 Γ 的结果时，理论 Γ 就是完备的 (Manzano 1989 [1999: 118])。演算的强完备性确立了其捕捉逻辑结果的充分性；即，每当一个句子从一组假设中合乎逻辑地得出时，演算中就有这个句子的证明，可能使用其中一些假设。相反，弱完备性则表示我们有所有有效性的证明。在完备[8]逻辑中，语言的表达能力和计算能力是平衡的。因此，完备性问题就是逻辑的基本组成部分之间的平衡问题：语义和逻辑演算。

有时，我们仅仅说一个逻辑是完备的，并将这个属性限定为抽象完备性。在这种情况下，我们只关心逻辑真值集（有效性）的计算特性，我们只需要知道它们是递归可枚举的。

第 3 节将多类别逻辑介绍为统一逻辑，我们将嵌入 MSL 的三个层次的过程描述为所研究逻辑完备性的途径：第一级抽象完备性，第三级强完备性。

2.3 多类别逻辑的完备性

多类别演算的完备性证明可以按照众所周知的 Henkin (1949) 的一阶逻辑策略进行。重要的问题是能够证明每个一致的公式集都有一个模型，因此句法一致性和语义可满足性是等价的（假设健全性）。证明基本上分为两个步骤：

每个一致的公式集都可以扩展为具有见证的最大一致集。

一旦我们有了具有见证的最大一致集，我们就会将其用作指南，构建由该集合的公式描述的精确模型。原因是最大一致集是对结构的非常详细的描述。

通过这样做，我们证明：

Henkin 定理：如果 Γ⊆ Form(L) 是一致的，则 Γ 有一个可数模型。[9]

完备性定理

强完备性：如果 Γ⊨φ 则 Γ⊢φ

很容易从中得出。

为了说明 Henkin 定理蕴含着强完备性，我们假设先行式为 Γ⊨φ。因此，Γ∪{¬φ} 不可满足，它没有模型。利用 Henkin 定理，我们得出结论：Γ∪{¬φ} 是矛盾的，因此 Γ∪{¬φ}⊢φ。微积分规则允许我们去掉 ¬φ 并推断出 Γ⊢φ。

作为先前结果的推论，可以得到：

弱完备性：如果 ⊨φ 则 ⊢φ。

紧致性定理：Γ 有一个模型当且仅当它的每个有限子集都有一个模型。

Löwenheim-Skolem：如果 Γ 有一个模型，那么它有一个可数模型。

在 Manzano (1996: 245–257) 中，完备性定理在强意义上被证明，并且适用于所有公式，而不仅仅是句子。完备性及其推论的证明遵循了 Ebbinghaus、Flum 和 Thomas (1984) 引入的路径。

多类别逻辑是一阶逻辑的适当（或严格）扩展吗？Lindström (1969) 证明，一阶逻辑可以被描述为同时具有 紧致性 和 Löwenheim-Skolem 属性的最强逻辑。此外，一阶逻辑是 Löwenheim-Skolem 成立且其有效句子集可递归枚举的最强逻辑。因此，多类别逻辑不能被视为一阶逻辑的适当扩展。

2.4 自动定理证明器

多类逻辑提供了结果的语义概念以及演绎演算，可用于从假设得出结论的数学过程。现在的问题是通过构建计算机程序进行演绎推理来自动化此推理过程。

正如我们已经提到的，健全性是演算的基本要求，而完整性保证所有语义结果都可以在演算中建立，因此有效性集是递归可枚举的。自动推理最相关的属性是可判定性和复杂性。当存在一种算法可以在有限的时间内对以下问题回答“是”或“否”时，逻辑是可判定的：公​​式φ是否有效？由于有效性和可满足性是可相互定义的（⊨φ当且仅当¬φ不可满足），因此这个问题通常被称为可满足性问题。计算机需要执行的基本任务包括可满足性和模型检查。

命题逻辑是可判定的，而一阶逻辑（包括多元逻辑）是不可判定的。然而，在命题逻辑和一阶逻辑之间存在可判定逻辑，如一元谓词逻辑（谓词都是一元谓词的一阶逻辑），以及不可判定逻辑的可判定片段[10]。此外，在可判定问题中，还有衡量计算机时间和内存寄存器使用时间的时间空间复杂度。

因此，在多元微积分的定理证明器中，不能保证得到这个问题的答案：Γ⊨φ吗？然而，在许多情况下，有高效的定理证明器能够解决这个问题；例如，当有可判定片段需要实现时。请参阅自动推理和 Church 类型理论的条目。 Church 类型理论条目的第 4 节专门介绍自动化，并提供了有关面向机器的证明演算以及早期证明助手的信息。介绍了 Church 类型理论的一系列优秀定理证明器。其中包括 LEO-II 和 LEO-III，后者据称“使用转换为多分类逻辑与一阶推理工具合作”。

Church 的简单类型理论通常仅从基类型“i”（个体/实体）和“o”（布尔值）开始，然后从这些开始迭代定义所有函数类型（例如“i=>o”、“i=>i”、“o=>o”、“i=>(i=>o)”等）。但实际上可以有任意多个基类型 i1、i2、i3、...，并应用类似的构造。这些基类型 i1、i2、i3、… 可以被视为排序。

我们的《圆满空性之书》中的例子可以使用 LEO-II 和 LEO-III 证明器进行形式化和检查。

thf(sortForObjects, type, (object: $tType)).

thf(sortForTimes, type, (time: $tType)).

thf(constantDawn, type, (dawn: time)).

thf(constantToday, type, (today: time)).

thf(constantIsExistsAt, type,

  (existsAt: object＞time＞$o)).

thf(constantPrecedesTo, type,

  (precedesTo: time＞time＞$o)).

thf(公理1，公理，(![X：时间]：

  ((?[Y：对象]：(existsAt @Y@X))

  =＞ (![Z：时间]：((precedesTo @Z@X)

  =＞ (?[V：对象]：(existsAt @V@Z)))))))。

thf(公理2，公理，

  (?[Y：对象]：(existsAt @Y@today)))。

thf(公理3，公理，

  (![Y：时间]：(precedesTo @dawn@Y)))。

thf(推测1，推测，

  (?[X：对象]：(existsAt @X@dawn)))。

3. 多类别逻辑作为统一框架

3.1 翻译

目前，数学、计算机科学、哲学和语言学中使用的逻辑系统的激增使得它们之间的关系以及它们之间的可能翻译成为一个紧迫的问题。我们在上面看到，多类别逻辑是一种用于推理多种对象的自然逻辑。在本节中，我们将把它作为一个统一的框架来介绍，我们可以在其中放置我们可用的大多数逻辑。将详细描述翻译成 MSL 的总体计划。确定了三个可能的翻译级别，在每个级别上，如果成功达到，就会获得一个完整性结果：第一级抽象完整性，第三级强完整性。因此，当将逻辑翻译成多类别逻辑时，我们只需要一个唯一的演绎演算，即多类别演算，以及一个有效的定理证明器。在诸如基本命题模态逻辑的情况下，公式可以翻译成只有两个变量的一阶逻辑的可判定片段，翻译机制意味着模态逻辑的可判定性。此外，多类别逻辑的一些元属性可以转移到被翻译的逻辑中。

翻译可以更好地理解被翻译的逻辑，并且可以用来比较两种逻辑，当它们被转换成一个共同的目标逻辑的理论时，在我们的例子中是多类别的一阶逻辑。它不是对“唯一正确的逻辑？”（参见条目经典逻辑）这个问题的肯定回答，因为这个问题没有被提出，也不符合这种翻译成多类别逻辑的精神。在《开放思想的模态逻辑》（van Benthem 2010）中，对一阶逻辑的翻译进行了广泛的讨论，其中有一节题为“讨论：翻译有什么好处”（2010：77），其中 Johan van Benthem 分析了表达能力和复杂性之间的平衡，并提倡采用串联方法来回答这个问题：翻译 ST 是否意味着我们可以忘记模态语言，只做一阶逻辑？

翻译

逻辑之间的翻译已被制定为一个雄心勃勃的范式，其工具将用于处理现有的多种逻辑。一些方法是面向证明的，另一些方法是面向模型的，最后还有一些是用纯粹抽象的超结构术语构思的。

从证明理论的角度来看，比较逻辑的风格将依赖于演绎演算。Dov Gabbay（1994 年和 1996 年）的“标记演绎系统”应运而生。

从模型理论的角度来看，人们可能会通过定义逻辑试图描述的结构之间的关系来比较逻辑，就像 Johan van Benthem (1983、1984a 和 2010) 的对应理论一样。

从超结构的角度来看，我们定义类别之间的态射。在逻辑的抽象方法中，我们强调了 José Meseguer (1989) 的“一般逻辑”以及 Narciso Martı́-Oliet 和 José Meseguer (1994) 的“重写逻辑”。Da Silva、D’Ottaviano 和 Sette (1999) 给出了逻辑之间翻译的一般定义，根据该定义，逻辑被描述为具有结果关系的集合；因此翻译是结果关系保留映射。

本条目中假设的逻辑翻译范式[11]属于第 2 项中提到的模型论传统，目标逻辑是多分类逻辑。

就内涵逻辑而言，让我们引用约翰·范·本特姆的话：

给定任何内涵逻辑，通常种类的完整可能世界语义可以看作是将该逻辑忠实地嵌入到某种适当增强的多分类谓词逻辑中（对可能世界进行量化），也许还提供了某种简单的辅助专用理论，用于“可访问性”、“逆转”等。谓词逻辑在这方面是否具有普遍性，因为每个有效公理化的内涵逻辑都可以以这种方式进行语义化？（1984b：995）