范畴逻辑（二）

即对于任意一个命题公式φ ，其在 ℙ 中可证明当且仅当其在这个模型 [·]ℙ 中为真。(9) 式是成立的可以完全从我们对 LT 代数的定义中看出来。这表明由于 LT 代数的存在，代数语义有着比命题逻辑的一般语义更为简洁明了的完全性定理：对于一般赋予真值的语义，完全性定理说的是如果一个公式 φ 在所有（一般）模型中都为真，则 φ 也能被我们的公理系统证明；但在代数语义下，我们不需要考虑所有的代数语义模型了，我们的完全性定理的信息包含在了这唯一的这一个语义模型 LT 代数当中，因为在其上为真已经完全等价于可证明了！我们把满足这样性质的模型，即其上的满足关系（satisfaction relation）和公理系统的证明关系完全对应，称为 ℙ 的泛模型（universal model）。换句话说，我们可以用逻辑的语言刻画我们的公理系统所表示的那个代数对象：一个命题逻辑系统 ℙ 所表示的布尔代数正是它的泛模型。

基于此，或者说基于 (9) 式，我们能够证明我们构造的 LT 代数Bℙ 满足如下的泛性质（universal property）：对于任意代数同态 f：Fmlₚ → B ，它是 ℙ 的一个代数语义模型（即它把 ℙ 中的公理映到最大元）当且仅当存在 Bℙ → B 使得如下图交换：

[·]ₚ

Fmlₚ↠Bℙ

↘ ⇣

f B

如果大家熟悉商空间的泛性质，前述是用范畴的语言重新描述了我们已经知道的如下事实：Bℙ 是自由代数 Fmlₚ 模掉由我们的公理系统 ℙ 生成的等价关系之后的商代数；上述泛性质本质上就是这个商的泛性质。这表明 ℙ 的所有一般模型可以有如下表达：

Mod(ℙ)≅Bool(Bℙ，2). (10)

这里Mod(ℙ) 表示所有 ℙ 的一般模型，Bool 是所有布尔代数构成的范畴。熟悉范畴论语言的朋友应该很清楚 Bool(Bℙ，2) 所代表的是在 Bool 这个范畴中所有从 Bℙ 到 2 的态射。(10) 式最为精炼地总结了我们在这一节中想要传达的观点：从代数的观点看，命题逻辑系统是一般代数的表示，具体方式便是由命题变元生成自由代数之后再由公理系统生成等价关系做一个商；这时任何一个经典命题系统都表示着某个布尔代数，且每个布尔代数也都由某个命题系统表示；这时，系统的模型（一般地或代数的）都可以看作是系统所表示的这个代数到其他代数的同态。

最后再说明两点。首先，由于在这样的观点下我们把命题系统看作是某个代数的表示，这预示着不同的命题系统可能会表示相同代数结构。这与我们最开始提到的群结构的两种公理化方式是类似的。从模型的角度来看，如果两个语形上不同的命题系统表示了同构的代数结构，则由 (10) 式我们可以看出它们也具有相同的模型。因此从本文在第一部分所设立的基于模型的角度来看待逻辑的大前提下，我们此时可以说这两个逻辑系统是等价的。在这个意义上，我们才有“经典命题逻辑 = 布尔代数”中的等号是成立的。第二，(10) 式和经典命题逻辑在一般语义下的完全性定理告诉我们，我们仅仅考虑Mod(ℙ) ，即所有从 Bℙ 到 2 的代数同态，我们就能够还原出 Bℙ 的结构，因为考虑所有一般模型的满足关系就能让我们还原出我们推理系统的证明关系，由此便可（在同构的意义上）唯一地确定 Bℙ 。经典命题逻辑的完全性定理在我们这个代数的观点下说明了一个非常深刻的数学定理：它说明每个布尔代数都有足够多的到 2 的态射使得从这些信息我们能够还原出其本身的代数结构。用更现代的数学语言来说，这就是有关布尔代数 Stone 对偶所表达的内容！在此处我们不过多地涉及了。

逻辑 = 范畴，模型 = 函子

如果你理解了前面命题逻辑的例子，你会发现几乎完全相同的思考方式能够毫不费力地推广到一阶逻辑的各个片段（fragment），只是我们此时必须考虑更一般的范畴，而不仅仅是诸如布尔代数这样的代数结构（后面我们会阐明，我们在这一节中采用范畴的语言所表述地严格地包含了之前命题逻辑的例子）。

让我们回到我们之前非常简单的群的等式逻辑的例子。其语言非常的简单，只有三个函数符号（此时我们把常量看作0-元函数符号），从这三个函数符号我们能生成许多的项（term），而逻辑公理是这些项之间的等式。我们把群的等式系统记为𝔾。类比之前我们对命题逻辑的陈述，我们应该已经能懂得如何从范畴的角度看待这样的逻辑系统了：首先，我们的逻辑语言本身可以看作是生成某种自由结构（free structure）的工具——由于我们本篇的篇名叫范畴逻辑，读者可以很放心大胆地猜测其生成的必定是某种自由的范畴——而我们的逻辑公理则描述了这个自由范畴上的某种等价关系，最终我们根据这个逻辑系统 𝔾 所生成的便是一个从一个自由范畴模掉一个等价关系之后所生成的商范畴 C𝔾 ，这个商范畴 C𝔾 便是类似于命题逻辑中 LT 代数 Bℙ 一样的构造。从代数的角度（这里更准确地说是从范畴的角度），这个商范畴必定满足与这个等价关系相对应的泛性质。用逻辑的语言来说，这表明我们的逻辑系统 𝔾 在任意范畴 D 中的模型，即 D 中的一个群，应该是从这个商范畴 C𝔾 到 D 的一个函子。从逻辑的角度来说，这个生成的商范畴 C𝔾 应该可以看作我们逻辑系统 𝔾 的一个泛模型，即其结构应该完全地反应了 𝔾 中的证明信息。最后的最后，我们应该有类似于 (10) 的式子将所有的这一切很好地总结起来。希望读者从之前对命题逻辑的叙述中已经能够基本理解这样的想法了。接下来便让我们更加详细具体地阐述这上面所提到的内容。

让我们首先看看什么是从𝔾 的语言中生成的自由范畴。如前述所讲， 𝔾 的语言中只包含着三个函数符号，可以用下图简洁地表示：

m i

G×G→G←G

↑e

1

直观地来讲，我们所生成的自由范畴中所有态射都应该是由这三个操作所生成的，且由于在其中我们应该能够计算笛卡尔积，我们应该要求我们生成的自由范畴有有限的笛卡尔积结构。所以总结来看，我们由𝔾 的语言生成的自由范畴 Tɢ 应该是由一个物体（object） G 以及如上图所示的三个态射所生成的自由有限笛卡尔积完备的范畴（the free finite product complete category on a single object G and three morphisms displayed as above）。 Tɢ 中的所有物体应该都同构于 Cᵐ，n∈ω ，所有的态射应包含 m，i，e 和所有的投影映射（包含恒等映射和到终对象的唯一映射），且应对所有有限笛卡尔积完备的范畴中的操作封闭，如复合运算和 〈·，·〉 运算。

此时我们所生成的自由范畴Tɢ 还不包含任何群公理的信息。为了使得其包含我们等式公理系统中 𝔾 的信息，我们必须在 Tɢ 上模掉由前述表达群公理的交换图所生成的等价关系；由此，我们得到的是一个商范畴 C𝔾 ，我们称其为群公理系统 𝔾 的语形范畴（syntactic category），这个语形范畴包含了和 𝔾 等价的信息。值得指出的是，由于我们的等价关系全部是在态射层面，模掉这个等价关系并不会影响我们范畴中的物体，只是令物体之间一些原本在自由范畴中不想等的态射变成相等的了。因此， C𝔾 和 T𝔾 有相同的物体。

首先可以确定的是，由于C𝔾 是通过在 Tɢ 上模掉一个等价关系而形成的，我们有一个从 Tɢ 到 C𝔾 的商函子（quotient functor）：

q：Tɢ↠C𝔾. (11)

q 作用在 Tɢ 上的方式是显然的：由于 C𝔾 和 Tɢ 有相同的物体，因此 q 作用在物体上是显然的；对于态射，它仅仅是将原本在 Tɢ 中的态射映射到其在 C𝔾 中的等价类上。可以验证， q 是一个良定义的函子。

其次，我们来看Tɢ 和 C𝔾 到其他范畴 D 的函子与 D 中的 𝔾 模型，即 D 中的群，的关系。假设 D 是有限笛卡尔积完备，即其上具有有限笛卡尔积结构，由于 Tɢ 是由一个物体 G 以及三个态射 m，i，e 自由生成的有限笛卡尔积完备范畴，任何从 Tɢ 到 D 的一个保持有限乘积（preserve finite product）的函子 F 就等价于我们在 D 中选出一个物体（即 G 在 F 下的像 F(G) ）和三个态射

F(m)：F(G) × F(G) → F(G)，F(i)：F(G) → F(G)，F(e)：1 → F(G). (12)

D 中这样的三个态射，或者等价地说从 Tɢ 到 D 的一个保持有限乘积的函子 F ，是 D 中的一个群当且仅当这个函子尊重 Tɢ 上由 𝔾 生成的等价关系，即在 (12) 中的这三个态射满足如前所述由交换图表表示的群公理；更进一步，由于 C𝔾 是通过这个等价关系生成的商，我们可以有如下通过泛性质地表述：从 Tɢ 到 D 的一个保持有限乘积的函子 F 定义了 D 中的一个群当且仅当存在 C𝔾 到 D 保持有限笛卡尔积的函子使得如下图表交换：

q

𝓣 ɢ↠𝓒 𝔾

↘ ⇣

F 𝓓

即与代数语义中模型和代数同态类似，我们再一次有D 中的群与从 C𝔾 到 D 保持有限笛卡尔积的函子等价！这一般称为范畴逻辑中的函子语义（functorial semantics）。再说得精炼一些，我们有如下的等价关系：

Mod𝔾(D)≅FP(C𝔾，D). (13)

其中，Mod𝔾(D) 表示 D 中的 𝔾 模型， FP 表示有限笛卡尔积完备的范畴和它们之间保持有限笛卡尔积结构的函子所构成的范畴。

至此，我们已经将所有的内容采用范畴的语言进行了推广于重述，最终得到了我们想要的式子 (13)。但在范畴论的背景下我们还有一些更多的内容需要注意。首先，当我们研究群的时候不仅是群结构本身对我们重要，同等重要的还有群之间的同态。假设我们有在D 中的两个群 M，N ，等价地两个保持有限笛卡尔积的函子 M，N：C𝔾 → D 。从群的观点出发，一个群同态可以理解为两个群结构之间的一个态射 h：M → N 使得它于这两个物体上的群结构如乘法和求逆等交换；如果你把这些条件显式地写出来，你会发现在将模型 M，N 看作函子的观点下这完全等价于从 M 到 N 的一个自然变换！这表明，(13) 式不仅仅在集合的意义上是成立的，它所描述的是两个范畴——即 D 中的群和群同态构成的范畴 Mod𝔾(D) 和从 C𝔾 到 D 所有保持有限笛卡尔积的函子范畴——的等价！

更为重要的是，(13) 所描述的等价对于范畴D 是自然的，即 (13) 是一个自然等价（natural equivalence）。这其实说的是我们构造的语形范畴 C𝔾 是取群模型的这个 2-函子（2-functor）Mod𝔾(·)：FP → Cat 的代表对象（representing object）。于是，根据 Yoneda 引理我们知道 C𝔾 就在等价的意义上被唯一地确定的了。如果我们回到我们之前提到过的用一个0元函数 e 和一个二元函数 ⨀ 来公理化群的等式逻辑系统，假设其记为 𝔾' 。由于我们前面提到 𝔾' 和 𝔾 是可双向翻译的（bi-interpretable），这表明 𝔾' 的模型和 𝔾 的模型是完全一致的，因此我们有下列一连串的自然等价：

FP(C𝔾'，D)≅Mod𝔾'(D)≅Mod𝔾(D)≅FP(C𝔾，D).

(14)

此时再由 Yoneda 引理，我们可以推断C𝔾'≅C𝔾。因此可见，尽管 𝔾 和 𝔾' 是两个不同的逻辑系统，但在这个意义上它们都可以看作是（在等价的意义下）同一个语形范畴 C𝔾 的不同表示。而语形范畴则是在保持某个逻辑系统所有的语义信息不变的情况下我们所得到的某种不依赖于具体表示（presentation invariant）的对象。在这种意义上，我们的语形范畴是在我们只关心逻辑的模型的大前提下对逻辑系统非常好的抽象。

逻辑片段与范畴结构

在本文的结尾部分我们来阐述本篇文章标题所指的内容。如果你非常严肃地看待前面两节的小标题，你会发现我们前面的描述其实并不完全准确。对于命题逻辑，我们仅仅指出了某种特殊的结构，即布尔代数，和经典逻辑的对应；对于推广的逻辑系统，我们也仅仅研究了最最简单的等式逻辑和有限乘积完备的范畴之间的对应关系。这些都只是一般情形的中很小的一部分特殊的结构。

事实上，逻辑和范畴结构之间的对应远比我们前面所描述的要来的深远。在等式逻辑中我们除了等号，其他所有的逻辑连词都无法使用。在这之上我们还有很多逻辑片段，这些逻辑片段与它们对应的范畴结构都列在下表中了：

逻辑片段 范畴结构

等式逻辑(=) 有限乘积完备范畴

笛卡尔逻辑（Cartesian Logic）（=，⊤，∧，∃！）

笛卡尔范畴（Cartesian Category）

正规逻辑（Regular Logic）（=，⊤，∧，∃） 正规范畴（Regular Category）

连贯逻辑（Coherent Logic）（=，⊤，∧，⊥，∨，∃）

连贯范畴（Coherent Category）

几何逻辑（Geometric Logic）（=，⊤，∧，⊥，∨，∃） 几何范畴（Geometric Category）

一阶直觉主义逻辑（=，⊤，∧，⊥，∨，→，∃，∀）海廷范畴（Heyting Category）

一阶经典逻辑（=，⊤，∧，⊥，∨，→，¬，∃，∀）

布尔范畴（Booleán Category）

每个逻辑片段都具有不同的逻辑连词，这些逻辑连词的逻辑性质几乎是在右边一一对应着范畴中的具体结构。例如解释有限合取（包括空合取⊤ ）我们便需要范畴中有有限极限（finite limit），这对应于右边的笛卡尔范畴（左边笛卡尔逻辑中 ∃！ 并不是说我们有唯一存在的这个逻辑连词在我们的逻辑系统中，而是说如果从公理中我们能够推导出存在的唯一性我们便可使用这个存在量词；读者可以上网查阅具体细节）。在正规逻辑中我们能够使用存在量词，这对应着我们的范畴中除了是有限极限完备的，还要能够有对态射取图像（image）的操作，在范畴论中这样的范畴也叫做正规范畴。连贯逻辑加入了有限析取（包含空析取 ⊥ ），这对应着在我们的范畴结构中还需要有限余极限（colimit）的结构，并且这些余极限必须和极限结构相容，这些范畴也被称为连贯范畴。几何逻辑则是把有限的析取推广到了无限的析取，在范畴中的层面也对应着有无限余极限的结构。在一阶直觉主义逻辑和一阶逻辑中我们还加入了导出连词和全称量词，这些对应着范畴结构中的一些（局域）笛卡尔封闭结构（[locally] Cartesian closed），对应的范畴分别叫海廷范畴和布尔范畴。（值得进一步说明的是，以上的这些片段全部是在 sequent 形式下表述的，因此即使是在没有导出连词和全称量词的情况下在这些逻辑片段中我们一般也是可以表达一层的导出和全称量词的；具体更加细节的表述可以参考[1]）。

数学联邦政治世界观提示您：看后求收藏（笔尖小说网http://www.bjxsw.cc），接着再看更方便。