ST类型论 下面的系统是Mendelson的 ST量化的域被划分成上升的类型层次带有所有的个体都被指派了一个类型量化的变量确立范围只在一个类型上所以底层逻辑是一阶逻辑ST是简单的相对于数学原理中的类型论主要是因为任何关系的域和陪域的所有成员都必须是同一个类型的 有一个最低的类型它的个体没有成员并且是次最低类型的成员最低类型的个体对应于特定集合论中的基本元素urelement每个类型都有一个更高的类型类似于在皮亚诺算术中后继者ST对是否有极大类型保持沉默形成超限数个类型没有困难这些因素和回应于皮亚诺公理使它方便和习惯于指派自然数到每个类型开始于给最低类型这个类型论不要求自然数的先决定义 ST的特有符号是加右上角标的变量和中缀  displaystyle in  在任何给定的公式中无角标的变量都有相同的类型而有角标的变量 x  displaystyle x 取值于更高的类型上ST的原子公式与两种形式 x  y displaystyle xy 同一性和 y  x  displaystyle yin x 中缀符号  displaystyle in  暗示了预想的释义集合成员关系 出现在同一性定义和外延和概括公理中所有变量都取值于连贯的两个类型之上一个低层类型和另一个高层类型取值于高层类型上的变量加角标而取值于低层类型的变量不加ST的一阶公式化排除在类型上的量化所以每对连续的类型都要求它自己的外延和概括公理如果外延和概括公理采用公理模式的方式取值于类型上就是可能的 同一性定义 x  y   z   x  z   y  z   displaystyle xyLeftrightarrow forall zxin zleftrightarrow yin z  外延公理模式  x  x  y   x  z    y   z  displaystyle forall xxin yleftrightarrow xin zRightarrow yz  设Φx表示包含自由变量x的任何一阶公式 概括公理模式  z   x  x  z   Φ  x   displaystyle exists zforall xxin zleftrightarrow Phi x  备注相同类型的元素的任何搜集都可以形成更高类型的一个对象概括公理有关于 Φ  x  displaystyle Phi x 也有关于类型 无穷公理存在着在最低层类型的个体之上的非空二元关系R它是反自反的传递的和强连接的  x  y  x R y  y R x  displaystyle forall xyxRylor yRx  备注无穷公理是ST的唯一真正的并且本质上完全是数学的公理R也是一个严格全序带有同一的域和陪域如果被指派给最低层类型依次是对双元素集合单元素集合是有序对R的类型是这个公理强迫一个无穷集合的存在因为只有R的陪域是无穷的时候它才可以被满足如果关系以有序对的方式定义这个公理要求有序对的先决定义ST接受Kuratowski的定义文献没有给出ZFC和其他集合论的无穷公理存在归纳集合不能结合于ST的理由 ST披露了类型论可以制定得何其类似于公理化集合论而ST更加精致的本体论根源于现在所谓的集合的迭代构想导致了远比有着更简单的本体论的常规集合论如ZFC简单得多的公理模式公理化集合论起步于类型论但是它的公理本体论和术语不同于上面所述ST系统还包括新基础和ScottPotter集合论