ST type theory
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
The symbols peculiar to ST are primed variables and
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
- Identity, defined by .
- Extensionality. An axiom schema. .
Let denote any
- 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 ZFCof other set theories could not be married to ST.
ST reveals how type theory can be made very similar to
Formulations based on equality
This section needs expansion. You can help by adding to it. (September 2009) |
Church's type theory has been extensively studied by two of Church's students,
See also
References
- 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.
- ^ Stanford Encyclopedia of Philosophy: Church's Type Theory" – by Peter Andrews (adapted from his book).
- ^ P.T. Johnstone, Sketches of an elephant, p. 952