ST type theory

The following system is Mendelson's (1997, 289–293) ST <a href="/facts/Type_theory/xj0xzVqI">type theory</a>. 
ST is equivalent with Russell's ramified theory plus the <a href="/facts/Axiom_of_reducibility/zTW6FE35">Axiom of reducibility</a>. 
The <a href="/facts/Domain_of_discourse/T1WRQxx6">domain of quantification</a> is partitioned into an ascending hierarchy of types, with all <a href="/facts/Individual/hJbTjS2x">individuals</a> assigned a type. Quantified variables range over only one type; hence the underlying logic is <a href="/facts/First-order_logic/lcISqWIg">first-order logic</a>. ST is "simple" (relative to the type theory of <a href="/facts/Principia_Mathematica/7ufeceV4">Principia Mathematica</a>) primarily because all members of the <a href="/facts/Relation_(mathematics)/HjblDaMy">domain</a> and <a href="/facts/Relation_(mathematics)/HjblDaMy">codomain</a> of any <a href="/facts/Relation_(mathematics)/HjblDaMy">relation</a> 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 <a href="/facts/Urelement/YLbuKp37">urelements</a> of certain set theories. Each type has a next higher type, analogous to the notion of <a href="/facts/Successor_function/R1hhkSEG">successor</a> in <a href="/facts/Peano_arithmetic/DhhDnNug">Peano arithmetic</a>. While ST is silent as to whether there is a maximal type, a <a href="/facts/Transfinite_number/m2oTjXaj">transfinite number</a> of types poses no difficulty. These facts, reminiscent of the Peano axioms, make it convenient and conventional to assign a <a href="/facts/Natural_number/u65og8JE">natural number</a> 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 <a href="/facts/Infix_operator/LY0dMhay">infix operator</a> 
 
 
 
 ∈
 
 
 {\displaystyle \in }
 
. In any given formula, unprimed variables all have the same type, while primed variables (
 
 
 
 
 x
 ′
 
 
 
 {\displaystyle x'}
 
) range over the next higher type. The <a href="/facts/Atomic_formula/s9WMnbqT">atomic formulas</a> of ST are of two forms, 
 
 
 
 x
 =
 y
 
 
 {\displaystyle x=y}
 
 (<a href="/facts/Identity_(mathematics)/LR46j4uR">identity</a>) and 
 
 
 
 y
 ∈
 
 x
 ′
 
 
 
 {\displaystyle y\in x'}
 
. The infix-operator symbol 
 
 
 
 ∈
 
 
 {\displaystyle \in }
 
 suggests the intended <a href="/facts/Model_theory/vLWVV8sQ">interpretation</a>, 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 '
 
 
 
 ∈
 
 
 {\displaystyle \in }
 
', 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 <a href="/facts/Axiom_scheme/vKNTz5IT">axiom schemata</a> "ranging over" types.

<ul><li>Identity, defined by 
 
 
 
 x
 =
 y
 ↔
 ∀
 
 z
 ′
 
 [
 x
 ∈
 
 z
 ′
 
 ↔
 y
 ∈
 
 z
 ′
 
 ]
 
 
 {\displaystyle x=y\leftrightarrow \forall z'[x\in z'\leftrightarrow y\in z']}
 
.</li>
<li><a href="/facts/Axiom_of_extensionality/sz0G1dWV">Extensionality</a>. An <a href="/facts/Axiom_schema/vKNTz5IT">axiom schema</a>. 
 
 
 
 ∀
 x
 [
 x
 ∈
 
 y
 ′
 
 ↔
 x
 ∈
 
 z
 ′
 
 ]
 →
 [
 
 y
 ′
 
 =
 
 z
 ′
 
 ]
 
 
 {\displaystyle \forall x[x\in y'\leftrightarrow x\in z']\rightarrow [y'=z']}
 
.</li></ul>
Let 
 
 
 
 Φ
 (
 x
 )
 
 
 {\displaystyle \Phi (x)}
 
 denote any <a href="/facts/First-order_logic/lcISqWIg">first-order formula</a> containing the <a href="/facts/Free_variable/ndWnXXYs">free variable</a> 
 
 
 
 x
 
 
 {\displaystyle x}
 
.

<ul><li>Comprehension. An <a href="/facts/Axiom_schema/vKNTz5IT">axiom schema</a>. 
 
 
 
 ∃
 
 z
 ′
 
 ∀
 x
 [
 x
 ∈
 
 z
 ′
 
 ↔
 Φ
 (
 x
 )
 ]
 
 
 {\displaystyle \exists z'\forall x[x\in z'\leftrightarrow \Phi (x)]}
 
.</li></ul>
Remark. Any collection of elements of the same type may form an object of the next higher type. Comprehension is schematic with respect to 
 
 
 
 Φ
 (
 x
 )
 
 
 {\displaystyle \Phi (x)}
 
 as well as to types.
<ul><li><a href="/facts/Axiom_of_infinity/kDWQE32v">Infinity</a>. There exists a nonempty <a href="/facts/Binary_relation/r9BwGgaK">binary relation</a> 
 
 
 
 R
 
 
 {\displaystyle R}
 
 over the individuals of the lowest type, that is <a href="/facts/Reflexive_relation/NzTytEg9">irreflexive</a>, <a href="/facts/Transitive_relation/9r90y50r">transitive</a>, and strongly connected: 
 
 
 
 ∀
 x
 ,
 y
 [
 x
 ≠
 y
 →
 [
 x
 R
 y
 ∨
 y
 R
 x
 ]
 ]
 
 
 {\displaystyle \forall x,y[x\neq y\rightarrow [xRy\vee yRx]]}
 
 and with codomain contained in domain.</li></ul>
Remark. Infinity is the only true axiom of ST and is entirely mathematical in nature. It asserts that 
 
 
 
 R
 
 
 {\displaystyle R}
 
 is a strict <a href="/facts/Total_order/xnTtmuYJ">total order</a>, with a <a href="/facts/Relation_(mathematics)/HjblDaMy">codomain</a> contained in its <a href="/facts/Relation_(mathematics)/HjblDaMy">domain</a>. If 0 is assigned to the lowest type, the type of 
 
 
 
 R
 
 
 {\displaystyle R}
 
 is 3. Infinity can be satisfied only if the (co)domain of 
 
 
 
 R
 
 
 {\displaystyle R}
 
 is <a href="/facts/Infinity/cF506uD7">infinite</a>, thus forcing the existence of an infinite set. If relations are defined in terms of <a href="/facts/Ordered_pair/EInLVI0r">ordered pairs</a>, 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 <a href="/facts/Axiom_of_infinity/kDWQE32v">axiom of infinity</a> (there exists an <a href="/facts/Inductive_set_(axiom_of_infinity)/kDWQE32v">inductive set</a>) of <a href="/facts/ZFC/UYIsPbXw">ZFC</a> of other set theories could not be married to ST.
ST reveals how type theory can be made very similar to <a href="/facts/Axiomatic_set_theory/1ptfsvUP">axiomatic set theory</a>. Moreover, the more elaborate <a href="/facts/Ontology_(information_science)/SQlhl6lp">ontology</a> 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 <a href="/facts/ZFC/UYIsPbXw">ZFC</a>, with simpler ontologies. Set theories whose point of departure is type theory, but whose axioms, <a href="/facts/Ontology_(information_science)/SQlhl6lp">ontology</a>, and terminology differ from the above, include <a href="/facts/New_Foundations/jT6vAvj5">New Foundations</a> and <a href="/facts/Scott%E2%80%93Potter_set_theory/nG1MhvYS">Scott–Potter set theory</a>.

ST type theory open-in-new

ST type theory