类型理论的历史

类型理论最初是为了避免各种形式逻辑和重写系统中的悖论而产生的。后来，类型理论指的是一类形式系统，其中一些可以作为天真的集合理论的替代品，作为所有数学的基础。从《数学原理》到今天的证明助手，它一直与形式数学联系在一起。

罗素的类型理论的起源在一封信给戈特洛夫-弗雷格（1902年），伯特兰-罗素宣布他发现的悖论在弗雷格的Begriffsschrift。弗雷格迅速作出回应，承认了这个问题，并在关于层次的技术讨论中提出了一个解决方案。引用弗雷格的话顺便说一句，在我看来，一个谓词是以它自己为前提的表达方式并不确切。谓词通常是一个xxx层次的函数，这个函数需要一个对象作为参数，而不能有它自己作为参数（主语）。因此，我更愿意说一个概念是以它自己的扩展为前提的。他试图说明这可能是可行的，但似乎又从它那里拉回来。由于什么已经成为众所周知的罗素悖论的后果，弗雷格和罗素不得不迅速修正他们在印刷厂的作品。在罗素附加到他的《数学原理》（1903年）的附录B中，人们发现了他暂定的类型理论。这个问题困扰了罗素大约五年。威拉德-奎因(WillardQuine)对类型理论和类型的分支理论的起源作了一个历史性的概述：在考虑放弃类型理论（1905年）之后，罗素又提出了三种理论。在考虑放弃类型理论（1905年）之后，罗素依次提出了三种理论：人字形理论、大小限制理论、无类理论（1905-1906年），然后，又重新提出了类型理论（1908年以后），奎因认为，罗素引入表象变量的概念有以下结果。所有"和"任何"之间的区别。所有"是由普遍量化的约束（"表象"）变量表达的，它在一个类型的范围内，而"任何"是由自由（"真实"）变量表达的，它示意性地指任何未指定的事物，而不论其类型。奎因否定了这种约束变量的概念，认为除了类型理论的某个方面之外，它是毫无意义的。

奎因对夯实理论的解释如下。它之所以被称为类型，是因为一个函数的类型既取决于它的参数的类型，也取决于它（或它的表达式）所包含的表观变量的类型，如果这些变量超过参数的类型的话。斯蒂芬-克莱因在他1952年的《元数学导论》中这样描述类型的拉姆化理论。主要对象或个体（即不受逻辑分析的给定事物）被分配到一个类型（比如说0型），个体的属性被分配到1型，个体的属性的属性被分配到2型，等等；不属于这些逻辑类型之一的属性是不被允许的（例如，这使属性"可预测的"和"不可预测的"...超出逻辑的范畴）。一个更详细的说明将描述其他对象的公认类型，如关系和类。

然后，为了排除一个类型中的不可预测的定义，0型以上的类型被进一步分离成不同的顺序。因此，对于类型1来说，没有提到任何总体而定义的属性属于阶0，而用某一阶的属性的总体来定义的属性则属于下一个更高的阶。...但是，这种对秩序的分离使得我们不可能构建熟悉的分析，我们在上面看到的分析包含了暗示性的定义。为了摆脱这种结果，罗素提出了他的可还原性公理，该公理断言，对于任何属于最低阶以上的属性，都有一个0阶的共延属性（即完全相同的对象所具有的属性）。

但是，由于公羊理论的规定将被证明是（引用奎因的话）繁琐的，罗素在他的1908年数学逻辑为基础的类型理论也将提出他的可还原性公理。到了1910年，怀特海和罗素在他们的《数学原理》中，将用矩阵的概念进一步增强这个公理--一个函数的完全延伸性规范。从矩阵中可以通过泛化的过程推导出一个函数，反之亦然，即这两个过程是可逆的--（i）从矩阵泛化到函数（通过使用表观变量），以及（ii）通过表观变量的参数的值程替换来减少类型的反向过程。通过这种方法，可以避免不对称性。

1921年，埃米尔-波斯特（EmilPost）发展了真值函数及其真值表的理论，它取代了表变量的概念。