范畴逻辑（一）

从大的方面来说，我们几乎可以从两个大的方面来理解数理逻辑所做的工作：作为一个数学分支的数理逻辑和作为数学基础的数理逻辑。在这两种观点下，对逻辑的看法以及我们能够使用的数学工具将截然不同。如果你把数理逻辑，特别是算数系统和公理集合论，看作是奠定所有其他数学基础的基本语言，那么你所采取的观点将会非常的不一样。首先，由于你的目标是给数学提供坚实的基础，原则上讲你能依赖的所有工具只有有限组合数学的内容。这就是为什么我们在学习皮亚诺算数系统时我们总会将定理陈述为如下的形式：“如果 PA 是相容（consistent）的，则……“。在我们的元理论不够强大的情况下，我们是无法证明 PA 的相容性的，更别说一阶逻辑的完全性定理或者其他数理逻辑中著名的定理了（一阶逻辑的完全性定理依赖于选择公理）。例如著名的 Gentzen 对 PA 相容性的证明便用到了一直到序数ε₀＝sup{ω，ωω，ωωω，· · ·} 的超限归纳法（transfinite induction），这显然超过了 PA 自身的能力（但所需要的严格小于公理集合论如 ZF 所具有的能力）。

对大部分人而言，我们不是在如上所述为数学奠定基础的语境下谈论逻辑的。此时，数理逻辑便成为了数学的一个分支。特别的，我们已经假设了有足够强大的数学公理可以任我们使用，我们在这些足够强大的公理下可以证明一些关于逻辑系统非常有用的性质，比如前面提到的一阶逻辑的完全性定理以及 PA 的相容性等等。在这篇文章中我们都将从这个角度来理解数理逻辑，而将忽略逻辑对与数学基础相关问题的重要作用。这确定了这篇文章探讨的大语境前提。

其次，对逻辑的理解还取决于你用逻辑来理解和研究什么类型的问题。研究的问题不同决定了你对何为一个逻辑这个问题的答案。与之相关一个最基本的问题便是：在什么情况下你认为两个逻辑系统是等价的？一个普世的回答是：如果两个逻辑系统对你关心的所有问题都给出相同的答案，则我们就认为这两个逻辑系统（在你所考虑的问题的范围下）是等价的。而考虑的问题不同时，你所得出的等价的概念，或者说你所认为的一个逻辑的概念则就是不同的。例如，在这个专栏的第一篇文章 一阶算数理论中的自指性 中，我们探讨了一阶算术系统中的自指性问题。在那篇文章中我们得到的一个非常重要的印象是，自指性问题（或更一般的 intentionality 的问题）对逻辑语言的许多参数是非常敏感的。比如，即便一个算术系统是 PA 的一个保守扩张（conservative extension），它们在对与自指性有关的问题上也会给出不同的答案。因此，从自指性的角度看待逻辑，我们得到的是一个对不同逻辑系统非常精细的划分。

但从数理逻辑的角度，我们显然不希望过多地区分 PA 和它的保守扩张。这是因为，数理逻辑一般是站在模型的角度来看待逻辑系统的。这与数理逻辑的基本任务是相关的：数理逻辑的一个非常主要的任务是对我们在研究中遇到的不同的数学结构作出分类、并对不同的类别作出系统的研究。比如泛代数（universal algebra）便是从逻辑的角度对何为代数结构作出了划分，并研究一般的代数的性质。在数理逻辑和范畴论的语境下，只有公理系统能够用等式逻辑（equational logic）描述的才能严格地称之为代数。其中这包含着一些我们熟悉的例子，如群（group）、幺半群（monoid）、阿贝尔群（abelian group）、环（ring）、交换环（commutative ring）、格（lattice）等等。但一些同样我们日常生活中看作代数结构的对象如域（field）则不属于此列，因为域的公理必须使用存在量词（existential quantifier）。我们将在后面看到，这种从逻辑的角度对不同数学结构的划分是非常重要的；且严格来说，其重要性也必须通过范畴论的视角才得以最完美地显现。

基于此，本篇是从模型的角度出发来理解数理逻辑的。两个逻辑系统如果拥有相同的模型（这个表述目前并不完全准确，下面会更加详细地说明），我们就认为这两个逻辑系统是等价的。此处仅仅多阐述一点，这并不是一个微不足道的条件；并不一定仅仅在保守扩张的条件下两个逻辑系统才拥有相同的模型。这里仅举一个例子：考虑一个只有一个二元函数符号 ⨀ 和一个常量 e 的等式逻辑系统，且只有一条非逻辑公理如下：

(x⨀(((x⨀y)⨀z)⨀(y⨀e)))⨀(e⨀e)＝z.

(1)

如果你有足够的时间，你可以证明在我们的意义上，这个逻辑系统和我们一般见到的群的等式系统是等价的！尽管它们具有不同构的函数符号（它们的 signature 不同），但它们是能双向翻译的（bi-interpertable)。在这篇文章的后面我们还会看到其他等价的层次。

范畴对逻辑模型的推广

既然前面确定了我们在这篇文章中对逻辑以模型为基础的态度，我们现在便来仔细地谈谈在范畴论的角度逻辑系统的语义到底应该如何描述。对于单纯学习逻辑的读者来说，可能不知道的是逻辑的语义已经通过范畴论在现代数学家中有了极大的推广。

我们先以之前提到的群的等式逻辑为例。此时我们考虑一般的对群的公理化而不是上面 (1) 的公理化。即一个群是这样的一个结构：有一个对象G ，一个常项 e：G ，一个一元函数 i：G → G ，一个二元函数 m：G × G → G 。群的公理在等式逻辑中如下：

m(x，m)(y，z))＝m(m(x，y)，z)

m(i(x)，x)＝m(x，i(x))＝e

m(e，x)＝m(x，e)＝x (2)

值得注意的是，与 (2) 中的公理完全等价的，我们可以用交换图的形式重写上面的等式。感兴趣的读者可以先自己尝试一下。例如，乘法m 的结合律便可用下图的交换性来表示：

m×π₂

G×G×G → G×G

π₀×m ↓ ↓m

G×G → G

m

类似的，关于逆和幺元的公理可以用如下图表的交换性来表达：

1ɢ×e e×1ɢ

G×1 → G×G ← 1×G

π₀ ↘ ↓m ↙π₁

G

〈1ɢ，i〉〈i，1ɢ〉

G → G×G ← G

！ɢ ↓ ↓m ↓！ɢ

1 → G ← 1

e e

其中1ɢ 是 G 的恒等映射（identity）， 1 可以暂时理解为一个一元集合（singleton）， ！ɢ 表示从 G 到 1 唯一的映射。可能和大家原本的思维习惯不太相同的是，为了采用图表（态射）的语言，常量 e：G 被解释成为了从一元集合到 G 的一个映射 e：1 → G 。如果大家是第一次看见交换图表，可能会感觉这样的表述方式有一些奇怪。但稍加思考大家便可以验证，上面的表述与用等式逻辑写下的群的公理是完全等价的。

以此来看，上面采用交换图表重写群的公理并没有任何实际的意义，毕竟它们表达了相同的内容。但范畴论的抽象性在此时就能发挥出其巨大的优势了：这些图表并不一定要看成是范畴 Set 中的图表；在任何一个具有有限乘积（finite product）——0元乘积代表范畴的终对象（terminal object）——的范畴中，上面的图表都是有意义的！这意味着如果我们将上面的这些交换图表改换成群的定义，我们就不仅能在 Set 这个范畴中谈论什么是一个群。

比如，我们可以在Top 这个范畴考虑什么是一个群。首先， G 此时是一个拓扑空间。在它上面我们同样要求有群的乘法、逆和幺元，并且满足一般的群公理。唯一的不同是，由于我们是在 Top 这个范畴中考虑上方的图表，上面所有的映射必须都是连续的。因此我们可以总结如下：在 Top 中的群就是一个具有拓扑的（一般意义上的）群，且在这个拓扑下我们要求群的乘法和逆运算都是连续的。这正是数学家们一般所考虑的拓扑群（topological group）的定义！其它的许多定义也如此，比如李群（Lie group）就是光滑流形范畴中的一个群，一个代数群（algebraic group，group variety）则是代数簇（algebraic variety）范畴中的一个群。感兴趣的读者还可以考虑 Grp 或者 Vect 等范畴中的一个群是什么（群范畴中的群是阿贝尔群，其证明依赖于著名的 Eckmann-Hilton argument；线性空间范畴中每一个线性空间上都有唯一的一个群结构，是其上的加法）。

由此可见，范畴论的出现极大地推广了逻辑系统可以应用的范围。更为重要的是，通过逻辑与范畴的结合，我们再一次将不同数学分支不同范畴内”相似“的结构和定义严格地统一在一个概念下：它们都是群的等式逻辑系统在不同范畴下的模型！

在某种意义下范畴和逻辑是等价的。如果范畴与逻辑的结合仅仅停留在扩展了逻辑的语义上，我们显然还无法作出这个论断。但我想可能会令许多学习数理逻辑的读者惊讶的是，逻辑与范畴的结合远比上一节所描述的紧密的多！从本节的小标题可以看出，这一节想要说明的便是在我们这篇文章的大前提——即以模型为考虑基础——下逻辑系统和范畴是等价的，模型则与函子是等价的。在范畴逻辑中，这样的观点一般可以统称为函子语义（functorial semantics）。为了说给读者讲清楚这个道理，我们先从大家可能更为熟悉也更为简单的经典命题逻辑（classical propositional logic）和代数语义（algebraic semantics）讲起。

经典命题逻辑 = 布尔代数，模型 = 代数同态

假设我们有一个命题逻辑系统ℙ （为了简化，在此我们假设 ℙ 是经典命题逻辑，但其实完全相同的论述同样适用于其他任何一般的命题逻辑系统，我们仅将在最后提到这一点），其语言由 P 这个集合中的元素作为命题变元（propositional letter）。在一般的语义下， ℙ 的一个模型是对 P 中元素的一个二元赋值，即一个函数 h：P → 2 ，其中 2＝{0，1} 。我们把在命题变元为 P 是所有命题公式的集合记为 Fmlₚ ，这样的一个赋值函数 h 会进一步诱导出有公式的一个赋值：

∼h：Fmlₚ → 2. (3)

在逻辑上一般我们会说我们对∼h 的定义是递归的（recursive），即从命题变元的真值我们能够递归地定义所有命题公式的真值。从代数（或者说范畴）的角度来说，这个诱导出的赋值函数 ∼h 之所以存在是因为 Fmlₚ 是 P 上在我们给定的逻辑连词下的绝对自由代数（absolutely free algebra）。且注意，这样诱导出的 ∼h 是一个代数同态。例如对于合取（conjunction）我们有

∼h(φ∧ψ)＝∼h(φ)∧∼h(ψ). (4)

注意，(4) 的等式右边中的∧ 函数是在这个真值的集合 2 上定义的。对其它的逻辑连词类似的等式也是成立的。而这样的一个函数 h ，或者等价的 ∼h 是我们命题系统 ℙ 的一个模型当且仅当 ∼h 将所有 ℙ 中的公理都赋予真值 1。这便是一般命题逻辑语义的代数化表达。

而命题逻辑的代数语义则扩展了我们对命题逻辑语义的理解。此时我们不再要求必须从真值的角度给出命题逻辑的解释了，而我们可以在任何一个一般的布尔代数（Boolean algebra）当中解释我们的命题逻辑。对任意的布尔代数B ，对于我们命题系统 ℙ 的一个代数模型是一个函数 f：P → B ；同样，由于 Fmlₚ 是 P 上的自由代数， f 会诱导一个代数同态

∼f：Fmlₚ → B， (5)

将任意Fmlₚ 中的公式解释为 B 中的一个元素。同样，在逻辑的语境下我们会说 ∼f 是递归定义的；这样的一个函数 f ，或者等价的说一个代数同态 ∼f ，是 ℙ 的一个代数模型当且仅当 ∼f 把所有 ℙ 中的公理都映射到 B 的最大元 1。如果我们类比之前所提到的范畴论对逻辑系统可解释范围的推广，在命题逻辑的语境下只考虑真值 2 就与我们原先仅仅考虑 Set 这个范畴中的模型是完全类似的；在代数语义的语境下将命题逻辑的解释推广到任意布尔代数则与之前范畴论把一般的逻辑系统推广到任意（满足一定性质结构的）范畴是完全类似的。值得注意的是，(5) 式表明在代数语义下， ℙ 的一个模型则与满足一定条件的从 Fmlₚ 到 B 代数同态完全一致了！

此处讲一些题外话。我们在上面看到的2 和 Set 的对应并不是偶然，这与范畴论的推广 n-阶范畴（ n- category）有直接的联系。一般的范畴可以认为 1-阶范畴；因为一个范畴中包含的数据是一些物体（objects）和它们之间的态射（morphisms）。我们还有更高阶的范畴，如 2-阶范畴或者是 ∞-阶范畴。一个 2-阶范畴不仅包含物体和它们之间的态射的信息，它们的态射之间还存在态射。但令人惊讶的是，我们同样有 -1-阶范畴和 -2-阶范畴。事实上 2 在 0-阶范畴中所处的地位和 Set 在 1-阶范畴中所处的地位是完全一致的。感兴趣的同学可以参考 John Baez 的一个讲稿：Lectures on n-Categories and Cohomology 的前半部分，在 arxiz 上可以找到。当然，如果读者熟悉同伦类型（Homotopy Type）相信对这样的认识更不会陌生了。

回到我们的正题。在命题逻辑的代数语义下，除了我们能够把命题逻辑的语义推广到一般的布尔代数上，最重要的构造是 Lindenbaum-Tarski algebra！在此为了行文方便，我们将其简称为 LT 代数。对于每一个基于命题变元集P 的命题逻辑系统 ℙ ，我们都可以构造一个对应的 LT 代数，让我们记为 Bℙ 。它的构造其实是非常自然的：作为一个集合， Bℙ 不过是 Fmlₚ 的一个商集（quotient），其设置的等价关系也非常直观：

φ∼ℙ ψ ⇔ ⊢ℙ φ↔ψ， (6)

即Fmlₚ 中的两个命题公式 φ，ψ 是等价的当且仅当它们在逻辑系统 ℙ 下是证明等价的（provably equivalent）。容易看出这是一个良定义的等价关系，我们也定义 ℙ 的 LT 代数的元素就是这所有的等价类构成的集合 Bℙ ≅ Fmlₚ/∼ℙ。我们可以证明的是， Bℙ 的确是一个布尔代数，其上的代数运算由下式的形式给出：

[φ]ℙ∧[ψ]ℙ＝[φ∧ψ]ℙ， (7)

其它的连词类似，其中[φ]ℙ 表示 φ 在 ∼ℙ 关系下所在的等价类。你可以根据简单的逻辑系统的证明性质得出 (7) 是良定义的，即其定义并不依赖于等价类中的代表元的选择。(7) 式具有着更为重要的意义：它表明我们取等价类的操作 [·]ℙ 实际上定义了一个代数同态：

[·]ℙ：Fmlₚ ↠ Bℙ. (8)

之所以 (8) 中的箭头写成↠ 的形式是因为其不仅简单地是一个代数同态，它还是一个商映射。

我们有两种方式来看这个商映射[·]ℙ 。首先我们可以从代数的角度来看逻辑系统是在干什么。从代数的角度，我们会发现一个逻辑系统事实上是某种表示（presentation）的工具，即我们是通过一个命题变元集 P 和一些逻辑连词先生成了一个自由代数，再在逻辑系统中通过规定什么是证明来给出一个等价关系；我们最后得到的便是这个抽象的代数结构 Bℙ 的一个表示。如果读者不太明白这个观点，可以类比我们在交换代数中表示一个交换环的方式。例如考虑这个非常重要的环 ℤ[x]/x² ，其中 ℤ[x] 是一个自由变量的多项式环（polynomial ring）。多项式环之所以在交换代数中非常重要就是因为 ℤ[Ⅹ] 是集合 X 上的自由环。而环 ℤ[x]/x² 就是通过先生成一个自由环，再模掉一个由等式 x²＝0 所生成的等价关系所得到的。在逻辑中是完全类似的： Fmlₚ 是我们生成的自由代数，命题逻辑系统 ℙ 的公理则类似于上面的等式 x²＝0 ，而命题逻辑的证明系统则规定了由这些等式生成的等价关系是什么，最后你所得到的是一个模掉了这个等价关系之后的商代数 Bℙ 。和交换代数中所有的环都有一个如前所述的表示一样（即所有的交换环都同构于一个自由环模掉一个等价关系），所有的布尔代数也都可以写成用前述经典命题逻辑表示的形式。对于任意一个布尔代数 B 你可以几乎重言式地构造一个命题逻辑系统如下：将命题变元集就取为 |B| ，即 B 所对应的集合。命题系统的公理则可再次重言式地取为所有在 B 中成立的公式都作为公理。你很容易可见，这样的命题公理所表示的那个 LT 代数正是 B 本身。因此我们再次总结强调：从代数的观点来看，经典命题逻辑是所有布尔代数结构的表示。

⊢⊤

我们还可以从逻辑的角度来看待 (8) 中的商映射。我们前面说明了，当我们把命题逻辑的语义推广到一般的布尔代数上，任何一个从Fmlₚ 出发且将 ℙ 中的公理都映射到最大元的代数同态都确定了 ℙ 的一个代数语义模型。特别地，(8) 满足这样的条件：对于任意可证明的命题公式 ⊢ℙφ，我们均有 ⊢ℙφ↔⊤ ，因此在我们的等价类下 [φ]ℙ＝[⊤]ℙ 。这表明根据我们 LT 代数的定义， [·]ℙ 确定了一个 ℙ 的代数语义模型。更为重要的是，这个模型满足下面的性质：

⊢ℙφ⇔[·]ℙ╞ φ， (9)

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