ST类型论
下面的系统是Mendelson的（1997: 289-93）ST。量化的域被划分成上升的类型层次，带有所有的个体都被指派了一个类型。量化的变量确立范围只在一个类型上；所以底层逻辑是一阶逻辑。ST是"简单的"（相对于《数学原理》中的类型论）主要是因为任何关系的域和陪域的所有成员都必须是同一个类型的。
有一个最低的类型，它的个体没有成员并且是次最低类型的成员。最低类型的个体对应于特定集合论中的基本元素（urelement）。每个类型都有一个更高的类型，类似于在皮亚诺算术中后继者。ST对是否有极大类型保持沉默，形成超限数个类型没有困难。这些因素，和回应于皮亚诺公理，使它方便和习惯于指派自然数到每个类型，开始于0给最低类型。这个类型论不要求自然数的先决定义。
ST的特有符号是加右上角标的变量和中缀。在任何给定的公式中，无角标的变量都有相同的类型，而有角标的变量（）取值于更高的类型上。ST的原子公式与两种形式，（同一性）和。中缀符号暗示了预想的释义，集合成员关系。
出现在同一性定义和外延和概括公理中所有变量都取值于连贯的两个类型之上。一个"低层"类型和另一个"高层"类型。取值于高层类型上的变量加角标；而取值于低层类型的变量不加。ST的一阶公式化排除在类型上的量化。所以每对连续的类型都要求它自己的外延和概括公理，如果“外延”和“概括”公理采用公理模式的方式取值于类型上就是可能的。
同一性定义：。
![{\displaystyle x=y\Leftrightarrow \forall z'[x\in z'\leftrightarrow y\in z']}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f538805b00ad49b5797aa9eac9a5a14c747065a5)
![{\displaystyle \forall x[x\in y'\leftrightarrow x\in z']\Rightarrow y'=z'}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2ff5d9fb42ed7ed0e147a4ca2eaaad58632c3b16)
概括公理模式：。
![{\displaystyle \exists z'\forall x[x\in z'\leftrightarrow \Phi (x)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/eb4a658d2361622ebd2a3a36796fcd632e6094da)
备注:相同类型的元素的任何搜集都可以形成更高类型的一个对象。概括公理有关于也有关于类型。
无穷公理。存在着在最低层类型的个体之上的非空二元关系R，它是反自反的、传递的和强连接的（）。
![{\displaystyle \forall x,y[xRy\lor yRx]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cfb6c11a0acd492a9a947672b8014daf418592bb)
备注:无穷公理是ST的唯一真正的，并且本质上完全是数学的公理。R也是一个严格全序，带有同一的域和陪域。如果0被指派给最低层类型（依次1是对（双元素集合，单元素集合），2是有序对），R的类型是3。这个公理强迫一个无穷集合的存在，因为只有R的（陪）域是无穷的时候它才可以被满足。如果关系以有序对的方式定义，这个公理要求有序对的先决定义；ST接受Kuratowski的定义。文献没有给出ZFC和其他集合论的无穷公理（存在归纳集合）不能结合于ST的理由。
ST披露了类型论可以制定得何其类似于公理化集合论。而ST更加精致的本体论，根源于现在所谓的“集合的迭代构想”，导致了远比有着更简单的本体论的常规集合论如ZFC简单得多的公理（模式）。公理化集合论起步于类型论，但是它的公理、本体论和术语不同于上面所述ST系统，还包括新基础和Scott-Potter集合论。
参见
参考文献
- Mendelson, Elliot, 1997. Introduction to Mathematical Logic, 4th ed. Chapman & Hall.
- W. Farmer, The seven virtues of simple type theory, Journal of Applied Logic, Vol. 6, No. 3. (September 2008), pp. 267–286.