types, theory of

Russell's own reaction to his paradox of the class of all classes that are not members of themselves (see Russell's paradox ) was to suggest that the definition is ill-formed because it involves the illegitimate notion of ‘all classes’. If the entities of a theory are classified in a hierarchy, with individuals at the lowest level, sets of individuals at the next, sets of sets further up again, and if prohibitions are introduced against sets containing members of different types, then the paradox cannot be formulated.

When Russell published his solution he was also influenced by Poincaré's constructivist response to the contradictions of set theory . This suggested that in any application of the axiom of comprehension, (∃y )((∀x )(x ∈y ↔ F x )), the variable x should not range over entities including the set y . If it does, the definition becomes impredicative, and offends against the vicious circle principle . To prohibit this, Russell sorted predicates into orders, again with restrictions on well-formedness. The result is called the ramified theory of types. Unfortunately it proved impossible to construct classical mathematics within the ramified theory, and Russell was forced to introduce the axiom of reducibility, whose effect is to collapse the hierarchy of predicates.

Although the non-ramified or simple theory of types has attracted much subsequent work, all type theory suffers from a problem of unintuitive duplication. Thus for Russell there exists not one but an infinite number of the number 2, since there are sets of all sets having two members at each level in the hierarchy. Expressions needed at each type level, such as ‘=’, are supposedly systematically ambiguous, and in some developments there are an infinite number of identity symbols.

The relative consistency of type theory has been proved within Zermelo–Fraenkel set theory , thereby also showing that the latter is stronger than the former. Few logicians now believe that there is any reason to build type restrictions into the formal systems within which set-theoretic and mathematical reasoning is best represented.