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.
\in
x'
x=y
y\inx'
\in
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 '
\in
x=y\leftrightarrow\forallz'[x\inz'\leftrightarrowy\inz']
\forallx[x\iny'\leftrightarrowx\inz'] → [y'=z']
Let
\Phi(x)
x
\existsz'\forallx[x\inz'\leftrightarrow\Phi(x)]
Remark. Any collection of elements of the same type may form an object of the next higher type. Comprehension is schematic with respect to
\Phi(x)
R
\forallx,y[x ≠ y → [xRy\veeyRx]]
Remark. Infinity is the only true axiom of ST and is entirely mathematical in nature. It asserts that
R
R
R
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.
Church's type theory has been extensively studied by two of Church's students, Leon Henkin and Peter B. Andrews. Since ST is a higher order logic, and in higher order logics one can define propositional connectives in terms of logical equivalence and quantifiers, in 1963 Henkin developed a formulation of ST based on equality, but in which he restricted attention to propositional types. This was simplified later that year by Andrews in histheory Q0.[1] In this respect ST can be seen as a particular kind of a higher-order logic, classified by P.T. Johnstone in Sketches of an Elephant, as having a lambda-signature, that is a higher-order signature that contains no relations, and uses only products and arrows (function types) as type constructors. Furthermore, as Johnstone put it, ST is "logic-free" in the sense that it contains no logical connectives or quantifiers in its formulae.[2]