类型论

对类(集合)作类型区别以排除悖论的一种关于类(集合)的逻辑理论，包括简单类型论和分支类型论。类型论由B．罗素在20世纪初，特别是在他1908年的文章中建立，后来经其他逻辑学家加以简化和改进，现在通常说的罗素的类型论，由K．哥德尔和A．塔尔斯基在他们的30年代的著作中首先采用。罗素在对悖论进行分析研究后，认为产生悖论的根源在于把一个类的分子和类本身同等看待，即采用了如下假定：一类事物可以包括本类的整体作为分子，例如，一切类所构成的总体还是一个类。更精确些说，这个假定是，一类事物可以包括只能根据此类的总体而定义的东西作为分子。罗素称这样的类为“不合法的总体”。承认“不合法的总体”就会引起恶性循环，导致悖论。为了排除悖论，罗素提出了类型论。

简单类型论 在简单类型论中(在本节的下文中，省去限制词“简单”)，把类区分为不同的类型：个体的类型为0，个体的类的类型为1，个体的类的类的类型为2，……，等等。每一对象都有一确定的类型，只有类型为n的东西才能说是否属于类型为n+1的类。因此，只能说某一类型的对象构成的类，某一类型的所有对象的类，等等，而说一类是否为其自身的一分子，所有类的类，等等，都是无意义的。把类区分为不同的类型，在类型论的语言中，就表现为包括无穷多不同类型的变元，每一变元都加上一右上标：x，y，z，x，…；x，y，z，x，…；x，y，z，x，…；……。0型的变元为个体变元：1型的变元的变程为类型为1的类，即以个体的类为值；2型变元的变程为类型为2的类，即以个体的类的类为值，等等。除了无穷多不同类型的变元外，类型论语言的初始符号包括∈。x∈y表示：x属于y，x是y的分子。公式的形成规则规定，x∈y是合式公式当且仅当i+1=j。因此，x∈x不是类型论中的合式公式，是无意义的。一变元在一公式中所有出现自然有相同的类型。但有可能出现这样的情形，x∈y，y∈x作为两个公式都是合式的，而当用联结词∧把它们联结组成一个公式x∈y∧y∈x时，却不是一个合式公式。因此，在公式的形成规则中还必须规定，对任一公式A，对在其中出现的所有变元都指定一类型后，A中形如x∈y的部分都合式，A才是合式的。对于公式x=y，只有当i=j时，才是合式的。此外，在把逻辑公理应用于类型论时，也必须满足有关公式的类型的要求。例如，公理xA(x)→A(y)，其中x和y的类型必须相同。在类型论中，除了无穷多不同类型的变元外，只需以∈(或者包括等词=)作为初始符号，而把性质和关系都代之以类来处理。即把一个性质F等同于由具有性质F的对象所构成的类｛x∶F(x)｝，把关系R等同于由具有关系R的对象x和y的有序对〈x，y〉所构成的类，即｛〈x，y〉∶R(x，y)｝。有序对〈x，y〉定义为类｛｛x｝，｛x，y｝｝。在类型论中，一个类的分子都具有相同的类型，当R为x和y之间关系时，x和y的类型不同，此时用｛x｝代替x，构成有序对〈｛x｝，y〉。通常把这样构造的简单类型论系统记作T。T的公理有4条：概括公理(模式)、外延公理、无穷公理和乘法公理。

概括公理模式：

其中φ(x)是任意公式，x在其中自由出现，y不在其中自由出现，左方的“( )”表示把φ(x)中除x外的自由变元都用全称量词约束起来。概括公理表示存在类y，y由所有满足条件φ(x)的n类型对象所组成。

外延公理：

外延公理表示由相同的分子组成的类相等，一个类由它的分子决定。

关于无穷公理和乘法公理的陈述，参见集合论的公理系统。

简单类型论系统T排除了已知的集合论悖论——罗素悖论、康托尔悖论和布拉里－福蒂悖论。由于x∈x不是合式公式，从而xx(即(x∈x))也不是合式公式，因此不存在得出罗素悖论的“不是自身的分子的类的类”，自然也就不能在系统中得出罗素悖论。关于康托尔悖论，只需注意到，在系统T中不存在所有类的类，因而也不存在所有基数组成的类。就所有n类型对象组成的类V来说，V的所有子类组成的类｛x∶xV｝，是一n+2类型的类，这个n+2类型的类既不是V的分子也不是V的子类，因此推不出导致康托尔悖论的｛x∶xV｝的基数小于V的基数。布拉里－福蒂悖论的情形类似。在包括无穷公理和乘法公理的系统T中，能够推出康托尔集合论，也就是说，罗素用类型论重建了康托尔集合论。从T能推出大部分数学。系统T和公理集合论ZFC系统一样为数学提供了一个基础。

分支类型论 简单类型论是罗素在1903年提出来的，1908年他又提出分支类型论。罗素提出分支类型论的一个原因是，在他提出简单类型论后，又发现了后来称为语义悖论的新的悖论，特别是1905年J．理查德发表了“实数可定义性悖论”。用简单类型论不能排除包括理查德悖论在内的语义悖论。另一个原因是在H．彭加勒影响下，罗素对逻辑和数学采取构造性的态度。彭加勒认为，产生悖论的根源在于非直谓定义，或者说决定一个类的条件的非直谓性质。非直谓性质导致恶性循环。罗素同意彭加勒的看法，提出了“(禁止)恶性循环原则”。对于同一类型的类或谓词来说，还可以区分不同层次。以个体谓词为例，一般个体谓词只涉及某些个体，而有的个体谓词，在它的定义中涉及了所有的个体谓词，这种个体谓词就比一般个体谓词的层次高。拿罗素所用的例子来说：

一个典型的英国人具有大多数英国人所具有的性质。

这里，“具有大多数英国人所具有的性质”也是一个性质，可是这性质涉及到个体谓词的全体，是高一层次的个体谓词。最低层次的谓词称为直谓的，涉及某一类型谓词的全体而又属于此类型的谓词称为非直谓的。就类来说，在它的定义中涉及某一类型的类的全体而又属于此类型的类是非直谓的。就前面说的概括公理模式来说，由条件φ(x)决定的类y就可能是非直谓的。让φ(x)为：z(x∈z∧z∈u)，根据概括公理模式有：

(*)满足简单类型论关于合式公式的类型的要求，但决定类y的条件φ(x)中的存在量词“z”涉及n+1型的类的全体，包括y自身在内。因此，由条件z(x∈z∧z∈u)决定的类y是非直谓的。根据(禁止)恶性循环原则，需要对概括公理模式中的条件φ(x)加上新的限制。按照分支类型论，同一类型的类又区分为不同的层次，高层次的类不能再作低层次的类看待，否则就将造成“不合法的总体”，导致恶性循环的错误。分支类型论的具体做法是，每一变元除加上右上标表示类型外，又加上一左上标表示层次，即把变元表示成：x。最低层次的类是直谓的。而概括公理模式的陈述则改变为：

如果在φ(x)中出现的类型为i+1的任何约束变元的最高层为j则

分支类型论系统记为RT。RT系统中排除了语义悖论。但达到这个目的却付出了很大的代价。在系统RT中，不能说一切个体的类如何，而必须区分层次。对于同一类型而不同层次的类构成的许多类，虽然同属于一个类，也不能笼统地说，此类的所有分子有什么性质，而必须分层次来作断定。实数就是这样的类，因之对实数也不能作一个单一的断定。分支类型论要排除非直谓定义，而非直谓定义在数学中是很多的。一非空实数集合S的最小上界u就是非直谓的。S的最小上界u即是S的并∪S，即

根据前面关于公式(*)的说明，可知u与约束变元y有相同的类型，u也在约束变元y的变程之中，因此是非直谓的。在RT中，不能证明定理：一非空的实数集合S如果有上界则有最小上界。很大一部分数学不能在RT中推出。这是与罗素的从逻辑推出数学的目的相违背的。为弥补这一严重缺陷，罗素引入一条可约性公理(可化归性公理)：

相应于某一类型和任何层次的每一类，存在一个同一类型且层次为1的类，此类与那个高层次的类包括相同的分子。

有了可化归性公理后，就可以用直谓的类代替非直谓的类，从而可以对一类的所有分子作出单一的判断。但是这实质上等于取消了分支类型论关于层次的区分，也去掉了分支类型论要求排除非直谓定义的构造性性质。不过分支类型论可以被认为是K．哥德尔的在集合论的元数学研究中起了重要作用的可构成性概念的一个先驱。在可构成集中，没有使用类型的概念，但使用了分层的概念。

关于类型论的元数学结果 已经在比较弱的假定下证明分支类型论(包括无穷公理但不包括可化归性公理)是协调的。根据哥德尔的不完全性定理，简单类型论T的协调性是不能在系统T自身中证明的。证明T的协调性比证明RT的协调性要求强得多的假定。但是对不包括无穷公理的简单类型论已经证明是协调的。根据哥德尔不完性定理，类型论相对于在所有主要解释下都真的公式(主要常真公式)是不完全的。但是L．亨金证明，类型论相对于在一切可靠解释(sound interpretation)下都真的公式是完全的。