多分类逻辑（五）

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

我们要做的第一件事是设置一个多分类语言 MSLPML，其中包含：每个原子命题的一元关系符号 P∈Atom，表示可访问性关系的二元关系符号 S，成员符号，以及个体和集合的相等性。MSLPML 包含个体变量以及集合变量。翻译是标准的（如第 3.2 节中所述）：我们在目标逻辑 MSLPML 中表达被翻译公式的语义解释。[21]具体来说，

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

我们将使用的多排序结构是通过添加包含状态或世界集的宇宙从模态结构中获得的。给定一个克里普克结构

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的表示定理：

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

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

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

模态逻辑 S4 的第一级

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

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

S4的表示定理很容易得到

PML中的⊨Dφ⟺MSL中的Δ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φ

模态逻辑与其多分类对应物之间的演绎对应关系可实现

Π⊢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}。

L 的变量将被视为 L∗ 的变量，忘记排序。多类别语言 L 与对应的单类别语言 L∗ 的区别在于，我们为每个 i∈Sort 添加了新的一元关系符号 Qi。此外，L 的 OperSym 中的符号也存在于 L∗ 中，但在前一种语言中，它们有元数和类别，而在后一种语言中，它们只有元数。

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

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

示例：作为示例，我们将使用《圆满空性之书》中已经提出的论证。在单排序的一阶逻辑中，我们可以引入这种语言：

Exy:=x 存在于时刻 yPxy:=x 早于 yOx:=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 中。

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

∃x Qix，对于每个 i∈Sort

∀x1…xn(Qi1x1∧…∧Qinxn→Qi0(f x1…xn))，其中 Rank(f)=⟨i1,…,in,i0⟩，f∈OperSym

Qic，对于每个 c∈OperSym，其中 Rank(c)=i。

请注意，前一个定理的结构 A∗ 是 Π 的模型。此外，Π 的一排序模型 E 很容易转换为多排序模型 E‡。我们取 QEi 作为第 i 类的域，得到严格的关系和函数作为对相应域的限制，从而得到具有所需类别的关系和函数。[29] 根据 Π 中的公理，可以进行 E‡ 的构造。现在很容易得到以下结果。

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

Γ⊨MSLφ 当且仅当 Trans(Γ)∪Π⊨FOLTrans(φ)

我们使用 ⊨MSL 和 ⊨FOL 来区分多类逻辑和单类逻辑中的结果。

前一个定理使我们能够从相应的一类结果中推断出以下三个 MSL 的语义定理：紧致性定理、可枚举性定理和 Löwenheim-Skolem 定理（参见 Enderton 1972：281）。但我们已经得到了它们，因为我们已经证明了 MSL 的完备性（第 2.3 节）。显然，从多类定理中我们可以免费得到一类版本。

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