Types, theory of

A formal first-order theory (cf. Formal system), one variant of which — the simple theory of types — is described below. The terminology "theory of types" has no rigidly fixed meaning. It denotes formal theories which are distinguished in the following way. First, there are linguistic tools available in the formal system for expressing relationships described in words as: "the sequence $x_1,\dots,x_n$ belongs to $y$" or "$y$ is performed on $x_1,\dots,x_n$" ; let $ y (x _{1} \dots x _{n} ) $ denote the expression in quotation marks. Secondly, there is the decomposition of the object domain into strata, or types, forming a hierarchy of types (not necessarily linear, and not necessarily countable), and the presence of type-theoretic comprehension axioms (or their equivalents). If variables running through the objects of type $ \sigma $ are denoted by $ x ^ \sigma ,\ y ^ \sigma ,\ z ^ \sigma \dots $ then type-theoretical comprehension axioms have the form $$ \tag{*} \exists y ^ \rho \forall (x _{1} ^ {\sigma _{1}} \dots x _{n} ^ {\sigma _{n}} ) (y ^ \rho (x _{1} ^ {\sigma _{1}} \dots x _{n} ^ {\sigma _{n}} ) \iff \phi (x _{1} ^ {\sigma _{1}} \dots x _{n} ^ {\sigma _{n}} )) , $$ where $ \phi (x _{1} ^ {\sigma _{1}} \dots x _{n} ^ {\sigma _{n}} ) $ is a formula relative to the system with free variables $ x _{1} ^ {\sigma _{1}} \dots x _{n} ^ {\sigma _{n}} $ , and the type $ \rho $ of the variable $ y ^ \rho $ must belong (this is the main point of type-theoretic systems) to a higher level in the hierarchy of types than the types $ \sigma _{1} \dots \sigma _{n} $ . The type $ \rho $ is usually uniquely determined by the types $ \sigma _{1} \dots \sigma _{n} $ . It is denoted by $ ( \sigma _{1} \dots \sigma _{n} ) $ . Thus, in a type-theoretic system a property $ y $ and objects $ x _{1} \dots x _{n} $ which satisfy this property belong to different strata. One often adds an extensionality axiom, which identifies properties with equal content. In this case the type-theoretic system can be regarded as a set-theoretic system, since it satisfies the principle that "a set is completely determined by its elements" .

Type-theoretic systems were introduced by B. Russell in connection with his discovery of a contradiction in set theory. Putting a set and its elements at different levels leads to a point of view regarding antinomies (cf. Antinomy) according to which the appearance of a contradiction is explained by the non-predicative nature of some set-theoretical definitions. Here a definition of some object is called non-predicative if the object itself takes part in the definition, or, what amounts to the same thing, if the definition makes no sense without assuming in advance the existence of the object. Thus, in (*), regarded as a definition of the object $ y $ , the non-predicativity has not been completely removed since, in the formula $ \phi (x _{1} ^ {\sigma _{1}} \dots x _{n} ^ {\sigma _{n}} ) $ , there may appear quantifiers in variables which run through the same domain that the object $ y $ belongs to. Hence one considers also predicative type-theoretic systems, in which one carries out a further decomposition of the object domains. In such systems, $ y $ in (*) must belong to a domain distinct from the domains run through by the bound variables in $ \phi (x _{1} ^ {\sigma _{1}} \dots x _{n} ^ {\sigma _{n}} ) $ .

One considers type-theoretic systems in which the types are ordered as some initial segment of the ordinal numbers or as the set of (positive and negative) integers, and also systems in which all formulas are objects of a well-defined type, and systems which allow expressions of infinite length (or the means of substituting such expressions, for example quantifiers over an index type). Logics of the second and higher orders may be regarded as type-theoretic systems.

The simple theory of types.

The language of the simple theory of types consists of: for each natural number $ n \geq 0 $ , variables of type $ n $ , $ x _{1} ^{n} ,\ x _{2} ^{n} , . . . $ ; the two-place predicate symbol $ \in $ ; the logical connectives and quantifiers, $ \supset $ , $ \lor $ , $ \& $ , $ \neg $ , $ \forall $ , $ \exists $ ; and the brackets ( and ).

The formulas of the simple theory of types are constructed in the usual inductively-defined way: the expressions of the form $ (x _{i} ^{n} \in x _{j} ^ {n + 1} ) $ are formulas; if $ \phi $ and $ \psi $ are formulas and $ v $ is a variable, then $ ( \phi \supset \psi ) $ , $ ( \phi \lor \psi ) $ , $ ( \phi \& \psi ) $ , $ \neg \phi $ , $ \forall v \ \phi $ , $ \exists v \ \phi $ are formulas. The notation $ ( \phi \iff \psi ) $ is used as an abbreviation for $ (( \phi \supset \psi ) \& ( \psi \supset \phi )) $ .

Non-logical axioms of the simple theory of types.

A1) The comprehension axiom $$ \exists y \forall x \ (x \in y \iff \phi ), $$ where $ x $ and $ y $ are variables of types $ n $ and $ n + 1 $ , respectively, and $ \phi $ is an arbitrary formula in the language of the simple theory of types not containing the free variable $ y $ .

A2) The extensionality axiom: $$ \forall t \ (t \in x \iff t \in y) \supset \forall z \ (x \in z \supset y \in z), $$ where $ t,\ x,\ y,\ z $ are variables of types $ n,\ n + 1,\ n + 2 $ , respectively.

A3) The infinity axiom: $$ \exists x \ ( \exists w \ (w \in x) \& \forall u \in x \ \exists v \in x \ (u \ \subseteq \ v \ \& \ \exists t \ (t \in v \ \& \ \neg t \in u))), $$ where $ x $ is a variable of type 2. The types of the remaining variables can be recovered uniquely. Here the notations $ \forall u \in x \ \phi $ and $ \exists v \in x \ \phi $ denote the formulas $ \forall u \ (u \in x \supset \phi ) $ and $ \exists v \ (v \in x \ \& \ \phi ) $ , respectively, and the expression $ u \subseteq v $ is an abbreviation for $ \forall z \ (z \in u \ \supset \ z \in v) $ .

Logical axioms and inference rules. These are the logical axioms and inference rules (cf. Derivation rule) of the classical predicate calculus, reformulated in the appropriate language. These axioms and rules determine the class of derivable formulas or theorems in the simple theory of types. This class can be defined semantically.

A mathematical structure $ M = (V _{0} ,\ V _{1} , . . ; \ \in _{M} ) $ , where $ \in _{M} \subseteq \cup _ {n = 0} ^ \infty (V _{n} \times V _ {n + 1} ) $ , is called a model of the simple theory of types if all non-logical axioms of the simple theory of types are satisfied in it. Gödel's completeness theorem for the predicate calculus implies that the class of theorems for the simple theory of types coincides with the class of formulas which are true in all models of the simple theory of types. The simple theory of types is a fairly strong theory. Within it one can imbed arithmetic and analysis (that is, second-order arithmetic), and consider the initial ordinal numbers $ \omega _{0} \dots \omega _{n} $ , where $ n $ is any natural number given in advance. It has a simple intuitive set-theoretic model. For $ V _{0} $ one can take any infinite set, and each subsequent level $ V _ {n + 1} $ consists of the subsets of the previous level. The relation $ \in _{M} $ is the natural one. The existence of a set-theoretic model can be used for a formal proof of the consistency of the simple theory of types in the framework of a sufficiently powerful axiomatic theory. Such a consistency proof can be constructed, for example, within the Zermelo system, which is obtained from the Zermelo–Fraenkel system $ ZF $ by omitting the axiom of substitution, but retaining the axiom of separation.

References

[1]	A.N. Whitehead, B. Russell, "Principia Mathematica" , 1–3 , Cambridge Univ. Press (1910)
[2]	A.A. Fraenkel, Y. Bar-Hillel, "Foundations of set theory" , North-Holland (1958)
[3]	J. Barwise (ed.) , Handbook of mathematical logic , North-Holland (1977)
[4]	G. Takeuti, "Proof theory" , North-Holland (1975)