多类逻辑 many-sorted (María Manzano and Víctor Aranda)

首次发表于 2022 年 12 月 15 日星期四

古典逻辑是描述包含单个宇宙或论域的数学结构的适当形式语言。相比之下，多类逻辑（MSL）允许量化多个领域（称为类别）。因此，它是处理涉及不同类型对象的陈述的合适工具，这在数学、哲学、计算机科学和形式语义学中无处不在。每个类别将一组唯一的对象分类（例如，在 2 类结构中，点和直线是不同类型的对象）。

尽管增加了这种表达资源，多类逻辑“保持在”一阶逻辑内，因此可以证明主要的元定理（完备性、插值等）。多类逻辑还作为将各种逻辑系统转化为统一框架的工具；例如，一些内涵和高阶逻辑可以自然地转化为多类逻辑。多类一阶逻辑在语法和语义上都可以简化为一类一阶逻辑。多类一阶逻辑还可以扩展为称为“类别逻辑”的多类二阶逻辑。

郝尔·王在 1952 年引入了多类逻辑的公理演算法，他在王（1952）中对一类和多类理论进行了比较。1967 年，所罗门·费弗曼为多类逻辑提供了一个序列演算法，证明了其完备性以及割除和插值定理（费弗曼 1968）。费弗曼（2008）总结了多类插值定理在模型论中的一些应用。（有关更多信息，请参见早期历史的补充说明。）

第 1 节阐述了多类逻辑的基础知识，提供了一些例子，并解释了形式语言、结构和语义与经典逻辑的异同。第 2 节解释了如何修改一阶演算以获得多类版本；此外，还讨论了完备性，并提及了一些自动定理证明器。第 3 节描述了一个计划，其中多类逻辑作为一个通用框架用于翻译各种逻辑系统。第 4 节和第 5 节分别将这个计划应用于二阶逻辑和非经典逻辑（模态逻辑和动态逻辑）。最后，第 6 节对多类逻辑的进一步结果进行评论。

1. 语法和语义

1.1 例子

我们从一些例子开始，以说明如何将关于不同类型数据的常见陈述形式化为多类一阶逻辑。

例子：欧几里得的第一原理

让我们从几何学开始，谈论直线和点。根据欧几里得的第一原理：

可以画出一条直线连接任意两点。

在多类的一阶逻辑中，可以使用 X、Y 等作为 l（直线）的变量，使用 x、y 等作为 p（点）的变量。为了表达欧几里得原理，我们写成：

∀x∀y(x≠y→∃X(Join(Xxy)∧∀Y(Join(Yxy)→X=Y)))

在这个例子中，Join 是一个三元谓词符号，它关联一条直线和两个点，

Join(Yxy):=Y 连接 x 和 y

从字面上看，我们的形式化表达是：“对于任意两点，存在一条唯一的直线连接它们”。

例子：二元关系

另一个数学例子是关于不对称性和反对称性的，它们都是一些二元关系的属性。假设我们想要表达这样的主张：

每个不对称的二元关系也是反对称的。

要将该陈述形式化为一个单一的逻辑上有效的句子，我们需要：（1）表达不对称性和反对称性，以及（2）对二元关系进行量化。在一个适当的一阶语言中，包括 R 作为二元关系符号，要表达 R 是不对称的，我们写成：

Asymm(R):=∀x∀y(Rxy→¬Ryx)

并且说 R 是反对称的，我们写作：

Anti-symm(R):=∀x∀y(Rxy∧Ryx→x=y)

在普通的一类排序的一阶逻辑中，这将是一个逻辑上有效的方案：

Asymm(R)→Anti-symm(R)

我们得到的是通过将 R 替换为任何其他二元关系符号而获得的无限集合的公式。然而，我们想要一个单一的逻辑上有效的句子，因此我们需要对二元关系进行量化。在二阶逻辑中，我们用 X2、Y2 等变量表示二元关系，我们写成：

∀X2(Asymm(X2)→Anti-symm(X2))

但是由于标准的二阶逻辑缺乏一阶逻辑的一些良好性质（第 4.1 节），可以选择使用两类的一阶逻辑，其中个体和个体之间的关系都是一等公民，可以对其进行量化。我们将有属于 i 类（个体）的变量 x，y，...，以及属于 r 类（个体之间的二元关系）的 X2，Y2，...。然而，仅仅将变量标记为个体或二元关系是不够的，我们需要它们像二阶变量一样运行。需要添加一个三元谓词符号来关联二元关系和个体，ϵ2xyX2，以使 Asymm(X2)变为：

Asymm(X2):=∀x∀y(ϵ2xyX2→¬ϵ2yxX2)

同样地，对于反对称性（X2）也是如此。

正如我们将在 4.2 节中看到的那样，将二阶逻辑公式 X2xy 重写为 ϵ2xyX2 是将二阶逻辑翻译为多类逻辑时所做的全部工作；添加了一些关于谓词 ϵn 的公理，并引入了适当的多类逻辑学理论来描述 ϵn 关系。在多类逻辑中的公式

∀X2（Asymm（X2）→Anti-symm（X2））

是多类理论中提到的一个定理。

例子：理解公理

让我们引入另一个更加哲学的例子。如果我们想要形式化：

每个属性都有一个否定。

我们可以使用二阶逻辑并写成：

∀X∃Y∀x(Yx↔¬Xx)

当我们将其重写为多类公式时，它变成了：

∀X∃Y∀x(ϵ1xY↔¬ϵ1xX)

使用 x，y，...作为 i（个体）的变量和 X，Y，...作为 π（属性）的变量。

公式 ∀X∃Y∀x(Yx↔¬Xx) 是对包含方案的一个实例的概括

∃Yn∀x1…∀xn(Ynx1…xn↔φ)

（变量 Yn 在 φ 中不是自由的）。第 4 节和第 5 节讨论了这个方案在从二阶逻辑到多类一阶逻辑的翻译中所起的作用。

正如您将在第 6.1 节中看到的那样，每个多类公式都有一个在一个一类一阶语言中的版本，该版本通过删除类别而获得。在这种新语言中，所有变量都属于一个类别，但是当从多类表达式转换为一类表达式时，我们添加一元谓词以恢复丢失的信息。我们还需要确保这些新谓词，它们代表量化的丢失宇宙，由非空集合进行解释，因为在经典逻辑中，量化的宇宙是非空的。

在欧几里得的例子中，我们添加了公理 ∃xLx 和 ∃xPx 以及公式

∀x∀y(x≠y→∃X(Join(Xxy)∧∀Y(Join(Yxy)→X=Y)))

现在变成

∀x∀y(Px∧Py∧x≠y→∃z((Lz∧Join(zxy))∧∀w((Lw∧Join(wxy))→z=w)))

为了表示在单一排序的一阶逻辑中，每个属性都有一个否定，我们使用 x、y、z 等变量来表示我们现在拥有的唯一排序，并写成：

∀x(Px→∃y(Py∧∀z(Oz→(ϵ1zx↔¬ϵ1zy))))

其中

Px:= 断言 x 是一个属性 Ox:= 断言 x 是一个对象 ϵ1zx:= 断言 z 属于（举例或实例化）x

添加了一些关于谓词 ϵ1 的公理，以及谓词 P 和 O 永远不被解释为空集的公理，即 ∃xOx 和 ∃xPx。此外，谓词 ϵ1、P 和 O 之间的联系由以下公式表示：

∀x∀y(ϵ1xy→Ox∧Py)∀x(Px→¬Ox)

1.2 基本思想

要指定多类语言和相关结构的语法，首先需要说明我们的（可数的）多类集合是什么。我们将 Sort={s1,…,sn}作为 n 类语言的类别。[1]

结构：多类结构具有多个非空域，每个类别都有一个，给定类别的变量取值于相应的域。n 元关系可以自由地在不同域的元素之间建立，也可以只在某些元素之间建立。这两种选择分别称为自由和严格。自由关系可以关联任意域的对象，只需说明关系的元数（自然数）。对于严格关系，还必须指定所涉及的类别以及元数。
字母表：多类语言 L 的字母表包括一个称为 OperSym 的集合中的所有关系、函数和常量符号，以及每个类别 si∈Sort 的无限个变量，相应的变量集是不相交的。n 元关系符号 R 可以是严格的或自由的，在第一种情况下，我们必须提供有关所涉及类别的信息。为了满足这个要求，我们定义了一个函数 Rank，其定义域是 OperSym 集合，其值要么是非零的自然数（自由选项），要么是 Sort∪{0}的有限字符串（严格选项）。对于任何严格的 f∈OperSym，其值 Rank(f)总是具有形式 ⟨i1,…,im,i0⟩，其中 i0,i1,…,im∈Sort∪{0}。当 f 是 m 元谓词时，i0=0，当 f 是 m 元函数符号时，i0≠0；个体常量被视为元数为零的函数符号，其 Rank(f)=⟨i0⟩，简化为 i0。
签名：通过签名 Σ，我们指的是有序三元组 Σ=⟨Sort,OperSym,Rank⟩ 相等性是一个二元符号，可以是严格的或自由的。在我们的语言中，等号符号 ≈，其 Rank(≈)=2 是自由的（具有二元性并允许在任何类别的术语之间工作）。[2] 量词 ∃xi 用于任何类别 i 的变量 xi。

在欧几里得的例子中，我们有两种类别，即线（l）和点（p），以及一个三元谓词 Join，其 Rank(Join)=⟨l,p,p,0⟩。在二元关系的例子中，我们有两种类别，即个体（i）和二元关系（r），以及一个三元谓词符号 ϵ2，其 Rank(ϵ2)=⟨i,i,r,0⟩。对于理解的例子，我们有两种类别，即个体（i）和属性（π），以及一个二元谓词符号 ϵ1，其 Rank(ϵ1)=⟨i,π,0⟩。

1.3 形式语言

术语和公式

正如我们在经典的一阶逻辑中所做的那样，从字母表的有限元素字符串集合中选择 L 的表达式：术语和公式。唯一的区别是，在多类逻辑中，术语具有类别，我们必须指定它。

因此，多类逻辑的术语如下递归定义：每个类别为 si 的变量或个体常量都是相同类别 si 的术语。如果 f∈OperSym 满足 Rank(f)=⟨i1,…,im,i0⟩，其中 i0≠0，τ1,…,τm 是类别为 i1,…,im 的术语，则 f τ1…τm 是类别为 i0 的术语。

原子公式通过谓词和术语来定义：如果 R∈OperSym 满足 Rank(R)=⟨i1,…,im,0⟩，τ1,…,τm 是类别为 i1,…,im 的术语，则 Rτ1…τm 是一个公式（当 R 是自由谓词时，我们省略术语的类别要求）。对于任意的术语 τ1 和 τ2，表达式 τ1≈τ2 是一个公式。请注意，τ1 和 τ2 的类别并不重要，因为我们选择的等号符号是自由的。[3]

复杂的良构公式（wffs）通常在一阶语言中定义（参见经典逻辑的条目），除了量化表达式。新规则如下：如果 φ 是一个公式，xi 是一个多类变量，那么 ∃xiφ 也是一个公式。

自由变量和约束变量

与经典一阶逻辑一样，公式中的变量出现可以是自由的或约束的；当变量在量词的范围下时，它们是约束的，否则是自由的。如果一个公式中至少有一个自由出现的变量，那么该变量在该公式中是自由的。没有自由变量的公式称为句子。我们用 Sent(L)表示语言 L 的句子集合。

例子：《完美空无之书》

考虑以下来自《列子》（第 5 卷，1-2 章）的内容：

《完美空无之书》：唐英问葛：“时间的黎明时刻，事物存在吗？”

夏格回答道：“如果事物在时间的黎明时期不存在，它们如何可能存在于今天？同样地，未来的人们可能会相信今天事物不存在。”

为了分析这个例子，我们应该确定前提和结论；我们很容易观察到，最初的修辞问题实际上是这个论证的结论。考虑到的论证是一个省略论，因为它似乎是在支持统治宇宙的法则的持久性（特别是关于物体存在的法则）。支持这个论证的隐藏假设可能是以下法则：

如果事物在某个时间点存在，那么在任何给定的先前时间点，事物必定存在。

这个规则并不是说一个特定对象的存在是永恒的，而是说存在的链条是永远回溯的。

因此，这个论证可以用以下方式重新表述，其中 α、β 和 γ 是前提，δ 是结论：

α:= 如果事物在某个时间点存在，那么在任何给定的之前的时间点，事物必定存在。
β:= 今天存在着的事物。
γ:= 时间的黎明先于一切。
δ:= 时间的黎明时存在着的事物。

现在，前提和结论可以通过一个双类语言（Sort={i,τ}）进行形式化，其中包括对象（类别 i）和时间瞬间（类别 τ）。OperSym 集合包含给定时间存在的二元谓词 E，时间瞬间之间的二元谓词 P，以及代表今天（t）和时间黎明（d）的两个个体常量。因此，在这种情况下，

Rank(E)=⟨i,τ,0⟩，Rank(P)=⟨τ,τ,0⟩，且 Rank(d)=τ=Rank(t)。

现在，论证可以表述为：

α:=∀xτ(∃yiEyixτ→∀zτ(Pzτxτ→∃viEvizτ))β:=∃yiEyitγ:=∀yτ Pdyτδ:=∃xiExid

在多类逻辑学中，通过使用演绎演算（见第 2 节），可以很容易地从这些假设中得出结论。因此，一旦我们接受了有问题的假设 α，这个论证在形式上是正确的。在第 2.4 节中，我们重新编写了使用定理证明器 LEO-II 和 LEO-III 的论证。

1.4 多类结构

多类逻辑的语义与经典的一阶逻辑非常相似，因为它遵循塔斯基的真理定义来引入结构中的真理概念（参见塔斯基 1933 年和塔斯基和沃特 1956 年；有关历史澄清，请参见霍奇斯 1986 年和塔斯基真理定义条目）。在我们的情况下，客体语言是多类逻辑，元语言是集合论。集合论是常用的元语言，其中关系符号被解释为在数学结构的宇宙（集合）上定义的关系。

在多类一阶逻辑中，结构被理解为一个元组，其中包含一族非空集合作为域，以及在这些域上定义的一族操作（函数和关系）。这些关系和函数根据给定的签名进行定义。

多类结构的示例

《完美空无之书》中的示例需要一个适当的结构 E，它包括两个宇宙：时间瞬间 Aτ 和对象 Ai。它还有两个特殊的瞬间，即今天和时间的黎明，对象和瞬间之间的二元关系，以及二元的时间先后关系。 E=⟨⟨Ai,Aτ⟩,EE,PE,tE,dE⟩ 在这样的结构中，tE,dE∈Ai，EE⊆Ai×Aτ，PE⊆Aτ×Aτ。
第二阶标准结构（或完整结构） A=⟨A,⟨℘(An)⟩n∈N,⟨fA⟩f∈OperSym⟩ 是多类结构的另一个例子。该结构包括个体域 A 以及每个自然数 n 上的 n 元关系的二阶域的家族 ℘(An)。⟨fA⟩f∈OperSym 中的关系和函数是在个体的宇宙上定义的一阶关系和函数（有关二阶逻辑的更多细节，请参见二阶和高阶逻辑的条目）。
一个二阶一般结构 A=⟨A,⟨An⟩n∈N,…⟩ 也可以被视为多类的。与标准结构一样，A 包含了个体域 A 以及每个自然数 n 的 n 元关系域 An⊆℘(An)。但由于 A 是一个一般结构，宇宙 An 并不是任意选择的，因为它们必须满足理解模式。因此，宇宙在可定义性下是封闭的（关于一般结构的更多信息请参见第 4.1 节）。

多类结构

一个多类 Σ-结构 A 具有多个对象宇宙（或域），它们是非空集合 Ai 的一个家族（对于每个 i∈Sort）。结构 A 还包含：对于每个关系符号 R，一个 m 元关系 RA；对于每个 n 元函数符号 f，一个 n 元函数 fA；对于每个个体常量 c，一个可区分元素 cA∈Ai。这些关系和函数必须在考虑它们在函数 Rank 下的值的情况下在域家族的元素之间建立起来。[4]

使用在 1.5 节中定义的结构 A，我们定义了在该结构中句子 φ 的真值，表示为 A⊨φ。

我们可以添加不同域之间的空交集的要求。遵守此要求的结构称为“严格”的，否则称为“宽松”的（或“自由”的）。对于严格的结构，我们可以考虑为每个类别添加一个相等符号 ≈i，其中每个符号的等级为 Rank(≈i)=⟨i,i,0⟩。我们要求相等符号（无论是严格的还是宽松的）被解释为真实的同一性，即在一个对象和自身之间成立，而在任何其他两个对象之间不成立。

结构之间的相似关系

对于单类结构，研究它们之间的不同关系是非常常见的：同态、嵌入、同构、子结构和扩展（参见 Manzano 1989 [1999: 19–33]）。可以以类似的方式为多类结构定义这些关系。具有相同标记的两个结构 A 和 A'之间的同态是一个函数 π，它将 A 的宇宙的并集映射到 A'的宇宙的并集，并满足以下条件：首先，π 对于每个 i∈Sort 的限制必须是从 Ai 到 A'i 的函数。其次，如果元素 n 元组 ⟨ai,...,an⟩ 在 n 元关系 RA 中，则元组 ⟨π(ai),...,π(an)⟩ 在关系 RA'中。最后，

π(fA(ai,...,am))=fA'(π(ai),...,π(am))

和 π(cAi)=cA'i.

嵌入是一个同态映射，其中涉及的函数是单射，并且第二个条件在两个方向上都成立。同构是一个嵌入，其中定义的映射是双射。当函数 π 是一个同构时，我们说 A 和 A'是同构的，并写作 A≅A'。

如果且仅如果包含映射 i（将每个元素映射到自身）是从 A'到 A 的嵌入，我们说 A'是 A 的子结构（或者 A 是 A'的扩展）。

所有已经提到的关系都是在具有相同签名的结构之间建立的。我们也可以定义在签名不同的结构之间的缩减和扩展。给定一个多类结构 A，通过从 A 的签名中简单地删除一些类别、函数或关系符号，可以得到 A 的一个缩减 A'。如果 A'是 A 的缩减，则我们说 A 是 A'的扩展。

1.5 语义学

术语的指称和公式的满足

给定一个语言和一个结构，它们共享相同的签名，语言的每个封闭术语将指称结构中的一个元素，每个原子句在结构中要么为真要么为假。然而，我们的定义范围扩大，以便每个术语都能接收一个指称，每个公式都有一个真值。为了实现这一点，我们从变量集合到结构的域中定义了赋值 [5]，参数和值应该是相同的类别。对于任意个体 x∈Ai 和类别 i 的变量 xi，我们使用 s(x/xi)来表示赋值，它类似于赋值 s，只是 xi 处的值必须是 x。

要定义“结构 A 中句子 φ 的真值”（A⊨φ）的重要概念，我们需要先定义在赋值 s 下公式 φ 在 A 中的满足概念（记作 A,s⊨φ），以及术语的指称。

术语的指称

设 A 为一个 L-结构（语言和结构共享签名 Σ），s 为一个赋值。I=⟨A,s⟩ 被称为一个解释。在解释 I 下，术语 τ 的指称 I(τ)的递归定义按照通常的方式进行，就像在经典的一类排序一阶逻辑中一样。对于原子和复合术语：I(xi)=s(xi)，I(c)=cA，以及

I(f τ1…τn)=fA(I(τ1)…I(τn)).

很容易检查某种排序的术语表示该排序的个体。

定义（塔斯基的真理）。该定义与经典的一阶逻辑几乎相同，请参见经典逻辑的条目。

对于原子公式：当且仅当 A，s ⊨ Rτ1...τn 时，

⟨I(τ1),…,I(τn)⟩ ∈ RA，

并且当且仅当两个术语在结构 A 中表示相同的对象时，A，s ⊨ τ1≈τ2；即，I(τ1)=I(τ2)。

在多类逻辑中，连接词是标准的，因此我们使用基于它们构建的公式的经典满足定义。对于诸如 ∃xiφ 的量化公式，定义如下：当且仅当存在一个 x∈Ai 使得 A,s(x/xi)⊨φ 时，A,s⊨∃xiφ。

巧合引理

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

对于一个公式 φ(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'之间的元嵌入 π 是满足以下条件的嵌入：

当且仅当 A'⊨φ [π(x1),…π(xn)] 时，A⊨φ [x1,…,xn]

对于所有 Σ-公式 φ(x1,…,xn)和结构的域中的元素 x1,…,xn，变量和具有相同排序的元素。

如果且仅如果它们的理论相同，即 Th(A)=Th(B)，则两个结构 A 和 B 在元素上是等价的。

可满足性、有效性和推论

可满足性、有效性和推论的概念与经典的一阶逻辑中的定义相同。给定语言 L 的签名 Σ 和公式 φ 的 L：如果存在一个 Σ-结构 A 和其上的赋值 s 使得 A,s⊨φ 成立，则 φ 是可满足的；如果对于所有的 Σ-结构 A 和任意的 A 上的赋值 s，都有 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）的多类扩展。早期从事多类逻辑研究的先驱逻辑学家之一 Hao Wang（1952: 106）已经在他的开创性工作中引入了这种逻辑的公理演算（有关早期历史的补充信息，请参见附录）。

如常，为了表示从一组公式中推导出一个公式，我们写作 Δ⊢φ。当需要时，我们将推导符号 ⊢ 写作下标，即 ⊢MSL。在这些演算中的任何一个中，证明的概念都是有效的，因为只要给出了一系列有限的公式序列，就可以有效地确定它是否是一个证明。这些演算中的任何一个都是不可判定的，因为没有算法可以检查 ⊢φ 是否成立。实际上，这是不可避免的，因为对于多类逻辑的可满足性问题（即确定给定公式的有效性或等价地测试其可满足性）是不可判定的。因此，我们面临着与单类一阶逻辑相同的情况。

当然，如果一个演算法要有帮助，它绝不能允许错误的推理：它不会把我们从真实的假设推导到错误的结论。它必须是一个可靠的演算法。此外，我们非常希望从一组假设 Γ 中能够推导出 Γ 的所有后果。也就是说，我们希望有一个强完备的演算法。在我们的第 2.3 节中，您将找到这种完备性证明的概述。

最大一致性和具有见证者属性

另外，语法概念的定义也是标准的；[7] 即一致性、最大一致性和具有见证者属性的定义。在目前的情况下，一个公式集包含见证者，如果每个存在量词公式都有一个见证者 (∃xiφ∈Δ 意味着 φ(t/xi)∈Δ，其中 t 是第 i 类的一个项)。这三个属性都是公式和/或公式集的属性，在它们的定义中我们使用了可导性；即演绎逻辑学。

一致性可以被看作是满足性的句法对应物，就像 ⊢ 和 ⊨ 相互对应一样。事实上，亨金的完备性证明基本上是通过构造每个一致集的模型来完成的。

2.2 完备性概念

证明和真理是通过独立的方法定义的，证明它们在外延上是相同的并不是微不足道的，而是必要的。当这个性质被谓词化为一个完备的演算时，这就是完备性定理的内容。当它被谓词化为一个理论时，完备性还有另一种意义：对于每个句子，要么 φ 成立，要么 ¬φ 是 Γ 的推论（Manzano 1989 [1999: 118]）。演算的强完备性确立了它捕捉逻辑推论的充分性；也就是说，每当一个句子从一组假设中逻辑地推出时，就有一个在演算中证明这个句子的证明，可能使用其中一些假设。相反，弱完备性意味着我们对所有有效性都有证明。在一个完备的 [8] 逻辑中，语言的表达能力和计算能力是平衡的。因此，完备性的问题就是关于逻辑的基本组成部分之间的平衡的问题：它的语义和逻辑演算。

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

第 3 节将多类逻辑作为统一逻辑，并描述了嵌入到 MSL 中的三个层次的过程，作为研究逻辑完备性的路径：第一层的抽象完备性，第三层的强完备性。

2.3 多类逻辑的完备性

多类演算的完备性证明可以通过遵循著名的 Henkin（1949）策略来完成一阶逻辑。重要的问题是能够展示每个一致的公式集都有一个模型，因此句法一致性和语义可满足性是等价的（假设完备性）。证明基本上分为两个步骤：

每个一致的公式集都可以扩展为具有见证者的最大一致公式集。
一旦我们有了具有见证者的最大一致公式集，我们将其用作构建由该集合中的公式描述的精确模型的指南。原因是最大一致公式集是对结构的非常详细的描述。

通过这样做，我们证明：

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

完备性定理

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

容易从中得出。

要看到亨金定理意味着强完备性，让我们假设前提，Γ⊨φ。因此，Γ∪{¬φ}不可满足，它没有模型。使用亨金定理，我们得出结论，Γ∪{¬φ}是矛盾的，因此 Γ∪{¬φ}⊢φ。演算规则允许我们摆脱 ¬φ 并推断出 Γ⊢φ。

作为前面结果的推论，我们得到以下结论：

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

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

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，...，in，并应用类似的构造。这些基本类型 i1，i2，i3，...，in 可以被视为多类。

我们从《完美空无之书》中的例子可以通过 LEO-II 和 LEO-III 证明器进行形式化和检查。

thf(sortForObjects, type, (object: ��)).�ℎ�(��,��,(��:tType)). thf(constantDawn, type, (dawn: time)). thf(constantToday, type, (today: time)). thf(constantIsExistsAt, type, (existsAt: object>time>�)).�ℎ�(��,��,(��:��>��>o)). thf(axiom1, axiom, (! [X:time]: ((?[Y:object]: (existsAt @Y@X)) => (! [Z:time]: ((precedesTo @Z@X) => (?[V:object]: (existsAt @V@Z))))))). thf(axiom2, axiom, (?[Y:object]: (existsAt @Y@today))). thf(axiom3, 公理, (! [Y:time]: (precedesTo @dawn@Y))). thf(conjecture1, 猜想, (?[X:object]: (existsAt @X@dawn))).

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

3.1 解释

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

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

翻译

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

从证明论的角度来看，比较逻辑的风格将依赖于演绎演算。Dov Gabbay（1994 年和 1996 年）的“标记演绎系统”出现。
从模型论的角度来看，人们可能会通过定义逻辑试图描述的结构之间的关系来比较逻辑，就像 Johan van Benthem（1983 年，1984 年和 2010 年）的对应理论一样。
从超结构的角度来看，我们定义范畴之间的态射。在逻辑的抽象方法中，我们强调 José Meseguer（1989 年）的“一般逻辑”以及 Narciso Martı́-Oliet 和 José Meseguer（1994 年）的“重写逻辑”。Da Silva，D’Ottaviano 和 Sette（1999 年）根据一种通用的翻译定义，将逻辑之间的翻译特征化为具有推理关系的集合；因此，翻译是保持推理关系的映射。

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

就意向逻辑而言，让我们引用 Johan van Benthem 的话：

对于任何意向逻辑，通常情况下的完备可能世界语义可以被视为将该逻辑忠实地嵌入到某种适当增强的多类谓词逻辑（带有对可能世界的量化）中，也许还配备了一些简单的辅助专用理论，用于“可及性”、“逆转”等等。谓词逻辑在这方面是普遍的吗？也就是说，每个有效公理化的意向逻辑都可以以这种方式进行语义化吗？（1984b: 995）

3.2 基本模态语言的对应语言

在所谓的“非经典逻辑”中，模态逻辑作为第一位，其历史可以追溯到亚里士多德、梅加拉人、斯多亚派和其他希腊哲学家。多年来，它被用来讨论必要性和可能性、时间和计算机程序。请参阅有关模态逻辑的条目，以及 Blackburn 和 van Benthem（2007）和 van Benthem（2010）。

对于本篇关于多类逻辑的条目，模态逻辑最相关的特征是真值可以被限定（或相对化），而模态模型包括所谓的“可能世界”的一个宇宙。在模型中，传统的语义真值概念 A⊨φ 现在被写作在一个世界 w 中的真值 A,w⊨φ。

基本命题模态语言中的公式由原子、经典联结词和模态运算符 □（方框）和 ◊（菱形）构建。模态公式在 Kripke 结构中进行解释。

A=⟨W,R,⟨PA⟩P∈Atom⟩

具有非空状态或世界域 W，定义在其上的二元可达关系 R，以及每个原子命题符号 P 的 W 的子集的集合。在模型 A 中，模态公式 φ 在世界 w 处为真（φ 在 A 中的满足条件为真），当满足以下归纳条件时：

A,w⊨P 当且仅当 w∈P A,w⊭⊥ 对于所有的 w A,w⊨¬φ 当且仅当不是 A,w⊨φ A,w⊨φ∧ψ 当且仅当 A,w⊨φ 并且 A,w⊨ψ A,w⊨□φ 当且仅当对于所有的 v 满足 ⟨w,v⟩∈R:A,v⊨φ

在模型 A 中，如果公式 φ 在所有的世界中都被满足，则称其为全局真 (A⊨φ)。如果公式 φ 在所有模型中都是全局真，则称其为有效 (⊨φ)。在整个 Kripke 模型类中的有效性集合（当没有对可达性关系施加任何限制时）是基本模态逻辑的有效性，也称为最小模态逻辑或 System K。[12]

Blackburn 和 van Benthem (2007: 5) 注意到

模态满足定义的内在特性：模态公式从内部讨论 Kripke 模型

由于模态公式在特定点进行评估。直觉是模态运算符 □ 是一种普遍量词，而模态结构是具有二元关系和一组子集的一阶关系结构。在一阶语言中，要讨论这些结构，需要一个二元关系符号 S，以及一组一元关系符号。这种语言被称为一阶对应语言，因为每个基本模态公式对应一个一阶公式。模态公式 φ 的标准翻译是一个带有一个自由变量的一阶公式，表达模态公式的语义：

STx(P):=PxSTx(⊥):=x≠xSTx(¬φ):=¬STx(φ)STx(φ∧ψ):=STx(φ)∧STx(ψ)STx(□φ):=∀y(Sxy→[y/x] STy(φ)), 其中 y 是一个新变量。

这个定义背后的思想是用对应语言表达模态公式的语义解释：两种语言都在谈论相同的结构，因为 Kripke 结构可以被视为一个简单的一阶关系结构。从这个定义中得到以下等价性：

切换引理：A,w⊨φ 当且仅当 A ⊨STx(φ)[x:=w]

（赋值将变量 x 映射到世界 w）

从这个引理中，可以推导出基本模态逻辑（Blackburn＆van Benthem 2007：11）的紧致性、Löwenheim-Skolem 和可枚举性定理，只需使用一阶逻辑的相应属性。

基本模态逻辑的有效性集不仅是可递归可枚举的（正如可枚举性定理所证明的），而且可满足性问题也是可判定的。我们想知道，将一个可判定的逻辑翻译成一个不可判定的逻辑有什么好处？我们是否失去了可判定性？答案是我们并没有失去可判定性；实际上，可以使用翻译来证明基本模态逻辑的可判定性。

关于将基本模态逻辑翻译成一阶对应语言，至少有两个值得强调的结果：

第一个相关结果是基本命题模态逻辑可以被翻译成一阶逻辑的两个变量片段 [13]（只使用两个变量的一阶逻辑公式），而两个变量片段的可满足性问题是可判定的。
第二个相关结果是模态特征定理 [14]，它建立了对于任何具有自由变量的一阶公式，等价于模态公式并且在双模拟下不变的关系（参见 van Benthem 2010: 26–27 进行定义）。双模拟是一个有用的结果，因为它可以通过双模拟构造使模型 A 尽可能小，也可以使模型变得更大。

然而，这些结果适用于基本模态逻辑；在该逻辑中，我们谈论的是可满足性，意思是“在某个模型上可满足”，对可达性关系没有施加任何限制（如传递性）。对于除了 K 系统以外的任何模态逻辑，我们都在寻找具有附加属性的模型。的确，当相关属性可以用只有两个变量的一阶公式来表示时，类似的方法可以应用于其他命题系统。然而，传递性是一个明显的反例。

在第 5.2 节中，处理了各种模态系统（包括 S4，其可达关系是自反和传递的），并使用 MSL 储备库为它们证明了几个元定理。翻译被定义为具有第二阶风味的多类一阶逻辑，因为该节中使用的多类结构包含在被翻译的模态逻辑中可定义的相关数学集合（和关系）的类别。

在接下来的几节中，我们将以多类逻辑的形式进行翻译，作为完备性的三个阶段的路径。[15]

3.3 总体计划

总体计划如下：正在研究的逻辑（称之为 XL）的签名被转换为多类签名，逻辑 XL 的表达式被翻译为适用于 XL 的多类语言（MSLXL），逻辑 XL 的结构被转换为多类结构。因此，我们需要定义一个递归函数 Trans 来进行翻译，以及一个直接转换结构 Conv1。

通过直接转换结构，我们希望获得原始结构 XL 中的有效性等价性的结果，简称为 Str(XL)，以及在转换结构类 S∗（其中 S∗=Conv1(Str(XL))）中的某类多类公式（翻译）的有效性。

下一个要问的问题是 S∗ 是否可以被一组多类公式 Δ 的模型所替代。因此，定义 Trans 和 Conv1 的关键是简化语义等价性的证明，而在这方面，所获得结果的相关性强烈依赖于公理化 S∗ 的可能性。如果你得到了一个递归的多类公式集 Δ（或者至少使得 S∗⊆Mod(Δ)），我们应该证明在 MSLXL 中，XL 中的有效性等价于从 Δ 中推出的结果。

如果您获得了集合 Δ，则应定义结构的反向转换 Conv2。因此，从 Δ 的多类模型中，我们得到了 Str(XL)中的结构。我们定义它的目标是证明从多类结构 B（Δ 的一个模型）开始，如果且仅当其翻译的全称闭包在 B 中为真时，XL 的公式 φ 在 Conv2(B)中为真。

3.4 第一层：表示定理

正在研究的逻辑是 XL，我们定义了一个递归函数 Trans 来进行到 MSLXL 的翻译，以及结构的直接转换 Conv1。我们的第一个目标是陈述并证明以下内容：

定理 1：对于 XL 逻辑的每个句子 φ，

在 XL 中 ⊨Str(XL)φ 当且仅当在多类逻辑中 ⊨S∗∀Trans(φ)，

其中 ∀Trans(φ)是 Trans(φ)的全称闭包，而 S∗=Conv1Str(XL)。

我们想知道，在结构类别 S∗ 中，是否可以用多类公式集合 Δ 中的推论来替代有效性？下一个目标是找到这样的 Δ，至少找到一个满足 S∗⊆Mod(Δ)的集合。为了完成第一层次，需要证明一个表示定理；即，以下形式的陈述：

表示定理：存在一个递归的多类句子集合 Δ，满足 S∗⊆Mod(Δ)，并且

在 XL 中，⊨Str(XL)φ 当且仅当在 MSL 中，Δ⊨Str(MSLXL)∀Trans(φ)。

对于逻辑学 XL 的每个句子 φ。

从表示定理可以得出逻辑学 XL 的可枚举性。换句话说，XL 的有效性集是递归可枚举的。因此，从抽象意义上说，XL 是完备的。

备注：因此，我们得知对于 XL 来说，一个演算是一个自然的需求，但我们也得知在多类逻辑学中，我们可以模拟这样一个演算，然后我们可以使用一个定理证明器来处理多类逻辑学。

3.5 第二层次：主要定理

当受到审查的 XL 逻辑具有逻辑推论的概念时，我们可以尝试证明主要定理；即，在 XL 中的推论（Π⊨Str(XL)φ）等同于在 MSL 中的翻译推论，模除理论 Δ。为了证明主要定理，应使用结构的逆转换 Conv2。我们定义它的目标是证明以下内容：

引理 2：对于任意 φ∈Sent(XL)和 B∈Mod(Δ)

Conv2(B)⊨φ 当且仅当 B⊨∀Trans(φ)

其中 ∀Trans(φ)是 Trans(φ)的全称闭包。

从之前的结果中，我们得出了我们的主要定理：

主定理：存在一个递归集合 Δ⊆Sent(L∗)，其中 S∗⊆Mod(Δ)，使得

Π⊨Str(XL)φ 当且仅当 Trans(Π)∪Δ⊨Str(MXL∗)Trans(φ)

对于所有的 Π∪{φ}⊆Sent(XL)。

推论：紧致性和 Löwenheim-Skolem 定理适用于 XL。

备注：我们已经有了可枚举性。现在，从主定理以及 MSL 的紧致性和 Löwenheim-Skolem 定理，我们很容易得到 XL 的紧致性和 Löwenheim-Skolem 定理。因此，所研究的逻辑学可以具有强完备的演算法。您可以定义它或使用多类演算法。

3.6 第三层：演绎对应

当 XL 逻辑学也随附一个演绎演算时，我们可以尝试使用对应关系的机制来证明，如果可能的话，XL 的正确性和完备性。为了证明这些定理，需要证明 XL 演算与多类演算之间的演绎对应定理，模 Δ。因此，下一个目标是证明：

演绎对应定理：设 Δ 如主定理所定义，则：

如果且仅如果 Π⊢XLφ，则 Trans(Π)∪Δ⊢MSLTrans(φ)。

由于我们已经有了主定理（Main theorem）以及多类逻辑（MSL）的完备性和合理性，一旦我们得到了这个演绎对应定理（Theorem of deductive correspondence），下面的图像给出了 XL 的合理性和强完备性：

( *)(* )( )Trans(Π)∪Δ⊨Str(MSL)Trans(φ)⟺Π⊨Str(XL)φ⇕Trans(Π)∪Δ⊢MSLTrans(φ)⟺Π⊢XLφ

推论：XL 的合理性和强完备性

如果且仅如果 Π⊢XLφ，那么 Π⊨Str(XL)φ

备注：我们已经达到了完备性的终点，但重要的是强调我们正在使用已经证明的 MSL 的完备性结果来证明 XL 的强完备性。

4. 二阶逻辑作为多类逻辑

4.1 二阶逻辑

二阶逻辑（SOL）是一种非常表达力强的形式语言，与一阶逻辑（FOL，一类排序的一阶逻辑）在以下几个方面有所不同：（1）字母表，（2）标准和非标准语义，以及（3）标准语义下的压倒性表达能力。请参阅关于二阶和高阶逻辑的条目，以及关于丘奇类型理论的条目。

二阶逻辑的字母表是通过包括一阶一类排序变量并添加可以量化的关系变量来获得的。因此，除了公式 ∀xφ 表示“对于所有个体 φ 成立”，我们还有公式 ∀Xφ，∀X2φ 等表示“对于所有属性 φ 成立”，“对于所有二元关系 φ 成立”，等等。

从语义学的角度来看，为了赋予新变量以意义，我们需要新的宇宙，其元素是个体宇宙 A 上的集合和关系。在所谓的标准语义学中，集合变量的范围是个体宇宙的幂集，℘(A)，而 n 元关系变量的范围是个体宇宙的 n 元笛卡尔积的幂集，℘(An)。举个例子，用标准语义学的二阶逻辑的表达能力来表达算术归纳法。

∀X(Xc∧∀x(Xx→Xσx)→∀xXx)

而二阶皮亚诺算术（PA2）变得范畴化，也就是说，PA2 的任何两个模型都是同构的。然而，我们为了表达能力付出了很高的代价，我们牺牲了逻辑：紧致性失败，Löwenheim-Skolem 失败，完备性也失败（强和弱）。

当然，后者的结果是通过标准语义获得的。在 Henkin 1950 年的论文中，他宣布如果允许“更广泛的模型类别”（非标准模型），那么不完备性问题是可以解决的。因此，他引入了标准结构、一般结构和框架。这些结构的类别按照集合包含的顺序进行排序。

SS⊆GS⊆F

相应地，每个类别中的有效性集合遵循相反的顺序 [16]。

ValF⊆ValGS⊆ValSS

在框架的语义学中，集合和关系变量都被允许范围在标准宇宙的子集上。然而，仅凭这个条件并不能保证我们有足够的集合和关系来处理二阶能力。我们希望在宇宙中包括我们形式语言中的所有可定义的宇宙。这是对一般模型（Henkin 模型）提出的一个相当自然的要求，以获得完备性。

实际上，根据框架的语义学，有效性的集合与在一个二阶演算中可推导的句子的集合相一致，该演算只是通过添加新的量词规则来扩展一阶演算。这个多类演算是由 Henkin（1953）在一篇论文中单独提出的，他在其中引入了理解模式。

∃Xn∀x1…xn(Xnx1…xn↔φ)

作为摆脱 Church（1956）复杂替换规则的一种方式。很明显，如果你对第二阶结构的宇宙只有一个要求，那就是它们是标准宇宙的子集，那么它们不一定是包容性的模型。这就是为什么我们需要一般结构遵守额外的规则，宇宙必须在可定义性下封闭。对于一般结构，有效性的集合与在第二阶演算中可推导的句子集合相一致。因此，我们回到了在一阶逻辑中遇到的情况，你会恢复：紧致性、Löwenheim-Skolem 和完备性。

显然，具有一般语义的 SOL 比具有标准语义的 SOL 表达能力更弱。例如，∀X(Xx↔Xy)不再是个体之间真正等同的定义。因此，我们将其作为原始的，并要求等式 ≈ 被解释为等同性。对于更高的类型，我们有等同性公理。

∀XnYn(Xn≈Xn↔∀x1…xn(Xnx1…xn↔Xnx1…xn))

已添加。

这些结果的结论是什么？正如您所知，逻辑学就像一个天平：一边是表达能力，另一边是可计算能力。如果您想保留逻辑属性，就必须改变语义并失去一些表达能力，无法同时达到最大值，它们是“最优不可能”。可以通过引用林德斯特伦的结果（Lindström 1969）来以更技术的方式表达相同的观点，该结果在第 2.3 节中提到。

有关二阶逻辑的更多信息，请参阅有关二阶和高阶逻辑的条目，以及 Church 1956 和 Enderton 1972。强烈推荐 Henkin 1996 以及《Leon Henkin 的生活和工作》中的一些论文（参见 Manzano，Sain 和 Alonso 2014），特别是：“改变语义，机会主义还是勇气？”（Andréka，van Benthem，Bezhanishvili 和 Németi 2014），“关于完备性的 Henkin”（Manzano 2014b）和“4 月 19 日”（Manzano 2014a）。

4.2 公式的翻译和结构的转换

根据相应部分（§3.4 或 §3.5）中的说明，我们定义了从 SOL 到多类 SOL 的语法翻译，以及两种结构的转换，直接和反向转换。

首先，我们意识到二阶结构实际上是多类的，具有某些特殊性质：在大多数情况下，它们是我们所称的严格的，因为任意两个不同宇宙之间的交集为空，但它们都是相关的，因为它们是在个体宇宙上定义的。此外，在一般的结构中，宇宙服从某些规则，比如满足外延性和包容性的模型。

设 L 为一个具有操作符号集 OperSym 的二阶语言。如果我们将 SOL 中的表达式与多类逻辑中的表达式进行比较，我们会发现 Xnx1…xn 不是多类逻辑的公式，因为它只是一串变量。我们所做的是引入一个新的多类语言 MSLSOL，其中保留了 OperSym 中的所有符号，但签名现在扩展了新的成员关系符号 ϵn，其解释将成为一种成员关系。多类签名 ΣSOL 包括一个集合 Sorts，其元素是 SOL 结构中的类型；即，1 和 ⟨1,…,1n,0⟩，其中 n≥1。[17]

因此，从 SOL 到 MSLSOL 的语法翻译使得除了上述类型的原子公式之外，其他公式保持不变；即：

TransSOL(Xnx1…xn):=ϵnx1…xnXn

从 SOL 到 MSLSOL 的直接转换：让我们定义 Conv1 为一个函数，它接受任何结构 A∈Str(SOL)，并返回一个结构 A∗∈Str(MSLSOL)。这些结构基本上是相同的，唯一的区别是我们现在添加的成员关系。这个多类语言的成员关系符号 ϵn 被解释为真实的成员关系，

ϵA∗n={⟨x1,…,xn,Xn⟩∈An×An:⟨x1,…,xn⟩∈Xn}

（其中 A 是个体的宇宙，属于第 1 类，An 是 n 元关系的宇宙，属于 ⟨1,…,1n,0⟩ 类，An 是 A 的 n 元笛卡尔积）

以下结果很容易证明。

命题：对于每个 SOL 的句子 φ，都有：

⊨G.Sφ 在 SOL 中当且仅当 ⊨S∗TransSOL(φ)在多类逻辑学中

（其中 ⊨G.Sφ 表示在一般结构中的有效性，而 S∗=Conv1(Str(SOL))）

现在我们问，我们能否对 S∗ 进行公理化？答案是肯定的。我们想要使用的结构是多类逻辑学中具有不相交宇宙的外延性和包容性的 MSLSOL 模型。因此，让 Δ 为：

Ext(n):=∀XnYn(∀x1…xn(ϵnx1…xnXn↔ϵnx1…xnYn)→Xn≈Yn)∀Comph(n)φ:=∀∃Xn∀x1…xn(ϵnx1…xnXn↔φ)Disjn,m:=¬∃XnYmXn≈Ym(for n≠m)

从多类逻辑学到逻辑学的逆向转换：结构的逆向转换分为四个步骤。[18]

我们想要处理的结构是具有多类逻辑学的外延性和包含性的模型，其中包含了不相交的宇宙。因此，它们必须是 Δ 的模型。在这样的模型中，排序为 ⟨1,…,1,0⟩ 的宇宙不一定是 ℘(An1)的子集。然而，A1 和 A⟨1,…,1,0⟩ 之间通过 ϵAn 相关联，但这种关系不一定是“真正的”成员关系。
从一个多类结构 A，其签名为 ΣSOL 且是 Δ 的模型，我们转向另一个相同签名的多类结构 B，但是在这里，排序 ⟨1,…,1,0⟩ 的宇宙现在是 ℘(Bn1)的子集，而 ϵBn 是真正的成员关系。通过定义一个函数 H:Mod(Δ)→Conv1(Str(SOL))，我们得到了新的多类结构 B。该函数根据 ϵAn 中给出的信息来构建 B⟨1,…,1,0⟩，因此 B=H(A)。这个新结构基本上是一个具有真正成员关系的二阶结构。[19]

H:Mod(Δ)→Conv1(Str(SOL))

that follows the information given in ϵAn to build B⟨1,…,1,0⟩, thus B=H(A). The new structure is basically a general second order structure with the genuine membership relation.[19]

显然，新的结构 B 与原始的 A 同构，因此 A≊B。
从上述类型的多类结构 B∈Conv1(Str(SOL))，我们通过一个简单的构造变换定义了一个 SOL 结构；即，删除成员关系并将签名调整为二阶。这只是对 Conv1 中所做的变换的逆过程。

逆转换的最终结果就是 Conv−11(H(A))，因此我们相应地定义 Conv2。

定义：Conv2=Conv−11∘H。

有了所有这些定义，我们现在证明：

命题：对于每个多类结构 C∈Mod(Δ)，存在一个 SOL-结构 Conv2(C)∈Str(SOL)，使得

如果且仅如果 C 是 TransSOL(φ)的模型，那么 Conv2(C)是 φ 的模型。

对于所有的 SOL 句子。

4.3 关于 SOL 和 MSL 之间的语义定理

通过应用之前的结果，很容易证明以下语义定理：

表示定理：对于 SOL 的每个句子 φ：在 SOL 中 ⊨G.Sφ 当且仅当

Δ⊨ 多类逻辑学转换 SOL(φ)

在多类逻辑学中。

主要定理：如果且仅如果 Π⊨G.Sφ 在逻辑学中，那么

如果 TransSOL(Π)∪Δ⊨MSLTrans(φ)。

在多类逻辑学中。

如第 3.5 节所解释的，通过使用表示和主要定理，MSL 的一些重要元定理现在可以转移到 SOL。

定理：具有一般语义的 SOL 具有以下特性：可枚举性、紧致性和 Löwenheim-Skolem 性质。

备注：可枚举性和紧致性定理告诉我们，所研究的逻辑学可能具有一个强完备的演算法。实际上，我们可以使用多类理论 Δ 来推导多类演算法中的 SOL 定理。

然而，如果我们已经有了一个 SOL 的演算法，我们可以使用翻译的机制来证明其正确性和完备性。

4.4 SOL 的正确性和完备性

我们只需按照我们的总体计划中第三层（第 3.6 节）提出的策略来证明 SOL 演算的正确性和完备性。需要证明的是以下定理。

推理对应定理：在二阶演算中，Π⊢SOLφ 当且仅当

TransSOL(Π)∪Δ⊢ 多类 TransSOL(φ)

在多类演算中，MSL。

根据总体计划，从主定理、演绎对应以及 MSL 的完备性和声音性，我们得到了具有一般语义的 SOL 的完备性和声音性。

强完备性和声音性：对于所有的 Π∪{φ}⊆Sent(L2)，Π⊨G.Sφ 当且仅当 Π⊢SOLφ。

5. 用第二阶外观进行多类逻辑的翻译

5.1 总体计划

如前所述，在 Henkin 1953 年，通过从 Church 1956 年的演算中消除一些替换规则并引入包含模式，定义了第二阶逻辑的新演算。在本文中，Henkin 定义了两个演算 F∗ 和 F∗∗（基本上是演算 MSL 和 SOL）：第一个是通过为新的量词添加规则从一阶演算中获得的，而第二个是一个适当的第二阶演算。这两个演算在标准语义下都是不完备的。Henkin 提到我们可以通过框架语义获得 F∗ 演算的完备性结果。事实上，我们已经看到了 MSL 的完备性以及第二阶演算在一般语义下的完备性。

还有一个有趣的想法，在 1953 年的论文中明确提出，也非常有用。这个想法是：如果我们削弱理解力，我们就得到了 F∗ 和 F∗∗ 之间的一个演算。而且很容易找到这样定义的逻辑的语义。当然，这类结构位于 F 和 GS 之间。这个新的逻辑，称为 XL，也是完备的；主要原因是这类模型再次是可公理化的。

在接下来的内容中，这个想法在几个命题模态逻辑以及具有 Kripke 语义的命题动态逻辑中得到了应用（请参阅有关模态逻辑的条目以及有关命题动态逻辑的条目）。

标题中提到的二阶外观如下：在定义结构转换为 MSL 时，我们将添加包含在 PML（或 PDL）中可以谈论的所有数学对象类别的新宇宙；因此，我们添加了这些逻辑中定义的所有集合和关系以及它们各自的公式和程序。因此，我们在某种程度上转向了 SOL 结构。我们还可以在语言中添加成员关系符号，并将成员关系添加到结构中，就像我们在 SOL 转换为 MSL 时所做的那样；我们最终将得到 MSL，但灵感来自 SOL。

5.2 命题模态逻辑作为多类逻辑

我们首先要做的是建立一个包含以下内容的多类语言 MSLPML：对于每个原子命题 P∈Atom，有一元关系符号；用于表示可达关系的二元关系符号 S；成员关系符号和个体与集合的相等符号。 MSLPML 包含个体变量和集合变量。翻译是标准的（如第 3.2 节所述）：我们在目标逻辑 MSLPML 中表达正在翻译的公式的语义解释。[21] 特别地，

Trans(P)[u]:=PuTrans(□φ)[u]:=∀v(Suv→Trans(φ)[v])

我们将使用的多类结构是通过在模态结构中添加一个包含状态或世界集合的宇宙而获得的。给定一个 Kripke 结构

A=⟨W,R,⟨PA⟩P∈Atom⟩

我们说如果且仅如果 AG 是在 A 上构建的一般结构

AG=⟨W,W′,R,ϵA1,⟨PA⟩P∈Atom⟩

其中 Def⊆W′⊆℘(W)。集合 Def 和 W′包含了家族 ⟨PA⟩P∈Atom 中的所有成员，并且在几个操作下是封闭的。[22] 可以证明，在模态结构 A 中，模态公式 φ 为真的世界集合与其在建立在 A 上的一般结构 AG 中的翻译所定义的集合是相同的。

让我们用 G 来指代所有建立在上述定义的模态结构上的一般结构的类，即我们转换后的结构。不难证明，在 PML 中，φ 的有效性等价于在类 G 中对公式的翻译的全称闭包的有效性。

模态逻辑 K 的一级

要完成翻译方法的一级，我们需要对 G 进行公理化。这是可能的吗？对于最小逻辑 K（基本模态逻辑），答案是肯定的，因为我们可以定义一个带有包含公理的理论 ΔK

∀∃X∀u(ε1uX↔φ)

主要研究通过模态公式的翻译获得的多类公式 φ。由于我们希望出现第二阶外观，将外延性公理添加到 ΔK 中。结果，我们得到了最小模态逻辑 K 的表示定理：

在 PML 中 ⊨φ⟺ 在 MSL 中 ΔK⊨∀uTrans(φ)[u]

（在逻辑 K 中使用整个 Kripke 结构类，对可达性关系没有施加任何条件）

如在 3.4 节中所解释的，从前一个定理中，我们实现了模态逻辑 K 的可枚举性定理。实际上，我们已经知道更多，正如我们在 3.2 节中提到的，系统 K 中的有效性集是可判定的。

模态逻辑 S4 的第一层

如果我们希望对另一个模态逻辑（比如 S4）获得类似的结果，可以将集合 ΔK 扩展为包括公理 T 和 4 的多类抽象条件的集合 ΔS4（即公式 MS(T)和 MS(4)[23]）。实际上，我们可以证明一阶公理的自反性和传递性等价于这些多类翻译句子。

ΔK⊢ 多类(T)↔ 自反性 ΔK⊢ 多类(4)↔ 传递性

S4 的表示定理很容易得到

⊨Dφ 在 PML⟺ΔS4⊨∀uTrans(φ)[u] 在多类逻辑学中

(D 是自反和传递的 Kripke 模型的类)

当我们进一步证明主定理时，这些结果是相关的。[24] 从这个定理中，我们免费获得了 K 和 S4 的紧致性和 Löwenheim-Skolem 定理。

模态逻辑 K 和 S4 的第三层

如果我们想要通过使用 MSL 的完备性来证明 K 和 S4 的模态演算是完备的（参见模态逻辑条目），就必须证明模态逻辑与其多类对应物之间的演绎对应关系。证明从命题模态逻辑到多类逻辑的演绎对应关系是容易的。

Π⊢Kφ⇒Trans(Π)∪ΔK⊢Trans(φ)Π⊢S4φ⇒Trans(Π)∪ΔS4⊢Trans(φ)

因为系统 K 的模态公理的翻译是 MSL 逻辑的定理，而 T 和 4 的翻译是 ΔS4 的定理。要证明 MSL 和 PML 之间的反向演绎对应关系，可以使用规范模型 [25] BK（或 BS4）来构建一般结构 BKG（或 BS4G）。通过使用构建在规范模型上的一般结构，最终达到了目标。很容易证明，如果一个模态公式 φ 在这个结构的一个世界上为真，那么公式 φ 属于这个世界。

因此，

BKG⊨∀u(Trans(φ)[u])⇒⊢KφBS4G⊨∀u(Trans(φ)[u])⇒⊢S4φ

模态逻辑与其多类对应的演绎关系是通过实现 BKG⊨∀u(Trans(φ)[u])⇒⊢KφBS4G⊨∀u(Trans(φ)[u])⇒⊢S4φ 来实现的

Π⊢Kφ⟺Trans(Π)∪ΔK⊢Trans(φ)Π⊢S4φ⟺Trans(Π)∪ΔS4⊢Trans(φ)

以第 3.6 节中解释的策略为指导，实现了对所研究的模态逻辑的正确性和完备性。

命题动态逻辑作为多类逻辑

在命题动态逻辑（PDL）中可以应用类似的方法。PDL 是一种模态逻辑，最初设计用于讨论状态和计算机程序，它具有一个完备的演算，其公理包括模态逻辑 K 中的通常公理以及描述程序组合的其他公理（参见命题动态逻辑条目）。其中，值得强调的是公理 5。这个公理也被称为“归纳公理”，它是 PDL 的一个特征，即其不紧凑性。因此，PDL 的演算在弱意义上是完备和正确的。

公式和程序转换为多类逻辑的预期结果：[26] 我们在目标逻辑 MSLPDL 中表达被翻译的公式和程序的语义解释。

对于结构的转换，我们采用类似于 PML 中使用的过程：我们将 Kripke 模型 A 扩展为建立在 A 上的一般结构 AE。

AE=⟨W,W′,W′′,R,ϵA1,ϵA2,⟨PA⟩P∈Atom⟩

新颖之处在于现在我们有另一个域 W′′，其中包括程序定义的二元关系。使用这些结构，可以证明动态公式的有效性等价于其在以这种方式获得的所有多类结构的类 E 中的翻译的普遍闭包的有效性。一旦我们定义了理论 ΔPDL，表示定理也是可用的。该理论包括作为公理的 PDL 公理的多类抽象条件，集合和关系的外延性以及由公式和程序的翻译定义的集合和关系的包含公理。

在过程结束时，不仅可以证明 PDL 中的有效性与从 ΔPDL 中的翻译的普遍闭包的推论的语义等价性，而且动态演算还证明了所有其翻译是我们理论 ΔPDL 的定理的公式作为定理。

⊨φ⟺ΔPDL⊨∀uTrans(φ)[u] ⊢PDLφ⟺ΔPDL⊢MSL∀uTrans(φ)[u]

弱完备性直接得出。[ 27]

6. 进一步的结果

6.1 将多类逻辑归约为一类逻辑

按照常见做法（Wang 1952，Feferman 1968 和 Enderton 1972），多类逻辑被认为可以轻松转换为一阶逻辑。在 Hao Wang（1952）中，这种等价性是建立在可证明性的基础上的，而在 Enderton 的书中则具有语义特征。

在这里，我们指出多类逻辑在以下意义上归约为经典的一阶逻辑（一类逻辑）：给定一个多类结构 A，对于 A 中的每个多类句子，都存在一个在 A∗ 上为真的一阶逻辑的翻译，其中 A∗ 是对 A 中所有类别进行统一的结果。从这个结果中，我们得到了两种逻辑之间的等价性，通过一个易于定义的理论 Π 来模拟。

句法翻译

对于句法翻译（也称为“量词的相对化”），让 L 是一个具有 Σ 签名的多类语言，让 OperSym 是其操作符号的集合。因此，我们需要一个一类语言 L∗，其中 OperSym∗=OperSym∪{Qi:i∈Sort}。

OperSym∗=OperSym∪{Qi:i∈Sort}。

L 的变量将被视为 L∗ 的变量，忽略了排序。多类语言 L 与相应的单类语言 L∗ 之间的区别在于，我们为每个 i∈Sort 添加了新的一元关系符号 Qi。此外，L 中的 OperSym 符号也在 L∗ 中，但在前者语言中它们具有 arity 和排序，而在后者中它们只有 arity。

翻译 Trans 保持每个术语和公式不变，唯一的例外是相对化的量化表达式：

Trans(∃xiϕ):=∃xi(Qixi∧Trans(ϕ))

例子：作为一个例子，我们将使用《完美空无之书》中已经提出的论证。在一类多类的一阶逻辑中，我们可以引入这种语言：

Exy:=x 存在于时刻 yPxy:=x 在 y 之前 Ox:=x 是一个对象 Ix:=x 是一个时间的:=时间的黎明 t:=今天

如您所见，我们不是使用不同种类的变量，而是添加了两个新的一元谓词 O 和 I。我们将论证形式化为：

α:=∀x(Ix∧∃y(Oy∧Eyx)→∀z(Iz∧Pzx→∃v(Ov∧Evz)))β:=∃y(Oy∧Eyt)γ:=∀y(Iy→Pdy)δ:=∃x(Ox∧Exd)

为了得出结论，我们还需要一个额外的假设，即时代的黎明和今天都是时间，(Id∧It)。我们可以添加几个关于我们新谓词的公式：

∀x(Ox→¬Ix)∀x∀y(Exy→Ox∧Iy)∀x∀y(Pxy→Ix∧Iy)

将多类结构转换为单类结构

对于任何具有签名 Σ 的多类结构 A，我们通过所谓的“域统一”构造其对应的单类结构 A∗。

A∗ 的域是 A 的个体域的并集，新的一元谓词 Qi 的解释对应于旧的域 Ai，因此保留了这些信息。OperSym 中其余元素的解释与多类结构 A 中的解释类似。唯一的困难在于具有 Rank(f)=⟨i1,…,in,i0⟩ 且 i0≠0 的操作符，因为现在宇宙是宇宙和函数 fA∗ 需要给出所有值的并集。值得注意的是，对于每个 fA，都有许多不同的扩展它的操作，这意味着上述转换生成了不同的单类结构。[28]

对于这些扩展结构中的任何一个，以下定理成立。

定理：设 A 是一个多类结构，A∗ 是其一类结构的对应物，L 是 A 的语言，φ 是 L 中的某个句子。那么

A⊨φ ⟺ A∗⊨Trans(φ)。

我们已经看到，多类结构总是可以转换为单类结构，现在我们考虑另一个方向。

将单类结构转换为多类结构

任何一个由签名 Σ∗ 定义的单类结构 E 是否可以转换为一个由签名 Σ 定义的多类结构？答案是否定的，因为有两个问题可能阻止转换：第一个问题是在多类结构中，所有的宇宙都应该是非空的，我们的想法是对于每个排序 i，将 QEi 作为排序 i 的一元关系作为宇宙，所以我们需要它是非空的；第二个困难涉及到符号 Rank(f)=⟨i1,…in,i0⟩ 的操作符，在结构 E 中的解释只是一个 n 元函数，但我们需要 fE↾(QEi1×…×QEin)的值在 QEi0 中。

我们所做的是用单类语言来制定三个条件，这些条件在模型中的有效性使其容易转换为多类语言。让 Π 是以下形式的所有句子的集合：

对于每个 i∈Sort，存在 x Qix
对于每个 x1…xn(Qi1x1∧…∧Qinxn→Qi0(f x1…xn))，其中 Rank(f)=⟨i1,…,in,i0⟩，f∈OperSym
对于每个满足 Rank(c)=i 的 c∈OperSym。

注意，前面定理中的结构 A∗ 是 Π 的一个模型。此外，Π 的一个单类模型 E 可以很容易地转换为一个多类模型 E‡。我们将 QEi 作为第 i 类的宇宙，通过将严格关系和函数限制到相应的域来获得具有所需类别的关系和函数。[29] 由于 Π 中的公理，可以进行 E‡的构造。现在很容易得到以下结果。

主定理：设 Γ∪{φ}⊆Sent(L)。

Γ⊨ 多类逻辑学 φ 当且仅当 Trans(Γ)∪Π⊨FOLTrans(φ)

我们使用 ⊨ 多类逻辑学和 ⊨ 一类逻辑学来区分多类逻辑和一类逻辑中的推论。

前面的定理允许我们从相应的一类结果推断出多类逻辑学的以下三个语义定理：紧致性定理、可枚举性定理和 Löwenheim-Skolem 定理（参见 Enderton 1972: 281）。但是，我们已经通过证明多类逻辑学的完备性（第 2.3 节）获得了它们。显然，从多类定理中我们可以免费获得一类版本。

然而，关于多类逻辑的其他定理并非直接从它们的单类版本中获得。特别是，多类逻辑的插值需要自己的证明（见第 6.2 节）。可解释性的概念在比较单类和多类理论时起着重要作用（见第 6.3 节和 Hook 1985）。不幸的是，多类理论之间的可解释性并非从它们的单类对应物中获得。关于比较，多类证明系统中的推导通常比我们在单类演算中得到的推导更短，这也是为什么多类逻辑在计算机科学中如此频繁使用的原因之一（Meinke＆Tucker 1993）。

6.2 插值定理

插值定理是逻辑学中具有“模型论中任何定理中最长的谱系”的定理之一（Wilfrid Hodges dixit），在逻辑学中起着重要作用。首先，一些重要结果，如 Beth 的可定义性定理和 Robinson 定理，可以直接从插值定理中获得（参见一阶模型论条目）。其次，插值可以被看作是一种中心逻辑属性，它“被用来揭示语法和语义之间的深层和谐”（Feferman 2008: 341）。

单类插值的版本由 William Craig 在 1957a 年证明。Roger Lyndon（1959 年）对 Craig 的定理进行了推广，并在 1968 年，Feferman 将后者的表述扩展到多类逻辑（参见 Feferman 2008: 349）。显然，单类版本是多类版本的特例。然而，多类插值不能直接从单类情况转移。

Craig 在 1957 年证明插值定理的思想基于一阶逻辑的完备性定理。原因是插值定理在某种程度上“位于”证明论（因为它遵循一些关于演算的元定理）和模型论（因为它的应用）的交集中。Henkin 表明，反过来也成立：完备性可以立即从 Craig-Lyndon 定理的扩展版本 [31] 中获得。

Craig 插值定理的句法表述如下：如果 φ 和 ψ 是句子且 ⊢φ→ψ，则：

Rel(φ)∩Rel(ψ)≠∅ 意味着存在一个“中间”公式 θ 满足 ⊢φ→θ 和 ⊢θ→ψ (θ 是一个句子，使得 Rel(θ)⊆Rel(φ)∩Rel(ψ)) 和
Rel(φ)∩Rel(ψ)=∅ 意味着 ⊢¬φ 或 ⊢ψ，

其中 Rel(α) 是 α 中的关系符号集合。其背后的直觉是：在证明条件公式 φ→ψ 的过程中，我们使用了今天所称的“插值” θ，一种最终消失的三段论中间项。

通过简单地将 φ 和 ψ 翻译成单类语言的相应公式，无法为多类逻辑建立定理。很容易看出，对于 ⊢Trans(φ)→Trans(ψ)的构造插值的逻辑形式不一定等同于多类公式的翻译。这就是为什么我们说这个结果不能直接从单类情况转移过来（详见 Otto 2000 以获取更多细节）。

与单类逻辑一样，多类逻辑的插值引理可以通过模型论风格（如 Kreisel＆Krivine 1967）或证明论风格（如 Feferman）来证明 [32]。

Feferman 的插值证明直接从他的序列定理之一的推论中获得（详见 Feferman 1968：56-62；定理 4.3），其应用是模型论的，这再次揭示了插值的特殊重要性。

6.3 解释性和理论等价性

从 FOL 到 MSL，另一个不能立即转移的概念是解释性。解释性是确定理论 T 和 T'之间比较的一个好标准，因为它可以用“模型的统一可定义性”或“保持逻辑形式和可证明性的解释映射的存在”来描述（Mceldowney 2020: 15）。它还有助于证明一致性，因为当在一致的 T 中进行解释时，T'被证明是一致的。然而，多类签名的理论之间的解释性并不能保证它们的（单类）翻译之间的解释性。

Mceldowney（2020）认为，双解释性的概念是 MSL 中理论等价性的最佳度量。对于具有相同签名的一阶理论之间的理论等价性，最古老的标准是定义等价性（参见 Eilenberg＆Mac Lane 1942, 1945 和 Glymour 1971）。因此，多类的对应性的必要性是显而易见的。结果，自 2016 年以来，关于 MSL 中等价性的性质的辩论一直在进行中。Barrett 和 Halvorson（2016）将定义扩展的思想推广为 Morita 扩展的概念：直观地说，T+是 T 的 Morita 扩展，当且仅当 T 和 T+都是 MSL 理论，并且 T+“不说更多”原始理论（有关详细形式，请参见 2016: 565）。

因此，他们声称在多类逻辑学中的理论等价性是具有共同的 Morita 扩展（这被称为“Morita 等价性”）。值得在这一点上回顾的是，Morita 扩展 T+可以通过在 T 的签名中添加新的类别符号以及相应的显式定义 [33] 到公理中来构建。有几种方法可以进行这种扩展：新的类别 τ 可以作为子类别、积类别、余积类别和商类别引入（参见 Barrett＆Halvorson 2016：563-64）。Morita 等价性也被用来试图澄清文献中所称的奎因的多类逻辑猜想（参见 Barrett＆Halvorson 2017）。

然而，根据 Mceldowney（2020）的说法，Morita 等价性的细致概念只是双解释性的一个特例。因此，他选择了基于可解释性而不是 Morita 扩展的多类逻辑学中的等价概念（参见 Mceldowney 2020 年第 404-407 页）。事实上，正如 Friedman 和 Visser（2014）指出的那样，双解释性保持了有限公理化、可决定性和 κ-范畴性。

6.4 多类逻辑向类别逻辑的扩展

除了将其简化为一类逻辑之外，多类一阶逻辑还可以扩展。多类逻辑是一种多类二阶逻辑，允许对新类进行量化，"观察" 公式被解释的结构之外。然后，除了在二阶逻辑中添加类别之外，我们还可以包括一个新的逻辑符号 ˜∃ 来量化新类别。

在多类逻辑中，涉及 ˜∃ 的良构公式必须遵守新类别条件（Väänänen 2014: 175），以确保对 φ 中的自由变量进行解释的域不会干扰量词 ˜∃ 的范围。唯一的新颖之处在于具有新量词的公式的解释，

如果且仅当 M,s⊨˜∃Xφ 时，对于 M 的某个 X 扩展 M'和某个 X∈℘(M'i1×…×M'ir)（其中变量 X 的类别为 ⟨i1,…,ir,0⟩），M',s(X/X)⊨φ。

在这个定义中，如果模型 M'包含了与 X 的多类所需的新宇宙(M'i1,...,M'ir)一样多的话，那么模型 M'被认为是模型 M 的 X 扩展。此外，M'对旧宇宙的限制是 M。

例如，公式

˜∃X∀x∀y(Xxy∧Xyx→x=y)

声称存在一种具有新的反对称关系的新类别；不知何故，我们说反对称性是一个一致的概念，因为它可以被举例证明。

Väänänen（2014）引入了一种用于多类逻辑的公理演算，作为二阶情况的扩展。因此，他加入了一个与 ˜∃ 相关的第二个理解公理，以及一些关于涉及新量词 ˜∃ 的证明规则的限制（参见 2014: 176–177）。

正如在每个高阶逻辑中发生的那样，具有标准语义的多类逻辑的完备性和紧致性都失败了。幸运的是，可以构建一个满足两个理解公理的 Henkin 结构，并转向一般语义。以这种方式改变语义会导致所提到的演算的完备性的恢复，正如 Väänänen（2014: 179–80）所指出的那样。该证明受到了 Henkin（1950）对类型理论的启发。

Väänänen（2014: 181）将多类逻辑应用于《数学基础》。他提出了在多类逻辑中可表征结构 A 中的真实概念，从而在这些结构中形成了一种新的一般真实 ⊨φ 和特定真实之间的区别。每当一般真实被归约为特定真实时，我们可以使用演算法来证明公式的可满足性。在某些约束条件下，任何在同构下封闭的结构类都可以在多类逻辑中定义（参见 Kennedy＆Väänänen 2021，定理 19）。因此，Väänänen 认为多类逻辑是一种“看待数学的替代方式”，与集合论不同，“关注的是定义而不是构造”（2014: 185）。它也是研究逻辑性和模型类的有趣工具（Kennedy＆Väänänen 2021）。

Bibliography

Abadi, Aharon, Alexander Rabinovich, and Mooly Sagiv, 2007, “Decidable Fragments of Many-Sorted Logic”, in Logic for Programming, Artificial Intelligence, and Reasoning, Nachum Dershowitz and Andrei Voronkov (eds.), (Lecture Notes in Computer Science 4790), Berlin, Heidelberg: Springer Berlin Heidelberg, 17–31. doi:10.1007/978-3-540-75560-9_4
Andréka, Hajnal, István Németi, and Johan van Benthem, 1998, “Modal Languages and Bounded Fragments of Predicate Logic”, Journal of Philosophical Logic, 27(3): 217–274. doi:10.1023/A:1004275029985
Andréka, Hajnal, Johan van Benthem, Nick Bezhanishvili, and István Németi, 2014, “Changing a Semantics: Opportunism or Courage?”, in Manzano, Sain, and Alonso 2014: 307–337. doi:10.1007/978-3-319-09719-0_20
Aranda, Víctor, 2022, “Completeness: From Husserl to Carnap”, Logica Universalis, 16(1–2): 57–83. doi:10.1007/s11787-021-00283-4
Barrett, Thomas William and Hans Halvorson, 2016, “Morita Equivalence”, The Review of Symbolic Logic, 9(3): 556–582. doi:10.1017/S1755020316000186
–––, 2017, “Quine’s Conjecture on Many-Sorted Logic”, Synthese, 194(9): 3563–3582. doi:10.1007/s11229-016-1107-z
Blackburn, Patrick and Johan van Benthem, 2007, “Modal Logic: A Semantic Perspective”, in Blackburn, van Benthem, and Wolter 2007: 1–84. doi:10.1016/S1570-2464(07)80004-8
Blackburn, Patrick, Johan van Benthem, and Frank Wolter (eds.), 2007, Handbook of Modal Logic, (Studies in Logic and Practical Reasoning 3), Amsterdam/Boston: Elsevier. [Blackburn, van Benthem, and Wolter 2007 available online]
van Benthem, Johan, 1983, Modal Logic and Classical Logic, (Indices 3), Napoli: Bibliopolis.
–––, 1984a, “Correspondence Theory”, in Handbook of Philosophical Logic, D. Gabbay and F. Guenthner (eds.), Dordrecht: Springer Netherlands, 167–247. doi:10.1007/978-94-009-6259-0_4
–––, 1984b, “Review: B. J. Copeland. On When a Semantics Is Not a Semantics: Some Reasons for Disliking the Routley–Semantics for Relevance Logic. Journal of Philosophical Logic, Vol. 8 (1979), pp. 399–413”, Journal of Symbolic Logic, 49(3): 994–995. doi:10.2307/2274161
–––, 2010, Modal Logic for Open Minds, (CSLI Lecture Notes 199), Stanford, CA: CSLI Publications.
Carnielli, Walter A., Marcelo E. Coniglio, and Itala M. L. D’Ottaviano, 2009, “New Dimensions on Translations Between Logics”, Logica Universalis, 3(1): 1–18. doi:10.1007/s11787-009-0002-5
Church, Alonzo, 1956, Introduction to Mathematical Logic, Volume 1, (Princeton Mathematical Series 17), Princeton, NJ: Princeton University Press. [Note: this was a new revised edition from a 1944 edition published as an Annals of Mathematics Studies volume (no. 13).]
Craig, William, 1957a, “Linear Reasoning. A New Form of the Herbrand-Gentzen Theorem”, Journal of Symbolic Logic, 22(3): 250–268. doi:10.2307/2963593
–––, 1957b, “Three Uses of the Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory”, Journal of Symbolic Logic, 22(3): 269–285. doi:10.2307/2963594
da Silva, Jairo J., Itala Marı́a L. D’Ottaviano, and A. M. Sette, 1999, “Translations between Logics”, in Models, Algebras, and Proofs, Xavier Caicedo and Carlos H. Montenegro (eds.), (Lecture Notes in Pure and Applied Mathematics 203), New York: Marcel Dekker, 435–448.
D’Ottaviano, Itala M. Loffredo and Hércules de Araújo Feitosa, 2019, “Translations Between Logics: A Survey”, in Philosophy of Logic and Mathematics: Proceedings of the 41st International Ludwig Wittgenstein Symposium, Gabriele M. Mras, Paul Weingartner, and Bernhard Ritter (eds.), Boston/Berlin: De Gruyter, 71–90. doi:10.1515/9783110657883-005
Ebbinghaus, Heinz-Dieter, Jörg Flum, and Wolfgang Thomas, 1984, Mathematical Logic, (Undergraduate Texts in Mathematics), New York: Springer-Verlag.
Eilenberg, Samuel and Saunders MacLane, 1942, “Group Extensions and Homology”, The Annals of Mathematics, 43(4): 757–831. doi:10.2307/1968966
–––, 1945, “General Theory of Natural Equivalences”, Transactions of the American Mathematical Society, 58(2): 231–294.
Enderton, Herbert B., 1972, A Mathematical Introduction to Logic, New York: Academic Press.
Feferman, Solomon, 1968, “Lectures on Proof Theory”, in Proceedings of the Summer School in Logic Leeds, 1967, M. H. Löb (ed.), (Lecture Notes in Mathematics 70), Berlin/Heidelberg: Springer Berlin Heidelberg, 1–107. doi:10.1007/BFb0079094
–––, 1974, “Applications of many-sorted interpolation theorems”, in Proceedings of the Tarski Symposium, L. Henkin, J. Addison, C. Chang, W. Craig, D. Scott and R. Vaught (eds.), (Proceedings of Symposia in Pure Mathematics, 25), Providence, RI: AMS, pp. 205–224.
–––, 2008, “Harmonious Logic: Craig’s Interpolation Theorem and Its Descendants”, Synthese, 164(3): 341–357. doi:10.1007/s11229-008-9354-2
–––, 2016, “Many-sorted first-order model theory as a conceptual framework for biological and other complex dynamical systems”, Keynote address to the AMS/ASL session on applications of Logic, Model Theory, and Theoretical Computer Science to System Biology, Seattle, 9 January 2016. [Feferman 2016 draft available online]
Friedman, Harvey and Visser, Albert, 2014, “When bi-interpretability implies synonymy”, Logic Group Preprint Series, 320: 1–19.
Gabbay, Dov M. (ed.), 1994, What Is a Logical System?, (Studies in Logic and Computation 4), Oxford: Clarendon Press.
–––, 1996, Labelled Deductive Systems, Volume 1, (Oxford Logic Guides 33), Oxford: Oxford University Press.
Gilmore, Paul, 1958, “An addition to ‘Logic of Many-Sorted Theories’”, Compositio Mathematica, 13: 277–281.
Glymour, Clark, 1971, “Theoretical Realism and Theoretical Equivalence”, in PSA: Proceedings of the Biennial Meeting of the Philosophy of Science Association, 1970, Roger C. Buck and Robert S. Cohen (eds.), (Boston Studies in the Philosophy of Science 8), Dordrecht: Springer Netherlands, 275–288. doi:10.1007/978-94-010-3142-4_19
Gödel, Kurt, 1931, “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I”, Monatshefte für Mathematik und Physik, 38–38(1): 173–198. doi:10.1007/BF01700692
Grzegorczyk, Andrzej, 1955, “The Systems of Leśniewski in Relation to Contemporary Logical Research”, Studia Logica, 3(1): 77–95. doi:10.1007/BF02067248
Henkin, Leon, 1949, “The Completeness of the First-Order Functional Calculus”, Journal of Symbolic Logic, 14(3): 159–166. doi:10.2307/2267044
–––, 1950, “Completeness in the Theory of Types”, Journal of Symbolic Logic, 15(2): 81–91. doi:10.2307/2266967
–––, 1953, “Banishing the Rule of Substitution for Functional Variables”, Journal of Symbolic Logic, 18(3): 201–208. doi:10.2307/2267403
–––, 1963a, “A Theory of Prepositional Types”, Fundamenta Mathematicae, 52(3): 323–344. doi:10.4064/fm-52-3-323-344
–––, 1963b, “An Extension of the Craig-Lyndon Interpolation Theorem”, Journal of Symbolic Logic, 28(3): 201–216. doi:10.2307/2271066
–––, 1996, “The Discovery of My Completeness Proofs”, Bulletin of Symbolic Logic, 2(2): 127–158. doi:10.2307/421107
Herbrand, Jacques, 1930, Recherches sur la théorie de la démonstration, PhD thesis, University of Paris.
Hodges, Wilfrid, 1986, “Truth in a Structure”, Proceedings of the Aristotelian Society, 86(1): 135–152. doi:10.1093/aristotelian/86.1.135
–––, 1993, Model Theory, Cambridge/New York: Cambridge University Press. doi:10.1017/CBO9780511551574
–––, 1998, “The Laws of Distribution for Syllogisms”, Notre Dame Journal of Formal Logic, 39(2): 221–230. doi:10.1305/ndjfl/1039293064
Hook, Julian L., 1985, “A Note on Interpretations of Many-Sorted Theories”, Journal of Symbolic Logic, 50(2): 372–374. doi:10.2307/2274223
Kennedy, Juliette and Väänänen, Jouko, 2021, “Logicality and Model Classes”, The Bulletin of Symbolic Logic, 27(4): 385–414. doi:10.1017/bsl.2021.42
Kreisel, Georg and J. L. Krivine, 1967, Éléments de logique mathématique, théorie des modèles (Monographies de la Société mathématique de France 3), Paris: Dunod; translated as Elements of Mathematical Logic: Model Theory (Studies in Logic and the Foundations of Mathematics), Amsterdam: North Holland, 1967.
Langford, C. H., 1939, “Review: Arnold Schmidt. ‘Über deduktive Theorien mit mehreren Sorten von Grunddingen’, Mathematische Annalen, 115. 4 (1938), pp. 485–506”, Journal of Symbolic Logic, 4(2): 98–98. doi:10.2307/2269080
Liezi, (列子, El libro de la perfecta vacuidad), Barcelona: Kairos, 1982. Translated directly from Chinese by Iñaki Preciado. Example translated to English for this Entry by Ulises Tindón.
Lindström, Per, 1969, “On Extensions of Elementary Logic”, Theoria, 35(1): 1–11. doi:10.1111/j.1755-2567.1969.tb00356.x
Lyndon, Roger C., 1959, “An Interpolation Theorem in the Predicate Calculus”, Pacific Journal of Mathematics, 9(1): 129–142.
Manzano, María, 1989 [1999], Teoría de modelos, Madrid: Alianza Editorial. Translated as Model Theory, Ruy J. G. B. de Queiroz (trans.), (Oxford Logic Guides 37), Oxford/New York: Clarendon Press ; Oxford University Press, 1999.
–––, 1993, “Introduction to Many-sorted logic”, Meinke and Tucker 1993: 3–86.
–––, 1996, Extensions of First Order Logic, (Cambridge Tracts in Theoretical Computer Science 19), Cambridge/New York: Cambridge University Press.
–––, 2014a, “April the 19th”, in Manzano, Sain, and Alonso 2014: 265–278. doi:10.1007/978-3-319-09719-0_18
–––, 2014b, “Henkin on Completeness”, in Manzano, Sain, and Alonso 2014: 149–175. doi:10.1007/978-3-319-09719-0_12
Manzano, Maria and Enrique Alonso, 2014, “Completeness: From Gödel to Henkin”, History and Philosophy of Logic, 35(1): 50–75. doi:10.1080/01445340.2013.816555
Manzano, María, Ildikó Sain, and Enrique Alonso (eds.), 2014, The Life and Work of Leon Henkin, (Studies in Universal Logic), Cham: Springer International Publishing. doi:10.1007/978-3-319-09719-0
Martí-Oliet, Narciso and José Meseguer, 1994, “General Logics and Logical Frameworks”, in What Is a Logical System?, Dov M. Gabbay (ed.), Oxford: Clarendon Press, 355–391.
Mceldowney, Paul Anh, 2020, “On Morita Equivalence and Interpretability”, The Review of Symbolic Logic, 13(2): 388–415. doi:10.1017/S1755020319000303
Meinke, Karl and John Tucker (eds.), 1993, Many-Sorted Logic and Its Applications, (Wiley Professional Computing), Chichester/New York: Wiley.
Meseguer, José, 1989, “General Logics”, in Logic Colloquium’87: Proceedings of the Colloquium Held in Granada, H.-D. Ebbinghaus, J. Fernandez-Prida, M. Garrido, D. Lascar, and M. Rodriquez Artalejo (eds.), (Studies in Logic and the Foundations of Mathematics 129), Amsterdam: North-Holland, 275–329. doi:10.1016/S0049-237X(08)70132-0
Otto, Martin, 2000, “An Interpolation Theorem”, Bulletin of Symbolic Logic, 6(4): 447–462. doi:10.2307/420966
Quine, Willard Van Orman, 1940, Mathematical Logic, New York: W. W. Norton & Company.
Schmidt, Arnold, 1938, “Über deduktive Theorien mit mehreren Sorten von Grunddingen”, Mathematische Annalen, 115(4): 485–506. doi:10.1007/BF01448954
Tarski, Alfred, 1933 [1983], Pojęcie prawdy w językach nauk dedukcyjnych, (Prace Towarzystwa Naukowego Warszawskiego, Wydzial III Nauk Matematyczno-Fizycznych, 34), Warsaw: Nakładem Towarzystwa Naukowego Warszawskiego. Translated as “The Concept of Truth in Formalized Languages”, J.H. Woodger (trans.), in Logic, Semantics, Metamathematics, second edition, J. Corcoran (ed.), Indianapolis, IN: Hackett, 1983, 152–278.
Tarski, Alfred and Robert Lawson Vaught, 1956, “Arithmetical Extensions of Relational Systems”, Compositio Mathematica, 13: 81–102.
Väänänen, Jouko, 1979, “Abstract Logic and Set Theory. I. Definability”, in Logic Colloquium ’78: Proceedings of the Colloquium Held in Mons, Maurice Boffa, Dirkvan Dalen, and Kenneth Mcaloon (eds.), (Studies in Logic and the Foundations of Mathematics 97), Amsterdam: Elsevier, 391–421. doi:10.1016/S0049-237X(08)71637-9
–––, 1982, “Abstract Logic and Set Theory. II. Large Cardinals”, Journal of Symbolic Logic, 47(2): 335–346. doi:10.2307/2273145
–––, 2014, “Sort Logic and Foundations of Mathematics”, in Infinity and Truth, by Chitat Chong, Qi Feng, Theodore A Slaman, and W Hugh Woodin, (Lecture Notes Series, Institute for Mathematical Sciences, National University of Singapore 25), Singapore: World Scientific, 171–186. doi:10.1142/9789814571043_0005
Wang, Hao, 1952, “Logic of Many-Sorted Theories”, Journal of Symbolic Logic, 17(2): 105–116. doi:10.2307/2266241

Academic Tools

Other Internet Resources

[Please contact the author with suggestions.]

上一页*基于逻辑的人工智能——见人工智能：基于逻辑的人工智能 logic-based artificial intelligence — see artificial intelligence: logic-based 下一页多值逻辑 many-valued (Siegfried Gottwald)

最后更新于9小时前