多分类逻辑（六）

6.2 插值定理

根据 Wilfrid Hodges 的说法，插值定理是“模型论定理中最长的谱系”，[30] 在逻辑中起着重要作用。首先，可以从中直接获得几个重要结果，例如 Beth 可定义性定理和 Robinson 定理（参见条目 一阶模型论）。其次，插值可以看作是一种核心逻辑属性，它“已被用来揭示语法和语义之间的深层和谐”（Feferman 2008：341）。

威廉·克雷格 (William Craig) 于 1957 年证明了单排序版本的插值。罗杰·林登 (Roger Lyndon) (1959) 对克雷格定理进行了推广，1968 年，费弗曼 (Feferman) 将后者的表述扩展到多排序逻辑 (参见 Feferman 2008: 349)。显然，单排序版本是多排序版本的特例。然而，多排序插值不能直接从单排序情况转移而来。

克雷格 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)。

因此，他们声称 MSL 中的理论等价就是有一个共同的 Morita 扩展 (这被称为“Morita 等价”)。值得一提的是，T 的 Morita 扩展 T+ 可以通过在 T 的签名中添加新的排序符号以及在公理中添加相应的显式定义[33]来构造。有几种方法可以实现这种扩展：可以将新排序 τ 引入为子排序、积、余积和商排序（参见 Barrett & Halvorson 2016：563–64）。Morita 等价也被用来试图阐明文献中所谓的 Quine 对多排序逻辑的猜想（参见 Barrett & Halvorson 2017）。

然而，根据 Mceldowney (2020) 的说法，Morita 等价的细微差别概念只是双可解释性的一个特例。出于这个原因，他选择了基于可解释性而非 Morita 扩展的 MSL 等价概念（参见 Mceldowney 2020 第 404-407 页）。事实上，正如 Friedman 和 Visser (2014) 所指出的，双解释性保留了有限公理化、可判定性和 κ-范畴性。

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

除了简化为单类别逻辑之外，多类别一阶逻辑还可以扩展。排序逻辑是一种多类别二阶逻辑，允许对新类别进行量化，“从外部看”公式被解释的结构。然后，除了在二阶逻辑中添加类别之外，我们还可以包含一个新的逻辑符号 ˜∃ 来对新类别进行量化。

在排序逻辑中，涉及 ˜∃ 的合式公式必须遵守一个新的排序条件 (Väänänen 2014: 175)，以保证 φ 中的自由变量的解释域不会干扰量词 ˜∃ 的范围。唯一的新颖之处在于使用新量词解释公式，

当且仅当 M 的某个 X 展开式 M′ 和某个 X∈℘(M′i1×…×M′ir) 时，M,s⊨˜∃Xφ 当且仅当 M′,s(X/X)⊨φ（其中变量 X 属于 ⟨i1,…,ir,0⟩ 类型）

在此定义中，模型 M′ 被视为 M 的 X 展开式当且仅当它包含与 X 类型所需的一样多的新宇宙（M′i1,…,M′ir）。此外，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）。