[科普中国]-分支类型论

基本介绍

分支类型论把类不仅划分成型，而且还划分成阶(亦称级)的类型论。英国罗素于1908年在《以类型论为基础的数理逻辑》一文中首次提出这一理论，并在《数学原理》(1910—1913)中对它作了系统的表述。罗素持“无类理论”的立场，他不是从类出发、而是从命题函数出发来构造分支类型论的。罗素对命题函数进行了严格的分层处理，最低层次的函数是个体，用字母表示个体变元，可称为0阶函数；比个体高一层次的是一阶函数，它是以个体为自变元或约束变元的函数，例如等等；更高一个层次的是二阶函数，它以个体和一阶函数为变元(自变元或约束变元)，且变元中至少包含一个一阶函数，例如，设为的一阶函数，则等都是二阶函数。一般的，如果一个函数中变元(自变元或约束变元)的最高阶是，则称这一函数是阶的。罗素遵从“恶性循环原则”，把命题函数区分为直谓的和非直谓的。对什么是直谓函数，他作了严格的定义：对一元函数而言，当函数的阶恰比它的自变元的阶高1时，称为直谓的，一般的，对于有个自变元的k元命题函数，若k个自变元的最高的阶为n，而函数的阶为，则称该k元函数是直谓的。由此可知，一阶函数都是直谓函数，但二阶和二阶以上的函数则划分为直谓与非直谓两种。罗素进而引入可归化公理：对任何命题函数，必存在一个与它形式等价的直谓函数。在这一公理和命题函数分层的基础上建立起类的理论并发展了数学。由于罗素的分支类型论过于复杂，近代数理逻辑学家在介绍分支类型论时往往采用与罗素不同的更为简洁的处理方式。这种处理方式以明确的类的观点为出发点，从“型”与“阶”(亦称为级)两个不同的方面进行分层。一方面按类进行外延的分层，即分为个体、个体的类或性质(谓词)，个体的类的类或个体的性质(谓词)的性质(谓词)，……分别称为0型，1型，2型，……;另一方面又对性质(谓词)作阶的划分，在定义方法上未涉及所有性质(谓词)的那些性质(谓词)是一阶的，它相当于直谓函数，下定义时仅涉及一阶性质(谓词)全体的那些性质(谓词)称为二阶的，……一般的，下定义时最高涉及阶性质(谓词)全体的那些性质(谓词)称为阶的，当阶时，这一性质(谓词)就相当于非直谓函数。分支类型论可避免一切已知的悖论，但是由于若不引入可归化公理就无法推出数学，而可归化公理的实际作用正是取消“阶”(亦称为级)的划分而保留“型”的划分，从而分支类型论就又将转化为简单类型论2。

描述论分析分支类型论是罗素所提出的一种解悖方案。罗素考察了其他悖论解决办法，觉得这些方案都不能令人满意。他认为“整个秘密的关键是逻辑类型的不同”，“自我指称”是所有悖论的共同特征，悖论就产生于一种恶性循环。这种恶性循环是定义其成员时要涉及集体的整体造成的。因此，只有消除恶性循环，才能避免悖论。正是根据“凡是涉及一个集体的整体的对象，它本身不能是该集体的成员”这样一个原则，罗素提出了他的分支类型论3。

罗素把论域分成类型，提出只有在这样的情况下才能谈到它们的全体：满足某一给定条件的所有对象都属于同一类型；因此一个类的所有成员必定全都具有同一类型。任何性质的分类都必须按照它所属的对象类型：给定的、未作逻辑分析的原始客体或个体属于第一层次类型，个体的性质属于第二层次类型，个体的性质的性质属于第三层次类型，以此类推。同时，对于基本类型以上的类型，还要给同一类型中的不同性质作出“级”的划分：下定义时没有提到任何总体性质的性质属于第一级，下定义时用到某级性质的总体的性质属于第二级，以此类推。由于任何性质都属于一定的类型和级，而级是在类型之内划分的，所以这种理论被叫作“分支类型论”。

根据“分支类型论”，如果我们作出这样的规定，每一类型中的对象都不能以这一类型的整体及更高类型中的对象定义，每一类型的性质只有当用于它之下的那个类型的对象时才具有意义；而且，每一级的性质都不能以这一级性质的总体和更高的级中的性质定义，凡是只能借助属于第13级的“所有性质”来定义的第n+1级的性质，决不能包含在第n级的性质中，如果不能具体指明属级，则涉及“所有性质”的表达式没有意义。由此，我们就能在整个系统中排除悖论。

这种解决方法非常好，分支类型论的确由此排除了一些悖论，但问题是，在排除一些悖论的同时也把许多合理的东西排除在外了。特别是一些重要的数学定理因而不能被证明，而一些必要的数学概念的定义则变成非法的。而且，一方面，分支类型论的悖论消解只是一种形式上的解决，在哲学层面，这种解悖方案始终不能令人满意；另一方面，分支类型论禁例太严，以致无法推出全部数学。因此，就RZH标准的“充分宽广”来说，分支类型论也遇到严重困难。正如哈克指出的：

无论在形式的水平上，还是在哲学的水平上，罗素的理论都陷入了困难。在形式上，罗素的做法有“因噎废食”的危险，他的限制避免了悖论却也限制了某些必要的推论。

分支类型论对于解决集合论悖论有效，毫无疑问抓住了其规定(类的规定)的关键，从而在形式上富有成效地解决了集合论悖论的构成问题。但它作为哲学上解决方法的恶性循环原则却没有真正深入哲学层面。恶性循环仍然属于悖论形成的逻辑形式方面的内容，它只是悖论而且是某些悖论形成的逻辑形式条件。违反这一原则并不一定导致悖论。而且被这一原则排除的循环并不一定是恶性的。因而罗素的解悖理论不是陷入形式上和哲学上的双重困难，而是因为其哲学的解决方法的实际缺失必然导致形式上的解决方法因不彻底而不可避免地陷入困难。

罗素解悖方案的实质是富有成效地从形式的解决方法人手，止于哲学的解决方法。这样必定导致其形式上的努力不受哲学基础的范导，或者说缺少哲学大背景——大坐标的参照和定位而“恶性”蔓延，从而有与“因噎废食”原则相悖的倾向。它所制定的限制在避免了悖论产生的同时，也限制了一些必要的推论。罗素将数学还原为逻辑的努力之所以没有获得最后成功，正是因为其类和级的限制不是建立在规定的相对性的基础之上，没有注意到类是级的规定，既与客体的属性相关，也与主体的认识目的和实践需要相关，因此与人类学特性相关，从而把类和级作了纯客观化的理解，形成了一种脱离主观规定的绝对的限制，堵死了许多必定建立在相对规定基础上的重要数学内容。

由于类型论起作用是因为类型的区分隔离了不同语言层次间规定发生冲突，只是一种形式上的处理，因而没有理论支撑，只是一种描述限制。正如戈德斯坦指出的：

罗素和怀特海把他们的规则称作“类型论”，但问题是这些规则后面根本没有真正的理论，就像他们自己沮丧承认的那样；对于为什么某种集合被允许而其他的不被允许，除了说如果人们允许不可允许的集合，那么他的系统里将会发生非常糟糕的事情之外，没有给出任何解释。他们的形式系统是通过法令(fiat)达成一致的。

“恶性循环”原则不成立，由此建立起来的“分支类型论”也行不通。分支类型论解悖方案不能解决悖论问题，罗素本人因此最后成了一个不可知论者。他在晚年时感叹道，“我所一直寻求的数学中的光辉的确定性，在令人困惑的迷宫中丧失了。”“寻求完美、最后定论和确定性的希望破灭了。”

作为一种形式上的解悖方案，分支类型论不仅因禁例太多而与数学不相协调，而且没有能够从哲学层面面对悖论问题。这一点，通过“理发师定理”的漫画式放大，将变得更为清楚。

20世纪60年代初，英国逻辑学家汤姆逊(J.F.Thomson)提出一条“定理”，试图找到“集合论悖论”的统一解。另一位英国逻辑学家麦基(J.L.Mackie)对其进行研究后把它叫作“理发师定理”。这条定理是这样的：

设S是一个集合，R是一个关系，这个关系至少在S上有定义。则S中不存在这样一个元素y，这个y仅仅同S中所有这样一些元素有关系R：这些元素自己同自己无R关系。

用“理发师定理”消解“理发师悖论”很简单。在所有萨尔维村的村民这个集合中，任取两个村民x，y，这两个村民可以是同一个人，那么，“x给y刮胡子”不是真的就是假的，即是说，这表明“……给……刮胡子”这个二元关系至少在该集合上有定义。由“理发师定理”可知，在萨尔维村的村民中根本不存在这样的理发师，他给且只给所有不给自己刮胡子的人刮胡子。这样一个“捣乱”的理发师根本就不存在，也就意味着根本不存在什么理发师悖论。

用“理发师定理”消解“目录障论”也很简单。

“目录障论”是“罗素悖论”的又一个通俗“版本”，由瑞士数学家贡赛斯(Gonseth)提出。我们可以把所有可能的目录分为两大类：一类是不把自身收入在内的目录，一类则是把自身收入在内的目录。所有不把自身收入在内的目录构成一个总目录，这个总目录本身也是目录。既然它也是目录，便有个是否把自身收入在内的问题。这样，悖理性就产生了：如果该总目录不把自身收入在内，它便把自身收入在内；如果它不把自身收人在内，则又把自身收入在内。

在目录悖论中，从所有可能的目录构成的集合中，任取两个目录x，y，这两个目录可以是相同的，则“x收入y”不是真的就是假的。即“……收入……”这个二元关系至少在该集合上有定义。由“理发师定理”可知，根本就不存在这样一个目录，它收入且仅收入所有那些不把自身收入在内的目录。这样一个“麻烦”的目录根本就不存在，也就意味着根本就不存在什么目录悖论。

也就是说，像罗素所说的“理发师”即使存在，也不在形式逻辑能解释和接受的范围。形式逻辑只能把悖论一笔抹除。

“理发师定理”是一条“局限性定理”，它企图证明逻辑悖论具有“局限性”。尽管人们认为事实上这只是证明了形式逻辑本身的局限性，但这条定理在消解悖论上有一定作用。根据“理发师定理”，汤姆逊解释了理发师悖论、形容词悖论、罗素悖论和理查德悖论。据汤姆逊论证，这些悖论都能变成“定理”，有的还可以算作数学定理。他认为罗素的“类型论”和塔尔斯基的“语言层次论”等规避悖论的方法，实质上与这个方法大同小异，而这个定理则更简洁。

在“理发师定理”发表十多年后，有人提出了异议。麦克伊(J.L.Mackie)就对它作了这样的评论：

这种证明解除了悖论吗?显然没有。它摆脱了理发师……但它不能摆脱罗素悖论或格雷林悖论，因为我们手上仍然有一个矛盾存在：一方面是“理发师定理”的适当解释；另一方面则显而易见地存在着不包含自身为元素的集合……这一个矛盾(“罗素集”是又不是自身的元素)，靠了否认这样的集合的存在而被解除，但一个更深刻的矛盾仍然存在：即否认这个集合的存在和这个集合的显然存在之间的矛盾。汤姆逊的解除方法自身成为这个更深的矛盾中的一方。

而且，“理发师定理”也不能直接用于“说谎者悖论”的解决。“理发师定理”像是“汤姆逊剃刀”，可以消解“理发师悖论”和“目录悖论”，但这把“剃刀”对“罗素悖论”却无能为力。

“理发师定理”的实质的确就是：不但“矛盾即荒谬”，而且“矛盾不存在”。汤姆逊的做法，事实上是一种把悖论变成规定的做法。的确，规定有时候可以是“蛮横”、“不讲理的”，但规定至少有个是否合理的问题。“理发师定理”之所以只能摆脱“理发师”而不能摆脱“罗素集”，就因为“理发师”是经验的而罗素集是逻辑的。经验的东西可以存在也可以不存在，而逻辑的东西是否存在是有其逻辑必然的。

“理发师定理”本身是新作出的一个规定。用“理发师定理”去消解“理发师悖论”和“目录悖论”，无非就是通过运用这个规定，将“只给所有不给自己刮胡子的人刮胡子的理发师”和“收入且仅收人所有那些不把自身收入在内的目录”给否定了。这里与其说是消解悖论，不如说在阉割悖论，把悖论变成了一般命题，把公鸡变成了阉鸡。这样消解理发师悖论和目录悖论当然是再容易不过了。“理发师定理”之所以不能用于消解罗素悖论，是因为这两个悖论所涉及的是有限集合，而罗素悖论涉及大全集，即所有集合的集合。而大全集并不存在。因此用“理发师定理”并不能否定“罗素集”的存在。正因为这个“定理”仅局限在理发师悖论和目录悖论的消解，所以英国逻辑学家麦基(J.L.Mackie)把它称作“理发师定理”的确是不无贬义的。其实，即使我们能够通过“理发师定理”否定“罗素集”的存在，也不能完全解决罗素悖论，这样做也更不是在有效解决悖论问题。

当我们进一步深入描述的深层就会看到，事实上，简单地否定“给且只给不给自己刮胡子的人刮胡子的理发师”、“不收入自身的目录的总目录”和“罗素集”，只是对悖论的消极的消解，并没有真正进入悖论的殿堂。因为从描述的角度看，这些在相应的描述中都是一些有意义的规定。在描述中，这些规定的存在是可以有不同层次含义的，不能简单地予以否定，即使“最大的自然数”这样的规定，也是不能简单地否定其存在及其意义的。与其说“最大的自然数是不存在的”，不如说我们不能写出一个最大的自然数。由此，我们也可以看到“最大的自然数”的描述意义。

通过否定“给且只给不给自己刮胡子的人刮胡子的理发师”、“收入且仅收入所有那些不把自身收入在内的目录”乃至“罗素集”的存在消解悖论，只是对悖论的头痛医头脚痛医脚式处理，没有深人悖论问题的深层。只有不断深入描述的深层，我们才可能把悖论问题的研究真正引向深入，而这已经是从描述人手探索悖论问题的开始。

从描述人手，类如“理发师”那样的概念从让人们左右为难的“怪物”变成了人类描述和认识中的一个新的梯阶；从而处理这些概念也不再是回避一个无从下手的难题。这样一来，“理发师定理”不再是一个无效排除“理发师”存在的规定，而是从一个层面向另一个更高层面过渡的界碑，人类描述(和规定)系统中分类的新依据。

“理发师定理”事实上是一把阉刀，其运用就是用规定阉割悖论。用规定来否定一个现象的存在，终究类似掩耳盗铃或鸵鸟行为，这样是回避不了悖论的。事实上，如果把“理发师定理”那样的东西看作规定，并进一步把这一规定的地位弄清楚，我们就会发现这是我们描述中的正常现象。只要我们不是把这些规定作为阉割悖论的阉刀，而是把它作为描述的界标，我们就能意识到人类描述的特殊处境。而从这一特殊处境我们可以看到，正是这些规定把人类描述推向一个个新的更高层面。

正是由于没有把“理发师”等作为整个描述和规定系统中的一个新界标，罗素的类型论未能解决而只是回避了集合论悖论，诚如杨熙龄先生谈到用类型论解决目录悖论时所指出的：

那么，罗素的“类型论”能否帮助卡里马楚斯摆脱困境呢?能，但是那等于是建议卡里马楚斯不要编这种目录，连那第一大类：“自身列入的目录的总目”也不要编，甚至连“自身列入的目录”也不要编。因为按照“类型论”的原则是：“一个集合不能是这个集合本身的元素；集合不准包含它自身在内。”如果要说甲属于乙，乙必须在“类型”上比甲高一级。因此，如果有一部目录包含它自己的名目，即违反“类型论”规则，而成为“无意义”。这样当然再不会出现一部目录列入不列入自身的问题。

那么卡里马楚斯虽然摆脱了困境，可是也就无事可做了。卡里马楚斯将会陷入新的困惑境地；毛病出在哪儿，是出在这种区分法上?两大类一分开之后，倒弄得不可分了?……

同罗素的“类型论”相比，许多悖论的推理倒显得很自然、很合理。

规定不准有这样一部“总目”，只显得这种规定自身的无力。目录可以有列入自身者，这是客观的事实，而罗素的“类型论”强加禁止。既有“列入自身”者，当然也会出现“不列入自身”者。这是符合“矛盾律”的，“矛盾律”要求这样划分。那么可以说后来的矛盾竟是因为执行了“矛盾律”才产生的，可是“矛盾律”又不允许这部“总目”既被列入又不被列入自身，“排中律”还规定要么列入自身，要么不列入自身，两者必居其一。这仿佛“矛盾律”和“排中律”在挑它们自己的刺儿。

其实，不仅罗素，理查德也采用了类似的解悖办法。在发表以他命名的悖论的同时，理查德也提出了他的解悖办法：避免一个集合中包含这样的元素，这个元素本身需要借助于这个集合来定义。理查德认为，只要不允许借助于一个总体来定义一个对象，而该对象本身又属于这一总体的情况存在，就能避免理查德悖论和其他悖论。这是一些典型的对悖论的形式化解决办法，只停留于对悖论问题的消极而不彻底的解决。

当一个描述超出或应用于作为其前提的规定时，描述会失去意义。这并不是描述或规定本身不合理，而是超出了原来的描述范围，必须有新的规定才能推进描述的发展。如果只停留于原先的描述框架，就会陷于悖理性，正像如果没有新的观念(规定、定律等)，相对论现象只能停留在牛顿力学描述框架中，以一种悖理性的方式存在3。