| has abstract
| - The following system is Mendelson's (1997, 289–293) ST type theory. ST is equivalent with Russell's ramified theory plus the Axiom of reducibility. The domain of quantification is partitioned into an ascending hierarchy of types, with all individuals assigned a type. Quantified variables range over only one type; hence the underlying logic is first-order logic. ST is "simple" (relative to the type theory of Principia Mathematica) primarily because all members of the domain and codomain of any relation must be of the same type.There is a lowest type, whose individuals have no members and are members of the second lowest type. Individuals of the lowest type correspond to the urelements of certain set theories. Each type has a next higher type, analogous to the notion of successor in Peano arithmetic. While ST is silent as to whether there is a maximal type, a transfinite number of types poses no difficulty. These facts, reminiscent of the Peano axioms, make it convenient and conventional to assign a natural number to each type, starting with 0 for the lowest type. But type theory does not require a prior definition of the naturals. The symbols peculiar to ST are primed variables and infix . In any given formula, unprimed variables all have the same type, while primed variables range over the next higher type. The atomic formulas of ST are of two forms, (identity) and . The infix symbol suggests the intended interpretation, set membership. All variables appearing in the definition of identity and in the axioms Extensionality and Comprehension, range over individuals of one of two consecutive types. Only unprimed variables (ranging over the "lower" type) can appear to the left of '', whereas to its right, only primed variables (ranging over the "higher" type) can appear. The first-order formulation of ST rules out quantifying over types. Hence each pair of consecutive types requires its own axiom of Extensionality and of Comprehension, which is possible if Extensionality and Comprehension below are taken as axiom schemata "ranging over" types.
* Identity, defined by .
* Extensionality. An axiom schema. . Let denote any first-order formula containing the free variable .
* Comprehension. An axiom schema. .Remark. Any collection of elements of the same type may form an object of the next higher type. Comprehension is schematic with respect to as well as to types.
* Infinity. There exists a nonempty binary relation over the individuals of the lowest type, that is irreflexive, transitive, and strongly connected: and with codomain contained in domain.Remark. Infinity is the only true axiom of ST and is entirely mathematical in nature. It asserts that is a strict total order, with a codomain contained in its domain. If 0 is assigned to the lowest type, the type of is 3. Infinity can be satisfied only if the (co)domain of is infinite, thus forcing the existence of an infinite set. If relations are defined in terms of ordered pairs, this axiom requires a prior definition of ordered pair; the Kuratowski definition, adapted to ST, will do. The literature does not explain why the usual axiom of infinity (there exists an inductive set) of ZFC of other set theories could not be married to ST. ST reveals how type theory can be made very similar to axiomatic set theory. Moreover, the more elaborate ontology of ST, grounded in what is now called the "iterative conception of set," makes for axiom (schemata) that are far simpler than those of conventional set theories, such as ZFC, with simpler ontologies. Set theories whose point of departure is type theory, but whose axioms, ontology, and terminology differ from the above, include New Foundations and Scott–Potter set theory. (en)
- 下面的系统是Mendelson的（1997: 289-93）ST。量化的域被划分成上升的类型层次，带有所有的个体都被指派了一个类型。量化的变量确立范围只在一个类型上；所以底层逻辑是一阶逻辑。ST是"简单的"（相对于《数学原理》中的类型论）主要是因为任何关系的域和陪域的所有成员都必须是同一个类型的。 有一个最低的类型，它的个体没有成员并且是次最低类型的成员。最低类型的个体对应于特定集合论中的基本元素（urelement）。每个类型都有一个更高的类型，类似于在皮亚诺算术中后继者。ST对是否有极大类型保持沉默，形成超限数个类型没有困难。这些因素，和回应于皮亚诺公理，使它方便和习惯于指派自然数到每个类型，开始于0给最低类型。这个类型论不要求自然数的先决定义。 ST的特有符号是加右上角标的变量和中缀。在任何给定的公式中，无角标的变量都有相同的类型，而有角标的变量（）取值于更高的类型上。ST的原子公式与两种形式，（同一性）和。中缀符号暗示了预想的释义，集合成员关系。 出现在同一性定义和外延和概括公理中所有变量都取值于连贯的两个类型之上。一个"低层"类型和另一个"高层"类型。取值于高层类型上的变量加角标；而取值于低层类型的变量不加。ST的一阶公式化排除在类型上的量化。所以每对连续的类型都要求它自己的外延和概括公理，如果“外延”和“概括”公理采用公理模式的方式取值于类型上就是可能的。 同一性定义：。 外延公理模式：。 设Φ(x)表示包含自由变量x的任何一阶公式。 概括公理模式：。 备注:相同类型的元素的任何搜集都可以形成更高类型的一个对象。概括公理有关于也有关于类型。 无穷公理。存在着在最低层类型的个体之上的非空二元关系R，它是反自反的、传递的和的（）。 备注:无穷公理是ST的唯一真正的，并且本质上完全是数学的公理。R也是一个严格全序，带有同一的域和陪域。如果0被指派给最低层类型（依次1是对（双元素集合，单元素集合），2是有序对），R的类型是3。这个公理强迫一个无穷集合的存在，因为只有R的（陪）域是无穷的时候它才可以被满足。如果关系以有序对的方式定义，这个公理要求有序对的先决定义；ST接受Kuratowski的定义。文献没有给出ZFC和其他集合论的无穷公理（存在归纳集合）不能结合于ST的理由。 ST披露了类型论可以制定得何其类似于公理化集合论。而ST更加精致的本体论，根源于现在所谓的“集合的迭代构想”，导致了远比有着更简单的本体论的常规集合论如ZFC简单得多的公理（模式）。公理化集合论起步于类型论，但是它的公理、本体论和术语不同于上面所述ST系统，还包括新基础和。 (zh)
|
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)