查看“︁ST类型论”︁的源代码

-{下面}-的系统是Mendelson的（1997: 289-93）'''ST'''。[[论域|量化的域]]被划分成上升的类型层次，带有所有的[[个体]]都被指派了一个类型。量化的变量确立范围只在一个类型上；所以底层逻辑是[[一阶逻辑]]。'''ST'''是"简单的"（相对于《[[数学原理]]》中的类型论）主要是因为任何[[关系 (数学)|关系]]的[[定义域|域]]和[[陪域]]的所有成员都必须是同一个类型的。

有一个最低的类型，它的个体没有成员并且是次最低类型的成员。最低类型的个体对应于特定集合论中的[[基本元素]]（urelement）。每个类型都有一个更高的类型，类似于在[[皮亚诺算术]]中[[后继函数|后继者]]。'''ST'''对是否有极大类型保持沉默，形成[[超限数]]个类型没有困难。这些因素，和回应于皮亚诺公理，使它方便和习惯于指派[[自然数]]到每个类型，开始于0给最低类型。这个类型论不要求自然数的先决定义。

'''ST'''的特有符号是加右上角标的变量和中缀<math>\in</math>。在任何给定的公式中，无角标的变量都有相同的类型，而有角标的变量（<math>x'</math>）取值于更高的类型上。'''ST'''的原子公式与两种形式，<math>x=y</math>（[[同一性]]）和<math>y \in x'</math>。[[中缀]]符号<math>\in</math>暗示了预想的[[模型论|释义]]，[[集合 (数学)|集合]]成员关系。

出现在同一性定义和外延和概括公理中所有变量都取值于连贯的两个类型之上。一个"低层"类型和另一个"高层"类型。取值于高层类型上的变量加角标；而取值于低层类型的变量不加。'''ST'''的一阶公式化排除在类型上的量化。所以每对连续的类型都要求它自己的外延和概括公理，如果“外延”和“概括”公理采用[[公理模式]]的方式取值于类型上就是可能的。

[[同一性]]定义：<math>x=y \Leftrightarrow \forall z' [x \in z' \leftrightarrow y \in z']</math>。

'''[[外延公理|外延]]'''[[公理模式]]：<math>\forall x[x \in y' \leftrightarrow x \in z'] \Rightarrow y'=z'</math>。

设Φ(''x'')表示包含[[自由变量]]''x''的任何[[一阶逻辑|一阶公式]]。

'''概括'''[[公理模式]]：<math>\exists z' \forall x[x \in z' \leftrightarrow \Phi(x)]</math>。

''备注'':相同类型的元素的任何搜集都可以形成更高类型的一个对象。概括公理有关于<math>\Phi (x)</math>也有关于类型。

'''[[无穷公理|无穷]]'''[[公理]]。存在着在最低层类型的个体之上的非空[[二元关系]]''R''，它是[[自反关系|反自反]]的、[[传递关系|传递]]的和[[完全关系|强连接]]的（<math>\forall x ,y [xRy \lor yRx]</math>）。

''备注'':无穷公理是'''ST'''的唯一真正的，并且本质上完全是数学的公理。''R''也是一个严格[[全序关系|全序]]，带有同一的[[定义域|域]]和[[陪域]]。如果0被指派给最低层类型（依次1是对（双元素集合，单元素集合），2是有序对），''R''的类型是3。这个公理强迫一个无穷集合的存在，因为只有''R''的（陪）域是[[无穷]]的时候它才可以被满足。如果关系以[[有序对]]的方式定义，这个公理要求有序对的先决定义；'''ST'''接受Kuratowski的定义。文献没有给出[[ZFC]]和其他集合论的[[无穷公理]]（存在归纳集合）不能结合于'''ST'''的理由。

'''ST'''披露了类型论可以制定得何其类似于[[公理化集合论]]。而'''ST'''更加精致的[[本体论]]，根源于现在所谓的“[[集合 (数学)|集合]]的[[迭代]]构想”，导致了远比有着更简单的[[本体论]]的常规集合论如[[ZFC]]简单得多的[[公理]]（[[模式]]）。[[公理化集合论]]起步于类型论，但是它的公理、[[本体论]]和术语不同于上面所述'''ST'''系统，还包括[[新基础]]和[[Scott-Potter集合论]]。

==参见==
* [[类型论]]

==参考文献==
{{refbegin}}
*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.&nbsp;267–286.
{{refend}}
{{reflist|colwidth=30em}}

[[Category:类型论]]