ST类型理论

下面的系统是门德尔森(1997,289-293)的ST类型理论。ST相当于罗素的夯实理论加上还原性公理。量化的领域被划分为类型的升序层次，所有的个体都被赋予一个类型。量化变量的范围只有一种类型；因此，基础逻辑是一阶逻辑。ST是简单的（相对于《数学原理》的类型理论而言），主要是因为任何关系的域和共域的所有成员都必须是同一类型。有一个最低的类型，其个体没有成员，是第二最低类型的成员。最低类型的个体对应于某些集合理论的urelements。每个类型都有一个下一个更高的类型，类似于Peano算术中的继承者概念。虽然ST对是否存在一个xxx的类型保持沉默，但无穷多的类型并不构成困难。这些事实，让人联想到皮亚诺公理，使得为每个类型分配一个自然数变得方便和传统，从最低类型的0开始。但类型理论并不要求事先对自然数进行定义。ST特有的符号是底层变量和infix所有出现在同一性定义以及扩展性和理解性公理中的变量，都在两个连续类型中的一个个体上活动。只有未定型的变量（范围在较低的类型上）可以出现在''的左边。而在它的右边，只有底层变量（范围在较高类型上）可以出现。ST的一阶表述排除了对类型的量化。因此，每一对连续的类型都需要它自己的扩展性公理和理解性公理，如果下面的扩展性和理解性被当作范围于类型的公理模式，这就是可能的。在最低类型的个体上，存在一个非空的二元关系R{displaystyleR}，该关系是非反射性的、传递性的、强连接的。{displaystyleforallx,y[xneqyrightarrow[xRyveeyRx]]]}，并且其子域包含在xRy和yRx之间。并且代码域包含在域中。备注。无穷大是ST的xxx真正的公理，完全是数学性质的。它宣称{displaystyleR}是一个严格的总秩序，其编码域包含在域中。

是一个严格的全能秩序，它的域中包含一个编码域。如果0被分配给最低的类型，那么，R的类型{displaystyleR}的类型是3。只有当R{displaystyleR}的（共）域为3时，才能满足无穷大。{displaystyleR}的（共）域是无限的，从而迫使一个无限域的存在。的（共）域是无限的，从而迫使一个无限集的存在。如果关系是用有序对来定义的，那么这个公理就需要事先对有序对进行定义；适应ST的Kuratowski定义就可以了。文献没有解释为什么其他集合理论的ZFC的通常的无限性公理（存在一个归纳集）不能与ST结合。ST揭示了如何使类型理论与公理集合理论非常相似。此外，ST的更复杂的本体论，以现在所谓的集合的迭代概念为基础，使得公理（图式）远比那些传统的集合理论，如ZFC，更简单的本体论简单。集合理论的出发点是类型理论，但其公理、本体论和术语与上述理论不同，包括新基础和斯科特-波特集合理论。基于平等的Church类型理论的公式已经被Church的两个学生LeonHenkin和PeterB.Andrews广泛地研究。由于ST是一种高阶逻辑，而在高阶逻辑中，人们可以用逻辑等价物和量词来定义命题连接词，1963年亨金发展了一种基于平等的ST的表述，但他在其中把注意力限制在命题类型上。