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

1. 语法和语义

1.1 示例

1.2 基本思想

1.3 形式语言

1.4 多类别结构

1.5 语义

2. 微积分

2.1 演绎演算

2.2 完备性概念

2.3 多类别逻辑的完备性

2.4 自动定理证明器

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

3.1 翻译

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

3.3 总体规划

3.4 第一级：表示定理

3.5 第二级：主要定理

3.6 第三级：演绎对应

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

4.1 二阶逻辑

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

4.3 语义定理SOL 和 MSL

4.4 SOL 的健全性和完整性

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

5.1 总体规划

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

6. 进一步的结果

6.1 多分类逻辑简化为单分类逻辑

6.2 插值定理

6.3 可解释性和理论等价性

6.4 多分类逻辑扩展为分类逻辑

参考书目

学术工具

其他互联网资源

相关条目

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 节），因此可以采用二分类一阶逻辑，其中个体和个体间关系都是可以量化的一等公民。我们将有变量 x、y、… 属于 i 类（个体），以及变量 X2、Y2、… 属于 r 类（个体间的二元关系）。但是，将我们的变量标记为个体或二元关系是不够的，我们需要它们像二阶变量一样发挥作用。需要添加一个与二元关系和个体相关的三位谓词符号 ϵ2xyX2，以便 Asymm(X2) 变为：

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

Anti-symm(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 元关系，也可以只在某些域之间建立 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 元谓词时，对于 m 元函数符号，i0=0，且 i0≠0；单个常量被视为零元函数符号，其 Rank(f)=⟨i0⟩，简化为 i0。

签名：签名 Σ 表示有序三元组

Σ=⟨Sort,OperSym,Rank⟩

等式是一个二元符号，可以是严格的，也可以是自由的。在我们的语言中，等式符号 ≈ 且 Rank(≈)=2 是自由的（具有 2 个元数，并且允许在任何类型的项之间工作）。[2]量词 ∃xi 用于任何 i 类的变量 xi。

在欧几里得的例子中，我们有两种类型，l（线）和 p（点），以及一个 3 位谓词 Join，其 Rank(Join)=⟨l,p,p,0⟩。在二元关系的例子中，我们有两种类型，i（个体）和 r（二元关系），以及一个 3 位谓词符号 ϵ2，其 Rank(ϵ2)=⟨i,i,r,0⟩。对于理解的例子，我们有两种类型，i（个体）和 π（属性），以及一个 2 位谓词符号 ϵ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 是 i 类变量，则 ∃xiφ 也是一个公式。

自由变量和约束变量

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

例子：《空论》

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

《空论》：英汤问格：“天开有物吗？”

夏格回答：“如果天开没有物，怎么可能存在今天？同样，后人也会相信今天没有物”。

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

如果事物在给定的时间点存在，那么在任何给定的时间点之前事物一定存在。

这条规则并不是说某个物体的存在是永恒的，而是说存在链可以永远追溯。

因此，该论证可以重新表述如下，其中 α、β 和 γ 是前提，δ 是结论：

α：= 如果事物在给定的时间点存在，那么在任何给定的时间点之前事物一定存在。

β：= 事物今天存在。

γ：= 时间的黎明先于一切。

δ:= 事物在时间的黎明就存在了。

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

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

该论证现在为：

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

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

1.4 多类别结构

多类别逻辑的语义与经典一阶逻辑的语义非常相似，因为它遵循塔斯基的真值定义，在结构中引入真值概念（参见 Tarski 1933 和 Tarski & Vaught 1956；有关历史说明，参见 Hodges 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 元关系域，An⊆℘(An)。但由于 A 是一个一般结构，因此宇宙 An 不是任意选择的，因为它们必须满足理解模式。因此，在可定义性下，宇宙是封闭的（有关一般结构的更多信息，请参见第 4.1 节）。

多分类结构

多分类 Σ 结构 A 具有非空集族 Ai（对于每个 i∈Sort）中的多个对象宇宙（或域）。结构 A 还包含：每个关系符号 R 的 m 元关系 RA，每个 n 元函数符号 f 的 n 元函数 fA，以及每个单独常数 c 的区别元素 cA∈Ai。必须在域族元素之间建立这些关系和函数，同时考虑它们在函数 Rank 下的值。[4]

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

我们可以添加不同域之间空交集的要求。满足这一要求的结构称为“严格”结构，否则称为“宽松”（或“自由”结构）。对于严格结构，我们可以考虑对每个类别≈i 都有一个等号，每个类别的 Rank(≈i)=⟨i,i,0⟩。我们要求等号（严格或自由）被解释为真正的身份，即对象与其自身之间存在的典型关系，而其他两个对象之间则不成立。

结构之间的相似关系

对于单排序结构，研究它们之间的不同关系非常常见：同态、嵌入、同构、子结构和扩展（参见 Manzano 1989 [1999: 19–33]）。人们可以以类似的方式为多排序结构定义这些关系。两个具有相同签名的结构 A 和 A′ 之间的同态是一个从 A 的宇宙并集到 A′ 的宇宙并集的函数 π，满足以下条件：首先，对于每个 i∈Sort，π 对 Ai 的限制必须是从 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⊨φ）这一重要概念，我们需要先定义公式 φ 在 A 中在赋值 s 下的满足概念（记为 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,s⊨τ1≈τ2当且仅当两个术语表示结构A中的同一对象；即I(τ1)=I(τ2)。

在多分类逻辑中，联结词是标准的，因此，我们对建立在它们之上的公式使用经典的满足定义。对于量化公式，如 ∃xiφ ，其定义如下：A,s⊨∃xiφ 当且仅当存在 x∈Ai 使得 A,s(x/xi)⊨φ。

重合引理

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