多分类逻辑（四）

从签名为 ΣSOL 的多排序结构 A（它是 Δ 的模型）传递到另一个签名相同的多排序结构 B，但其中 ⟨1,…,1,0⟩ 类型的宇宙现在是 ℘(Bn1) 的子集，并且 ϵBn 是真正的成员。新的多排序结构 B 是通过定义一个函数

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

得到的，该函数遵循ϵAn 中给出的信息来构建 B⟨1,…,1,0⟩，因此 B=H(A)。新结构基本上是一个具有真正成员关系的一般二阶结构。[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)，使得

Conv2(C) 是 φ 的模型当且仅当 C 是 TransSOL(φ) 的模型

对于所有 SOL 句子。

4.3 与 SOL 和 MSL 相关的语义定理

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

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

Δ⊨MSLTransSOL(φ)

在 MSLSOL 中。

主要定理：当且仅当

TransSOL(Π)∪Δ⊨MSLTrans(φ)

在MSLSOL中时，在SOL中Π⊨G.Sφ。

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

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

备注：可枚举性和紧凑性定理结合起来告诉我们，所研究的逻辑可以具有强完备演算。事实上，我们可以使用多分类理论Δ来推导多分类演算中的SOL定理。

但是，如果我们已经有了SOL的演算，我们可以使用翻译机制来证明它的可靠性和完备性。

4.4 SOL 的健全性和完备性

我们只是遵循了总体计划第三级（第 3.6 节）中提出的策略来证明 SOL 演算的健全性和完备性。需要证明的是以下定理。

演绎对应定理：二阶演算中的 Π⊢SOLφ 当且仅当

TransSOL(Π)∪Δ⊢MSLTransSOL(φ)

在多分类演算 MSL 中。

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

强完备性和健全性：Π⊨G.Sφ 当且仅当 Π⊢SOLφ 对所有 Π∪{φ}⊆Sent(L2) 都有。

5. 翻译成具有二阶表现的多类别逻辑

5.1 总体规划

如前所述，在 1953 年，Henkin 通过从 Church 1956[20] 中提出的演算中删除一些替换规则并引入理解模式，定义了一种新的二阶逻辑演算。在本文中，Henkin 定义了两个演算 F∗ 和 F∗∗（基本上是演算 MSL 和 SOL）：第一个演算是通过添加新量词的规则从一阶演算中获得的，而第二个演算是一个真正的二阶演算。这两个演算都是不完整的，具有标准语义。Henkin 提到，我们可以获得具有框架语义的 F∗ 演算的完备性结果。事实上，我们已经看到了 MSL 的完备性，并且二阶演算具有一般语义。

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

在下文中，这个想法在几个命题模态逻辑以及具有 Kripke 语义的命题动态逻辑中得到了利用（参见模态逻辑和命题动态逻辑的条目）。

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