多分类逻辑（三）_数学联邦政治世界观()

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

在所谓的“非经典逻辑”中，模态逻辑占据首位，因为它的历史可以追溯到亚里士多德、麦加拉学派、斯多葛学派和其他希腊哲学家。多年来，它一直被用来谈论必然性和可能性、时间和计算机程序。参见模态逻辑条目以及 Blackburn 和 van Benthem (2007) 和 van Benthem (2010)。

与此多分类逻辑条目最相关的模态逻辑特征是，真理可以被限定（或相对化），并且模态模型包括所谓的“可能世界”的宇宙。模型中真理的经典语义概念，写为 A⊨φ，现在被模型 A 中世界 w 处的真理所取代，写为 A,w⊨φ。

基本命题模态语言中的公式由原子、经典联结词和模态运算符、◻（盒子）和◊（菱形）构成。模态公式在克里普克结构中得到解释

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

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

A,w⊨P 当且仅当 w∈PAA,w⊭⊥ 对所有 wA,w⊨¬φ 当且仅当不是 A,w⊨φA,w⊨φ∧ψ 当且仅当 A,w⊨φ 且 A,w⊨ψA,w⊨◻φ 当且仅当对所有这样的 v即 ⟨w,v⟩∈R:A,v⊨φ

公式 φ 在模型 A 中全局成立，如果它在 A 中的所有世界中都得到满足（A⊨φ）。公式 φ 在所有模型中全局成立（⊨φ），则它有效。整个 Kripke 模型类中的有效性集（当对可及性关系没有施加任何限制时）是基本模态逻辑的有效性，也称为最小模态逻辑或系统 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 是一个新变量。

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

切换引理：A，w⊨φ当且仅当A⊨STx（φ）[x：=w]

（赋值将变量x发送给世界w）

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

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

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

第一个相关结果是，基本命题模态逻辑可以翻译成一阶逻辑的双变量片段[13]（仅使用两个变量的一阶逻辑公式），并且双变量片段的可满足性问题是可判定的。

第二个相关结果是模态特征定理[14]，该定理建立了对于任何具有自由变量的一阶公式，等价于模态公式和在双模拟下不变之间的等价性（定义见 van Benthem 2010: 26–27）。双模拟是一个有用的结果，因为它可以用来通过双模拟构造使模型 A 尽可能小，也可以制作更大的模型。

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

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

在以下各节中，我们将翻译成多类别逻辑作为实现完整性的三个阶段。[15]

3.3 总体规划

总体规划如下：将所研究逻辑的签名（称为 XL）转换为多类别签名，将逻辑 XL 的表达式翻译成 MSLXL（一种适合 XL 的多类别语言），并将逻辑 XL 的结构转换为多类别结构。因此，我们需要定义一个递归函数Trans来进行翻译和结构的直接转换，Conv1。

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

下一个要问的问题是，S∗ 是否可以被一组多排序公式 Δ 的模型所取代。因此，两个定义 Trans 和 Conv1 的关键在于简化语义等价的证明，在这方面，获得的结果的相关性在很大程度上取决于公理化 S∗ 的可能性。如果你得到这样一个 MSLXL 的递归公式集，比如 Δ，（或者至少是 S∗⊆Mod(Δ)），我们应该证明 XL 中的有效性等同于 MSLXL 中 Δ 的结果。

如果得到集合 Δ，应该定义一个结构的逆转换 Conv2。因此，从 Δ 的多排序模型中，我们得到 Str(XL) 中的结构。我们定义它的目的是为了证明，从一个多排序结构 B（Δ 的模型）开始，XL 的公式 φ 在 Conv2(B) 中为真当且仅当其平移的通用闭包在 B 处为真。

3.4 第一级：表示定理

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

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

⊨Str(XL)φ 在 XL 中当且仅当 ⊨S∗∀Trans(φ) 在 MSL 中

其中 ∀Trans(φ) 是 Trans(φ) 的通用闭包，并且 S∗=Conv1Str(XL)。

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

表示定理：存在一个递归的多排序句子集 Δ，其中 S∗⊆Mod(Δ)，并且

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

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

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

备注：因此，我们了解到 XL 的演算是一个自然需求，但我们也了解到在 MSL 中我们可以模拟这样的演算，然后我们可以使用 MSL 的定理证明器。

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)。

推论：XL 的紧致性和 Löwenheim-Skolem。

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

3.6 第三级：演绎对应

当 XL 逻辑还带有演绎演算时，我们可以尝试使用对应机制来证明（如果可能）XL 的健全性和完备性。为了证明这些定理，需要证明 XL 演算与多排序演算之间的模 Δ 演绎对应定理。因此，下一个目标是证明：

演绎对应定理：令 Δ 定义为主定理中所述，则：

Trans(Π)∪Δ⊢MSLTrans(φ) 当且仅当 Π⊢XLφ。

因为我们已经有了主定理（*），加上 MSL 的完备性和可靠性（**），一旦我们得到了这个演绎对应定理（***），下图就给出了 XL 的可靠性和强完备性：

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

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

Π⊨Str(XL)φ当且仅当Π⊢XLφ

备注：我们已经走到了完备性的尽头，但需要强调的是，我们正在使用已经证明的 MSL 完备性结果来证明 XL 的强完备性。

4. 二阶逻辑作为多排序逻辑

4.1 二阶逻辑

二阶逻辑 SOL 是一种非常具有表现力的形式语言，它与 FOL（一排序一阶逻辑）的区别在于：(1) 字母表，(2) 标准和非标准语义，以及 (3) 标准语义具有压倒性的表达能力。请参阅二阶和高阶逻辑条目以及 Church 的类型理论条目。

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

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

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

而二阶皮亚诺算术（PA2）则变成范畴论的，即任何两个PA2模型都是同构的。然而，我们为表达能力付出了高昂的代价，我们牺牲了逻辑：紧致性不成立，Löwenheim-Skolem不成立，完备性不成立（强完备性和弱完备性都成立）。

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

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))

被添加。

这些结果的结论是什么？正如你所知，逻辑就像一个天平：你在一个盘子里有表达能力，在另一个盘子里有可计算性。如果你想保留逻辑属性，你必须改变语义并失去一些表达能力，你不能同时拥有两者，它们是“最佳的不可能”。人们可以通过第 2.3 节中提到的 Lindström 的结果 (Lindström 1969) 以更技术的方式表达同样的想法。

有关二阶逻辑的更多信息，请参阅二阶和高阶逻辑条目，以及 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 到 MSLSOL 的句法翻译以及两种结构转换，直接转换和反向转换。

首先，我们意识到二阶结构实际上是具有某些特性的多分类结构：在大多数情况下，它们是我们所说的严格结构，因为任何两个不同宇宙之间的交集都是空的，但它们都是相关的，因为它们是在个体宇宙中定义的。此外，在一般结构中，宇宙遵循某些规则，例如外延性和理解性的模型。

让 L 成为具有一组操作符号 OperSym 的二阶语言。如果我们将 SOL 中的表达式与多分类逻辑中的表达式进行比较，我们会意识到 Xnx1…xn 不是多分类逻辑的公式，因为它只是一串变量。我们所做的是引入一种新的多类别语言 MSLSOL，其中我们保留了 OperSym 中的所有符号，但现在用新的成员关系符号 ϵn 扩大了签名，其解释将是一种成员关系。多类别签名 ΣSOL 包括一个集合 Sorts，其元素是 SOL 结构中的类型；即 1，以及对所有 n≥1 都有 ⟨1,…,1⏟n,0⟩。[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 的每个句子 φ：

当且仅当 MSLSOL 中的 ⊨S∗TransSOL(φ) 时，SOL 中的 ⊨G.Sφ

（其中 ⊨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(对于 n≠m)

结构的逆转换（从 MSLSOL 到 SOL）：结构的逆转换分四个步骤完成。[18]